# HG changeset patch # User urbanc # Date 1146094890 -7200 # Node ID a95176d0f0ddb2b8334fd2d19e95c18ee2b73549 # Parent 816f519f8b72c1f60576a4c063df9f29e279f04b 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 diff -r 816f519f8b72 -r a95176d0f0dd src/HOL/Nominal/Examples/CR.thy --- 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\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: "\x y N L. \x\y; x\L\ \ M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact have "x\y" by fact have "x\L" by fact - have "z\x" "z\y" "z\N" "z\L" by fact + have fs: "z\x" "z\y" "z\N" "z\L" by fact hence "z\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 - diff -r 816f519f8b72 -r a95176d0f0dd src/HOL/Nominal/Examples/Class.thy --- 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: "\(a::name). a\f3 \ (\t (r::'a::pt_name). a\f3 a t r)" + and a: "(t,r) \ 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' = "\pi a'. f3 a' ((pi@[(c,a')])\t) (r (pi@[(c,a')]))" --"helper function" + have fact1: "\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: "\pi. \(a''::name). a''\(?g' pi) \ a''\((?g' pi) a'')" + proof + fix pi::"name prm" + show "\(a''::name). a''\(?g' pi) \ a''\((?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" diff -r 816f519f8b72 -r a95176d0f0dd src/HOL/Nominal/Examples/Iteration.thy --- 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) \ it f1 f2 f3" shows "(pi\t,pi\r) \ it (pi\f1) (pi\f2) (pi\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: "\(a''::name). a''\?g \ a''\(?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\?g" proof - have "finite ((supp (a,t,f1,f2,f3))::name set)" using f by (simp add: supp_prod fs_name1) diff -r 816f519f8b72 -r a95176d0f0dd src/HOL/Nominal/Nominal.thy --- 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 \ 'x) list" -(* polymorphic operations for permutation and swapping*) +(* polymorphic operations for permutation and swapping *) consts perm :: "'x prm \ 'a \ 'a" (infixr "\" 80) swap :: "('x \ 'x) \ 'x \ 'x" +(* for the decision procedure involving permutations *) +(* (to make the perm-composition to be terminating *) +constdefs + "perm_aux pi x \ pi\x" + (* permutation on sets *) defs (overloaded) perm_set_def: "pi\(X::'a set) \ {pi\a | a. a\X}" @@ -1556,15 +1561,13 @@ and at: "at TYPE ('x)" and a1: "S supports x" and a2: "finite S" - and a3: "\S'. (finite S' \ S' supports x) \ S\S'" + and a3: "\S'. (S' supports x) \ S\S'" shows "S = (supp x)" proof (rule equalityI) show "((supp x)::'x set)\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)\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\supp x" by force + have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at]) + with a3 show "S\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) \ 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\X" @@ -1679,12 +1680,12 @@ show "?LHS" proof (rule ccontr) assume "(pi\f) \ f" - hence "\c. (pi\f) c \ f c" by (simp add: expand_fun_eq) - then obtain c where b1: "(pi\f) c \ f c" by force - from b have "pi\(f ((rev pi)\c)) = f (pi\((rev pi)\c))" by force - hence "(pi\f)(pi\((rev pi)\c)) = f (pi\((rev pi)\c))" + hence "\x. (pi\f) x \ f x" by (simp add: expand_fun_eq) + then obtain x where b1: "(pi\f) x \ f x" by force + from b have "pi\(f ((rev pi)\x)) = f (pi\((rev pi)\x))" by force + hence "(pi\f)(pi\((rev pi)\x)) = f (pi\((rev pi)\x))" by (simp add: pt_fun_app_eq[OF pt, OF at]) - hence "(pi\f) c = f c" by (simp add: pt_pi_rev[OF pt, OF at]) + hence "(pi\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\(set xs) = a\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\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\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\(pi2\x) = (pi2)\(pi1\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\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\'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\'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\'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: "\(a::'y). (a\h \ a\(h a))" + shows "pi\(fresh_fun h) = fresh_fun(pi\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\'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) + have cpc: "cp TYPE('y\'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb,OF cpa]) + have f2: "finite ((supp (pi\h))::'y set)" + proof - + from f1 have "finite (pi\((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'\h \ a'\(h a')" by force + hence c1: "a'\h" and c2: "a'\(h a')" by simp_all + have c3: "(pi\a')\(pi\h)" using c1 + by (simp add: pt_fresh_bij_ineq[OF ptc, OF ptb, OF at, OF cpc]) + have c4: "(pi\a')\(pi\h) (pi\a')" + proof - + from c2 have "(pi\a')\(pi\(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: "\(a::'y). (a\(pi\h) \ a\((pi\h) a))" using c3 c4 by force + have d1: "?LHS = pi\(h a')" using c1 a1 by (simp add: fresh_fun_app[OF ptb', OF at', OF f1]) + have d2: "?RHS = (pi\h) (pi\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\'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\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\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\(pi2\x) = (pi2)\(pi1\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\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\'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\'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\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\(pi1\x) = perm_aux (pi2\pi1) (pi2\x)" +proof - + have "(pi2@pi1) \ ((pi2\pi1)@pi2)" by (rule at_ds8) + hence "(pi2@pi1)\x = ((pi2\pi1)@pi2)\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\(pi2\x) = perm_aux (pi1\pi2) (pi1\x)" + using cp by (simp add: cp_def perm_aux_def) + lemma perm_eq_app: fixes f :: "'a\'b" and x :: "'a" @@ -2696,7 +2761,6 @@ shows "((pi\(\x. f x))=y) = ((\x. (pi\(f ((rev pi)\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 = diff -r 816f519f8b72 -r a95176d0f0dd src/HOL/Nominal/nominal_atoms.ML --- 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 is an instance of cp__ *) @@ -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 *) diff -r 816f519f8b72 -r a95176d0f0dd src/HOL/Nominal/nominal_permeq.ML --- 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