# HG changeset patch # User Christian Urban # Date 1285768046 14400 # Node ID 3b6a70e73006763951ce4e8de6d230c7ffd2b75b # Parent c7534584a7a007719ab4963613ca3eb5cfb18150 worked example Foo1 with induct_schema diff -r c7534584a7a0 -r 3b6a70e73006 Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Wed Sep 29 06:45:01 2010 -0400 +++ b/Nominal/Ex/Foo1.thy Wed Sep 29 09:47:26 2010 -0400 @@ -42,6 +42,238 @@ thm foo.supp thm foo.fresh +primrec + permute_bn1_raw +where + "permute_bn1_raw p (As_raw x y t) = As_raw (p \ x) y t" + +primrec + permute_bn2_raw +where + "permute_bn2_raw p (As_raw x y t) = As_raw x (p \ y) t" + +primrec + permute_bn3_raw +where + "permute_bn3_raw p (As_raw x y t) = As_raw (p \ x) (p \ y) t" + +quotient_definition + "permute_bn1 :: perm \ assg \ assg" +is + "permute_bn1_raw" + +quotient_definition + "permute_bn2 :: perm \ assg \ assg" +is + "permute_bn2_raw" + +quotient_definition + "permute_bn3 :: perm \ assg \ assg" +is + "permute_bn3_raw" + +lemma [quot_respect]: + shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw" + apply simp + apply clarify + apply (erule alpha_assg_raw.cases) + apply simp_all + apply (rule foo.raw_alpha) + apply simp_all + done + +lemma [quot_respect]: + shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw" + apply simp + apply clarify + apply (erule alpha_assg_raw.cases) + apply simp_all + apply (rule foo.raw_alpha) + apply simp_all + done + +lemma [quot_respect]: + shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw" + apply simp + apply clarify + apply (erule alpha_assg_raw.cases) + apply simp_all + apply (rule foo.raw_alpha) + apply simp_all + done + +lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted] +lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted] +lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted] + +lemma uu1: + shows "alpha_bn1 as (permute_bn1 p as)" +apply(induct as rule: foo.inducts(2)) +apply(auto)[6] +apply(simp add: permute_bn1) +apply(simp add: foo.eq_iff) +done + +lemma uu2: + shows "alpha_bn2 as (permute_bn2 p as)" +apply(induct as rule: foo.inducts(2)) +apply(auto)[6] +apply(simp add: permute_bn2) +apply(simp add: foo.eq_iff) +done + +lemma uu3: + shows "alpha_bn3 as (permute_bn3 p as)" +apply(induct as rule: foo.inducts(2)) +apply(auto)[6] +apply(simp add: permute_bn3) +apply(simp add: foo.eq_iff) +done + +lemma tt1: + shows "(p \ bn1 as) = bn1 (permute_bn1 p as)" +apply(induct as rule: foo.inducts(2)) +apply(auto)[6] +apply(simp add: permute_bn1 foo.bn_defs) +apply(simp add: atom_eqvt) +done + +lemma tt2: + shows "(p \ bn2 as) = bn2 (permute_bn2 p as)" +apply(induct as rule: foo.inducts(2)) +apply(auto)[6] +apply(simp add: permute_bn2 foo.bn_defs) +apply(simp add: atom_eqvt) +done + +lemma tt3: + shows "(p \ bn3 as) = bn3 (permute_bn3 p as)" +apply(induct as rule: foo.inducts(2)) +apply(auto)[6] +apply(simp add: permute_bn3 foo.bn_defs) +apply(simp add: atom_eqvt) +done + + +lemma strong_exhaust1: + fixes c::"'a::fs" + assumes "\name ca. \c = ca; y = Var name\ \ P" + and "\trm1 trm2 ca. \c = ca; y = App trm1 trm2\ \ P" + and "\name trm ca. \{atom name} \* ca; c = ca; y = Lam name trm\ \ P" + and "\assn trm ca. \set (bn1 assn) \* ca; c = ca; y = Let1 assn trm\ \ P" + and "\assn trm ca. \set (bn2 assn) \* ca; c = ca; y = Let2 assn trm\ \ P" + and "\assn trm ca. \set (bn3 assn) \* ca; c = ca; y = Let3 assn trm\ \ P" + shows "P" +apply(rule_tac y="y" in foo.exhaust(1)) +apply(rule assms(1)) +apply(auto)[2] +apply(rule assms(2)) +apply(auto)[2] +apply(subgoal_tac "\q. (q \ {atom name}) \* c \ supp (Lam name trm) \* q") +apply(erule exE) +apply(erule conjE) +apply(rule assms(3)) +apply(perm_simp) +apply(assumption) +apply(rule refl) +apply(drule supp_perm_eq[symmetric]) +apply(simp) +apply(rule at_set_avoiding2) +apply(simp add: finite_supp) +apply(simp add: finite_supp) +apply(simp add: finite_supp) +apply(simp add: foo.fresh fresh_star_def) +apply(subgoal_tac "\q. (q \ (set (bn1 assg))) \* c \ supp ([bn1 assg]lst.trm) \* q") +apply(erule exE) +apply(erule conjE) +apply(rule assms(4)) +apply(simp add: set_eqvt) +apply(simp add: tt1) +apply(rule refl) +apply(simp) +apply(simp add: foo.eq_iff) +apply(drule supp_perm_eq[symmetric]) +apply(simp) +apply(simp add: tt1 uu1) +apply(rule at_set_avoiding2) +apply(simp add: finite_supp) +apply(simp add: finite_supp) +apply(simp add: finite_supp) +apply(simp add: Abs_fresh_star) +apply(subgoal_tac "\q. (q \ (set (bn2 assg))) \* c \ supp ([bn2 assg]lst.trm) \* q") +apply(erule exE) +apply(erule conjE) +apply(rule assms(5)) +apply(simp add: set_eqvt) +apply(simp add: tt2) +apply(rule refl) +apply(simp) +apply(simp add: foo.eq_iff) +apply(drule supp_perm_eq[symmetric]) +apply(simp) +apply(simp add: tt2 uu2) +apply(rule at_set_avoiding2) +apply(simp add: finite_supp) +apply(simp add: finite_supp) +apply(simp add: finite_supp) +apply(simp add: Abs_fresh_star) +apply(subgoal_tac "\q. (q \ (set (bn3 assg))) \* c \ supp ([bn3 assg]lst.trm) \* q") +apply(erule exE) +apply(erule conjE) +apply(rule assms(6)) +apply(simp add: set_eqvt) +apply(simp add: tt3) +apply(rule refl) +apply(simp) +apply(simp add: foo.eq_iff) +apply(drule supp_perm_eq[symmetric]) +apply(simp) +apply(simp add: tt3 uu3) +apply(rule at_set_avoiding2) +apply(simp add: finite_supp) +apply(simp add: finite_supp) +apply(simp add: finite_supp) +apply(simp add: Abs_fresh_star) +done + +thm foo.exhaust + +lemma strong_exhaust2: + assumes "\x y t ca. \c = ca; as = As x y t\ \ P" + shows "P" +apply(rule_tac y="as" in foo.exhaust(2)) +apply(rule assms(1)) +apply(auto)[2] +done + + +lemma + fixes t::trm + and as::assg + and c::"'a::fs" + assumes a1: "\x c. P1 c (Var x)" + and a2: "\t1 t2 c. \\d. P1 d t1; \d. P1 d t2\ \ P1 c (App t1 t2)" + and a3: "\x t c. \{atom x} \* c; \d. P1 d t\ \ P1 c (Lam x t)" + and a4: "\as t c. \set (bn1 as) \* c; \d. P2 d as; \d. P1 d t\ \ P1 c (Let1 as t)" + and a5: "\as t c. \set (bn2 as) \* c; \d. P2 d as; \d. P1 d t\ \ P1 c (Let2 as t)" + and a6: "\as t c. \set (bn3 as) \* c; \d. P2 d as; \d. P1 d t\ \ P1 c (Let3 as t)" + and a7: "\x y t c. \d. P1 d t \ P2 c (As x y t)" + shows "P1 c t" "P2 c as" +using assms +apply(induction_schema) +apply(rule_tac y="t" in strong_exhaust1) +apply(blast) +apply(blast) +apply(blast) +apply(blast) +apply(blast) +apply(blast) +apply(rule_tac as="as" in strong_exhaust2) +apply(blast) +apply(relation "measure (sum_case (\y. size (snd y)) (\z. size (snd z)))") +apply(auto)[1] +apply(simp_all add: foo.size) +done end diff -r c7534584a7a0 -r 3b6a70e73006 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Wed Sep 29 06:45:01 2010 -0400 +++ b/Nominal/Ex/Let.thy Wed Sep 29 09:47:26 2010 -0400 @@ -30,13 +30,6 @@ thm trm_assn.fresh thm trm_assn.exhaust - -lemma fin_bn: - shows "finite (set (bn l))" - apply(induct l rule: trm_assn.inducts(2)) - apply(simp_all) - done - primrec permute_bn_raw where diff -r c7534584a7a0 -r 3b6a70e73006 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Sep 29 06:45:01 2010 -0400 +++ b/Nominal/Nominal2.thy Wed Sep 29 09:47:26 2010 -0400 @@ -612,6 +612,7 @@ ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) + ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) in (0, lthy9') end handle TEST ctxt => (0, ctxt)