# HG changeset patch # User urbanc # Date 1151854030 -7200 # Node ID 89c5afe4139af40d2678aae1c6cec9efeb432ae9 # Parent ddf69abaffa8b7a6d0239cfd9c61a8a267128f53 added more infrastructure for the recursion combinator diff -r ddf69abaffa8 -r 89c5afe4139a src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Fri Jun 30 18:26:36 2006 +0200 +++ b/src/HOL/Nominal/Examples/Fsub.thy Sun Jul 02 17:27:10 2006 +0200 @@ -178,7 +178,7 @@ have "\ (pi\\) ok" by fact moreover have "X\(domain \)" by fact - hence "(pi\X)\(domain (pi\\))" by (simp add: fresh_eqvt domain_eqvt[symmetric]) + hence "(pi\X)\(domain (pi\\))" by (simp add: fresh_bij domain_eqvt[symmetric]) moreover have "T closed_in \" by fact hence "(pi\T) closed_in (pi\\)" by (simp add: closed_in_eqvt) @@ -341,7 +341,7 @@ dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst] simp add: domain_eqvt) apply(force) -apply(force intro!: S_Forall simp add: fresh_prod fresh_eqvt) +apply(force intro!: S_Forall simp add: fresh_prod fresh_bij) done text {* The most painful part of the subtyping definition is the strengthening of the diff -r ddf69abaffa8 -r 89c5afe4139a src/HOL/Nominal/Examples/Iteration.thy --- a/src/HOL/Nominal/Examples/Iteration.thy Fri Jun 30 18:26:36 2006 +0200 +++ b/src/HOL/Nominal/Examples/Iteration.thy Sun Jul 02 17:27:10 2006 +0200 @@ -104,15 +104,11 @@ done have fs1: "a1\f3 a1 r1" using b f1 apply(auto) - apply(case_tac "a=a1") - apply(simp) apply(rule_tac pi="[(a1,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst]) apply(perm_simp add: calc_atm fresh_prod) done have fs2: "a2\f3 a2 r2" using b f2 apply(auto) - apply(case_tac "a=a2") - apply(simp) apply(rule_tac pi="[(a2,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst]) apply(perm_simp add: calc_atm fresh_prod) done @@ -155,7 +151,7 @@ have fs_pi: "\(a::name). a\(pi\f3) \ (\(r::'a::pt_name). a\(pi\f3) a r)" proof - from c obtain a where fs1: "a\f3" and fs2: "\(r::'a::pt_name). a\f3 a r" by force - have "(pi\a)\(pi\f3)" using fs1 by (simp add: fresh_eqvt) + have "(pi\a)\(pi\f3)" using fs1 by (simp add: fresh_bij) moreover have "\(r::'a::pt_name). (pi\a)\((pi\f3) (pi\a) r)" using fs2 by (perm_simp add: fresh_right) ultimately show "\(a::name). a\(pi\f3) \ (\(r::'a::pt_name). a\(pi\f3) a r)" by blast diff -r ddf69abaffa8 -r 89c5afe4139a src/HOL/Nominal/Examples/SN.thy --- a/src/HOL/Nominal/Examples/SN.thy Fri Jun 30 18:26:36 2006 +0200 +++ b/src/HOL/Nominal/Examples/SN.thy Sun Jul 02 17:27:10 2006 +0200 @@ -217,7 +217,7 @@ shows "valid (pi\\)" using a apply(induct) -apply(auto simp add: fresh_eqvt) +apply(auto simp add: fresh_bij) done (* typing judgements *) @@ -281,7 +281,7 @@ using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) next case (t3 \ \ \ a t) - moreover have "(pi\a)\(pi\\)" by (simp add: fresh_eqvt) + moreover have "(pi\a)\(pi\\)" by (simp add: fresh_bij) ultimately show "(pi\\) \ (pi\Lam [a].t) :\\\" by force qed (auto) diff -r ddf69abaffa8 -r 89c5afe4139a src/HOL/Nominal/Examples/Weakening.thy --- a/src/HOL/Nominal/Examples/Weakening.thy Fri Jun 30 18:26:36 2006 +0200 +++ b/src/HOL/Nominal/Examples/Weakening.thy Sun Jul 02 17:27:10 2006 +0200 @@ -42,7 +42,7 @@ shows "valid (pi\\)" using a apply(induct) -apply(auto simp add: fresh_eqvt) +apply(auto simp add: fresh_bij) done (* typing judgements *) @@ -76,7 +76,7 @@ using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) next case (t3 \ \ \ a t) - moreover have "(pi\a)\(pi\\)" by (simp add: fresh_eqvt) + moreover have "(pi\a)\(pi\\)" by (simp add: fresh_bij) ultimately show "(pi\\) \ (pi\Lam [a].t) :\\\" by force qed (auto) diff -r ddf69abaffa8 -r 89c5afe4139a src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Fri Jun 30 18:26:36 2006 +0200 +++ b/src/HOL/Nominal/Nominal.thy Sun Jul 02 17:27:10 2006 +0200 @@ -87,6 +87,16 @@ shows "pi\(b::bool) = b" by (cases b) auto +lemma perm_boolI: + assumes a: "P" + shows "pi\P" + using a by (simp add: perm_bool) + +lemma perm_boolE: + assumes a: "pi\P" + shows "P" + using a by (simp add: perm_bool) + (* permutation on options *) primrec (unchecked perm_option) perm_some_def: "pi\Some(x) = Some(pi\x)" @@ -865,6 +875,13 @@ apply(simp add: supp_def dj_perm_forget[OF dj]) done +lemma at_fresh_ineq: + fixes a :: "'x" + and b :: "'y" + assumes dj: "disjoint TYPE('y) TYPE('x)" + shows "a\b" + by (simp add: fresh_def dj_supp[OF dj]) + section {* permutation type instances *} (* ===================================*) @@ -1406,6 +1423,15 @@ shows "a\x" using a by (simp add: pt_fresh_bij[OF pt, OF at]) +lemma pt_fresh_eqvt: + fixes pi :: "'x prm" + and x :: "'a" + and a :: "'x" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + shows "pi\(a\x) = (pi\a)\(pi\x)" + by (simp add: perm_bool pt_fresh_bij[OF pt, OF at]) + lemma pt_perm_fresh1: fixes a :: "'x" and b :: "'x" @@ -1556,6 +1582,29 @@ thus ?thesis by (simp add: pt2[OF pt]) qed +section {* equivaraince for some connectives *} + +lemma pt_all_eqvt: + fixes pi :: "'x prm" + and x :: "'a" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + shows "pi\(\(x::'a). P x) = (\(x::'a). (pi\P) x)" +apply(auto simp add: perm_bool perm_fun_def) +apply(drule_tac x="pi\x" in spec) +apply(simp add: pt_rev_pi[OF pt, OF at]) +done + +lemma imp_eqvt: + fixes pi::"'x prm" + shows "pi\(A\B) = ((pi\A)\(pi\B))" + by (simp add: perm_bool) + +lemma conj_eqvt: + fixes pi::"'x prm" + shows "pi\(A\B) = ((pi\A)\(pi\B))" + by (simp add: perm_bool) + section {* facts about supports *} (*==============================*) diff -r ddf69abaffa8 -r 89c5afe4139a src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Fri Jun 30 18:26:36 2006 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Sun Jul 02 17:27:10 2006 +0200 @@ -668,6 +668,7 @@ 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_fresh_ineq = thm "Nominal.at_fresh_ineq"; val at_calc = thms "Nominal.at_calc"; val at_supp = thm "Nominal.at_supp"; val dj_supp = thm "Nominal.dj_supp"; @@ -679,8 +680,11 @@ val fresh_bij = thm "Nominal.pt_fresh_bij"; val fresh_aux_ineq = thm "Nominal.pt_fresh_aux_ineq"; val fresh_aux = thm "Nominal.pt_fresh_aux"; + val fresh_eqvt = thm "Nominal.pt_fresh_eqvt"; + val all_eqvt = thm "Nominal.pt_all_eqvt"; val pt_pi_rev = thm "Nominal.pt_pi_rev"; val pt_rev_pi = thm "Nominal.pt_rev_pi"; + val at_exists_fresh = thm "Nominal.at_exists_fresh"; (* Now we collect and instantiate some lemmas w.r.t. all atom *) @@ -761,7 +765,12 @@ ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])] ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])] - ||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])] + ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])] + ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[])] + ||>> PureThy.add_thmss + let val thms1 = inst_at [at_fresh] + val thms2 = inst_dj [at_fresh_ineq] + in [(("fresh_atm", thms1 @ thms2),[])] end ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])] ||>> PureThy.add_thmss let val thms1 = inst_pt_at [abs_fun_pi] @@ -792,7 +801,10 @@ ||>> PureThy.add_thmss let val thms1 = inst_pt_at [fresh_bij] and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] - in [(("fresh_eqvt", thms1 @ thms2),[])] end + in [(("fresh_bij", thms1 @ thms2),[])] end + ||>> PureThy.add_thmss + let val thms1 = inst_pt_at [fresh_eqvt] + in [(("fresh_eqvt", thms1),[])] end ||>> PureThy.add_thmss let val thms1 = inst_pt_at [fresh_aux] and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]