# HG changeset patch # User Christian Urban # Date 1290305839 0 # Node ID 6c131c089ce2730ce1fa070cbe03f85f606a09b3 # Parent 73196608ec0427f6e96ad405f52347b858786873 added example Foo2.thy diff -r 73196608ec04 -r 6c131c089ce2 Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Mon Nov 15 20:54:01 2010 +0000 +++ b/Nominal/Ex/Foo1.thy Sun Nov 21 02:17:19 2010 +0000 @@ -127,6 +127,30 @@ done +lemma Let1_rename: + assumes "supp ([bn1 assn]lst. trm) \* p" + shows "Let1 assn trm = Let1 (permute_bn1 p assn) (p \ trm)" +using assms +apply - +apply(drule supp_perm_eq[symmetric]) +apply(simp only: permute_Abs) +apply(simp only: tt1) +apply(simp only: foo.eq_iff) +apply(rule conjI) +apply(rule refl) +apply(rule uu1) +done + +lemma Let1_rename_a: + fixes c::"'a::fs" + assumes "y = Let1 assn trm" + shows "\p. (p \ (set (bn1 assn))) \* c \ y = Let1 (permute_bn1 p assn) (p \ trm)" +using assms +apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric]) +apply(simp del: permute_Abs) +apply(rule at_set_avoiding3) +apply(simp_all only: finite_supp Abs_fresh_star finite_set) +done lemma strong_exhaust1: fixes c::"'a::fs" @@ -158,20 +182,12 @@ 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(drule Let1_rename_a) apply(erule exE) apply(erule conjE) apply(rule assms(4)) -apply(perm_simp add: tt1) +apply(simp only: set_eqvt tt1) apply(assumption) -apply(drule supp_perm_eq[symmetric]) -apply(simp add: foo.eq_iff) -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) diff -r 73196608ec04 -r 6c131c089ce2 Nominal/Ex/Foo2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/Foo2.thy Sun Nov 21 02:17:19 2010 +0000 @@ -0,0 +1,158 @@ +theory Foo2 +imports "../Nominal2" +begin + +(* + Contrived example that has more than one + binding clause +*) + +atom_decl name + +nominal_datatype foo: trm = + Var "name" +| App "trm" "trm" +| Lam x::"name" t::"trm" bind x in t +| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2 +| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2 +and assg = + As_Nil +| As "name" x::"name" t::"trm" "assg" +binder + bn::"assg \ atom list" +where + "bn (As x y t a) = [atom x] @ bn a" +| "bn (As_Nil) = []" + +thm foo.perm_bn_simps + + +thm foo.distinct +thm foo.induct +thm foo.inducts +thm foo.exhaust +thm foo.fv_defs +thm foo.bn_defs +thm foo.perm_simps +thm foo.eq_iff +thm foo.fv_bn_eqvt +thm foo.size_eqvt +thm foo.supports +thm foo.fsupp +thm foo.supp +thm foo.fresh + +lemma uu1: + shows "alpha_bn as (permute_bn p as)" +apply(induct as rule: foo.inducts(2)) +apply(auto)[5] +apply(simp add: foo.perm_bn_simps) +apply(simp add: foo.eq_iff) +apply(simp add: foo.perm_bn_simps) +apply(simp add: foo.eq_iff) +done + +lemma tt1: + shows "(p \ bn as) = bn (permute_bn p as)" +apply(induct as rule: foo.inducts(2)) +apply(auto)[5] +apply(simp add: foo.perm_bn_simps foo.bn_defs) +apply(simp add: foo.perm_bn_simps foo.bn_defs) +apply(simp add: atom_eqvt) +done + + +lemma Let1_rename: + assumes "supp ([bn assn1]lst. trm1) \* p" "supp ([bn assn2]lst. trm2) \* p" + shows "Let1 assn1 trm1 assn2 trm2 = Let1 (permute_bn p assn1) (p \ trm1) (permute_bn p assn2) (p \ trm2)" +using assms +apply - +apply(drule supp_perm_eq[symmetric]) +apply(drule supp_perm_eq[symmetric]) +apply(simp only: permute_Abs) +apply(simp only: tt1) +apply(simp only: foo.eq_iff) +apply(simp add: uu1) +done + +lemma strong_exhaust1: + fixes c::"'a::fs" + assumes "\name. y = Var name \ P" + and "\trm1 trm2. y = App trm1 trm2 \ P" + and "\name trm. \{atom name} \* c; y = Lam name trm\ \ P" + and "\assn1 trm1 assn2 trm2. + \((set (bn assn1)) \ (set (bn assn2))) \* c; y = Let1 assn1 trm1 assn2 trm2\ \ P" + and "\x1 x2 trm1 trm2. \{atom x1, atom x2} \* c; y = Let2 x1 x2 trm1 trm2\ \ P" + shows "P" +apply(rule_tac y="y" in foo.exhaust(1)) +apply(rule assms(1)) +apply(assumption) +apply(rule assms(2)) +apply(assumption) +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(simp) +apply(drule supp_perm_eq[symmetric]) +apply(perm_simp) +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 (bn assg1))) \* c \ supp ([bn assg1]lst. trm1) \* q") +apply(subgoal_tac "\q. (q \ (set (bn assg2))) \* c \ supp ([bn assg2]lst. trm2) \* q") +apply(erule exE)+ +apply(erule conjE)+ +apply(rule assms(4)) +apply(simp add: set_eqvt union_eqvt) +apply(simp add: tt1) +apply(simp add: fresh_star_union) +apply(rule conjI) +apply(assumption) +apply(rotate_tac 3) +apply(assumption) +apply(simp add: foo.eq_iff) +apply(drule supp_perm_eq[symmetric])+ +apply(simp add: tt1 uu1) +apply(auto)[1] +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(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) +thm foo.eq_iff +apply(subgoal_tac + "\q. (q \ {atom name1}) \* c \ supp ([[atom name1]]lst. trm1) \* q") +apply(subgoal_tac + "\q. (q \ {atom name2}) \* c \ supp ([[atom name2]]lst. trm2) \* q") +apply(erule exE)+ +apply(erule conjE)+ +apply(rule assms(5)) +apply(perm_simp) +apply(simp (no_asm) add: fresh_star_insert) +apply(rule conjI) +apply(simp add: fresh_star_def) +apply(rotate_tac 3) +apply(simp add: fresh_star_def) +apply(simp) +apply(simp add: foo.eq_iff) +apply(drule supp_perm_eq[symmetric])+ +apply(simp add: atom_eqvt) +apply(rule conjI) +oops + + +end + + + diff -r 73196608ec04 -r 6c131c089ce2 Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Mon Nov 15 20:54:01 2010 +0000 +++ b/Nominal/Nominal2_Base.thy Sun Nov 21 02:17:19 2010 +0000 @@ -1579,6 +1579,15 @@ apply(auto simp add: fresh_star_def) done +lemma at_set_avoiding3: + assumes "finite xs" + and "finite (supp c)" "finite (supp x)" + and "xs \* x" + shows "\p. (p \ xs) \* c \ x = p \ x" +using at_set_avoiding2[OF assms] +by (auto simp add: supp_perm_eq) + + lemma at_set_avoiding2_atom: assumes "finite (supp c)" "finite (supp x)" and b: "a \ x"