|
1 theory Foo2 |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 (* |
|
6 Contrived example that has more than one |
|
7 binding clause |
|
8 *) |
|
9 |
|
10 atom_decl name |
|
11 |
|
12 nominal_datatype foo: trm = |
|
13 Var "name" |
|
14 | App "trm" "trm" |
|
15 | Lam x::"name" t::"trm" bind x in t |
|
16 | Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2 |
|
17 | Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2 |
|
18 and assg = |
|
19 As_Nil |
|
20 | As "name" x::"name" t::"trm" "assg" |
|
21 binder |
|
22 bn::"assg \<Rightarrow> atom list" |
|
23 where |
|
24 "bn (As x y t a) = [atom x] @ bn a" |
|
25 | "bn (As_Nil) = []" |
|
26 |
|
27 thm foo.perm_bn_simps |
|
28 |
|
29 |
|
30 thm foo.distinct |
|
31 thm foo.induct |
|
32 thm foo.inducts |
|
33 thm foo.exhaust |
|
34 thm foo.fv_defs |
|
35 thm foo.bn_defs |
|
36 thm foo.perm_simps |
|
37 thm foo.eq_iff |
|
38 thm foo.fv_bn_eqvt |
|
39 thm foo.size_eqvt |
|
40 thm foo.supports |
|
41 thm foo.fsupp |
|
42 thm foo.supp |
|
43 thm foo.fresh |
|
44 |
|
45 lemma uu1: |
|
46 shows "alpha_bn as (permute_bn p as)" |
|
47 apply(induct as rule: foo.inducts(2)) |
|
48 apply(auto)[5] |
|
49 apply(simp add: foo.perm_bn_simps) |
|
50 apply(simp add: foo.eq_iff) |
|
51 apply(simp add: foo.perm_bn_simps) |
|
52 apply(simp add: foo.eq_iff) |
|
53 done |
|
54 |
|
55 lemma tt1: |
|
56 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
|
57 apply(induct as rule: foo.inducts(2)) |
|
58 apply(auto)[5] |
|
59 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
|
60 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
|
61 apply(simp add: atom_eqvt) |
|
62 done |
|
63 |
|
64 |
|
65 lemma Let1_rename: |
|
66 assumes "supp ([bn assn1]lst. trm1) \<sharp>* p" "supp ([bn assn2]lst. trm2) \<sharp>* p" |
|
67 shows "Let1 assn1 trm1 assn2 trm2 = Let1 (permute_bn p assn1) (p \<bullet> trm1) (permute_bn p assn2) (p \<bullet> trm2)" |
|
68 using assms |
|
69 apply - |
|
70 apply(drule supp_perm_eq[symmetric]) |
|
71 apply(drule supp_perm_eq[symmetric]) |
|
72 apply(simp only: permute_Abs) |
|
73 apply(simp only: tt1) |
|
74 apply(simp only: foo.eq_iff) |
|
75 apply(simp add: uu1) |
|
76 done |
|
77 |
|
78 lemma strong_exhaust1: |
|
79 fixes c::"'a::fs" |
|
80 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
81 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
82 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
83 and "\<And>assn1 trm1 assn2 trm2. |
|
84 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
|
85 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
86 shows "P" |
|
87 apply(rule_tac y="y" in foo.exhaust(1)) |
|
88 apply(rule assms(1)) |
|
89 apply(assumption) |
|
90 apply(rule assms(2)) |
|
91 apply(assumption) |
|
92 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
|
93 apply(erule exE) |
|
94 apply(erule conjE) |
|
95 apply(rule assms(3)) |
|
96 apply(perm_simp) |
|
97 apply(assumption) |
|
98 apply(simp) |
|
99 apply(drule supp_perm_eq[symmetric]) |
|
100 apply(perm_simp) |
|
101 apply(simp) |
|
102 apply(rule at_set_avoiding2) |
|
103 apply(simp add: finite_supp) |
|
104 apply(simp add: finite_supp) |
|
105 apply(simp add: finite_supp) |
|
106 apply(simp add: foo.fresh fresh_star_def) |
|
107 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg1))) \<sharp>* c \<and> supp ([bn assg1]lst. trm1) \<sharp>* q") |
|
108 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg2))) \<sharp>* c \<and> supp ([bn assg2]lst. trm2) \<sharp>* q") |
|
109 apply(erule exE)+ |
|
110 apply(erule conjE)+ |
|
111 apply(rule assms(4)) |
|
112 apply(simp add: set_eqvt union_eqvt) |
|
113 apply(simp add: tt1) |
|
114 apply(simp add: fresh_star_union) |
|
115 apply(rule conjI) |
|
116 apply(assumption) |
|
117 apply(rotate_tac 3) |
|
118 apply(assumption) |
|
119 apply(simp add: foo.eq_iff) |
|
120 apply(drule supp_perm_eq[symmetric])+ |
|
121 apply(simp add: tt1 uu1) |
|
122 apply(auto)[1] |
|
123 apply(rule at_set_avoiding2) |
|
124 apply(simp add: finite_supp) |
|
125 apply(simp add: finite_supp) |
|
126 apply(simp add: finite_supp) |
|
127 apply(simp add: Abs_fresh_star) |
|
128 apply(rule at_set_avoiding2) |
|
129 apply(simp add: finite_supp) |
|
130 apply(simp add: finite_supp) |
|
131 apply(simp add: finite_supp) |
|
132 apply(simp add: Abs_fresh_star) |
|
133 thm foo.eq_iff |
|
134 apply(subgoal_tac |
|
135 "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> supp ([[atom name1]]lst. trm1) \<sharp>* q") |
|
136 apply(subgoal_tac |
|
137 "\<exists>q. (q \<bullet> {atom name2}) \<sharp>* c \<and> supp ([[atom name2]]lst. trm2) \<sharp>* q") |
|
138 apply(erule exE)+ |
|
139 apply(erule conjE)+ |
|
140 apply(rule assms(5)) |
|
141 apply(perm_simp) |
|
142 apply(simp (no_asm) add: fresh_star_insert) |
|
143 apply(rule conjI) |
|
144 apply(simp add: fresh_star_def) |
|
145 apply(rotate_tac 3) |
|
146 apply(simp add: fresh_star_def) |
|
147 apply(simp) |
|
148 apply(simp add: foo.eq_iff) |
|
149 apply(drule supp_perm_eq[symmetric])+ |
|
150 apply(simp add: atom_eqvt) |
|
151 apply(rule conjI) |
|
152 oops |
|
153 |
|
154 |
|
155 end |
|
156 |
|
157 |
|
158 |