|
1 theory LetSimple1 |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 lemma Abs_lst_fcb2: |
|
6 fixes as bs :: "atom list" |
|
7 and x y :: "'b :: fs" |
|
8 and c::"'c::fs" |
|
9 assumes eq: "[as]lst. x = [bs]lst. y" |
|
10 and fcb1: "(set as) \<sharp>* f as x c" |
|
11 and fresh1: "set as \<sharp>* c" |
|
12 and fresh2: "set bs \<sharp>* c" |
|
13 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
|
14 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
15 shows "f as x c = f bs y c" |
|
16 proof - |
|
17 have "supp (as, x, c) supports (f as x c)" |
|
18 unfolding supports_def fresh_def[symmetric] |
|
19 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
|
20 then have fin1: "finite (supp (f as x c))" |
|
21 by (auto intro: supports_finite simp add: finite_supp) |
|
22 have "supp (bs, y, c) supports (f bs y c)" |
|
23 unfolding supports_def fresh_def[symmetric] |
|
24 by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) |
|
25 then have fin2: "finite (supp (f bs y c))" |
|
26 by (auto intro: supports_finite simp add: finite_supp) |
|
27 obtain q::"perm" where |
|
28 fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and |
|
29 fr2: "supp q \<sharp>* Abs_lst as x" and |
|
30 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
|
31 using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] |
|
32 fin1 fin2 |
|
33 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
|
34 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
|
35 also have "\<dots> = Abs_lst as x" |
|
36 by (simp only: fr2 perm_supp_eq) |
|
37 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp |
|
38 then obtain r::perm where |
|
39 qq1: "q \<bullet> x = r \<bullet> y" and |
|
40 qq2: "q \<bullet> as = r \<bullet> bs" and |
|
41 qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" |
|
42 apply(drule_tac sym) |
|
43 apply(simp only: Abs_eq_iff2 alphas) |
|
44 apply(erule exE) |
|
45 apply(erule conjE)+ |
|
46 apply(drule_tac x="p" in meta_spec) |
|
47 apply(simp add: set_eqvt) |
|
48 apply(blast) |
|
49 done |
|
50 have "(set as) \<sharp>* f as x c" by (rule fcb1) |
|
51 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
|
52 by (simp add: permute_bool_def) |
|
53 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
|
54 apply(simp add: fresh_star_eqvt set_eqvt) |
|
55 apply(subst (asm) perm1) |
|
56 using inc fresh1 fr1 |
|
57 apply(auto simp add: fresh_star_def fresh_Pair) |
|
58 done |
|
59 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
60 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
|
61 apply(simp add: fresh_star_eqvt set_eqvt) |
|
62 apply(subst (asm) perm2[symmetric]) |
|
63 using qq3 fresh2 fr1 |
|
64 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
|
65 done |
|
66 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
|
67 have "f as x c = q \<bullet> (f as x c)" |
|
68 apply(rule perm_supp_eq[symmetric]) |
|
69 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
|
70 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
|
71 apply(rule perm1) |
|
72 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
|
73 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
74 also have "\<dots> = r \<bullet> (f bs y c)" |
|
75 apply(rule perm2[symmetric]) |
|
76 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
|
77 also have "... = f bs y c" |
|
78 apply(rule perm_supp_eq) |
|
79 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
|
80 finally show ?thesis by simp |
|
81 qed |
|
82 |
|
83 lemma Abs_lst1_fcb2: |
|
84 fixes a b :: "atom" |
|
85 and x y :: "'b :: fs" |
|
86 and c::"'c :: fs" |
|
87 assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" |
|
88 and fcb1: "a \<sharp> f a x c" |
|
89 and fresh: "{a, b} \<sharp>* c" |
|
90 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
|
91 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
|
92 shows "f a x c = f b y c" |
|
93 using e |
|
94 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"]) |
|
95 apply(simp_all) |
|
96 using fcb1 fresh perm1 perm2 |
|
97 apply(simp_all add: fresh_star_def) |
|
98 done |
|
99 |
|
100 |
|
101 atom_decl name |
|
102 |
|
103 nominal_datatype trm = |
|
104 Var "name" |
|
105 | App "trm" "trm" |
|
106 | Let x::"name" "trm" t::"trm" bind x in t |
|
107 |
|
108 print_theorems |
|
109 |
|
110 thm trm.fv_defs |
|
111 thm trm.eq_iff |
|
112 thm trm.bn_defs |
|
113 thm trm.bn_inducts |
|
114 thm trm.perm_simps |
|
115 thm trm.induct |
|
116 thm trm.inducts |
|
117 thm trm.distinct |
|
118 thm trm.supp |
|
119 thm trm.fresh |
|
120 thm trm.exhaust |
|
121 thm trm.strong_exhaust |
|
122 thm trm.perm_bn_simps |
|
123 |
|
124 nominal_primrec |
|
125 height_trm :: "trm \<Rightarrow> nat" |
|
126 where |
|
127 "height_trm (Var x) = 1" |
|
128 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
|
129 | "height_trm (Let x t s) = max (height_trm t) (height_trm s)" |
|
130 apply (simp only: eqvt_def height_trm_graph_def) |
|
131 apply (rule, perm_simp, rule, rule TrueI) |
|
132 apply (case_tac x rule: trm.exhaust(1)) |
|
133 apply (auto)[3] |
|
134 apply(simp_all)[5] |
|
135 apply (subgoal_tac "height_trm_sumC t = height_trm_sumC ta") |
|
136 apply (subgoal_tac "height_trm_sumC s = height_trm_sumC sa") |
|
137 apply simp |
|
138 apply(simp) |
|
139 apply(erule conjE) |
|
140 apply(erule_tac c="()" in Abs_lst1_fcb2) |
|
141 apply(simp_all add: fresh_star_def pure_fresh)[2] |
|
142 apply(simp_all add: eqvt_at_def)[2] |
|
143 apply(simp) |
|
144 done |
|
145 |
|
146 termination |
|
147 by lexicographic_order |
|
148 |
|
149 |
|
150 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
|
151 frees_set :: "trm \<Rightarrow> atom set" |
|
152 where |
|
153 "frees_set (Var x) = {atom x}" |
|
154 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
|
155 | "frees_set (Let x t s) = (frees_set s) - {atom x} \<union> (frees_set t)" |
|
156 apply(simp add: eqvt_def frees_set_graph_def) |
|
157 apply(rule, perm_simp, rule) |
|
158 apply(erule frees_set_graph.induct) |
|
159 apply(auto)[3] |
|
160 apply(rule_tac y="x" in trm.exhaust) |
|
161 apply(auto)[3] |
|
162 apply(simp_all)[5] |
|
163 apply(simp) |
|
164 apply(erule conjE) |
|
165 apply(subgoal_tac "frees_set_sumC s - {atom x} = frees_set_sumC sa - {atom xa}") |
|
166 apply(simp) |
|
167 apply(erule_tac c="()" in Abs_lst1_fcb2) |
|
168 apply(simp add: fresh_minus_atom_set) |
|
169 apply(simp add: fresh_star_def fresh_Unit) |
|
170 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
|
171 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
|
172 done |
|
173 |
|
174 termination |
|
175 by lexicographic_order |
|
176 |
|
177 |
|
178 nominal_primrec |
|
179 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90) |
|
180 where |
|
181 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
182 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
183 | "atom x \<sharp> (y, s) \<Longrightarrow> (Let x t t')[y ::= s] = Let x (t[y ::= s]) (t'[y ::= s])" |
|
184 apply(simp add: eqvt_def subst_graph_def) |
|
185 apply (rule, perm_simp, rule) |
|
186 apply(rule TrueI) |
|
187 apply(auto)[1] |
|
188 apply(rule_tac y="a" and c="(aa, b)" in trm.strong_exhaust) |
|
189 apply(blast)+ |
|
190 apply(simp_all add: fresh_star_def fresh_Pair_elim)[1] |
|
191 apply(blast) |
|
192 apply(simp_all)[5] |
|
193 apply(simp (no_asm_use)) |
|
194 apply(simp) |
|
195 apply(erule conjE)+ |
|
196 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
|
197 apply(simp add: Abs_fresh_iff) |
|
198 apply(simp add: fresh_star_def fresh_Pair) |
|
199 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
200 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
201 done |
|
202 |
|
203 termination |
|
204 by lexicographic_order |
|
205 |
|
206 |
|
207 end |