isar-keywords.el
- I am not sure what has changed here
nominal.thy
- includes a number of new lemmas (including freshness
and perm_aux things)
nominal_atoms.ML
- no particular changes here
nominal_permeq.ML
- a new version of the decision procedure using
for permutation composition the constant perm_aux
examples
- various adjustments
--- a/src/HOL/Nominal/Examples/CR.thy Wed Apr 26 22:40:46 2006 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy Thu Apr 27 01:41:30 2006 +0200
@@ -32,7 +32,7 @@
assumes asm: "a\<sharp>t\<^isub>1"
shows "t\<^isub>1[a::=t\<^isub>2] = t\<^isub>1"
using asm by (nominal_induct t\<^isub>1 avoiding: a t\<^isub>2 rule: lam.induct)
- (auto simp add: abs_fresh fresh_atm)
+ (auto simp add: abs_fresh fresh_atm)
lemma fresh_fact:
fixes a :: "name"
@@ -108,7 +108,7 @@
have ih: "\<And>x y N L. \<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
have "x\<noteq>y" by fact
have "x\<sharp>L" by fact
- have "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact
+ have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact
hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact)
show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS")
proof -
--- a/src/HOL/Nominal/Examples/Class.thy Wed Apr 26 22:40:46 2006 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Thu Apr 27 01:41:30 2006 +0200
@@ -176,6 +176,31 @@
apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
done
+lemma rec_fin_supp:
+assumes f: "finite ((supp (f1,f2,f3,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12))::name set)"
+ and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>t (r::'a::pt_name). a\<sharp>f3 a t r)"
+ and a: "(t,r) \<in> trm_rec_set f1 f2 f3"
+ shows "finite ((supp r)::name set)"
+using a
+proof (induct)
+ case goal1 thus ?case using f by (finite_guess add: supp_prod fs_name1)
+next
+ case goal2 thus ?case using f by (finite_guess add: supp_prod fs_name1)
+next
+ case (goal3 c t r)
+ have ih: "finite ((supp r)::name set)" by fact
+ let ?g' = "\<lambda>pi a'. f3 a' ((pi@[(c,a')])\<bullet>t) (r (pi@[(c,a')]))" --"helper function"
+ have fact1: "\<forall>pi. finite ((supp (?g' pi))::name set)" using f ih
+ by (rule_tac allI, finite_guess add: perm_append supp_prod fs_name1)
+ have fact2: "\<forall>pi. \<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')"
+ proof
+ fix pi::"name prm"
+ show "\<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" using f c ih
+ by (rule_tac f3_freshness_conditions_simple, simp_all add: supp_prod)
+ qed
+ show ?case using fact1 fact2 ih f by (finite_guess add: fresh_fun_eqvt perm_append supp_prod fs_name1)
+qed
+
text {* Induction principles *}
thm trm.induct_weak --"weak"
--- a/src/HOL/Nominal/Examples/Iteration.thy Wed Apr 26 22:40:46 2006 +0200
+++ b/src/HOL/Nominal/Examples/Iteration.thy Thu Apr 27 01:41:30 2006 +0200
@@ -264,7 +264,7 @@
and a: "(t,r) \<in> it f1 f2 f3"
shows "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
using a proof(induct)
- case it1 show ?case by (perm_simp add: it.intros)
+ case it1 show ?case by (perm_simp add: it.intros perm_compose')
next
case it2 thus ?case by (perm_simp add: it.intros)
next
@@ -375,8 +375,9 @@
have fin_g: "finite ((supp ?g)::name set)"
using f by (finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
have fr_g: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')" using f c
- by (rule_tac f3_freshness_conditions_simple, auto simp add: supp_prod,
- finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
+ apply (rule_tac f3_freshness_conditions_simple, auto simp add: supp_prod,
+ finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
+ done
have fresh_b: "b\<sharp>?g"
proof -
have "finite ((supp (a,t,f1,f2,f3))::name set)" using f by (simp add: supp_prod fs_name1)
--- a/src/HOL/Nominal/Nominal.thy Wed Apr 26 22:40:46 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Apr 27 01:41:30 2006 +0200
@@ -17,11 +17,16 @@
types
'x prm = "('x \<times> 'x) list"
-(* polymorphic operations for permutation and swapping*)
+(* polymorphic operations for permutation and swapping *)
consts
perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80)
swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
+(* for the decision procedure involving permutations *)
+(* (to make the perm-composition to be terminating *)
+constdefs
+ "perm_aux pi x \<equiv> pi\<bullet>x"
+
(* permutation on sets *)
defs (overloaded)
perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
@@ -1556,15 +1561,13 @@
and at: "at TYPE ('x)"
and a1: "S supports x"
and a2: "finite S"
- and a3: "\<forall>S'. (finite S' \<and> S' supports x) \<longrightarrow> S\<subseteq>S'"
+ and a3: "\<forall>S'. (S' supports x) \<longrightarrow> S\<subseteq>S'"
shows "S = (supp x)"
proof (rule equalityI)
show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
next
- have s1: "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
- have "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
- hence "finite ((supp x)::'x set)" using a2 by (simp add: finite_subset)
- with s1 a3 show "S\<subseteq>supp x" by force
+ have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
+ with a3 show "S\<subseteq>supp x" by force
qed
lemma supports_set:
@@ -1620,10 +1623,8 @@
and fs: "finite X"
shows "(supp X) = X"
proof (rule subset_antisym)
- case goal1
show "(supp X) \<subseteq> X" using at_fin_set_supports[OF at] using fs by (simp add: supp_is_subset)
next
- case goal2
have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite)
{ fix a::"'x"
assume asm: "a\<in>X"
@@ -1679,12 +1680,12 @@
show "?LHS"
proof (rule ccontr)
assume "(pi\<bullet>f) \<noteq> f"
- hence "\<exists>c. (pi\<bullet>f) c \<noteq> f c" by (simp add: expand_fun_eq)
- then obtain c where b1: "(pi\<bullet>f) c \<noteq> f c" by force
- from b have "pi\<bullet>(f ((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" by force
- hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))"
+ hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: expand_fun_eq)
+ then obtain x where b1: "(pi\<bullet>f) x \<noteq> f x" by force
+ from b have "pi\<bullet>(f ((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" by force
+ hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))"
by (simp add: pt_fun_app_eq[OF pt, OF at])
- hence "(pi\<bullet>f) c = f c" by (simp add: pt_pi_rev[OF pt, OF at])
+ hence "(pi\<bullet>f) x = f x" by (simp add: pt_pi_rev[OF pt, OF at])
with b1 show "False" by simp
qed
qed
@@ -2056,6 +2057,116 @@
shows "a\<sharp>(set xs) = a\<sharp>xs"
by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
+section {* disjointness properties *}
+(*=================================*)
+lemma dj_perm_forget:
+ fixes pi::"'y prm"
+ and x ::"'x"
+ assumes dj: "disjoint TYPE('x) TYPE('y)"
+ shows "pi\<bullet>x=x"
+ using dj by (simp add: disjoint_def)
+
+lemma dj_perm_perm_forget:
+ fixes pi1::"'x prm"
+ and pi2::"'y prm"
+ assumes dj: "disjoint TYPE('x) TYPE('y)"
+ shows "pi2\<bullet>pi1=pi1"
+ using dj by (induct pi1, auto simp add: disjoint_def)
+
+lemma dj_cp:
+ fixes pi1::"'x prm"
+ and pi2::"'y prm"
+ and x ::"'a"
+ assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ and dj: "disjoint TYPE('y) TYPE('x)"
+ shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
+ by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
+
+lemma dj_supp:
+ fixes a::"'x"
+ assumes dj: "disjoint TYPE('x) TYPE('y)"
+ shows "(supp a) = ({}::'y set)"
+apply(simp add: supp_def dj_perm_forget[OF dj])
+done
+
+section {* composition instances *}
+(* ============================= *)
+
+lemma cp_list_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(induct_tac x)
+apply(auto)
+done
+
+lemma cp_set_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(auto simp add: perm_set_def)
+apply(rule_tac x="pi2\<bullet>aa" in exI)
+apply(auto)
+done
+
+lemma cp_option_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(case_tac x)
+apply(auto)
+done
+
+lemma cp_noption_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(case_tac x)
+apply(auto)
+done
+
+lemma cp_unit_inst:
+ shows "cp TYPE (unit) TYPE('x) TYPE('y)"
+apply(simp add: cp_def)
+done
+
+lemma cp_bool_inst:
+ shows "cp TYPE (bool) TYPE('x) TYPE('y)"
+apply(simp add: cp_def)
+apply(rule allI)+
+apply(induct_tac x)
+apply(simp_all)
+done
+
+lemma cp_prod_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ and c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
+using c1 c2
+apply(simp add: cp_def)
+done
+
+lemma cp_fun_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ and c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
+ and pt: "pt TYPE ('y) TYPE('x)"
+ and at: "at TYPE ('x)"
+ shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
+using c1 c2
+apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
+apply(simp add: perm_rev[symmetric])
+apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
+done
+
+
section {* Andy's freshness lemma *}
(*================================*)
@@ -2149,6 +2260,47 @@
with b show "fr = h a" by force
qed
+lemma fresh_fun_equiv_ineq:
+ fixes h :: "'y\<Rightarrow>'a"
+ and pi:: "'x prm"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and ptb':"pt TYPE('a) TYPE('y)"
+ and at: "at TYPE('x)"
+ and at': "at TYPE('y)"
+ and cpa: "cp TYPE('a) TYPE('x) TYPE('y)"
+ and cpb: "cp TYPE('y) TYPE('x) TYPE('y)"
+ and f1: "finite ((supp h)::'y set)"
+ and a1: "\<exists>(a::'y). (a\<sharp>h \<and> a\<sharp>(h a))"
+ shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
+proof -
+ have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at'])
+ have ptc: "pt TYPE('y\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at])
+ have cpc: "cp TYPE('y\<Rightarrow>'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb,OF cpa])
+ have f2: "finite ((supp (pi\<bullet>h))::'y set)"
+ proof -
+ from f1 have "finite (pi\<bullet>((supp h)::'y set))"
+ by (simp add: pt_set_finite_ineq[OF ptb, OF at])
+ thus ?thesis
+ by (simp add: pt_perm_supp_ineq[OF ptc, OF ptb, OF at, OF cpc])
+ qed
+ from a1 obtain a' where c0: "a'\<sharp>h \<and> a'\<sharp>(h a')" by force
+ hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by simp_all
+ have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1
+ by (simp add: pt_fresh_bij_ineq[OF ptc, OF ptb, OF at, OF cpc])
+ have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
+ proof -
+ from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))"
+ by (simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at,OF cpa])
+ thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
+ qed
+ have a2: "\<exists>(a::'y). (a\<sharp>(pi\<bullet>h) \<and> a\<sharp>((pi\<bullet>h) a))" using c3 c4 by force
+ have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF ptb', OF at', OF f1])
+ have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2
+ by (simp add: fresh_fun_app[OF ptb', OF at', OF f2])
+ show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
+qed
+
lemma fresh_fun_equiv:
fixes h :: "'x\<Rightarrow>'a"
and pi:: "'x prm"
@@ -2192,117 +2344,6 @@
apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
done
-section {* disjointness properties *}
-(*=================================*)
-lemma dj_perm_forget:
- fixes pi::"'y prm"
- and x ::"'x"
- assumes dj: "disjoint TYPE('x) TYPE('y)"
- shows "pi\<bullet>x=x"
- using dj by (simp add: disjoint_def)
-
-lemma dj_perm_perm_forget:
- fixes pi1::"'x prm"
- and pi2::"'y prm"
- assumes dj: "disjoint TYPE('x) TYPE('y)"
- shows "pi2\<bullet>pi1=pi1"
- using dj by (induct pi1, auto simp add: disjoint_def)
-
-lemma dj_cp:
- fixes pi1::"'x prm"
- and pi2::"'y prm"
- and x ::"'a"
- assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
- and dj: "disjoint TYPE('y) TYPE('x)"
- shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
- by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
-
-lemma dj_supp:
- fixes a::"'x"
- assumes dj: "disjoint TYPE('x) TYPE('y)"
- shows "(supp a) = ({}::'y set)"
-apply(simp add: supp_def dj_perm_forget[OF dj])
-done
-
-
-section {* composition instances *}
-(* ============================= *)
-
-lemma cp_list_inst:
- assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
- shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
-using c1
-apply(simp add: cp_def)
-apply(auto)
-apply(induct_tac x)
-apply(auto)
-done
-
-lemma cp_set_inst:
- assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
- shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
-using c1
-apply(simp add: cp_def)
-apply(auto)
-apply(auto simp add: perm_set_def)
-apply(rule_tac x="pi2\<bullet>aa" in exI)
-apply(auto)
-done
-
-lemma cp_option_inst:
- assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
- shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
-using c1
-apply(simp add: cp_def)
-apply(auto)
-apply(case_tac x)
-apply(auto)
-done
-
-lemma cp_noption_inst:
- assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
- shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
-using c1
-apply(simp add: cp_def)
-apply(auto)
-apply(case_tac x)
-apply(auto)
-done
-
-lemma cp_unit_inst:
- shows "cp TYPE (unit) TYPE('x) TYPE('y)"
-apply(simp add: cp_def)
-done
-
-lemma cp_bool_inst:
- shows "cp TYPE (bool) TYPE('x) TYPE('y)"
-apply(simp add: cp_def)
-apply(rule allI)+
-apply(induct_tac x)
-apply(simp_all)
-done
-
-lemma cp_prod_inst:
- assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
- and c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
- shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
-using c1 c2
-apply(simp add: cp_def)
-done
-
-lemma cp_fun_inst:
- assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
- and c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
- and pt: "pt TYPE ('y) TYPE('x)"
- and at: "at TYPE ('x)"
- shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
-using c1 c2
-apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
-apply(simp add: perm_rev[symmetric])
-apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
-done
-
-
section {* Abstraction function *}
(*==============================*)
@@ -2680,6 +2721,30 @@
section {* lemmas for deciding permutation equations *}
(*===================================================*)
+lemma perm_aux_fold:
+ shows "perm_aux pi x = pi\<bullet>x" by (simp only: perm_aux_def)
+
+lemma pt_perm_compose_aux:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi2\<bullet>(pi1\<bullet>x) = perm_aux (pi2\<bullet>pi1) (pi2\<bullet>x)"
+proof -
+ have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
+ hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
+ thus ?thesis by (simp add: pt2[OF pt] perm_aux_def)
+qed
+
+lemma cp1_aux:
+ fixes pi1::"'x prm"
+ and pi2::"'y prm"
+ and x ::"'a"
+ assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "pi1\<bullet>(pi2\<bullet>x) = perm_aux (pi1\<bullet>pi2) (pi1\<bullet>x)"
+ using cp by (simp add: cp_def perm_aux_def)
+
lemma perm_eq_app:
fixes f :: "'a\<Rightarrow>'b"
and x :: "'a"
@@ -2696,7 +2761,6 @@
shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)"
by (simp add: perm_fun_def)
-
section {* test *}
lemma at_prm_eq_compose:
fixes pi1 :: "'x prm"
@@ -2745,10 +2809,18 @@
method_setup perm_simp =
{* perm_eq_meth *}
- {* tactic for deciding equalities involving permutations *}
+ {* simp rules and simprocs for analysing permutations *}
method_setup perm_simp_debug =
{* perm_eq_meth_debug *}
+ {* simp rules and simprocs for analysing permutations including debuging facilities *}
+
+method_setup perm_full_simp =
+ {* perm_full_eq_meth *}
+ {* tactic for deciding equalities involving permutations *}
+
+method_setup perm_full_simp_debug =
+ {* perm_full_eq_meth_debug *}
{* tactic for deciding equalities involving permutations including debuging facilities *}
method_setup supports_simp =
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Apr 26 22:40:46 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Apr 27 01:41:30 2006 +0200
@@ -520,6 +520,7 @@
val cp_option_inst = thm "cp_option_inst";
val cp_noption_inst = thm "cp_noption_inst";
val pt_perm_compose = thm "pt_perm_compose";
+
val dj_pp_forget = thm "dj_perm_perm_forget";
(* shows that <aj> is an instance of cp_<ak>_<ai> *)
@@ -645,32 +646,32 @@
(* abbreviations for some lemmas *)
(*===============================*)
- val abs_fun_pi = thm "nominal.abs_fun_pi";
- val abs_fun_pi_ineq = thm "nominal.abs_fun_pi_ineq";
- val abs_fun_eq = thm "nominal.abs_fun_eq";
- val dj_perm_forget = thm "nominal.dj_perm_forget";
- val dj_pp_forget = thm "nominal.dj_perm_perm_forget";
- val fresh_iff = thm "nominal.fresh_abs_fun_iff";
- val fresh_iff_ineq = thm "nominal.fresh_abs_fun_iff_ineq";
- val abs_fun_supp = thm "nominal.abs_fun_supp";
- val abs_fun_supp_ineq = thm "nominal.abs_fun_supp_ineq";
- val pt_swap_bij = thm "nominal.pt_swap_bij";
- val pt_fresh_fresh = thm "nominal.pt_fresh_fresh";
- val pt_bij = thm "nominal.pt_bij";
- val pt_perm_compose = thm "nominal.pt_perm_compose";
- val pt_perm_compose' = thm "nominal.pt_perm_compose'";
- val perm_app = thm "nominal.pt_fun_app_eq";
- val at_fresh = thm "nominal.at_fresh";
- val at_calc = thms "nominal.at_calc";
- val at_supp = thm "nominal.at_supp";
- val dj_supp = thm "nominal.dj_supp";
- val fresh_left_ineq = thm "nominal.pt_fresh_left_ineq";
- val fresh_left = thm "nominal.pt_fresh_left";
- val fresh_bij_ineq = thm "nominal.pt_fresh_bij_ineq";
- val fresh_bij = thm "nominal.pt_fresh_bij";
- val pt_pi_rev = thm "nominal.pt_pi_rev";
- val pt_rev_pi = thm "nominal.pt_rev_pi";
- val fresh_fun_eqvt = thm "nominal.fresh_fun_equiv";
+ val abs_fun_pi = thm "nominal.abs_fun_pi";
+ val abs_fun_pi_ineq = thm "nominal.abs_fun_pi_ineq";
+ val abs_fun_eq = thm "nominal.abs_fun_eq";
+ val dj_perm_forget = thm "nominal.dj_perm_forget";
+ val dj_pp_forget = thm "nominal.dj_perm_perm_forget";
+ val fresh_iff = thm "nominal.fresh_abs_fun_iff";
+ val fresh_iff_ineq = thm "nominal.fresh_abs_fun_iff_ineq";
+ val abs_fun_supp = thm "nominal.abs_fun_supp";
+ val abs_fun_supp_ineq = thm "nominal.abs_fun_supp_ineq";
+ val pt_swap_bij = thm "nominal.pt_swap_bij";
+ val pt_fresh_fresh = thm "nominal.pt_fresh_fresh";
+ val pt_bij = thm "nominal.pt_bij";
+ val pt_perm_compose = thm "nominal.pt_perm_compose";
+ val pt_perm_compose' = thm "nominal.pt_perm_compose'";
+ val perm_app = thm "nominal.pt_fun_app_eq";
+ val at_fresh = thm "nominal.at_fresh";
+ val at_calc = thms "nominal.at_calc";
+ val at_supp = thm "nominal.at_supp";
+ val dj_supp = thm "nominal.dj_supp";
+ val fresh_left_ineq = thm "nominal.pt_fresh_left_ineq";
+ val fresh_left = thm "nominal.pt_fresh_left";
+ val fresh_bij_ineq = thm "nominal.pt_fresh_bij_ineq";
+ val fresh_bij = thm "nominal.pt_fresh_bij";
+ val pt_pi_rev = thm "nominal.pt_pi_rev";
+ val pt_rev_pi = thm "nominal.pt_rev_pi";
+ val fresh_fun_eqvt = thm "nominal.fresh_fun_equiv";
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
(* types; this allows for example to use abs_perm (which is a *)
--- a/src/HOL/Nominal/nominal_permeq.ML Wed Apr 26 22:40:46 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Apr 27 01:41:30 2006 +0200
@@ -1,22 +1,23 @@
(* $Id$ *)
-(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
+(* METHODS FOR SIMPLIFYING PERMUTATIONS AND *)
+(* FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
local
(* pulls out dynamically a thm via the simpset *)
-fun dynamic_thms ss name =
- ProofContext.get_thms (Simplifier.the_context ss) (Name name);
-fun dynamic_thm ss name =
- ProofContext.get_thm (Simplifier.the_context ss) (Name name);
+fun dynamic_thms ss name = ProofContext.get_thms (Simplifier.the_context ss) (Name name);
+fun dynamic_thm ss name = ProofContext.get_thm (Simplifier.the_context ss) (Name name);
-(* initial simplification step in the tactic *)
+(* a tactic simplyfying permutations *)
+val perm_fun_def = thm "nominal.perm_fun_def"
+val perm_eq_app = thm "nominal.pt_fun_app_eq"
+
fun perm_eval_tac ss i =
let
fun perm_eval_simproc sg ss redex =
let
-
- (* the "application" case below is only applicable when the head *)
+ (* the "application" case below is only applicable when the head *)
(* of f is not a constant or when it is a permuattion with two or *)
(* more arguments *)
fun applicable t =
@@ -38,14 +39,10 @@
val name = Sign.base_name n
val at_inst = dynamic_thm ss ("at_"^name^"_inst")
val pt_inst = dynamic_thm ss ("pt_"^name^"_inst")
- val perm_eq_app = thm "nominal.pt_fun_app_eq"
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
(* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
- | (Const("nominal.perm",_) $ pi $ (Abs _)) =>
- let
- val perm_fun_def = thm "nominal.perm_fun_def"
- in SOME (perm_fun_def) end
+ | (Const("nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
(* no redex otherwise *)
| _ => NONE) end
@@ -54,112 +51,137 @@
Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval"
["nominal.perm pi x"] perm_eval_simproc;
- (* applies the pt_perm_compose lemma *)
- (* *)
- (* pi1 o (pi2 o x) = (pi1 o pi2) o (pi1 o x) *)
- (* *)
- (* in the restricted case where pi1 is a swapping *)
- (* (a b) coming from a "supports problem"; in *)
- (* this rule would cause loops in the simplifier *)
- val pt_perm_compose = thm "pt_perm_compose";
-
- fun perm_compose_simproc i sg ss redex =
- (case redex of
- (Const ("nominal.perm", _) $ (pi1 as Const ("List.list.Cons", _) $
- (Const ("Pair", _) $ Free (a as (_, T as Type (tname, _))) $ Free b) $
- Const ("List.list.Nil", _)) $ (Const ("nominal.perm",
- Type ("fun", [Type ("List.list", [Type ("*", [U, _])]), _])) $ pi2 $ t)) =>
+ (* these lemmas are created dynamically according to the atom types *)
+ val perm_swap = dynamic_thms ss "perm_swap"
+ val perm_fresh = dynamic_thms ss "perm_fresh_fresh"
+ val perm_bij = dynamic_thms ss "perm_bij"
+ val perm_pi_simp = dynamic_thms ss "perm_pi_simp"
+ val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
+ in
+ ("general simplification step", asm_full_simp_tac (ss' addsimprocs [perm_eval]) i)
+ end;
+
+(* applies the perm_compose rule such that *)
+(* *)
+(* pi o (pi' o lhs) = rhs *)
+(* *)
+(* is transformed to *)
+(* *)
+(* (pi o pi') o (pi' o lhs) = rhs *)
+(* *)
+(* this rule would loop in the simplifier, so some trick is used with *)
+(* generating perm_aux'es for the outermost permutation and then un- *)
+(* folding the definition *)
+val pt_perm_compose_aux = thm "pt_perm_compose_aux";
+val cp1_aux = thm "cp1_aux";
+val perm_aux_fold = thm "perm_aux_fold";
+
+fun perm_compose_tac ss i =
+ let
+ fun perm_compose_simproc sg ss redex =
+ (case redex of
+ (Const ("nominal.perm", Type ("fun", [Type ("List.list",
+ [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("nominal.perm",
+ Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $
+ pi2 $ t)) =>
let
- val ({bounds = (_, xs), ...}, _) = rep_ss ss
- val ai = find_index (fn (x, _) => x = a) xs
- val bi = find_index (fn (x, _) => x = b) xs
val tname' = Sign.base_name tname
+ val uname' = Sign.base_name uname
in
- if ai = length xs - i - 1 andalso
- bi = length xs - i - 2 andalso
- T = U andalso pi1 <> pi2 then
+ if pi1 <> pi2 then (* only apply the composition rule in this case *)
+ if T = U then
SOME (Drule.instantiate'
[SOME (ctyp_of sg (fastype_of t))]
[SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
(mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
- PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose)))
+ PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
+ else
+ SOME (Drule.instantiate'
+ [SOME (ctyp_of sg (fastype_of t))]
+ [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
+ (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS
+ cp1_aux)))
else NONE
end
| _ => NONE);
-
- fun perm_compose i =
+
+ val perm_compose =
Simplifier.simproc (the_context()) "perm_compose"
- ["nominal.perm [(a, b)] (nominal.perm pi t)"] (perm_compose_simproc i);
-
- (* these lemmas are created dynamically according to the atom types *)
- val perm_swap = dynamic_thms ss "perm_swap"
- val perm_fresh = dynamic_thms ss "perm_fresh_fresh"
- val perm_bij = dynamic_thms ss "perm_bij"
- val perm_pi_simp = dynamic_thms ss "perm_pi_simp"
- val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
+ ["nominal.perm pi1 (nominal.perm pi2 t)"] perm_compose_simproc;
+
+ val ss' = Simplifier.theory_context (the_context ()) empty_ss
+
in
- ("general simplification step",
- FIRST [rtac conjI i,
- SUBGOAL (fn (g, i) => asm_full_simp_tac
- (ss' addsimprocs [perm_eval,perm_compose (length (Logic.strip_params g)-2)]) i) i])
- end;
-
-(* applies the perm_compose rule - this rule would loop in the simplifier *)
-(* in case there are more atom-types we have to check every possible instance *)
-(* of perm_compose *)
-fun apply_perm_compose_tac ss i =
- let
- val perm_compose = dynamic_thms ss "perm_compose";
- val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose
- in
- ("analysing permutation compositions on the lhs",FIRST (tacs))
+ ("analysing permutation compositions on the lhs",
+ EVERY [rtac trans i,
+ asm_full_simp_tac (ss' addsimprocs [perm_compose]) i,
+ asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i])
end
(* applying Stefan's smart congruence tac *)
fun apply_cong_tac i =
("application of congruence",
- (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
+ (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
-(* unfolds the definition of permutations applied to functions *)
+(* unfolds the definition of permutations *)
+(* applied to functions such that *)
+(* *)
+(* pi o f = rhs *)
+(* *)
+(* is transformed to *)
+(* *)
+(* %x. pi o (f ((rev pi) o x)) = rhs *)
fun unfold_perm_fun_def_tac i =
let
val perm_fun_def = thm "nominal.perm_fun_def"
in
("unfolding of permutations on functions",
- simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i)
+ rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
end
-(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
-fun expand_fun_eq_tac i =
- ("extensionality expansion of functions",
- EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]);
+(* applies the ext-rule such that *)
+(* *)
+(* f = g goes to /\x. f x = g x *)
+fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
+(* FIXME FIXME FIXME *)
+(* should be able to analyse pi o fresh_fun () = fresh_fun instances *)
+fun fresh_fun_eqvt_tac i =
+ let
+ val fresh_fun_equiv = thm "nominal.fresh_fun_equiv_ineq"
+ in
+ ("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i)
+ end
+
(* debugging *)
fun DEBUG_tac (msg,tac) =
CHANGED (EVERY [tac, print_tac ("after "^msg)]);
fun NO_DEBUG_tac (_,tac) = CHANGED tac;
-(* Main Tactic *)
-
+(* Main Tactics *)
fun perm_simp_tac tactical ss i =
DETERM (tactical (perm_eval_tac ss i));
+(* perm_full_simp_tac is perm_simp_tac plus additional tactics *)
+(* to decide equation that come from support problems *)
+(* since it contains looping rules the "recursion" - depth is set *)
+(* to 10 - this seems to be sufficient in most cases *)
+fun perm_full_simp_tac tactical ss =
+ let fun perm_full_simp_tac_aux tactical ss n =
+ if n=0 then K all_tac
+ else DETERM o
+ (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
+ fn i => tactical (perm_eval_tac ss i),
+ fn i => tactical (perm_compose_tac ss i),
+ fn i => tactical (apply_cong_tac i),
+ fn i => tactical (unfold_perm_fun_def_tac i),
+ fn i => tactical (ext_fun_tac i),
+ fn i => tactical (fresh_fun_eqvt_tac i)]
+ THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
+ in perm_full_simp_tac_aux tactical ss 10 end;
-(* perm_simp_tac plus additional tactics to decide *)
-(* support problems *)
-(* the "recursion"-depth is set to 10 - this seems sufficient *)
-fun perm_supports_tac tactical ss n =
- if n=0 then K all_tac
- else DETERM o
- (FIRST'[fn i => tactical (perm_eval_tac ss i),
- (*fn i => tactical (apply_perm_compose_tac ss i),*)
- fn i => tactical (apply_cong_tac i),
- fn i => tactical (unfold_perm_fun_def_tac i),
- fn i => tactical (expand_fun_eq_tac i)]
- THEN_ALL_NEW (TRY o (perm_supports_tac tactical ss (n-1))));
-
-(* tactic that first unfolds the support definition *)
-(* and strips off the intros, then applies perm_supports_tac *)
+(* tactic that first unfolds the support definition *)
+(* and strips off the intros, then applies perm_full_simp_tac *)
fun supports_tac tactical ss i =
let
val supports_def = thm "nominal.op supports_def";
@@ -167,16 +189,19 @@
val fresh_prod = thm "nominal.fresh_prod";
val simps = [supports_def,symmetric fresh_def,fresh_prod]
in
- EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i),
- tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)),
- tactical ("geting rid of the imps", rtac impI i),
- tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)),
- tactical ("applying perm_simp ", perm_supports_tac tactical ss 10 i)]
+ EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i),
+ tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)),
+ tactical ("geting rid of the imps ", rtac impI i),
+ tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)),
+ tactical ("applying perm_full_simp ", perm_full_simp_tac tactical ss i
+ (*perm_simp_tac tactical ss i*))]
end;
-(* tactic that guesses the finite-support of a goal *)
-
+(* tactic that guesses the finite-support of a goal *)
+(* it collects all free variables and tries to show *)
+(* that the support of these free variables (op supports) *)
+(* the goal *)
fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs
| collect_vars i (v as Free _) vs = v ins vs
| collect_vars i (v as Var _) vs = v ins vs
@@ -219,17 +244,18 @@
in
-
fun simp_meth_setup tac =
Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
(Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
-val perm_eq_meth = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
-val perm_eq_meth_debug = simp_meth_setup (perm_simp_tac DEBUG_tac);
-val supports_meth = simp_meth_setup (supports_tac NO_DEBUG_tac);
-val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac);
-val finite_gs_meth = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
-val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac);
+val perm_eq_meth = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
+val perm_eq_meth_debug = simp_meth_setup (perm_simp_tac DEBUG_tac);
+val perm_full_eq_meth = simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
+val perm_full_eq_meth_debug = simp_meth_setup (perm_full_simp_tac DEBUG_tac);
+val supports_meth = simp_meth_setup (supports_tac NO_DEBUG_tac);
+val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac);
+val finite_gs_meth = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
+val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac);
end