[isabelle-dev] partial_function
Christian Sternagel
c.sternagel at gmail.com
Tue Aug 6 07:40:40 CEST 2013
Dear all,
I'm currently checking IsaFoR [1] against the repository versions of
Isabelle (8d8cb75ab20a) and the AFP (05436df687d1). Doing so, I stumbled
across a "partial_function" definition that worked with Isabelle2013 but
aborts now with a "Unification bound exceeded".
Is anybody aware of changes in "partial_function" or unification (or
somewhere I didn't think of) that could explain this?
The general shape of the function (which is employed to parse XML into
an internal datatype) is:
partial_function (parse_result)
...
where
"parser x y = xml1element ''tag name'' (xml_options [
(''tag name 1'', parser_1),
(''tag name 2'', parser_2,
...
(''tag name N'', parser_N)
]) ..."
where some of the "parser_i" use "parser" recursively. Currently we have
around 20 parsers in the above list and the error disappears if I reduce
that to 14 (with "unify_search_bound = 90").
If anybody has the energy to look at the real code ;) see [2], theory
CPF_Parser.thy, partial function "xml2dp_termination_proof". You will
also have to apply a patch from my local patch queue (which is
attached), since the "official" repository is for Isabelle2013.
cheers
chris
[1] http://cl-informatik.uibk.ac.at/software/ceta/
[2] http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR
-------------- next part --------------
# HG changeset patch
# Parent 7ae645e2834dc163bd8890e3b7a8dd3a95f63766
adapt to repository versions of Isabelle and AFP
diff --git a/IsaFoR/Bounded_Increase.thy b/IsaFoR/Bounded_Increase.thy
--- a/IsaFoR/Bounded_Increase.thy
+++ b/IsaFoR/Bounded_Increase.thy
@@ -25,19 +25,21 @@
We generalize the result, since we only demand minimality or unique normal forms. *}
text {* free variables of a constraint, as set and as list *}
-fun vars_cc :: "('f,'v)cond_constraint \<Rightarrow> 'v set" where
- "vars_cc (CC_cond ct (s,t)) = vars_term s \<union> vars_term t"
+fun vars_cc :: "('f, 'v) cond_constraint \<Rightarrow> 'v set" where
+ "vars_cc (CC_cond ct (s, t)) = vars_term s \<union> vars_term t"
| "vars_cc (CC_rewr s t) = vars_term s \<union> vars_term t"
| "vars_cc (CC_impl cs c) = \<Union>(vars_cc ` set cs) \<union> vars_cc c"
| "vars_cc (CC_all x c) = vars_cc c - {x}"
-fun vars_cc_list :: "('f,'v)cond_constraint \<Rightarrow> 'v list" where
- "vars_cc_list (CC_cond ct (s,t)) = vars_term_list s @ vars_term_list t"
+fun vars_cc_list :: "('f, 'v) cond_constraint \<Rightarrow> 'v list" where
+ "vars_cc_list (CC_cond ct (s, t)) = vars_term_list s @ vars_term_list t"
| "vars_cc_list (CC_rewr s t) = vars_term_list s @ vars_term_list t"
| "vars_cc_list (CC_impl c1 c2) = concat (map vars_cc_list c1) @ vars_cc_list c2"
| "vars_cc_list (CC_all x c) = [ y . y <- vars_cc_list c, y \<noteq> x]"
-lemma vars_cc_list[simp]: "set (vars_cc_list c) = vars_cc c" by (induct c, auto)
+lemma vars_cc_list [simp]:
+ "set (vars_cc_list c) = vars_cc c"
+ by (induct c) auto
text {* constructor for adding multiple quantors *}
fun cc_bound :: "'v list \<Rightarrow> ('f,'v)cond_constraint \<Rightarrow> ('f,'v)cond_constraint" where
@@ -112,7 +114,8 @@
begin
text {* only the free variables matter, when checking the model condition *}
-lemma cc_models_vars: assumes "\<And> x. x \<in> vars_cc c \<Longrightarrow> \<sigma> x = \<tau> x"
+lemma cc_models_vars:
+ assumes "\<And> x. x \<in> vars_cc c \<Longrightarrow> \<sigma> x = \<tau> x"
shows "\<sigma> \<Turnstile> c = \<tau> \<Turnstile> c"
using assms
proof (induct c arbitrary: \<sigma> \<tau>)
@@ -1065,7 +1068,8 @@
have "funas_term (\<mu> x) \<subseteq> funas_term (Fun f rs)" using mu by auto
also have "\<dots> \<subseteq> funas_term r'" using subt by fastforce
also have "\<dots> \<subseteq> funas_term r" unfolding r funas_term_subst by auto
- also have "\<dots> \<subseteq> F" using lr RF unfolding funas_trs_def funas_rule_def by force
+ also have "\<dots> \<subseteq> F"
+ using lr RF unfolding funas_trs_def funas_rule_def [abs_def] by force
finally have F: "funas_term ?x \<subseteq> F" using tauF unfolding funas_term_subst by auto
have "(?x \<in> NF_trs R) = (?x \<in> NF (qrstep nfs {} R))" by simp
also have "\<dots>"
@@ -1124,3 +1128,4 @@
end
end
+
diff --git a/IsaFoR/Bounded_Increase_Impl.thy b/IsaFoR/Bounded_Increase_Impl.thy
--- a/IsaFoR/Bounded_Increase_Impl.thy
+++ b/IsaFoR/Bounded_Increase_Impl.thy
@@ -792,3 +792,4 @@
by (cases prof, cases merge, auto simp: conditional_general_reduction_pair_proc_def Let_def)
end
+
diff --git a/IsaFoR/CPF_Parser.thy b/IsaFoR/CPF_Parser.thy
--- a/IsaFoR/CPF_Parser.thy
+++ b/IsaFoR/CPF_Parser.thy
@@ -826,7 +826,8 @@
(\<lambda> c b a ccs. Cond_Red_Pair_Prf c ccs b a)"
partial_function (parse_result)
- xml2dp_termination_proof :: "('f :: key, 'l :: key) lab xmlt \<Rightarrow> ('f, 'l, string) dp_termination_proof xmlt"
+ xml2dp_termination_proof ::
+ "('f :: key, 'l :: key) lab xmlt \<Rightarrow> ('f, 'l, string) dp_termination_proof xmlt"
where
[code]: "xml2dp_termination_proof xml2name x = xml1element ''dpProof'' (xml_options [
(''pIsEmpty'', xml0elements ''pIsEmpty'' P_is_Empty),
diff --git a/IsaFoR/Conditional_Rewriting.thy b/IsaFoR/Conditional_Rewriting.thy
--- a/IsaFoR/Conditional_Rewriting.thy
+++ b/IsaFoR/Conditional_Rewriting.thy
@@ -159,8 +159,8 @@
definition rules :: "('f,'v)crule \<Rightarrow> ('f,'v)trs"
where "rules crule \<equiv> (\<lambda> n. (lhs_n crule n, rhs_n crule n)) ` {n . n \<le> length (snd crule)}"
-definition UR :: "('f,'v)trs"
- where "UR \<equiv> \<Union>(rules ` R)"
+definition UR :: "('f, 'v) trs" where
+ "UR \<equiv> \<Union>(rules ` R)"
lemma UR_simulation_main: assumes lr: "((l, r), cs) \<in> R"
and i: "i \<le> length cs"
@@ -377,6 +377,7 @@
})"
*)
-hide_const (open) eqs;
+hide_const (open) eqs
end
+
diff --git a/IsaFoR/Dependency_Pair_Problem_Spec.thy b/IsaFoR/Dependency_Pair_Problem_Spec.thy
--- a/IsaFoR/Dependency_Pair_Problem_Spec.thy
+++ b/IsaFoR/Dependency_Pair_Problem_Spec.thy
@@ -276,7 +276,3 @@
end
-
-
-
-
diff --git a/IsaFoR/Error_Monad.thy b/IsaFoR/Error_Monad.thy
--- a/IsaFoR/Error_Monad.thy
+++ b/IsaFoR/Error_Monad.thy
@@ -26,11 +26,10 @@
definition
bind :: "'e + 'a \<Rightarrow> ('a \<Rightarrow> 'e + 'b) \<Rightarrow> 'e + 'b"
where
- "bind m f = (case m of Inr x \<Rightarrow> f x | e \<Rightarrow> e)"
+ "bind m f = (case m of Inr x \<Rightarrow> f x | Inl e \<Rightarrow> Inl e)"
-setup {*
- Adhoc_Overloading.add_variant @{const_name Monad_Syntax.bind} @{const_name bind}
-*}
+adhoc_overloading
+ Monad_Syntax.bind bind
abbreviation (input) return where "return \<equiv> Inr"
abbreviation (input) error where "error \<equiv> Inl"
@@ -61,7 +60,7 @@
catch :: "'e + 'a \<Rightarrow> ('e \<Rightarrow> 'f + 'a) \<Rightarrow> 'f + 'a"
("(try(/ _)/ catch(/ _))" [12, 12] 13)
where
- "try m catch f \<equiv> case m of Inl e \<Rightarrow> f e | x \<Rightarrow> x"
+ "(try m catch f) = (case m of Inl e \<Rightarrow> f e | Inr x \<Rightarrow> Inr x)"
abbreviation
update_error :: "'e + 'a \<Rightarrow> ('e \<Rightarrow> 'f) \<Rightarrow> 'f + 'a" (infixl "<+?" 61)
diff --git a/IsaFoR/Flat_Context_Closure.thy b/IsaFoR/Flat_Context_Closure.thy
--- a/IsaFoR/Flat_Context_Closure.thy
+++ b/IsaFoR/Flat_Context_Closure.thy
@@ -353,8 +353,10 @@
and wft: "funas_term t \<subseteq> F" by auto
from rstep_imp_C_s_r[OF rstep] obtain D \<sigma> l r where R: "(l,r) \<in> R"
and s: "s = D\<langle>l\<cdot>\<sigma>\<rangle>" and t: "t = D\<langle>r\<cdot>\<sigma>\<rangle>" by auto
- have vl: "vars_term l \<subseteq> vars_trs R" using R unfolding vars_trs_def vars_rule_def by auto
- have vr: "vars_term r \<subseteq> vars_trs R" using R unfolding vars_trs_def vars_rule_def by auto
+ have vl: "vars_term l \<subseteq> vars_trs R"
+ using R unfolding vars_trs_def vars_rule_def [abs_def] by auto
+ have vr: "vars_term r \<subseteq> vars_trs R"
+ using R unfolding vars_trs_def vars_rule_def [abs_def] by auto
from flat_ctxts[THEN bspec[where x=C],OF C] have distinct: "vars_ctxt C \<inter> vars_trs R = {}"
using is_flat_ctxt_imp_flat_ctxt by best
from R pres have "(l,r) \<in> R' \<or> (\<forall>C\<in>fcs. (C\<langle>l\<rangle>,C\<langle>r\<rangle>) \<in> R')" by auto
@@ -498,7 +500,8 @@
hence "x \<in> vars_term C\<langle>r\<rangle>" unfolding vars_term_ctxt_apply by auto
with vars have "x \<in> vars_term C\<langle>l\<rangle>" by auto
hence xx: "x \<in> vars_ctxt C \<union> vars_term l" unfolding vars_term_ctxt_apply .
- from x lr have "x \<in> vars_trs (R \<union> S)" unfolding vars_trs_def vars_rule_def by force
+ from x lr have "x \<in> vars_trs (R \<union> S)"
+ unfolding vars_trs_def vars_rule_def [abs_def] by force
with distinct xx show "x \<in> vars_term l" by auto
qed
qed
@@ -518,7 +521,8 @@
and SN: "SN_rel (rstep(FC G R)) (rstep (FC G S))"
shows "SN_rel (rstep R) (rstep S)"
proof -
- from finite have fin: "finite(vars_trs (R \<union> S))" unfolding vars_trs_def vars_rule_def by auto
+ from finite have fin: "finite(vars_trs (R \<union> S))"
+ unfolding vars_trs_def vars_rule_def [abs_def] by auto
have fcs: "\<forall>C\<in>?fcs. is_flat_ctxt (vars_trs (R \<union> S)) G C" using flat_ctxt_is_flat[OF fin] by best
have complete: "\<forall>(f,n)\<in>G.\<forall>i<n.\<exists>ss1 ss2. More f ss1 \<box> ss2 \<in> ?fcs \<and> length ss1 = i \<and> length ss2 = n - i - 1"
proof (intro ballI2 allI impI)
@@ -547,19 +551,20 @@
shows "funs_trs R \<noteq> {}"
proof -
from ne have "funas_trs R \<noteq> {}" unfolding flat_ctxts_def by auto
- then obtain l r where R: "(l,r) \<in> R" and "funas_term l \<union> funas_term r \<noteq> {}" unfolding funas_rule_def funas_trs_def by force
+ then obtain l r where R: "(l,r) \<in> R" and "funas_term l \<union> funas_term r \<noteq> {}"
+ unfolding funas_rule_def [abs_def] funas_trs_def by force
hence "funas_term l \<noteq> {} \<or> funas_term r \<noteq> {}" by simp
thus "funs_trs R \<noteq> {}"
proof
assume "funas_term l \<noteq> {}"
then obtain f ss where "l = Fun f ss" by (induct l) auto
hence "f \<in> funs_term l" by simp
- with R show ?thesis unfolding funs_trs_def funs_rule_def by force
+ with R show ?thesis unfolding funs_trs_def funs_rule_def [abs_def] by force
next
assume "funas_term r \<noteq> {}"
then obtain f ss where "r = Fun f ss" by (induct r) auto
hence "f \<in> funs_term r" by simp
- with R show ?thesis unfolding funs_trs_def funs_rule_def by force
+ with R show ?thesis unfolding funs_trs_def funs_rule_def [abs_def] by force
qed
qed
@@ -706,7 +711,7 @@
have "(\<Union>x\<in>vars_term r. funas_term (Var x \<cdot> \<sigma>)) \<subseteq> funas_trs ?R \<union> funas_args_trs P"
by auto
moreover from `(l, r) \<in> R` have "funas_term r \<subseteq> funas_trs ?R"
- unfolding funas_defs by auto
+ unfolding funas_defs [abs_def] by auto
ultimately have "funas_term (r \<cdot> \<sigma>) \<subseteq> funas_trs ?R \<union> funas_args_trs P"
unfolding funas_term_subst by auto
moreover from fs have "funas_ctxt D \<subseteq> funas_trs ?R \<union> funas_args_trs P"
@@ -743,7 +748,7 @@
from `(l, r) \<in> R`
have vl: "vars_term l \<subseteq> vars_trs R"
and vr: "vars_term r \<subseteq> vars_trs R"
- unfolding vars_defs by auto
+ unfolding vars_defs [abs_def] by auto
from vl have l_subst_R: "l \<cdot> (\<sigma> |s vars_trs R) = l \<cdot> \<sigma>"
unfolding term_subst_eq_conv subst_restrict_def by auto
from vr have r_subst_R: "r \<cdot> (\<sigma> |s vars_trs R) = r \<cdot> \<sigma>"
@@ -1047,7 +1052,7 @@
lemma superset_of_blocked:
assumes "\<forall>rule\<in>R. block_rule f rule \<in> R'"
shows "block_trs f R \<subseteq> R'"
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t assume "(s, t) \<in> block_trs f R"
then obtain r where st: "block_rule f r = (s, t)" and "r \<in> R" by auto
with assms have "block_rule f r \<in> R'" by blast
@@ -1227,7 +1232,7 @@
proof -
from t_in_P
have funas_ti: "funas_args_term (t i) \<subseteq> ?F'"
- unfolding funas_args_trs_def funas_args_rule_def by auto
+ unfolding funas_args_trs_def funas_args_rule_def [abs_def] by auto
moreover have "funas_args_term ?t = (\<Union>t\<in>set ts. funas_term (t \<cdot> ?\<sigma>))"
unfolding funas_args_term_subst_apply[OF `is_Fun (t i)`]
unfolding ti by auto
@@ -1406,5 +1411,4 @@
with finite2 show False unfolding finite_dpp_def by blast
qed
-
-end
\ No newline at end of file
+end
diff --git a/IsaFoR/Flat_Context_Closure_Impl.thy b/IsaFoR/Flat_Context_Closure_Impl.thy
--- a/IsaFoR/Flat_Context_Closure_Impl.thy
+++ b/IsaFoR/Flat_Context_Closure_Impl.thy
@@ -403,7 +403,7 @@
lemma check_superset_of_blocked_sound:
assumes "isOK (check_superset_of_blocked f P' P)"
shows "set (block_trs_list f P) \<subseteq> set P'"
-proof (rule subsetI2)
+proof (rule subrelI)
from assms[unfolded check_superset_of_blocked_def]
have a: "\<forall>r\<in>set P. block_rule f r \<in> set P'" by simp
fix s t assume "(s, t) \<in> set (block_trs_list f P)"
@@ -440,7 +440,7 @@
lemma block_trs_list_unblock_trs_list[simp]:
assumes "set (block_trs_list f P) \<subseteq> set P'"
shows "set P \<subseteq> set (unblock_trs_list f P')"
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t assume "(s, t) \<in> set P"
hence "block_rule f (s, t) \<in> block_rule f ` set P" by simp
with assms have "block_rule f (s, t) \<in> set P'" unfolding block_defs by auto
@@ -736,4 +736,3 @@
end
-
diff --git a/IsaFoR/Generalized_Usable_Rules.thy b/IsaFoR/Generalized_Usable_Rules.thy
--- a/IsaFoR/Generalized_Usable_Rules.thy
+++ b/IsaFoR/Generalized_Usable_Rules.thy
@@ -51,11 +51,11 @@
| in_U: "(l,r) \<in> R \<Longrightarrow> compat_root l t \<Longrightarrow> gen_usable_rule r lr \<Longrightarrow> gen_usable_rule t lr"
| in_arg: "i < length ts \<Longrightarrow> gen_usable_rule (ts ! i) lr \<Longrightarrow> lr' \<in> {lr} ^^^ \<pi> (f,length ts) i \<Longrightarrow> gen_usable_rule (Fun f ts) lr'"
-definition gen_usable_rules :: "('f,'v)term \<Rightarrow> ('f,'v)trs"
- where "gen_usable_rules t \<equiv> {lr. gen_usable_rule t lr}"
+definition gen_usable_rules :: "('f, 'v) term \<Rightarrow> ('f, 'v) trs" where
+ "gen_usable_rules t = {lr. gen_usable_rule t lr}"
-definition gen_usable_rules_pairs :: "('f,'v)trs \<Rightarrow> ('f,'v)trs"
- where "gen_usable_rules_pairs P \<equiv> \<Union>(gen_usable_rules ` snd ` P)"
+definition gen_usable_rules_pairs :: "('f, 'v) trs \<Rightarrow> ('f, 'v) trs" where
+ "gen_usable_rules_pairs P = \<Union>(gen_usable_rules ` snd ` P)"
lemma gen_usable_rulesI[intro]: "gen_usable_rule t lr \<Longrightarrow> lr \<in> gen_usable_rules t"
unfolding gen_usable_rules_def by auto
@@ -247,7 +247,8 @@
from wwf_qtrs_imp_left_fun[OF wwf lr] obtain g ls where l: "l = Fun g ls" by auto
from wwf only_applicable_rules[OF nf] lr
have vars_lr: "vars_term r \<subseteq> vars_term l" unfolding wwf_qtrs_def by auto
- from RF lr have rF: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def by force
+ from RF lr have rF: "funas_term r \<subseteq> F"
+ unfolding funas_trs_def funas_rule_def [abs_def] by force
show ?case
proof (cases C)
case Hole
@@ -597,12 +598,12 @@
definition rel_of :: "bool \<Rightarrow> ('f,'v)trs" where
"rel_of ct \<equiv> if ct then S else NS"
-definition normal_F_subst :: "('f,'v)subst \<Rightarrow> bool"
- where "normal_F_subst \<sigma> \<equiv> (\<Union>(funas_term ` range \<sigma>) \<subseteq> F) \<and> range \<sigma> \<subseteq> NF_trs R"
+definition normal_F_subst :: "('f, 'v) subst \<Rightarrow> bool" where
+ "normal_F_subst \<sigma> \<longleftrightarrow> (\<Union>(funas_term ` range \<sigma>) \<subseteq> F) \<and> range \<sigma> \<subseteq> NF_trs R"
text {* if we have minimality (m is true), then demand strong normalization *}
-definition m_SN :: "('f,'v)term \<Rightarrow> bool" where
- "m_SN t \<equiv> m \<longrightarrow> SN_on (qrstep nfs Q R) {t}"
+definition m_SN :: "('f, 'v) term \<Rightarrow> bool" where
+ "m_SN t \<longleftrightarrow> m \<longrightarrow> SN_on (qrstep nfs Q R) {t}"
fun cc_models :: "('f,'v)subst \<Rightarrow> ('f,'v)cond_constraint \<Rightarrow> bool" (infix "\<Turnstile>" 51) where
"\<sigma> \<Turnstile> CC_cond ct (s,t) = ((s \<cdot> \<sigma>,t \<cdot> \<sigma>) \<in> rel_of ct)"
@@ -985,7 +986,7 @@
from R have RR: "R = Rs \<union> Rw" by simp
from QF have QF': "QF_cond F Q" unfolding QF_cond_def by auto
from PF have PF': "\<And> s t. (s,t) \<in> P \<union> Pw \<Longrightarrow> funas_args_term t \<subseteq> F"
- unfolding funas_args_trs_def funas_args_rule_def by force
+ unfolding funas_args_trs_def funas_args_rule_def [abs_def] by force
from clean_min_ichain_below[of Q Rs Rw, unfolded R, OF NFQ QF' RF PF wwf _ var_cond chain]
nvar ndef obtain \<sigma> where "min_ichain_sig ?D F s t \<sigma>" by blast
from conditional_general_reduction_pair_chains[where Pb = Pb, OF U_NS this nvar var_cond ndef[unfolded RR] PF' orient cS cNS cB ccs R]
@@ -1077,3 +1078,4 @@
end
end
+
diff --git a/IsaFoR/Icap.thy b/IsaFoR/Icap.thy
--- a/IsaFoR/Icap.thy
+++ b/IsaFoR/Icap.thy
@@ -862,8 +862,10 @@
then Var (Inl ())
else t')"
-definition icap' :: "('f,string)cap_fun"
- where "icap' R Q S t \<equiv> if vars_term t \<union> \<Union>(vars_term ` S) \<subseteq> range x_var then icap R Q S t else Var (Inl ())"
+definition icap' :: "('f, string) cap_fun" where
+ "icap' R Q S t =
+ (if vars_term t \<union> \<Union>(vars_term ` S) \<subseteq> range x_var then icap R Q S t
+ else Var (Inl ()))"
lemma vars_term_icap: "vars_term (icap R Q S t) \<subseteq> Inr ` vars_term t \<union> {Inl ()}"
by (induct t, auto simp: Let_def)
@@ -1067,6 +1069,5 @@
no_notation Icap.fresh_instances_subst ("[_]'__")
no_notation Icap.fresh_instances ("[_]")
-
end
diff --git a/IsaFoR/Innermost_Loops.thy b/IsaFoR/Innermost_Loops.thy
--- a/IsaFoR/Innermost_Loops.thy
+++ b/IsaFoR/Innermost_Loops.thy
@@ -933,8 +933,8 @@
qed
qed auto
-definition conflict_terms :: "('f,'v)term \<Rightarrow> ('f,'v)term \<Rightarrow> ('f,'v)term set"
- where "conflict_terms s t \<equiv> \<Union>((\<lambda> u. {v . u \<unrhd> v}) ` (subst_range \<mu> \<union> {s,t}))"
+definition conflict_terms :: "('f, 'v) term \<Rightarrow> ('f, 'v) term \<Rightarrow> ('f, 'v) term set" where
+ "conflict_terms s t = \<Union>((\<lambda> u. {v . u \<unrhd> v}) ` (subst_range \<mu> \<union> {s,t}))"
lemma conflict_terms_subst: "conflict_terms s (\<mu> x) \<subseteq> conflict_terms s (Var x)"
"conflict_terms (\<mu> x) s \<subseteq> conflict_terms (Var x) s"
@@ -1720,3 +1720,4 @@
end
end
+
diff --git a/IsaFoR/Innermost_Loops_Impl.thy b/IsaFoR/Innermost_Loops_Impl.thy
--- a/IsaFoR/Innermost_Loops_Impl.thy
+++ b/IsaFoR/Innermost_Loops_Impl.thy
@@ -408,3 +408,4 @@
qed
end
+
diff --git a/IsaFoR/Linear_Orders.thy b/IsaFoR/Linear_Orders.thy
--- a/IsaFoR/Linear_Orders.thy
+++ b/IsaFoR/Linear_Orders.thy
@@ -20,7 +20,6 @@
Labelings
Term
"~~/src/HOL/Library/List_lexord"
- "~~/src/HOL/Library/Char_nat"
"$AFP/Datatype_Order_Generator/Derive"
begin
@@ -47,3 +46,4 @@
derive linorder "term"
end
+
diff --git a/IsaFoR/Linear_Poly_Order.thy b/IsaFoR/Linear_Poly_Order.thy
--- a/IsaFoR/Linear_Poly_Order.thy
+++ b/IsaFoR/Linear_Poly_Order.thy
@@ -1284,7 +1284,8 @@
proof (rule sig_mono_imp_SN_rel_ce[OF inter_s_F_mono F_unary orient _ F])
fix l r
assume "(l,r) \<in> inter_ns \<inter> Rw"
- with F have ns: "(l,r) \<in> inter_ns" and Fl: "funas_term l \<subseteq> F" and Fr: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def by force+
+ with F have ns: "(l,r) \<in> inter_ns" and Fl: "funas_term l \<subseteq> F"
+ and Fr: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def [abs_def] by force+
show "vars_term r \<subseteq> vars_term l"
proof (rule ccontr)
assume "\<not> ?thesis"
@@ -2550,3 +2551,4 @@
end
end
+
diff --git a/IsaFoR/Matchbounds.thy b/IsaFoR/Matchbounds.thy
--- a/IsaFoR/Matchbounds.thy
+++ b/IsaFoR/Matchbounds.thy
@@ -858,11 +858,12 @@
(* lemma 22a *)
-lemma e_bounded_compact: assumes wf_trs: "wf_trs R"
- and bounded: "e_bounded e c R L"
- and L: "\<Union>(funas_term ` L) \<subseteq> F"
- and R: "finite R"
- and F: "finite F"
+lemma e_bounded_compact:
+ assumes wf_trs: "wf_trs R"
+ and bounded: "e_bounded e c R L"
+ and L: "\<Union>(funas_term ` L) \<subseteq> F"
+ and R: "finite R"
+ and F: "finite F"
shows "compact (lift_term 0 ` L) (cover e R)"
proof -
from finite_list[OF R] obtain Rl where R: "R = set Rl" by auto
@@ -1097,3 +1098,4 @@
hide_const (open) raise
end
+
diff --git a/IsaFoR/Matchbounds_Impl.thy b/IsaFoR/Matchbounds_Impl.thy
--- a/IsaFoR/Matchbounds_Impl.thy
+++ b/IsaFoR/Matchbounds_Impl.thy
@@ -171,7 +171,7 @@
hence "base ((const,0),0) \<in> funas_term ll" unfolding base
unfolding funas_term_map_term by force
hence "(const,0) \<in> funas_term ll" by auto
- with llrr False have False unfolding funas_trs_def funas_rule_def by auto
+ with llrr False have False unfolding funas_trs_def funas_rule_def [abs_def] by auto
} hence const_new: "((const,0),0) \<notin> funas_term l" ..
with lsyms have lsyms: "funas_term l \<subseteq> ta_syms TA" by auto
from compat[unfolded ta_trs_compatible_def] lr lsyms have
diff --git a/IsaFoR/Multiset2.thy b/IsaFoR/Multiset2.thy
--- a/IsaFoR/Multiset2.thy
+++ b/IsaFoR/Multiset2.thy
@@ -403,8 +403,8 @@
by (unfold_locales, unfold o_def, rule ext, auto simp: ac_simps)
lemma [simp]: "mset_sum (M + N) = mset_sum M + mset_sum N"
- unfolding comp_fun_commute.fold_mset_union[OF comp_fun_commute_plus]
- unfolding comp_fun_commute.fold_mset_fun_comm[OF comp_fun_commute_plus]
+ unfolding comp_fun_commute.fold_mset_union [OF comp_fun_commute_plus]
+ unfolding comp_fun_commute.fold_mset_fun_left_comm [OF comp_fun_commute_plus]
by simp
lemma [simp]: "mset_sum {# x #} = x"
@@ -504,3 +504,4 @@
qed
end
+
diff --git a/IsaFoR/Narrowing_Impl.thy b/IsaFoR/Narrowing_Impl.thy
--- a/IsaFoR/Narrowing_Impl.thy
+++ b/IsaFoR/Narrowing_Impl.thy
@@ -316,4 +316,4 @@
qed
qed
-end
\ No newline at end of file
+end
diff --git a/IsaFoR/Non_Inf_Order.thy b/IsaFoR/Non_Inf_Order.thy
--- a/IsaFoR/Non_Inf_Order.thy
+++ b/IsaFoR/Non_Inf_Order.thy
@@ -127,9 +127,9 @@
text {* for compatibility (monotonicity) we only consider F-terms, not all terms as in CADE07 *}
-definition dep_compat :: "'f sig \<Rightarrow> ('f,'v)term rel \<Rightarrow> 'f dep \<Rightarrow> bool"
- where "dep_compat F r \<pi> \<equiv> \<forall> f bef s t aft. \<Union>(funas_term ` ({s,t} \<union> set bef \<union> set aft)) \<subseteq> F \<longrightarrow>
- {(s,t)} ^^^ \<pi> (f,Suc (length bef + length aft)) (length bef) \<subseteq> r \<longrightarrow> (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \<in> r"
+definition dep_compat :: "'f sig \<Rightarrow> ('f, 'v) term rel \<Rightarrow> 'f dep \<Rightarrow> bool" where
+ "dep_compat F r \<pi> \<longleftrightarrow> (\<forall> f bef s t aft. \<Union>(funas_term ` ({s,t} \<union> set bef \<union> set aft)) \<subseteq> F \<longrightarrow>
+ {(s,t)} ^^^ \<pi> (f,Suc (length bef + length aft)) (length bef) \<subseteq> r \<longrightarrow> (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \<in> r)"
lemma dep_compatE[elim]: assumes dep: "dep_compat F r \<pi>" shows "funas_args_term (Fun f (bef @ s # aft)) \<subseteq> F \<Longrightarrow> funas_term t \<subseteq> F \<Longrightarrow>
{(s,t)} ^^^ \<pi> (f,Suc (length bef + length aft)) (length bef) \<subseteq> r
@@ -147,16 +147,19 @@
text {* F-stability (closure under F-substitutions) is the same as in CADE07 *}
-definition F_subst_closed :: "'f sig \<Rightarrow> ('f,'v)trs \<Rightarrow> bool"
- where "F_subst_closed F r \<equiv> \<forall> \<sigma> s t. \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<longrightarrow> (s,t) \<in> r \<longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> r"
+definition F_subst_closed :: "'f sig \<Rightarrow> ('f, 'v) trs \<Rightarrow> bool" where
+ "F_subst_closed F r \<longleftrightarrow>
+ (\<forall> \<sigma> s t. \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<longrightarrow> (s,t) \<in> r \<longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> r)"
-lemma F_subst_closedI[intro]: assumes "\<And> \<sigma> s t. \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<Longrightarrow> (s,t) \<in> r \<Longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> r"
+lemma F_subst_closedI[intro]:
+ assumes "\<And> \<sigma> s t. \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<Longrightarrow> (s,t) \<in> r \<Longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> r"
shows "F_subst_closed F r" using assms unfolding F_subst_closed_def by blast
lemma F_subst_closedE[elim]: "F_subst_closed F r \<Longrightarrow> \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<Longrightarrow> (s,t) \<in> r \<Longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> r"
unfolding F_subst_closed_def by auto
-lemma F_subst_closed_UNIV: "F_subst_closed F r \<Longrightarrow> F = UNIV \<Longrightarrow> subst_closed r" unfolding F_subst_closed_def
+lemma F_subst_closed_UNIV:
+ "F_subst_closed F r \<Longrightarrow> F = UNIV \<Longrightarrow> subst_closed r" unfolding F_subst_closed_def
using subst_closedI[of r] by auto
text {* a locale to have all nice properties together *}
diff --git a/IsaFoR/Non_Inf_Order_Impl.thy b/IsaFoR/Non_Inf_Order_Impl.thy
--- a/IsaFoR/Non_Inf_Order_Impl.thy
+++ b/IsaFoR/Non_Inf_Order_Impl.thy
@@ -19,20 +19,24 @@
imports Non_Inf_Order Show Monadic_Check
begin
-datatype ('f,'v)c_constraint = Conditional_C bool "('f,'v)rule" "('f,'v)rule" | Unconditional_C bool "('f,'v)rule"
+datatype ('f, 'v) c_constraint =
+ Conditional_C bool "('f, 'v) rule" "('f, 'v) rule" |
+ Unconditional_C bool "('f, 'v) rule"
-fun cc_satisfied :: "'f sig \<Rightarrow> ('f,'v)trs \<Rightarrow> ('f,'v)trs \<Rightarrow> ('f,'v)c_constraint \<Rightarrow> bool" where
- "cc_satisfied F S NS (Unconditional_C stri (s,t)) = (\<forall> \<sigma>. \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> (if stri then S else NS))"
-| "cc_satisfied F S NS (Conditional_C stri (u,v) (s,t)) = (\<forall> \<sigma>. \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<longrightarrow> (u \<cdot> \<sigma>,v \<cdot> \<sigma>) \<in> (if stri then S else NS) \<longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> (if stri then S else NS))"
+fun cc_satisfied :: "'f sig \<Rightarrow> ('f, 'v) trs \<Rightarrow> ('f, 'v) trs \<Rightarrow> ('f, 'v) c_constraint \<Rightarrow> bool" where
+ "cc_satisfied F S NS (Unconditional_C stri (s, t)) =
+ (\<forall> \<sigma>. \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> (if stri then S else NS))"
+| "cc_satisfied F S NS (Conditional_C stri (u, v) (s, t)) =
+ (\<forall> \<sigma>. \<Union>(funas_term ` range \<sigma>) \<subseteq> F \<longrightarrow> (u \<cdot> \<sigma>, v \<cdot> \<sigma>) \<in> (if stri then S else NS) \<longrightarrow> (s \<cdot> \<sigma>, t \<cdot> \<sigma>) \<in> (if stri then S else NS))"
-record ('f,'v)non_inf_order =
+record ('f, 'v) non_inf_order =
valid :: "shows check"
- ns :: "('f, 'v)rule \<Rightarrow> shows check"
- cc :: "('f,'v)c_constraint \<Rightarrow> shows check"
+ ns :: "('f, 'v) rule \<Rightarrow> shows check"
+ cc :: "('f, 'v) c_constraint \<Rightarrow> shows check"
af :: "'f dep"
desc :: "shows"
-hide_const(open) valid ns af desc cc
+hide_const (open) valid ns af desc cc
locale generic_non_inf_order_impl =
fixes generate_non_inf_order :: "'a \<Rightarrow> ('f \<times> nat) list \<Rightarrow> ('f :: show,'v :: show)non_inf_order"
@@ -45,3 +49,4 @@
Ball (set cc) (cc_satisfied (set F) S NS)"
end
+
diff --git a/IsaFoR/Nonloop_Impl.thy b/IsaFoR/Nonloop_Impl.thy
--- a/IsaFoR/Nonloop_Impl.thy
+++ b/IsaFoR/Nonloop_Impl.thy
@@ -641,4 +641,4 @@
insert ok, auto)
qed
-end
\ No newline at end of file
+end
diff --git a/IsaFoR/Nontermination_Impl.thy b/IsaFoR/Nontermination_Impl.thy
--- a/IsaFoR/Nontermination_Impl.thy
+++ b/IsaFoR/Nontermination_Impl.thy
@@ -1065,3 +1065,4 @@
qed
end
+
diff --git a/IsaFoR/Parser_Monad2.thy b/IsaFoR/Parser_Monad2.thy
--- a/IsaFoR/Parser_Monad2.thy
+++ b/IsaFoR/Parser_Monad2.thy
@@ -27,15 +27,22 @@
partial_function_definitions parse_result_ord "flat_lub PNonterm"
by (rule flat_interpretation)
-declaration {* Partial_Function.init "parse_result" @{term parse_result.fixp_fun}
- @{term parse_result.mono_body} @{thm parse_result.fixp_rule_uc}
+declaration {*
+ Partial_Function.init
+ "parse_result"
+ @{term parse_result.fixp_fun}
+ @{term parse_result.mono_body}
+ @{thm parse_result.fixp_rule_uc}
+ @{thm parse_result.fixp_induct_uc}
NONE *}
-
-fun bind :: "('e,'a) parse_result \<Rightarrow> ('a \<Rightarrow> ('e,'b) parse_result) \<Rightarrow> ('e,'b) parse_result"
- where "bind PNonterm f = PNonterm"
- | "bind (PError e) f = PError e"
- | "bind (PResult x) f = f x"
+fun
+ bind ::
+ "('e, 'a) parse_result \<Rightarrow> ('a \<Rightarrow> ('e, 'b) parse_result) \<Rightarrow> ('e, 'b) parse_result"
+where
+ "bind PNonterm f = PNonterm" |
+ "bind (PError e) f = PError e" |
+ "bind (PResult x) f = f x"
lemma bind_cong[fundef_cong]:
assumes "xs = ys" and "\<And>x. ys = PResult x \<Longrightarrow> f x = g x"
@@ -64,18 +71,19 @@
show "parse_result_ord (bind (B f) (\<lambda>y. C y f)) (bind (B g) (\<lambda>y'. C y' g))" .
qed
-setup {*
- Adhoc_Overloading.add_variant @{const_name Monad_Syntax.bind} @{const_name bind}
-*}
+adhoc_overloading
+ Monad_Syntax.bind bind
hide_const (open) bind
fun
- catch :: "('e,'a) parse_result \<Rightarrow> ('e \<Rightarrow> ('f,'a) parse_result) \<Rightarrow> ('f,'a) parse_result"
- ("(try(/ _)/ catch(/ _))" [12, 12] 13)
- where "(try PNonterm catch f) = PNonterm "
- | "(try (PError a) catch f) = f a"
- | "(try (PResult a) catch f) = PResult a"
+ catch ::
+ "('e, 'a) parse_result \<Rightarrow> ('e \<Rightarrow> ('f, 'a) parse_result) \<Rightarrow> ('f, 'a) parse_result"
+ ("(try(/ _)/ catch(/ _))" [12, 12] 13)
+where
+ "(try PNonterm catch f) = PNonterm " |
+ "(try (PError a) catch f) = f a" |
+ "(try (PResult a) catch f) = PResult a"
lemma catch_mono[partial_function_mono]:
assumes mf: "mono_parse_result B" and mg: "\<And>y. mono_parse_result (\<lambda>f. C y f)"
@@ -144,3 +152,4 @@
by (cases p, auto)
end
+
diff --git a/IsaFoR/Poly_Order.thy b/IsaFoR/Poly_Order.thy
--- a/IsaFoR/Poly_Order.thy
+++ b/IsaFoR/Poly_Order.thy
@@ -109,7 +109,9 @@
thus ?thesis by simp
qed
-lemma pos_assign_F_subst: fixes \<sigma> :: "('f,'v)subst" assumes F: "\<Union>(funas_term ` range \<sigma>) \<subseteq> F" and alpha: "pos_assign \<alpha>"
+lemma pos_assign_F_subst:
+ fixes \<sigma> :: "('f, 'v) subst"
+ assumes F: "\<Union>(funas_term ` range \<sigma>) \<subseteq> F" and alpha: "pos_assign \<alpha>"
shows "pos_assign (\<lambda>x. eval_poly \<alpha> (eval_term I (\<sigma> x)))"
unfolding pos_assign_def
proof
@@ -153,10 +155,10 @@
unfolding trans_def inter_s_def using poly_gt_trans by auto
lemma inter_ns_s_s: "inter_ns O inter_s \<subseteq> inter_s"
- by (rule subsetI2, clarify, unfold inter_s_def inter_ns_def, simp add: poly_compat)
+ by (rule subrelI, clarify, unfold inter_s_def inter_ns_def, simp add: poly_compat)
lemma inter_s_ns_s: "inter_s O inter_ns \<subseteq> inter_s"
- by (rule subsetI2, clarify, unfold inter_s_def inter_ns_def, simp add: poly_compat2)
+ by (rule subrelI, clarify, unfold inter_s_def inter_ns_def, simp add: poly_compat2)
end
locale non_inf_poly_order_carrier = poly_order_carrier default gt power_mono discrete
@@ -1526,9 +1528,10 @@
in (if check_poly_ge ss tt then OK else
check (check_poly_ge (poly_add ss vv) (poly_add tt uu)) (''could not ensure '' +#+ shows u + at + '' >= '' +#+ shows v + at + '' ==> '' +#+ shows s + at + '' >= '' +#+ shows t))))"
-lemma check_cc: fixes I :: "('f :: show,'a :: {show,poly_carrier})poly_inter" and cc :: "('f,'v ::show)c_constraint"
+lemma check_cc:
+ fixes I :: "('f :: show,'a :: {show,poly_carrier})poly_inter" and cc :: "('f,'v ::show)c_constraint"
assumes check: "isOK (check_cc sqrt gt I cc)" and pre: "pre_poly_order d gt power_mono discrete I F"
- and non: "non_inf_poly_order_carrier d gt power_mono discrete"
+ and non: "non_inf_poly_order_carrier d gt power_mono discrete"
shows "cc_satisfied F (pre_poly_order.inter_s gt I) (pre_poly_order.inter_ns I) cc"
proof -
interpret pre_poly_order d gt power_mono discrete I F by fact
@@ -1737,3 +1740,4 @@
qed
end
+
diff --git a/IsaFoR/QDP_Framework.thy b/IsaFoR/QDP_Framework.thy
--- a/IsaFoR/QDP_Framework.thy
+++ b/IsaFoR/QDP_Framework.thy
@@ -16,7 +16,9 @@
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)
theory QDP_Framework
-imports Q_Relative_Rewriting Relative_Rewriting2
+imports
+ Q_Relative_Rewriting
+ Relative_Rewriting2
begin
type_synonym ('f, 'v) dpp =
@@ -192,7 +194,7 @@
qed
definition minimal_cond where
- "minimal_cond nfs Q R s t \<sigma> \<equiv> \<forall>i. SN_on (qrstep nfs Q R) {t i \<cdot> \<sigma> i}"
+ "minimal_cond nfs Q R s t \<sigma> \<longleftrightarrow> (\<forall>i. SN_on (qrstep nfs Q R) {t i \<cdot> \<sigma> i})"
text {* A \emph{minimal infinite chain} is an infinite chain where additionally all @{text \<sigma>}-instances
of terms in the sequence~@{text t} are terminating w.r.t.~the system~@{text R}. *}
@@ -201,8 +203,11 @@
where
"min_ichain (nfs,m,P, Pw, Q, R, Rw) s t \<sigma> = (ichain (nfs,m,P, Pw, Q, R, Rw) s t \<sigma> \<and> (m \<longrightarrow> minimal_cond nfs Q (R \<union> Rw) s t \<sigma>))"
-definition funas_ichain :: "(nat \<Rightarrow> ('f, 'v) term) \<Rightarrow> (nat \<Rightarrow> ('f, 'v) term) \<Rightarrow> (nat \<Rightarrow> ('f, 'v) subst) \<Rightarrow> 'f sig" where
- "funas_ichain s t \<sigma> \<equiv> \<Union>{\<Union>(funas_term ` range (\<sigma> i)) | i. True}"
+definition
+ funas_ichain ::
+ "(nat \<Rightarrow> ('f, 'v) term) \<Rightarrow> (nat \<Rightarrow> ('f, 'v) term) \<Rightarrow> (nat \<Rightarrow> ('f, 'v) subst) \<Rightarrow> 'f sig"
+where
+ "funas_ichain s t \<sigma> = \<Union>{\<Union>(funas_term ` range (\<sigma> i)) | i. True}"
lemma funas_ichain_shift: "funas_ichain (shift s i) (shift t i) (shift \<sigma> i) \<subseteq> funas_ichain s t \<sigma>" unfolding funas_ichain_def by auto
@@ -269,13 +274,14 @@
using assms by (cases DPP) simp_all
-definition ci_subset :: "('f,'v)trs \<Rightarrow> ('f,'v)trs \<Rightarrow> bool"
-where "ci_subset R S \<equiv> \<forall> l r. (l,r) \<in> R \<longrightarrow> (\<exists> l' r' C. (l',r') \<in> S \<and> l = C\<langle>l'\<rangle> \<and> r = C\<langle>r'\<rangle>)"
+definition ci_subset :: "('f, 'v) trs \<Rightarrow> ('f, 'v) trs \<Rightarrow> bool" where
+ "ci_subset R S \<longleftrightarrow> (\<forall> l r. (l,r) \<in> R \<longrightarrow> (\<exists> l' r' C. (l',r') \<in> S \<and> l = C\<langle>l'\<rangle> \<and> r = C\<langle>r'\<rangle>))"
notation (xsymbols)
ci_subset ("(_/ \<subseteq>ci _)" [50,51] 50)
-lemma ci_subsetI: assumes "R \<subseteq> S"
+lemma ci_subsetI:
+ assumes "R \<subseteq> S"
shows "ci_subset R S"
unfolding ci_subset_def
proof (intro allI impI)
@@ -1052,7 +1058,8 @@
(* map each (P,Pw,..) chain to an (P',Pw',...)-chain via function f, where invariant I is established *)
-lemma finite_dpp_map: fixes P Pw R Rw P' Pw' R' Rw' :: "('f,'v)trs" and Q Q' :: "('f,'v)terms" and nfs nfs' m m'
+lemma finite_dpp_map:
+ fixes P Pw R Rw P' Pw' R' Rw' :: "('f,'v)trs" and Q Q' :: "('f,'v)terms" and nfs nfs' m m'
defines QR: "QR \<equiv> qrstep nfs Q R"
defines QRw: "QRw \<equiv> qrstep nfs Q Rw"
defines QP: "QP \<equiv> rqrstep nfs Q P \<inter> {(s,t). s \<in> NF_terms Q}"
@@ -1083,7 +1090,8 @@
(* map each (P,Pw,..) chain to an (P',Pw',...)-chain via function f, where invariant I is established *)
-lemma finite_dpp_map_min: fixes P Pw R Rw P' Pw' R' Rw' :: "('f,'v)trs" and Q Q' :: "('f,'v)terms" and m m' nfs nfs'
+lemma finite_dpp_map_min:
+ fixes P Pw R Rw P' Pw' R' Rw' :: "('f,'v)trs" and Q Q' :: "('f,'v)terms" and m m' nfs nfs'
defines QR: "QR \<equiv> qrstep nfs Q R"
defines QRw: "QRw \<equiv> qrstep nfs Q Rw"
defines QP: "QP \<equiv> rqrstep nfs Q P \<inter> {(s,t). s \<in> NF_terms Q}"
@@ -1316,16 +1324,16 @@
definition
subset_proc :: "(('f, 'v) dpp \<Rightarrow> ('f, 'v) dpp \<Rightarrow> bool) \<Rightarrow> bool"
where
- "subset_proc proc \<equiv> \<forall> nfs m P Pw Q R Rw nfs' m' P' Pw' Q' R' Rw'. proc (nfs,m,P,Pw,Q,R,Rw) (nfs',m',P',Pw',Q',R',Rw') \<longrightarrow>
+ "subset_proc proc \<longleftrightarrow> (\<forall> nfs m P Pw Q R Rw nfs' m' P' Pw' Q' R' Rw'. proc (nfs,m,P,Pw,Q,R,Rw) (nfs',m',P',Pw',Q',R',Rw') \<longrightarrow>
(R' \<union> Rw' \<subseteq> R \<union> Rw \<and> Q' = Q \<and> nfs' = nfs \<and> (m' \<longrightarrow> m) \<and> (\<forall>s t \<sigma>. min_ichain (nfs,m,P,Pw,Q,R,Rw) s t \<sigma> \<longrightarrow>
- (\<exists>i. ichain (nfs,m',P',Pw',Q',R',Rw') (shift s i) (shift t i) (shift \<sigma> i))))"
+ (\<exists>i. ichain (nfs,m',P',Pw',Q',R',Rw') (shift s i) (shift t i) (shift \<sigma> i)))))"
definition
sound_proc :: "(('f, 'v) dpp \<Rightarrow> ('f, 'v) dpp \<Rightarrow> bool) \<Rightarrow> bool"
where
- "sound_proc proc \<equiv> \<forall>nfs m P Pw Q R Rw nfs' m' P' Pw' Q' R' Rw'.
+ "sound_proc proc \<longleftrightarrow> (\<forall>nfs m P Pw Q R Rw nfs' m' P' Pw' Q' R' Rw'.
proc (nfs, m, P, Pw, Q, R, Rw) (nfs', m', P', Pw', Q', R', Rw') \<and> finite_dpp (nfs',m',P', Pw', Q', R', Rw') \<longrightarrow>
- finite_dpp (nfs,m,P, Pw, Q, R, Rw)"
+ finite_dpp (nfs,m,P, Pw, Q, R, Rw))"
lemma subset_proc_to_sound_proc:
assumes subset_proc: "subset_proc proc"
@@ -1365,3 +1373,4 @@
by (rule sound_proc[OF fin proc subset_proc_to_sound_proc[OF subset]])
end
+
diff --git a/IsaFoR/QDP_Framework_Impl.thy b/IsaFoR/QDP_Framework_Impl.thy
--- a/IsaFoR/QDP_Framework_Impl.thy
+++ b/IsaFoR/QDP_Framework_Impl.thy
@@ -120,6 +120,6 @@
abbreviation "shows_tp \<equiv> shows_tp' shows shows"
definition indent :: "shows \<Rightarrow> shows" where
- "indent p s \<equiv> concat (map (\<lambda>c. (if c = newline then newline # '' '' else [c])) (p s))"
+ "indent p s = concat (map (\<lambda>c. (if c = newline then newline # '' '' else [c])) (p s))"
-end
\ No newline at end of file
+end
diff --git a/IsaFoR/Q_Reduction.thy b/IsaFoR/Q_Reduction.thy
--- a/IsaFoR/Q_Reduction.thy
+++ b/IsaFoR/Q_Reduction.thy
@@ -36,7 +36,8 @@
from step obtain C l r \<sigma> where lr: "(l,r) \<in> R" and NF: "\<forall> u \<lhd> l \<cdot> \<sigma>. u \<in> ?Q'"
and s: "s = C\<langle>l\<cdot>\<sigma>\<rangle>" and t: "t = C\<langle>r\<cdot>\<sigma>\<rangle>"
and nfs: "NF_subst nfs (l,r) \<sigma> Q'" by auto
- from lr F have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def
+ from lr F have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F"
+ unfolding funas_trs_def funas_rule_def [abs_def]
by force+
from wf[unfolded wf_trs_def] lr have vars: "vars_term r \<subseteq> vars_term l" by auto
note switch = wwf_qtrs_imp_nfs_False_switch[OF wf_trs_imp_wwf_qtrs[OF wf], of nfs]
@@ -177,7 +178,8 @@
note SN = SN[OF this]
show "SN_on (qrstep nfs Q' (R \<union> Rw)) {t i \<cdot> \<sigma> i}"
proof (rule qrstep_reduced_Q_SN_on[OF inn _ F wf _ SN])
- from FP P[of i] have F: "funas_term (s i) \<subseteq> F" "funas_term (t i) \<subseteq> F" unfolding funas_trs_def funas_rule_def by force+
+ from FP P[of i] have F: "funas_term (s i) \<subseteq> F" "funas_term (t i) \<subseteq> F"
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
from NF_subterm[OF NF[of i] aliens_imp_supteq]
have nf: "set (aliens F (s i \<cdot> \<sigma> i)) \<subseteq> NF_terms Q" by auto
show "set (aliens F (t i \<cdot> \<sigma> i)) \<subseteq> NF_terms Q"
@@ -250,5 +252,4 @@
This will be the key for both relative termination and chains. Possible assumptions:
finite Q, type of function symbols is infinite *)
-
-end
\ No newline at end of file
+end
diff --git a/IsaFoR/Q_Reduction_Nonterm.thy b/IsaFoR/Q_Reduction_Nonterm.thy
--- a/IsaFoR/Q_Reduction_Nonterm.thy
+++ b/IsaFoR/Q_Reduction_Nonterm.thy
@@ -184,7 +184,8 @@
from step obtain C l r \<sigma> where lr: "(l,r) \<in> R" and NF: "\<forall> u \<lhd> l \<cdot> \<sigma>. u \<in> ?Q'"
and nfs: "NF_subst nfs (l,r) \<sigma> Q'"
and s: "s = C\<langle>l\<cdot>\<sigma>\<rangle>" and t: "t = C\<langle>r\<cdot>\<sigma>\<rangle>" by auto
- from lr F have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def
+ from lr F have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F"
+ unfolding funas_trs_def funas_rule_def [abs_def]
by force+
let ?\<sigma> = "clean_subst \<sigma>"
let ?c = clean_term
@@ -224,7 +225,7 @@
{
fix i
from P[of i] FP have F: "funas_term (s i) \<subseteq> F" "funas_term (t i) \<subseteq> F"
- unfolding funas_trs_def funas_rule_def by force+
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
note clean_subst_apply_term[OF F(1)] clean_subst_apply_term[OF F(2)]
} note subst = this
{
@@ -349,4 +350,4 @@
show ?thesis .
qed
-end
\ No newline at end of file
+end
diff --git a/IsaFoR/Q_Relative_Rewriting.thy b/IsaFoR/Q_Relative_Rewriting.thy
--- a/IsaFoR/Q_Relative_Rewriting.thy
+++ b/IsaFoR/Q_Relative_Rewriting.thy
@@ -53,7 +53,8 @@
ultimately show ?thesis by auto
qed
-definition qrs_ideriv where "qrs_ideriv nfs Q R S \<equiv> \<lambda> as. ideriv (qrstep nfs Q R) (qrstep nfs Q S) as"
+definition qrs_ideriv where
+ "qrs_ideriv nfs Q R S = (\<lambda> as. ideriv (qrstep nfs Q R) (qrstep nfs Q S) as)"
lemmas qrs_ideriv_defs = qrs_ideriv_def ideriv_def
@@ -111,10 +112,12 @@
by (rule SN_rel_ideriv)
definition rel_tt :: "(('f, 'v) qreltrs \<Rightarrow> ('f, 'v) qreltrs \<Rightarrow> bool) \<Rightarrow> bool" where
- "rel_tt tt \<equiv> \<forall>nfs Q R S rnfs rQ rR rS ts. (tt (nfs,Q, R, S) (rnfs,rQ, rR, rS) \<longrightarrow> qrs_ideriv nfs Q R S ts \<longrightarrow> (\<exists>ts'. qrs_ideriv rnfs rQ rR rS ts'))"
+ "rel_tt tt \<longleftrightarrow> (\<forall>nfs Q R S rnfs rQ rR rS ts.
+ (tt (nfs,Q, R, S) (rnfs,rQ, rR, rS) \<longrightarrow> qrs_ideriv nfs Q R S ts \<longrightarrow>
+ (\<exists>ts'. qrs_ideriv rnfs rQ rR rS ts')))"
definition SN_qrel :: "('f, 'v) qreltrs \<Rightarrow> bool" where
- "SN_qrel \<equiv> \<lambda>(nfs,Q, R, S). SN_rel (qrstep nfs Q R) (qrstep nfs Q S)"
+ "SN_qrel = (\<lambda>(nfs, Q, R, S). SN_rel (qrstep nfs Q R) (qrstep nfs Q S))"
lemma SN_qrel_split:
assumes sn1: "SN_qrel (nfs,Q, D \<inter> (R \<union> S), R \<union> S - D)"
@@ -128,7 +131,8 @@
show False unfolding SN_qrel_def rel_qrstep_SN by auto
qed
-lemma SN_qrel_map: fixes R Rw R' Rw' :: "('f,'v)trs" and Q Q' :: "('f,'v)terms" and nfs
+lemma SN_qrel_map:
+ fixes R Rw R' Rw' :: "('f, 'v) trs" and Q Q' :: "('f, 'v) terms" and nfs
defines QR: "QR \<equiv> qrstep nfs Q R"
defines QRw: "QRw \<equiv> qrstep nfs Q Rw"
defines QR': "QR' \<equiv> qrstep nfs Q' R'"
@@ -187,3 +191,4 @@
qed
end
+
diff --git a/IsaFoR/Q_Restricted_Rewriting.thy b/IsaFoR/Q_Restricted_Rewriting.thy
--- a/IsaFoR/Q_Restricted_Rewriting.thy
+++ b/IsaFoR/Q_Restricted_Rewriting.thy
@@ -221,7 +221,7 @@
(* and the special case standard rewriting *)
lemma qrstep_rstep_conv[simp]: "qrstep nfs {} R = rstep R"
-proof (intro equalityI subsetI2)
+proof (intro equalityI subrelI)
fix s t
assume "(s, t) \<in> rstep R"
then obtain C l r \<sigma> where s: "s = C \<langle> l \<cdot> \<sigma> \<rangle>" and t: "t = C \<langle> r \<cdot> \<sigma> \<rangle>"
@@ -1129,7 +1129,7 @@
lemma ctxt_closed_qrstep[intro]: "ctxt_closed (qrstep nfs Q R)"
unfolding ctxt_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t
assume "(s, t) \<in> CC (qrstep nfs Q R)"
thus "(s, t) \<in> qrstep nfs Q R" by induct auto
@@ -1280,7 +1280,7 @@
show "qrstep nfs Q ?U \<subseteq> qrstep nfs Q R" by (rule qrstep_rules_mono[OF applicable_rules_subset])
next
show "qrstep nfs Q R \<subseteq> qrstep nfs Q ?U"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t
assume "(s,t) \<in> qrstep nfs Q R"
then obtain l r C \<sigma> where "(l, r) \<in> R" and NF: "\<forall>u\<lhd>l \<cdot> \<sigma>. u \<in> NF_terms Q"
@@ -1557,7 +1557,8 @@
from qrstepE[OF step] obtain C \<sigma> l r
where nf: "\<forall>u\<lhd>l \<cdot> \<sigma>. u \<in> NF_terms Q" and lr: "(l, r) \<in> R" and s: "s = C\<langle>l \<cdot> \<sigma>\<rangle>" and t: "t = C\<langle>r \<cdot> \<sigma>\<rangle>" and nfs: "NF_subst nfs (l, r) \<sigma> Q" .
from only_applicable_rules[OF nf] lr wwf[unfolded wwf_qtrs_def] have vars: "vars_term r \<subseteq> vars_term l" by auto
- from RF lr have rF: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def by force
+ from RF lr have rF: "funas_term r \<subseteq> F"
+ unfolding funas_trs_def funas_rule_def [abs_def] by force
from sF show ?thesis unfolding s t using vars rF by (force simp: funas_term_subst)
qed
@@ -1602,7 +1603,7 @@
qed
next
show "?root \<union> ?nonroot \<subseteq> ?step"
- proof (intro subsetI2, elim UnE)
+ proof (intro subrelI, elim UnE)
fix s t assume "(s, t) \<in> rqrstep nfs Q R"
then obtain l r \<sigma> where NF: "\<forall>u\<lhd>l \<cdot> \<sigma>. u \<in> NF_terms Q" and
in_R: "(l, r) \<in> R" and s: "s = \<box>\<langle>l \<cdot> \<sigma>\<rangle>" and t: "t = \<box>\<langle>r \<cdot> \<sigma>\<rangle>"
@@ -3171,3 +3172,4 @@
qed
end
+
diff --git a/IsaFoR/ROOT b/IsaFoR/ROOT
--- a/IsaFoR/ROOT
+++ b/IsaFoR/ROOT
@@ -10,7 +10,6 @@
Ramsey
Zorn
-
session "HOL-AFP" = "HOL-Lib" +
description {* Theories from the Archive of Formal Proofs that are used by IsaFoR *}
options [document = false]
@@ -118,3 +117,4 @@
Show_Instances
Show_Generator
Show_Examples
+
diff --git a/IsaFoR/RPO.thy b/IsaFoR/RPO.thy
--- a/IsaFoR/RPO.thy
+++ b/IsaFoR/RPO.thy
@@ -1587,7 +1587,7 @@
proof (unfold_locales, rule RPO_S_SN)
show "subst_closed (RPO_NS_pr n)"
unfolding subst_closed_def
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t :: "('f, 'v) term"
assume "(s,t) \<in> CS (RPO_NS_pr n)"
then obtain u v and \<sigma>::"('f, 'v) subst"
@@ -1598,7 +1598,7 @@
next
show "subst_closed (RPO_S_pr n)"
unfolding subst_closed_def
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t :: "('f, 'v) term"
assume "(s,t) \<in> CS (RPO_S_pr n)"
then obtain u v and \<sigma> :: "('f, 'v) subst"
@@ -1956,3 +1956,4 @@
qed
end
+
diff --git a/IsaFoR/Semantic_Labeling.thy b/IsaFoR/Semantic_Labeling.thy
--- a/IsaFoR/Semantic_Labeling.thy
+++ b/IsaFoR/Semantic_Labeling.thy
@@ -2709,4 +2709,4 @@
sublocale sl_interpr_root_same \<subseteq> sl_interpr_same ..
-end
\ No newline at end of file
+end
diff --git a/IsaFoR/Show.thy b/IsaFoR/Show.thy
--- a/IsaFoR/Show.thy
+++ b/IsaFoR/Show.thy
@@ -142,7 +142,7 @@
val lthy'' = Class.prove_instantiation_instance (K (
Class.intro_classes_tac []
THEN rtac assoc_thm 1
- THEN unfold_tac [def_thm] (Simplifier.context lthy' HOL_basic_ss)
+ THEN unfold_tac [def_thm] lthy'
THEN rtac @{thm shows_list_aux_assoc} 1
THEN rtac @{thm ballI} 1
THEN rtac assoc_thm 1
diff --git a/IsaFoR/Signature_Extension.thy b/IsaFoR/Signature_Extension.thy
--- a/IsaFoR/Signature_Extension.thy
+++ b/IsaFoR/Signature_Extension.thy
@@ -21,8 +21,8 @@
Term_Impl
begin
-definition sig_step_below :: "'f sig \<Rightarrow> ('f,'v)trs \<Rightarrow> ('f,'v)trs"
- where "sig_step_below F R \<equiv> {(a,b) . (a,b) \<in> R \<and> funas_args_term a \<subseteq> F \<and> funas_args_term b \<subseteq> F}"
+definition sig_step_below :: "'f sig \<Rightarrow> ('f, 'v) trs \<Rightarrow> ('f, 'v) trs" where
+ "sig_step_below F R = {(a, b). (a,b) \<in> R \<and> funas_args_term a \<subseteq> F \<and> funas_args_term b \<subseteq> F}"
lemma sig_step_belowI[intro]: "(a,b) \<in> R \<Longrightarrow> funas_args_term a \<subseteq> F \<Longrightarrow> funas_args_term b \<subseteq> F \<Longrightarrow> (a,b) \<in> sig_step_below F R" unfolding sig_step_below_def by auto
@@ -64,7 +64,8 @@
proof -
have subset: "funas_trs(DP shp R) \<subseteq> F" using funas_DP_subset[of shp]
unfolding F_def sharp_sig_def by auto
- have "funas_term s \<subseteq> funas_trs(DP shp R)" using DP unfolding funas_trs_def funas_rule_def by auto
+ have "funas_term s \<subseteq> funas_trs (DP shp R)"
+ using DP unfolding funas_trs_def funas_rule_def [abs_def] by auto
with subset show ?thesis by auto
qed
@@ -152,7 +153,8 @@
from st obtain l r C \<sigma> where lr: "(l,r) \<in> R" and s: "s = C\<langle>l\<cdot>\<sigma>\<rangle>" and t: "t = C\<langle>r \<cdot> \<sigma>\<rangle>" and NF: "\<forall> u \<lhd> l \<cdot> \<sigma>. u \<in> NF_terms Q"
and nfs: "NF_subst nfs (l,r) \<sigma> Q" by auto
hence step: "(C\<langle>l\<cdot>\<sigma>\<rangle>,C\<langle>r\<cdot>\<sigma>\<rangle>) \<in> qrstep nfs Q {(l,r)}" by auto
- from lr F have r: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def by force
+ from lr F have r: "funas_term r \<subseteq> F"
+ unfolding funas_trs_def funas_rule_def [abs_def] by force
from only_applicable_rules[OF NF] have app: "applicable_rule Q (l,r)" .
note sF = sF[unfolded s]
from wwf[unfolded wwf_qtrs_def] lr app have "vars_term r \<subseteq> vars_term l" by auto
@@ -607,10 +609,10 @@
with fs have "?tsj i j \<in> set (args (t i \<cdot> \<sigma> i))" by simp
from j fs[of "Suc i"] argsteps[of i] have "ss (Suc i) ! j \<in> set (args (s (Suc i)))" by auto
with dpstep[of "Suc i"] subset_P have wf_s: "funas_term (ss (Suc i) ! j) \<subseteq> F"
- unfolding funas_args_defs by force
+ unfolding funas_args_defs [abs_def] by force
from j fs[of i] have "ts i ! j \<in> set (args (t i))" by auto
with dpstep[of i] subset_P have wf_t: "funas_term (ts i ! j) \<subseteq> F"
- unfolding funas_args_defs by force
+ unfolding funas_args_defs [abs_def] by force
have c_t: "ct(?tsj i j) = (?tsc i j)" unfolding ct_def cs_def
by (simp add: clean_subst_apply_term[OF wf_t])
have c_s: "ct(?ssj (Suc i) j) = (?ssc (Suc i) j)" unfolding ct_def cs_def
@@ -673,7 +675,8 @@
fix i
from ichain have "(s i, t i) \<in> P \<union> Pw" by (simp add: ichain.simps)
with subset_P non_var[OF this] obtain f ts where ti: "t i = Fun f ts" and tiP: "funas_args_term (Fun f ts) \<subseteq> F" and ndef: "(f, length (map (\<lambda> t. t \<cdot> cs (\<sigma> i)) ts)) \<notin> defs R"
- unfolding funas_args_trs_def funas_args_rule_def by (cases "t i", simp, force simp: defs_def)
+ unfolding funas_args_trs_def funas_args_rule_def [abs_def]
+ by (cases "t i") (simp, force simp: defs_def)
have "SN_on (rstep R) {t i \<cdot> (cs(\<sigma> i))}"
proof (simp add: ti, rule Trs.SN_args_imp_SN[OF _ nvar ndef])
fix u
@@ -929,7 +932,7 @@
proof (induct C)
case Hole
from lr FR have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F"
- unfolding funas_trs_def funas_rule_def by force+
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
from aliens_unary_subst[of r F \<sigma>, OF r unary]
have choice: "?a (r \<cdot> \<sigma>) = [] \<or> (\<exists> x \<in> vars_term r. ?a (r \<cdot> \<sigma>) = ?a (\<sigma> x))" by auto
show ?case
@@ -1006,7 +1009,7 @@
case Hole
let ?\<sigma> = "clean_subst \<sigma>"
from lr FR have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F"
- unfolding funas_trs_def funas_rule_def by force+
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
let ?pair = "(?c \<box>\<langle>l\<cdot>\<sigma>\<rangle>, ?c \<box>\<langle>r\<cdot>\<sigma>\<rangle>)"
have id: "?pair = (l \<cdot> ?\<sigma>, r \<cdot> ?\<sigma>)"
using clean_subst_apply_term[OF l] clean_subst_apply_term[OF r] by auto
@@ -1263,12 +1266,16 @@
qed
end
-locale cleaning_binary_const = cleaning_const F c const + cleaning_binary F c g n for F and c :: "('f,'v)term \<Rightarrow> ('f,'v)term" and const g n
+locale cleaning_binary_const =
+ cleaning_const F c const +
+ cleaning_binary F c g n
+ for F and c :: "('f, 'v) term \<Rightarrow> ('f, 'v) term" and const g n
begin
-lemma rstep_sig_step: fixes R :: "('f,'v)trs"
- assumes step: "(s,t) \<in> rstep R" and FR: "funas_trs R \<subseteq> F"
- shows "(clean_comb_term s,clean_comb_term t) \<in> sig_step F (rstep R)"
+lemma rstep_sig_step:
+ fixes R :: "('f, 'v) trs"
+ assumes step: "(s, t) \<in> rstep R" and FR: "funas_trs R \<subseteq> F"
+ shows "(clean_comb_term s, clean_comb_term t) \<in> sig_step F (rstep R)"
proof (rule sig_stepI[OF _ funas_term_clean_comb_term funas_term_clean_comb_term])
let ?c = "clean_comb_term"
from step obtain C l r \<sigma> where lr: "(l,r) \<in> R" and s: "s = C\<langle>l\<cdot>\<sigma>\<rangle>" and t: "t = C\<langle>r \<cdot> \<sigma>\<rangle>" by auto
@@ -1277,7 +1284,7 @@
case Hole
let ?\<sigma> = "clean_comb_subst \<sigma>"
from lr FR have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F"
- unfolding funas_trs_def funas_rule_def by force+
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
let ?pair = "(?c \<box>\<langle>l\<cdot>\<sigma>\<rangle>, ?c \<box>\<langle>r\<cdot>\<sigma>\<rangle>)"
have id: "?pair = (l \<cdot> ?\<sigma>, r \<cdot> ?\<sigma>)"
using clean_comb_subst_apply_term[OF l] clean_comb_subst_apply_term[OF r] by auto
@@ -1386,7 +1393,7 @@
let ?sR = "?ss (rstep ?R)"
let ?sS = "?ss (rstep ?S)"
have F: "funas_trs (?R \<union> ?S) = ?F"
- unfolding funas_trs_def funas_rule_def by auto
+ unfolding funas_trs_def funas_rule_def [abs_def] by auto
show ?thesis
proof (rule exI[of _ ?R], rule exI[of _ ?S], unfold F, rule conjI)
show "SN_rel ?sR ?sS" unfolding SN_rel_on_conv
@@ -1501,8 +1508,8 @@
from step obtain C l r \<sigma> where lr: "(l,r) \<in> R" and NF: "\<forall> u \<lhd> l \<cdot> \<sigma>. u \<in> ?Q"
and s: "s = C\<langle>l\<cdot>\<sigma>\<rangle>" and t: "t = C\<langle>r\<cdot>\<sigma>\<rangle>"
and nfs: "NF_subst nfs (l,r) \<sigma> Q" by auto
- from lr F have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def
- by force+
+ from lr F have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F"
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
note clr = clean_subst_apply_term[OF l] clean_subst_apply_term[OF r]
from only_applicable_rules[OF NF, of r] wwf lr have vars: "vars_term r \<subseteq> vars_term l"
unfolding wwf_qtrs_def by auto
@@ -1668,7 +1675,8 @@
with s have al: "a = l \<cdot> \<sigma>" by auto
from wwf_qtrs_imp_left_fun[OF wwf lr] obtain f ls where l: "l = Fun f ls" by auto
let ?f = "(f,length ls)"
- from F lr[unfolded l] have f: "?f \<in> F" unfolding funas_trs_def funas_rule_def by force
+ from F lr[unfolded l] have f: "?f \<in> F"
+ unfolding funas_trs_def funas_rule_def [abs_def] by force
hence "the (root a) \<in> F" unfolding al l by simp
with aliens_root[OF a] have False by auto
}
@@ -1724,7 +1732,7 @@
{
fix i
from P[of i] FP have F: "funas_term (s i) \<subseteq> F" "funas_term (t i) \<subseteq> F"
- unfolding funas_trs_def funas_rule_def by force+
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
} note F = this
note subst = clean_subst_apply_term[OF F(1)] clean_subst_apply_term[OF F(2)]
note qrsteps = clean_qrsteps[OF inn FR wwf, THEN conjunct1]
@@ -1734,7 +1742,8 @@
note qrelsteps = clean_rel_qrsteps[OF innB FRB wwfB, THEN conjunct1]
{
fix i
- from NF_subterm[OF NF[of i] aliens_imp_supteq] have "set (aliens F (s i \<cdot> \<sigma> i)) \<subseteq> ?Q" by auto
+ from NF_subterm[OF NF[of i] aliens_imp_supteq]
+ have "set (aliens F (s i \<cdot> \<sigma> i)) \<subseteq> ?Q" by auto
hence "set (aliens F (t i \<cdot> \<sigma> i)) \<subseteq> ?Q"
unfolding aliens_subst[OF F(1)]
unfolding aliens_subst[OF F(2)] using vars[OF P[of i]] by auto
@@ -1936,7 +1945,7 @@
fix i
from P[of i] non_var[OF P[of i]] FP have F: "funas_args_term (s i) \<subseteq> F" "is_Fun (s i)" "funas_args_term (t i) \<subseteq> F" "is_Fun (t i)"
"is_Fun (s i \<cdot> \<sigma> i)"
- unfolding funas_args_trs_def funas_args_rule_def by force+
+ unfolding funas_args_trs_def funas_args_rule_def [abs_def] by force+
} note F = this
note subst = clean_subst_apply_term_below[OF F(1-2)] clean_subst_apply_term_below[OF F(3-4)]
note qrsteps = clean_qrsteps_below[OF inn FR wwf, THEN conjunct1]
@@ -2024,7 +2033,8 @@
from step obtain C l r \<sigma> where lr: "(l,r) \<in> R" and NF: "\<forall> u \<lhd> l \<cdot> \<sigma>. u \<in> ?Q"
and s: "?c s = C\<langle>l\<cdot>\<sigma>\<rangle>" and u: "u = C\<langle>r\<cdot>\<sigma>\<rangle>"
and nfs: "NF_subst nfs (l,r) \<sigma> Q" by auto
- from lr F have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F" unfolding funas_trs_def funas_rule_def
+ from lr F have l: "funas_term l \<subseteq> F" and r: "funas_term r \<subseteq> F"
+ unfolding funas_trs_def funas_rule_def [abs_def]
by force+
note clr = clean_subst_apply_term[OF l] clean_subst_apply_term[OF r]
from only_applicable_rules[OF NF, of r] wwf lr have vars: "vars_term r \<subseteq> vars_term l"
@@ -2264,7 +2274,7 @@
from ichain have P: "(s i, t i) \<in> P \<union> Pw" by auto
from ichain have NF: "s i \<cdot> \<sigma> i \<in> ?Q" by auto
from P FP have F: "funas_term (s i) \<subseteq> F" "funas_term (t i) \<subseteq> F"
- unfolding funas_trs_def funas_rule_def by force+
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
note subst = clean_subst_apply_term[OF F(1)] clean_subst_apply_term[OF F(2)]
from NF_subterm[OF NF aliens_imp_supteq] have "set (aliens F (s i \<cdot> \<sigma> i)) \<subseteq> ?Q" by auto
hence aliens: "set (aliens F (t i \<cdot> \<sigma> i)) \<subseteq> ?Q"
@@ -2307,7 +2317,7 @@
from P FP non_var[OF P] have F: "funas_args_term (s i) \<subseteq> F" "is_Fun (s i)" "funas_args_term (t i) \<subseteq> F" "is_Fun (t i)"
and ndef: "\<not> defined (applicable_rules Q (R \<union> Rw)) (the (root (t i)))"
"\<not> defined (applicable_rules Q (R \<union> Rw)) (the (root (t i \<cdot> clean_subst (\<sigma> i))))"
- unfolding funas_args_trs_def funas_args_rule_def by force+
+ unfolding funas_args_trs_def funas_args_rule_def [abs_def] by force+
from F(4) obtain f ts where t: "t i = Fun f ts" by (cases "t i", auto)
from NF_subterm[OF NF aliens_below_imp_supteq] have "set (aliens_below F (s i \<cdot> \<sigma> i)) \<subseteq> ?Q" by auto
hence aliens: "set (aliens_below F (t i \<cdot> \<sigma> i)) \<subseteq> ?Q"
@@ -2336,4 +2346,5 @@
end
-end
\ No newline at end of file
+end
+
diff --git a/IsaFoR/Size_Change_Termination_Processors.thy b/IsaFoR/Size_Change_Termination_Processors.thy
--- a/IsaFoR/Size_Change_Termination_Processors.thy
+++ b/IsaFoR/Size_Change_Termination_Processors.thy
@@ -233,7 +233,7 @@
qed
next
show "?supteq O ?supt \<subseteq> ?supt"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s, t) \<in> ?supteq O ?supt"
then obtain u where fst: "(s, u) \<in> ?supteq" and snd: "(u, t) \<in> ?supt" by auto
have "(s, u) \<in> ?Rs" and "SN_on ?qrstep {s}" using fst unfolding restrict_SN_def by auto
@@ -428,3 +428,4 @@
qed
end
+
diff --git a/IsaFoR/String_Reversal.thy b/IsaFoR/String_Reversal.thy
--- a/IsaFoR/String_Reversal.thy
+++ b/IsaFoR/String_Reversal.thy
@@ -430,7 +430,8 @@
and "(l,r) \<in> R"
shows "unary_term l \<and> unary_term r"
proof -
- from assms have "unary_sig (funas_term l)" and "unary_sig (funas_term r)" unfolding unary_sig_def funas_trs_def funas_rule_def by auto
+ from assms have "unary_sig (funas_term l)" and "unary_sig (funas_term r)"
+ unfolding unary_sig_def funas_trs_def funas_rule_def [abs_def] by auto
with funas_unary_conv[of l] funas_unary_conv[of r] show ?thesis unfolding unary_sig_def by auto
qed
@@ -560,3 +561,4 @@
qed auto
end
+
diff --git a/IsaFoR/String_Reversal_Impl.thy b/IsaFoR/String_Reversal_Impl.thy
--- a/IsaFoR/String_Reversal_Impl.thy
+++ b/IsaFoR/String_Reversal_Impl.thy
@@ -36,7 +36,7 @@
show "(\<forall> x \<in> set R. (\<lambda>(l,r). unary_term l \<and> unary_term r) x) = ?r" (is "?l = _")
proof
assume ?l
- show ?r unfolding unary_sig_def funas_trs_def funas_rule_def
+ show ?r unfolding unary_sig_def funas_trs_def funas_rule_def [abs_def]
proof (rule ballI2)
fix f i
assume "(f,i) \<in> (\<Union>r \<in> set R. funas_term (fst r) \<union> funas_term (snd r))"
@@ -57,7 +57,7 @@
fix l r
assume lr: "(l, r) \<in> set R"
with `?r` lr have l: "\<forall> (f,i) \<in> funas_term l. i = 1" and r: "\<forall> (f,i) \<in> funas_term r. i = 1"
- unfolding unary_sig_def funas_trs_def funas_rule_def by auto
+ unfolding unary_sig_def funas_trs_def funas_rule_def [abs_def] by auto
show "unary_term l \<and> unary_term r" using funas_unary_conv[OF l] funas_unary_conv[OF r] ..
qed
qed
diff --git a/IsaFoR/Substitution.thy b/IsaFoR/Substitution.thy
--- a/IsaFoR/Substitution.thy
+++ b/IsaFoR/Substitution.thy
@@ -610,7 +610,10 @@
indDom: "subst_domain (subst_of ps) \<inter> \<Union> ((vars_term \<circ> snd) ` set eqs) \<subseteq> {}"
by auto
show "\<exists>f. subst_of (p # ps) = f \<and>
- (\<forall>p\<in>set (p # ps). f (the_Var (fst p)) = snd p) \<and> (\<forall>\<sigma>\<in>unifiers (set (p # ps)). \<sigma> = subst_of (p # ps) \<circ>s \<sigma>) \<and> subst_domain (subst_of (p # ps)) \<inter> \<Union>((vars_term \<circ> snd) ` set eqs) \<subseteq> {}"
+ (\<forall>p\<in>set (p # ps).
+ f (the_Var (fst p)) = snd p) \<and>
+ (\<forall>\<sigma>\<in>unifiers (set (p # ps)). \<sigma> = subst_of (p # ps) \<circ>s \<sigma>) \<and>
+ subst_domain (subst_of (p # ps)) \<inter> \<Union>((vars_term \<circ> snd) ` set eqs) \<subseteq> {}"
proof (cases p)
case (Pair s t)
show ?thesis
@@ -1654,3 +1657,4 @@
qed
end
+
diff --git a/IsaFoR/Term.thy b/IsaFoR/Term.thy
--- a/IsaFoR/Term.thy
+++ b/IsaFoR/Term.thy
@@ -251,14 +251,14 @@
fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P
fun tr' q = (q,
- fn [Const ("_bound", _) $ Free (v, T), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
+ K (fn [Const ("_bound", _) $ Free (v, T), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
(case AList.lookup (op =) trans (q, c, d) of
NONE => raise Match
| SOME (l, g) =>
if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
else raise Match)
- | _ => raise Match);
+ | _ => raise Match));
in [tr' All_binder, tr' Ex_binder] end
*}
@@ -524,7 +524,7 @@
declare ctxt_monoid_mult.mult_assoc[simp]
instantiation ctxt :: (type, type) monoid_mult begin
- definition [simp]: "1 \<equiv> \<box>"
+ definition [simp]: "1 = \<box>"
definition [simp]: "op * = op \<circ>c"
instance by (intro_classes) simp_all
end
@@ -952,7 +952,7 @@
subst_restrict :: "('f, 'v) subst \<Rightarrow> 'v set \<Rightarrow> ('f, 'v) subst"
(infix "|s" 67)
where
- "\<sigma> |s V \<equiv> (\<lambda>x. if x \<in> V then \<sigma>(x) else Var x)"
+ "\<sigma> |s V = (\<lambda>x. if x \<in> V then \<sigma>(x) else Var x)"
lemma subst_domain_Var[simp]: "subst_domain Var = {}" by (simp add: subst_domain_def)
@@ -1188,7 +1188,7 @@
definition
subst :: "'v \<Rightarrow> ('f, 'v) term \<Rightarrow> ('f, 'v) subst"
where
- "subst x t \<equiv> (\<lambda>y. if x = y then t else Var y)"
+ "subst x t = (\<lambda>y. if x = y then t else Var y)"
lemma Var_subst[simp]: "Var x \<cdot> subst x t = t" by (simp add: subst_def)
@@ -1487,8 +1487,6 @@
assumes "P x" and set:"\<And>y. y \<in> set xs \<Longrightarrow> P y" shows "y \<in> set(x#xs) \<Longrightarrow> P y"
using assms by auto
-
-
lemma ctxt_power_compose_distr:
"C ^ (m + n) = C ^ m \<circ>c C ^ n"
by (induct m) (simp_all)
@@ -1566,7 +1564,6 @@
show ?case unfolding id by (auto simp: ba)
qed simp
-
fun
subst_extend :: "('f, 'v,'w) gsubst \<Rightarrow> ('v \<times> ('f, 'w) term) list \<Rightarrow> ('f, 'v,'w) gsubst"
where
@@ -1591,7 +1588,8 @@
qed
lemma funas_term_args:
- shows "\<Union>(funas_term ` set (args t)) \<subseteq> funas_term t" by (cases t, auto)
+ shows "\<Union>(funas_term ` set (args t)) \<subseteq> funas_term t"
+ by (cases t) auto
lemma subst_extend_absorb:
assumes "distinct vs" and "length vs = length ss"
@@ -2021,10 +2019,9 @@
lemma var_type_conversion:
assumes inf: "infinite (UNIV :: 'v set)"
- and fin: "finite (T :: ('f,'w)term set)"
- shows "\<exists> (\<sigma> :: ('f,'w,'v)gsubst) \<tau>. \<forall>t\<in>T. t = t \<cdot> \<sigma> \<cdot> \<tau>"
+ and fin: "finite (T :: ('f, 'w) term set)"
+ shows "\<exists> (\<sigma> :: ('f, 'w, 'v) gsubst) \<tau>. \<forall>t\<in>T. t = t \<cdot> \<sigma> \<cdot> \<tau>"
proof -
- let ?m = "map_vars f :: ('f,'v)term \<Rightarrow> ('f,'w)term"
obtain V where V: "V = \<Union>(vars_term ` T)" by auto
have fin: "finite V" unfolding V
by (rule, rule, rule fin,
@@ -2073,7 +2070,6 @@
"map_vars Inr s \<cdot> (merge_substs \<sigma> \<delta>) = s \<cdot> \<delta>"
by (induct s) auto
-
fun map_vars_subst_ran :: "('w \<Rightarrow> 'u) \<Rightarrow> ('f, 'v,'w) gsubst \<Rightarrow> ('f, 'v,'u) gsubst" where
"map_vars_subst_ran m \<sigma> = (\<lambda>v. map_vars m (\<sigma> v))"
@@ -2115,7 +2111,6 @@
thus ?case by auto
qed
-
lemma map_term_ctxt_decomp: assumes "map_term fg t = C\<langle>s\<rangle>"
shows "\<exists> D u. C = map_ctxt fg D \<and> s = map_term fg u \<and> t = D\<langle>u\<rangle>"
using assms
@@ -2174,7 +2169,6 @@
lemma ground_ctxt_apply[simp]: "ground (C\<langle>t\<rangle>) = (ground_ctxt C \<and> ground t)"
by (induct C, auto)
-
lemma funas_term_map_vars[simp]: "funas_term (map_vars \<tau> t) = funas_term t"
by (induct t, auto)
@@ -2909,15 +2903,17 @@
hide_fact (open)
suptcp.arg suptcp.cases suptcp.induct suptcp.intros suptc.arg suptc.ctxt
-definition vars_subst :: "('f,'v)subst \<Rightarrow> 'v set"
- where "vars_subst \<sigma> \<equiv> subst_domain \<sigma> \<union> \<Union>(vars_term ` subst_range \<sigma>)"
-
-definition vars_subst_range where "vars_subst_range \<sigma> \<equiv> \<Union>(vars_term ` subst_range \<sigma>)"
-
-definition subst_compose' :: "('f,'v)subst \<Rightarrow> ('f,'v)subst \<Rightarrow> ('f,'v)subst"
- where "subst_compose' \<sigma> \<tau> \<equiv> \<lambda> x. if (x \<in> subst_domain \<sigma>) then \<sigma> x \<cdot> \<tau> else Var x"
-
-lemma vars_subst_compose': assumes "vars_subst \<tau> \<inter> subst_domain \<sigma> = {}"
+definition vars_subst :: "('f, 'v) subst \<Rightarrow> 'v set" where
+ "vars_subst \<sigma> = subst_domain \<sigma> \<union> \<Union>(vars_term ` subst_range \<sigma>)"
+
+definition vars_subst_range where
+ "vars_subst_range \<sigma> = \<Union>(vars_term ` subst_range \<sigma>)"
+
+definition subst_compose' :: "('f, 'v) subst \<Rightarrow> ('f, 'v) subst \<Rightarrow> ('f, 'v) subst" where
+ "subst_compose' \<sigma> \<tau> = (\<lambda> x. if (x \<in> subst_domain \<sigma>) then \<sigma> x \<cdot> \<tau> else Var x)"
+
+lemma vars_subst_compose':
+ assumes "vars_subst \<tau> \<inter> subst_domain \<sigma> = {}"
shows "\<sigma> \<circ>s \<tau> = \<tau> \<circ>s (subst_compose' \<sigma> \<tau>)" (is "?l = ?r")
proof
fix x
@@ -2961,7 +2957,8 @@
qed
qed
-lemma vars_subst_compose'_pow: assumes "vars_subst \<tau> \<inter> subst_domain \<sigma> = {}"
+lemma vars_subst_compose'_pow:
+ assumes "vars_subst \<tau> \<inter> subst_domain \<sigma> = {}"
shows "\<sigma> ^^ n \<circ>s \<tau> = \<tau> \<circ>s (subst_compose' \<sigma> \<tau>) ^^ n"
proof (induct n)
case 0 thus ?case by auto
@@ -2975,7 +2972,8 @@
finally show ?case by simp
qed
-lemma subst_pow_commute: assumes "\<sigma> \<circ>s \<tau> = \<tau> \<circ>s \<sigma>"
+lemma subst_pow_commute:
+ assumes "\<sigma> \<circ>s \<tau> = \<tau> \<circ>s \<sigma>"
shows "\<sigma> \<circ>s (\<tau> ^^ n) = \<tau> ^^ n \<circ>s \<sigma>"
proof (induct n)
case (Suc n)
@@ -2985,7 +2983,8 @@
finally show ?case .
qed simp
-lemma subst_power_commute: assumes "\<sigma> \<circ>s \<tau> = \<tau> \<circ>s \<sigma>"
+lemma subst_power_commute:
+ assumes "\<sigma> \<circ>s \<tau> = \<tau> \<circ>s \<sigma>"
shows "(\<sigma> ^^ n) \<circ>s (\<tau> ^^ n) = (\<sigma> \<circ>s \<tau>)^^n"
proof (induct n)
case (Suc n)
@@ -3001,7 +3000,8 @@
lemma vars_term_ctxt_apply: "vars_term (C\<langle>t\<rangle>) = vars_ctxt C \<union> vars_term t"
by (induct C, auto)
-lemma vars_ctxt_pos_term: assumes p: "p \<in> poss t"
+lemma vars_ctxt_pos_term:
+ assumes p: "p \<in> poss t"
shows "vars_term t = vars_ctxt (ctxt_of_pos_term p t) \<union> vars_term (t |_ p)"
proof -
let ?C = "ctxt_of_pos_term p t"
@@ -3013,15 +3013,17 @@
lemma Var_pow_Var[simp]: "Var ^^ n = Var"
by (rule, induct n, auto)
-definition var_renaming :: "('f,'v)subst \<Rightarrow> bool"
- where "var_renaming \<sigma> \<equiv> (\<forall>x. is_Var (\<sigma> x)) \<and> inj_on \<sigma> (subst_domain \<sigma>)"
-
-definition inverse_var_renaming :: "('f,'v)subst \<Rightarrow> ('f,'v)subst"
- where "inverse_var_renaming \<sigma> y \<equiv> if Var y \<in> subst_range \<sigma> then Var (the_inv_into (subst_domain \<sigma>) \<sigma> (Var y)) else Var y"
+definition var_renaming :: "('f, 'v) subst \<Rightarrow> bool" where
+ "var_renaming \<sigma> \<longleftrightarrow> (\<forall>x. is_Var (\<sigma> x)) \<and> inj_on \<sigma> (subst_domain \<sigma>)"
+
+definition inverse_var_renaming :: "('f, 'v) subst \<Rightarrow> ('f, 'v) subst" where
+ "inverse_var_renaming \<sigma> y = (
+ if Var y \<in> subst_range \<sigma> then Var (the_inv_into (subst_domain \<sigma>) \<sigma> (Var y))
+ else Var y)"
lemma var_renaming_inverse_domain:
assumes ren: "var_renaming \<sigma>"
- and x: "x \<in> subst_domain \<sigma>"
+ and x: "x \<in> subst_domain \<sigma>"
shows "Var x \<cdot> \<sigma> \<cdot> inverse_var_renaming \<sigma> = Var x" (is "_ \<cdot> ?\<sigma> = _")
proof -
note ren = ren[unfolded var_renaming_def]
@@ -3120,5 +3122,5 @@
qed
qed
-
end
+
diff --git a/IsaFoR/Term_Order.thy b/IsaFoR/Term_Order.thy
--- a/IsaFoR/Term_Order.thy
+++ b/IsaFoR/Term_Order.thy
@@ -34,7 +34,7 @@
lemma trans_split_NS_S_union:
assumes "r^* \<subseteq> (NS \<union> S)^*"
shows "r^* \<subseteq> S O S^* O NS^* \<union> NS^*"
-proof(rule subsetI2)
+proof(rule subrelI)
fix x y
assume "(x, y) \<in> r^*"
with assms have "(x,y) \<in> (NS \<union> S)^*" by auto
@@ -510,7 +510,9 @@
and cpx_class :: "('f,'v)complexity_measure \<Rightarrow> shows + complexity_class"
assumes cpx_class: "\<And> cm cc. cpx_class cm = Inr cc \<Longrightarrow> deriv_bound_measure_class S cm cc"
-locale cpx_ce_af_redtriple_order = ce_af_redtriple_order S NS NST \<pi> + cpx_term_rel S cpx_class for S NS NST :: "('f,'v)trs" and \<pi> and cpx_class
-
+locale cpx_ce_af_redtriple_order =
+ ce_af_redtriple_order S NS NST \<pi> + cpx_term_rel S cpx_class
+ for S NS NST :: "('f, 'v) trs" and \<pi> and cpx_class
end
+
diff --git a/IsaFoR/Term_Order_Extension.thy b/IsaFoR/Term_Order_Extension.thy
--- a/IsaFoR/Term_Order_Extension.thy
+++ b/IsaFoR/Term_Order_Extension.thy
@@ -165,7 +165,7 @@
fix l r
assume lr: "(l,r) \<in> R \<union> Rw"
with F have F: "funas_term l \<subseteq> F" "funas_term r \<subseteq> F"
- unfolding funas_trs_def funas_rule_def by force+
+ unfolding funas_trs_def funas_rule_def [abs_def] by force+
from SN_rel_imp_wf_reltrs[OF SN_rel_R_Rw]
have "wf_reltrs (R) (Rw)" .
with var_cond[of l r] lr orient(2) have vars: "vars_term r \<subseteq> vars_term l"
@@ -277,3 +277,4 @@
qed
end
+
diff --git a/IsaFoR/Termination_Problem_Spec.thy b/IsaFoR/Termination_Problem_Spec.thy
--- a/IsaFoR/Termination_Problem_Spec.thy
+++ b/IsaFoR/Termination_Problem_Spec.thy
@@ -153,4 +153,4 @@
end
-end
\ No newline at end of file
+end
diff --git a/IsaFoR/Trs.thy b/IsaFoR/Trs.thy
--- a/IsaFoR/Trs.thy
+++ b/IsaFoR/Trs.thy
@@ -40,35 +40,35 @@
subsection {* Variables of TRSs *}
definition vars_trs :: "('f, 'v) trs \<Rightarrow> 'v set" where
- "vars_trs R \<equiv> \<Union>r\<in>R. vars_rule r"
+ "vars_trs R = (\<Union>r\<in>R. vars_rule r)"
lemma vars_trs_union: "vars_trs (R \<union> S) = vars_trs R \<union> vars_trs S"
unfolding vars_trs_def by auto
lemma finite_trs_has_finite_vars:
assumes "finite R" shows "finite (vars_trs R)"
- using assms unfolding vars_trs_def vars_rule_def by simp
+ using assms unfolding vars_trs_def vars_rule_def [abs_def] by simp
lemmas vars_defs = vars_trs_def vars_rule_def
subsection {* Function Symbols of Rules *}
definition funs_rule :: "('f, 'v) rule \<Rightarrow> 'f set" where
- "funs_rule r \<equiv> funs_term (fst r) \<union> funs_term (snd r)"
+ "funs_rule r = funs_term (fst r) \<union> funs_term (snd r)"
text {* The same including arities. *}
definition funas_rule :: "('f, 'v) rule \<Rightarrow> 'f sig" where
- "funas_rule r \<equiv> funas_term (fst r) \<union> funas_term (snd r)"
+ "funas_rule r = funas_term (fst r) \<union> funas_term (snd r)"
subsection {* Function Symbols of TRSs *}
definition funs_trs :: "('f, 'v) trs \<Rightarrow> 'f set" where
- "funs_trs R \<equiv> \<Union>r\<in>R. funs_rule r"
+ "funs_trs R = (\<Union>r\<in>R. funs_rule r)"
definition funas_trs :: "('f, 'v) trs \<Rightarrow> 'f sig" where
- "funas_trs R \<equiv> \<Union>r\<in>R. funas_rule r"
+ "funas_trs R = (\<Union>r\<in>R. funas_rule r)"
lemma finite_funas_rule: "finite (funas_rule lr)"
unfolding funas_rule_def
@@ -85,19 +85,19 @@
unfolding funas_trs_def by blast
definition funas_args_rule :: "('f, 'v) rule \<Rightarrow> 'f sig" where
- "funas_args_rule r \<equiv> funas_args_term (fst r) \<union> funas_args_term (snd r)"
+ "funas_args_rule r = funas_args_term (fst r) \<union> funas_args_term (snd r)"
definition funas_args_trs :: "('f, 'v) trs \<Rightarrow> 'f sig" where
- "funas_args_trs R \<equiv> \<Union>r\<in>R. funas_args_rule r"
+ "funas_args_trs R = (\<Union>r\<in>R. funas_args_rule r)"
lemmas funas_args_defs =
funas_args_trs_def funas_args_rule_def funas_args_term_def
definition funas_root_rule :: "('f, 'v) rule \<Rightarrow> 'f sig" where
- "funas_root_rule r \<equiv> Option.set (root (fst r)) \<union> Option.set (root (snd r))"
+ "funas_root_rule r = Option.set (root (fst r)) \<union> Option.set (root (snd r))"
definition funas_root_trs :: "('f, 'v) trs \<Rightarrow> 'f sig" where
- "funas_root_trs R \<equiv> \<Union>r\<in>R. funas_root_rule r"
+ "funas_root_trs R = (\<Union>r\<in>R. funas_root_rule r)"
lemmas funas_root_defs =
funas_root_trs_def funas_root_rule_def
@@ -117,24 +117,26 @@
definition
defined :: "('f, 'v) trs \<Rightarrow> ('f \<times> nat) \<Rightarrow> bool"
where
- "defined R fn \<equiv> \<exists>l r. (l, r) \<in> R \<and> root l = Some fn"
+ "defined R fn \<longleftrightarrow> (\<exists>l r. (l, r) \<in> R \<and> root l = Some fn)"
text {* The set of all defined symbols. *}
definition
"defs" :: "('f, 'v) trs \<Rightarrow> ('f \<times> nat) set"
where
- "defs R \<equiv> {(f, n). defined R (f, n)}"
+ "defs R = {(f, n). defined R (f, n)}"
lemma defined_funas_trs: assumes d: "defined R fn" shows "fn \<in> funas_trs R"
proof -
- from d[unfolded defined_def] obtain l r where "(l,r) \<in> R" and "root l = Some fn" by auto
- thus ?thesis unfolding funas_trs_def funas_rule_def by (cases l, force+)
+ from d [unfolded defined_def] obtain l r
+ where "(l, r) \<in> R" and "root l = Some fn" by auto
+ thus ?thesis
+ unfolding funas_trs_def funas_rule_def [abs_def] by (cases l) force+
qed
-
text {* The remaining symbols are called \emph{constructor symbols}, since
they are only used to construct data. *}
-definition cons :: "('f, 'v) trs \<Rightarrow> ('f \<times> nat) set" where "cons R \<equiv> funas_trs R - defs R"
+definition cons :: "('f, 'v) trs \<Rightarrow> ('f \<times> nat) set" where
+ "cons R = funas_trs R - defs R"
text {* Closure under contexts of a binary relation on terms. *}
inductive_set
@@ -174,7 +176,7 @@
lemma ctxt_closed_trancl:
assumes "ctxt_closed R"
shows "ctxt_closed (R^+)"
-proof (unfold ctxt_closed_def, rule subsetI2)
+proof (unfold ctxt_closed_def, rule subrelI)
fix s t
assume "(s, t) \<in> CC (R\<^sup>+)"
thus "(s, t) \<in> R\<^sup>+"
@@ -237,7 +239,7 @@
assumes "ctxt_closed R" shows "quasi_commute R (op \<rhd>)" (is "quasi_commute ?r ?s")
proof -
have "?s O ?r \<subseteq> ?r O (?r \<union> ?s)^*"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix x y assume "(x,y) \<in> ?s O ?r"
then obtain z where "x \<rhd> z" and "(z,y) \<in> R" by best
with `ctxt_closed R` obtain w where "(x,w) \<in> R" and "w \<rhd> y"
@@ -253,7 +255,7 @@
lemma ctxt_closure_idemp[simp]: "CC (CC R) = (CC R)"
proof
show "CC(CC R) \<subseteq> CC R"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s,t) \<in> CC(CC R)"
thus "(s,t) \<in> CC R"
proof
@@ -269,7 +271,7 @@
qed
next
show "CC R \<subseteq> CC(CC R)"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s,t) \<in> CC R"
hence "(\<box>\<langle>s\<rangle>,\<box>\<langle>t\<rangle>) \<in> CC(CC R)" by (rule ctxt_closureI)
thus "(s,t) \<in> CC(CC R)" by auto
@@ -334,7 +336,7 @@
and s: "subst_closed s"
shows "subst_closed (r \<union> s)"
unfolding subst_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix x y
assume "(x,y) \<in> CS (r \<union> s)"
thus "(x,y) \<in> r \<union> s"
@@ -359,7 +361,7 @@
and s: "subst_closed s"
shows "subst_closed (r O s)"
unfolding subst_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix x y
assume "(x,y) \<in> CS (r O s)"
thus "(x,y) \<in> r O s"
@@ -381,7 +383,7 @@
assumes r: "subst_closed r"
shows "subst_closed (r^*)"
unfolding subst_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix x y
assume "(x,y) \<in> CS (r^*)"
thus "(x,y) \<in> r^*"
@@ -405,7 +407,7 @@
assumes r: "subst_closed r"
shows "subst_closed (r^+)"
unfolding subst_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix x y
assume "(x,y) \<in> CS (r^+)"
thus "(x,y) \<in> r^+"
@@ -464,7 +466,7 @@
lemma subst_subst_closed_subseteq_subst_closed:
fixes R::"('f, 'v) trs" shows "CS (CS R) \<subseteq> CS R"
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t :: "('f, 'v) term" assume a: "(s,t) \<in> CS (CS R)"
hence "\<exists>(\<sigma>::('f, 'v) subst) u v. (s = u\<cdot>\<sigma>) \<and> (t = v\<cdot>\<sigma>) \<and> (u,v) \<in> CS R"
using subst_closed_decompose by auto
@@ -484,7 +486,7 @@
lemma supteq_subst_closed: "subst_closed (op \<unrhd>)"
unfolding subst_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t :: "('f, 'v) term" assume "(s, t) \<in> CS (op \<unrhd>)"
then obtain u v and \<sigma> :: "('f, 'v) subst" where "u \<unrhd> v" and "u \<cdot> \<sigma> = s" and "v \<cdot> \<sigma> = t"
by (cases rule: subst_closure.cases) auto
@@ -493,7 +495,7 @@
lemma supt_subst_closed: "subst_closed (op \<rhd>)"
unfolding subst_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t :: "('f, 'v) term" assume "(s, t) \<in> CS (op \<rhd>)"
then obtain u v and \<sigma> :: "('f, 'v) subst" where s: "s = u \<cdot> \<sigma>" and t: "t = v \<cdot> \<sigma>" and "u \<rhd> v"
by (cases rule: subst_closure.cases) auto
@@ -548,7 +550,7 @@
unfolding ctxt_closed_def rstep_CC_CS ctxt_closure_idemp ..
lemma ctxt_closed_rstep_seq: "ctxt_closed ((rstep R)^*)" unfolding ctxt_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t assume "(s,t) \<in> CC((rstep R)^*)" thus "(s,t) \<in> (rstep R)^*"
proof (induct)
case (ctxt_closureI s t C) thus ?case
@@ -576,7 +578,7 @@
using subst_closure_rstep_subset unfolding subst_closed_def by auto
lemma subst_closed_rstep_seq: "subst_closed ((rstep R)^*)" unfolding subst_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t assume "(s,t) \<in> CS((rstep R)^*)" thus "(s,t) \<in> (rstep R)^*"
proof (induct)
case (subst_closureI s t \<sigma>) thus ?case
@@ -604,7 +606,7 @@
qed
lemma comp_subst_closed: assumes "subst_closed R" and "subst_closed S" shows "subst_closed(R O S)" unfolding subst_closed_def
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t assume "(s,t) \<in> CS(R O S)"
then obtain u v \<sigma> where s: "s = u \<cdot> \<sigma>" and t: "t = v \<cdot> \<sigma>" and "(u,v) \<in> R O S" by (cases rule: subst_closure.cases) auto
from `(u,v) \<in> R O S` obtain w where "(u,w) \<in> R" and "(w,v) \<in> S" by auto
@@ -644,7 +646,7 @@
definition
rstep_r_p_s :: "('f, 'v) trs \<Rightarrow> ('f, 'v) rule \<Rightarrow> pos \<Rightarrow> ('f, 'v) subst \<Rightarrow> ('f, 'v) trs"
where
- "rstep_r_p_s R r p \<sigma> \<equiv> {(s,t).
+ "rstep_r_p_s R r p \<sigma> = {(s,t).
let C = ctxt_of_pos_term p s in p \<in> poss s \<and> r \<in> R \<and> (C\<langle>fst r\<cdot>\<sigma>\<rangle> = s) \<and> (C\<langle>snd r\<cdot>\<sigma>\<rangle> = t)}"
lemma rstep_r_p_s_def': "rstep_r_p_s R r p \<sigma> = {(s,t). p \<in> poss s \<and> r \<in> R \<and> s |_ p = fst r \<cdot> \<sigma> \<and> t = replace_at s p (snd r \<cdot> \<sigma>)}" (is "?l = ?r")
@@ -718,7 +720,7 @@
definition
nrrstep :: "('f, 'v) trs \<Rightarrow> ('f, 'v) trs"
where
- "nrrstep R \<equiv> {(s,t). \<exists>r i ps \<sigma>. (s,t) \<in> rstep_r_p_s R r (i<#ps) \<sigma>}"
+ "nrrstep R = {(s,t). \<exists>r i ps \<sigma>. (s,t) \<in> rstep_r_p_s R r (i<#ps) \<sigma>}"
text {* An alternative characterisation of non-root rewrite steps. *}
lemma nrrstep_def':
@@ -726,7 +728,7 @@
(is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s, t) \<in> nrrstep R"
then obtain l r i ps \<sigma> where step: "(s, t) \<in> rstep_r_p_s R (l, r) (i <# ps) \<sigma>"
unfolding nrrstep_def by best
@@ -738,7 +740,7 @@
qed
next
show "?rhs \<subseteq> ?lhs"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s, t) \<in> ?rhs"
then obtain l r C \<sigma> where in_R: "(l, r) \<in> R" and "C \<noteq> \<box>"
and s: "s = C\<langle>l\<cdot>\<sigma>\<rangle>" and t: "t = C\<langle>r\<cdot>\<sigma>\<rangle>" by auto
@@ -761,7 +763,7 @@
definition
rrstep :: "('f, 'v) trs \<Rightarrow> ('f, 'v) trs"
where
- "rrstep R \<equiv> {(s,t). \<exists>r \<sigma>. (s,t) \<in> rstep_r_p_s R r \<epsilon> \<sigma>}"
+ "rrstep R = {(s,t). \<exists>r \<sigma>. (s,t) \<in> rstep_r_p_s R r \<epsilon> \<sigma>}"
text {* An alternative characterisation of root rewrite steps. *}
lemma rrstep_def': "rrstep R = {(s, t). \<exists>l r \<sigma>. (l, r) \<in> R \<and> s = l\<cdot>\<sigma> \<and> t = r\<cdot>\<sigma>}"
@@ -793,7 +795,7 @@
lemma rstep_iff_rrstep_or_nrrstep: "rstep R = (rrstep R \<union> nrrstep R)"
proof
show "rstep R \<subseteq> rrstep R \<union> nrrstep R"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s,t) \<in> rstep R"
then obtain l r p \<sigma> where rstep_rps: "(s,t) \<in> rstep_r_p_s R (l,r) p \<sigma>"
by (auto simp: rstep_iff_rstep_r_p_s)
@@ -801,7 +803,7 @@
qed
next
show "rrstep R \<union> nrrstep R \<subseteq> rstep R"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s,t) \<in> rrstep R \<union> nrrstep R"
thus "(s,t) \<in> rstep R" by (auto simp: rrstep_def nrrstep_def rstep_iff_rstep_r_p_s)
qed
@@ -841,7 +843,7 @@
using subst_closure_rstep_subset subst_closed_correctness unfolding subst_closed_def by blast
lemma supt_rstep_subset: "op \<rhd> O rstep R \<subseteq> rstep R O op \<rhd>"
-proof (rule subsetI2)
+proof (rule subrelI)
fix s t assume "(s,t) \<in> op \<rhd> O rstep R" thus "(s,t) \<in> rstep R O op \<rhd>"
proof (induct s)
case (Var x)
@@ -898,8 +900,8 @@
ultimately show ?case by fast
qed
-definition restrict_SN_supt :: "('f, 'v) trs \<Rightarrow> ('f, 'v) trs"
-where "restrict_SN_supt R \<equiv> (restrict_SN R R) \<union> (restrict_SN (op \<rhd>) R)"
+definition restrict_SN_supt :: "('f, 'v) trs \<Rightarrow> ('f, 'v) trs" where
+ "restrict_SN_supt R = (restrict_SN R R) \<union> (restrict_SN (op \<rhd>) R)"
lemma restrict_SN_imp_SN_subt:
assumes "ctxt_closed R" and "SN_on R {s}" and "s \<unrhd> t"
@@ -944,7 +946,7 @@
shows "quasi_commute (restrict_SN R R) (restrict_SN supt R)" (is "quasi_commute ?r ?s")
proof -
have "?s O ?r \<subseteq> ?r O (?r \<union> ?s)^*"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix x y
assume "(x,y) \<in> ?s O ?r"
from this obtain z where "(x,z) \<in> ?s" and "(z,y) \<in> ?r" by best
@@ -1748,12 +1750,12 @@
qed
lemma cs_subseteq_cs_ext1': "CS R \<subseteq> CS (R \<union> S)"
-by (intro subsetI2) (rule cs_subseteq_cs_ext1)
+by (intro subrelI) (rule cs_subseteq_cs_ext1)
lemma cs_union_distr: "CS(R \<union> S) = (CS R) \<union> (CS S)"
proof
show "CS (R \<union> S) \<subseteq> ((CS R) \<union> (CS S))"
- proof (intro subsetI2)
+ proof (intro subrelI)
fix s t assume "(s,t) \<in> CS(R \<union> S)"
then obtain \<sigma> u v where RS:"(u,v) \<in> (R \<union> S)" and s:"s = u\<cdot>\<sigma>" and t:"t = v\<cdot>\<sigma>"
by (cases rule: subst_closure.cases) auto
@@ -1768,7 +1770,7 @@
qed
next
show "(CS R) \<union> (CS S) \<subseteq> CS (R \<union> S)"
- proof (intro subsetI2)
+ proof (intro subrelI)
fix s t assume "(s,t) \<in> CS R \<union> CS S"
hence "(s,t) \<in> CS R \<or> (s,t) \<in> CS S" by simp
thus "(s,t) \<in> CS(R \<union> S)"
@@ -1802,7 +1804,7 @@
lemma cc_union_distr: "CC(R \<union> S) = (CC R) \<union> (CC S)"
proof
show "CC (R \<union> S) \<subseteq> (CC R \<union> CC S)"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s,t) \<in> CC(R \<union> S)"
then obtain C u v where RS:"(u,v) \<in> (R \<union> S)" and s:"s = C\<langle>u\<rangle>" and t:"t = C\<langle>v\<rangle>"
by (cases rule: ctxt_closure.cases) auto
@@ -1816,7 +1818,7 @@
qed
next
show "(CC R) \<union> (CC S) \<subseteq> CC (R \<union> S)"
- proof (rule subsetI2)
+ proof (rule subrelI)
fix s t assume "(s,t) \<in> CC R \<union> CC S"
hence "(s,t) \<in> CC R \<or> (s,t) \<in> CC S" by simp
thus "(s,t) \<in> CC(R \<union> S)"
@@ -2135,7 +2137,7 @@
by (auto intro: ctxt_closed_rtrancl ctxt_closed_comp)
definition all_ctxt_closed :: "('f, 'v) trs \<Rightarrow> bool" where
- "all_ctxt_closed r \<equiv> (\<forall>f ts ss.
+ "all_ctxt_closed r \<longleftrightarrow> (\<forall>f ts ss.
length ts = length ss \<and>
(\<forall>i. i < length ts \<longrightarrow> (ts ! i, ss ! i) \<in> r) \<longrightarrow> (Fun f ts, Fun f ss) \<in> r) \<and> (\<forall> x. (Var x, Var x) \<in> r)"
@@ -2480,13 +2482,17 @@
proof -
from `(s,t) \<in> rstep R` obtain l r C \<sigma> where R: "(l,r) \<in> R"
and s: "s = C\<langle>l\<cdot>\<sigma>\<rangle>" and t: "t = C\<langle>r\<cdot>\<sigma>\<rangle>" using rstep_imp_C_s_r[of s t R] by fast
- from `funas_trs R \<subseteq> F` and R have "funas_term r \<subseteq> F" unfolding funas_defs by force
+ from `funas_trs R \<subseteq> F` and R have "funas_term r \<subseteq> F"
+ unfolding funas_defs [abs_def] by force
from `wf_trs R` and R have "vars_term r \<subseteq> vars_term l" unfolding wf_trs_def by simp
have "funas_term s = funas_ctxt C \<union> funas_term(l\<cdot>\<sigma>)" unfolding s by simp
- hence funas_s: "funas_term s = funas_ctxt C \<union> funas_term l \<union> \<Union>(funas_term ` \<sigma> ` vars_term l)" using funas_term_subst by auto
+ hence funas_s: "funas_term s = funas_ctxt C \<union> funas_term l \<union> \<Union>(funas_term ` \<sigma> ` vars_term l)"
+ using funas_term_subst by auto
have "funas_term t = funas_ctxt C \<union> funas_term(r\<cdot>\<sigma>)" unfolding t by simp
- hence "funas_term t = funas_ctxt C \<union> funas_term r \<union> \<Union>(funas_term ` \<sigma> ` vars_term r)" using funas_term_subst by auto
- hence "funas_term t \<subseteq> funas_ctxt C \<union> funas_term r \<union> \<Union>(funas_term ` \<sigma> ` vars_term l)" using `vars_term r \<subseteq> vars_term l` by auto
+ hence "funas_term t = funas_ctxt C \<union> funas_term r \<union> \<Union>(funas_term ` \<sigma> ` vars_term r)"
+ using funas_term_subst by auto
+ hence "funas_term t \<subseteq> funas_ctxt C \<union> funas_term r \<union> \<Union>(funas_term ` \<sigma> ` vars_term l)"
+ using `vars_term r \<subseteq> vars_term l` by auto
with `funas_term r \<subseteq> F` `funas_term s \<subseteq> F` have "funas_term t \<subseteq> F" unfolding funas_s by force
thus ?thesis by auto
qed
@@ -2509,11 +2515,11 @@
lemma lhs_wf:
assumes R: "(l,r) \<in> R" and subset: "funas_trs R \<subseteq> F" shows "funas_term l \<subseteq> F"
- using assms unfolding funas_trs_def funas_rule_def by force
+ using assms unfolding funas_trs_def funas_rule_def [abs_def] by force
lemma rhs_wf:
assumes R: "(l,r) \<in> R" and subset: "funas_trs R \<subseteq> F" shows "funas_term r \<subseteq> F"
- using assms unfolding funas_trs_def funas_rule_def by force
+ using assms unfolding funas_trs_def funas_rule_def [abs_def] by force
lemma subst_dom: "s\<cdot>\<sigma> = s\<cdot>\<tau> \<Longrightarrow> vars_term t \<subseteq> vars_term s \<Longrightarrow> t\<cdot>\<sigma> = t\<cdot>\<tau>" by (induct t) (induct s,auto)
@@ -2588,7 +2594,8 @@
and "(f,length ss) \<notin> defs R"
shows "\<exists>ts. length ts = length ss \<and> t = Fun f ts \<and> (\<forall>i<length ss. (ss!i,ts!i) \<in> (rstep R)^*)"
proof -
- from assms obtain n where "(Fun f ss,t) \<in> (rstep R)^^n" using rtrancl_imp_relpow' by best
+ from assms obtain n where "(Fun f ss,t) \<in> (rstep R)^^n"
+ using rtrancl_imp_relpow by best
thus ?thesis
proof (induct n arbitrary: t)
case 0 thus ?case by auto
@@ -3173,8 +3180,8 @@
lemma map_trs_id[simp]: "map_trs id = id"
by (intro ext, auto simp: map_trs.simps)
-definition sig_step :: "'f sig \<Rightarrow> ('f,'v)trs \<Rightarrow> ('f,'v)trs"
- where "sig_step F R \<equiv> {(a,b) . (a,b) \<in> R \<and> funas_term a \<subseteq> F \<and> funas_term b \<subseteq> F}"
+definition sig_step :: "'f sig \<Rightarrow> ('f, 'v) trs \<Rightarrow> ('f, 'v) trs" where
+ "sig_step F R = {(a, b). (a, b) \<in> R \<and> funas_term a \<subseteq> F \<and> funas_term b \<subseteq> F}"
lemma sig_stepI[intro]: "(a,b) \<in> R \<Longrightarrow> funas_term a \<subseteq> F \<Longrightarrow> funas_term b \<subseteq> F \<Longrightarrow> (a,b) \<in> sig_step F R" unfolding sig_step_def by auto
@@ -3415,7 +3422,7 @@
"funas_trs(DP shp R)
\<subseteq> funas_trs R \<union> {(shp f,n) | f n. (f,n) \<in> funas_trs R}"
(is "?F \<subseteq> ?H \<union> ?I")
-proof (rule subsetI2)
+proof (rule subrelI)
fix f n
assume "(f,n) \<in> ?F"
then obtain s t where st: "(s,t) \<in> DP shp R" and "(f,n) \<in> funas_rule (s,t)"
@@ -3520,12 +3527,12 @@
qed
-definition instance_rule :: "('f,'v)rule \<Rightarrow> ('f,'w)rule \<Rightarrow> bool"
-where [code del]: "instance_rule lr st = (\<exists> \<sigma>. fst lr = fst st \<cdot> \<sigma> \<and> snd lr = snd st \<cdot> \<sigma>)"
+definition instance_rule :: "('f, 'v) rule \<Rightarrow> ('f, 'w) rule \<Rightarrow> bool" where
+ [code del]: "instance_rule lr st \<longleftrightarrow> (\<exists> \<sigma>. fst lr = fst st \<cdot> \<sigma> \<and> snd lr = snd st \<cdot> \<sigma>)"
(* instance rule has implementation in Substitution.thy *)
-definition eq_rule_mod_vars :: "('f,'v)rule \<Rightarrow> ('f,'v)rule \<Rightarrow> bool"
-where "eq_rule_mod_vars lr st \<equiv> instance_rule lr st \<and> instance_rule st lr"
+definition eq_rule_mod_vars :: "('f, 'v) rule \<Rightarrow> ('f, 'v) rule \<Rightarrow> bool" where
+ "eq_rule_mod_vars lr st \<longleftrightarrow> instance_rule lr st \<and> instance_rule st lr"
notation eq_rule_mod_vars ("(_/ =v _)" [51,51] 50)
@@ -3607,7 +3614,7 @@
definition
left_linear_trs :: "('f, 'v) trs \<Rightarrow> bool"
where
- "left_linear_trs R \<equiv> \<forall>(l, r)\<in>R. linear_term l"
+ "left_linear_trs R \<longleftrightarrow> (\<forall>(l, r)\<in>R. linear_term l)"
lemma left_linear_mono: assumes "left_linear_trs S" and "R \<subseteq> S" shows "left_linear_trs R"
using assms unfolding left_linear_trs_def by auto
@@ -3786,8 +3793,8 @@
"rhss R \<equiv> snd ` R"
-definition map_trs_wa :: "('f \<Rightarrow> nat \<Rightarrow> 'g) \<Rightarrow> ('f,'v)trs \<Rightarrow> ('g,'v)trs"
-where "map_trs_wa fg R \<equiv> (\<lambda>(l,r). (map_term_wa fg l, map_term_wa fg r)) ` R"
+definition map_trs_wa :: "('f \<Rightarrow> nat \<Rightarrow> 'g) \<Rightarrow> ('f, 'v) trs \<Rightarrow> ('g, 'v) trs" where
+ "map_trs_wa fg R = (\<lambda>(l, r). (map_term_wa fg l, map_term_wa fg r)) ` R"
lemma map_trs_wa_union: "map_trs_wa fg (R \<union> S) = map_trs_wa fg R \<union> map_trs_wa fg S"
unfolding map_trs_wa_def by auto
@@ -3829,19 +3836,19 @@
qed
-definition compact :: "('f,'v)term set \<Rightarrow> ('f,'v)trs \<Rightarrow> bool"
- where "compact L R \<equiv> \<exists> F. finite F \<and> \<Union>(funas_term ` {t | s t. s \<in> L \<and> (s,t) \<in> (rstep R)^*}) \<subseteq> F"
-
-definition locally_terminating :: "('f,'v)trs \<Rightarrow> bool"
- where "locally_terminating R \<equiv> \<forall> F. finite F \<longrightarrow> SN (sig_step F (rstep R))"
+definition compact :: "('f, 'v) term set \<Rightarrow> ('f, 'v) trs \<Rightarrow> bool" where
+ "compact L R \<longleftrightarrow> (\<exists> F. finite F \<and> \<Union>(funas_term ` {t | s t. s \<in> L \<and> (s,t) \<in> (rstep R)^*}) \<subseteq> F)"
+
+definition locally_terminating :: "('f, 'v) trs \<Rightarrow> bool" where
+ "locally_terminating R \<longleftrightarrow> (\<forall> F. finite F \<longrightarrow> SN (sig_step F (rstep R)))"
lemma locally_terminating_compact:
assumes lterm: "locally_terminating R"
- and compact: "compact L R"
- and t: "t \<in> L"
+ and compact: "compact L R"
+ and t: "t \<in> L"
shows "SN_on (rstep R) {t}"
proof -
- let ?L = "{s. (t,s) \<in> (rstep R)^*}"
+ let ?L = "{s. (t, s) \<in> (rstep R)^*}"
from compact[unfolded compact_def] t obtain F where
F: "finite F"
and wf_terms: "\<Union>(funas_term ` ?L) \<subseteq> F"
@@ -3935,10 +3942,10 @@
by (rule iffI) (auto simp: wf_trs_def is_Fun_Fun_conv)
definition wf_rule :: "('f, 'v) rule \<Rightarrow> bool" where
- "wf_rule r \<equiv> is_Fun (fst r) \<and> vars_term (snd r) \<subseteq> vars_term (fst r)"
+ "wf_rule r \<longleftrightarrow> is_Fun (fst r) \<and> vars_term (snd r) \<subseteq> vars_term (fst r)"
definition wf_rules :: "('f, 'v) trs \<Rightarrow> ('f, 'v) trs" where
- "wf_rules R \<equiv> {r. r \<in> R \<and> wf_rule r}"
+ "wf_rules R = {r. r \<in> R \<and> wf_rule r}"
lemma wf_trs_wf_rules[simp]: "wf_trs (wf_rules R)"
unfolding wf_trs_def' wf_rules_def wf_rule_def split_def by simp
@@ -3995,7 +4002,7 @@
lemmas rstep_wf_rules_subset = rstep_mono[OF wf_rules_subset]
definition map_vars_trs :: "('v \<Rightarrow> 'w) \<Rightarrow> ('f, 'v) trs \<Rightarrow> ('f, 'w) trs" where
- "map_vars_trs f R \<equiv> (\<lambda> (l, r). (map_vars f l, map_vars f r)) ` R"
+ "map_vars_trs f R = (\<lambda> (l, r). (map_vars f l, map_vars f r)) ` R"
lemma map_vars_rstep:
assumes "(s, t) \<in> rstep (map_vars_trs f R)" (is "_ \<in> rstep ?R")
@@ -4055,5 +4062,5 @@
lemma CS_rrstep_conv: "CS = rrstep"
by (intro ext, unfold rrstep_def', rule, insert subst_closed_decompose, blast, auto)
-
end
+
diff --git a/IsaFoR/Trs_Impl.thy b/IsaFoR/Trs_Impl.thy
--- a/IsaFoR/Trs_Impl.thy
+++ b/IsaFoR/Trs_Impl.thy
@@ -384,10 +384,10 @@
lemma funas_root_rules_list_sound[simp]:
"set (funas_root_rules_list rs) = funas_root_trs (set rs)"
- unfolding funas_root_rules_list_def funas_defs by simp
+ unfolding funas_root_rules_list_def funas_defs [abs_def] by simp
definition funas_trs_list :: "('f, 'v) rule list \<Rightarrow> ('f \<times> nat) list" where
- "funas_trs_list R \<equiv> remdups (concat (map funas_rule_list' R))"
+ "funas_trs_list R = remdups (concat (map funas_rule_list' R))"
lemma funas_trs_list_sound[simp]:
"set (funas_trs_list R) = funas_trs (set R)"
diff --git a/IsaFoR/XML_Parser.thy b/IsaFoR/XML_Parser.thy
--- a/IsaFoR/XML_Parser.thy
+++ b/IsaFoR/XML_Parser.thy
@@ -105,10 +105,8 @@
f x ts'
}"
-
-setup {*
- Adhoc_Overloading.add_variant @{const_name Monad_Syntax.bind} @{const_name bind}
-*}
+adhoc_overloading
+ Monad_Syntax.bind bind
lemma bind_cong[fundef_cong]:
fixes m1 :: "('t,'a)gen_parser"
@@ -419,8 +417,9 @@
lemma letters_impl [code]: "(c \<in> set letters) = letters_impl c"
proof (cases c)
case (Char n1 n2)
- show ?thesis unfolding Char letters_def
- by (cases n1, simp_all add: nat_of_char.simps, (cases n2, simp_all)+)
+ show ?thesis
+ unfolding Char letters_def
+ by (cases n1, simp_all add: nat_of_char_def) (cases n2, simp_all)+
qed
lemma many_letters [code_unfold]: "many_letters = many letters_impl"
@@ -804,3 +803,4 @@
}"
end
+
More information about the isabelle-dev
mailing list