154 case (t_Var \<Gamma> x T p c) |
154 case (t_Var \<Gamma> x T p c) |
155 then show ?case |
155 then show ?case |
156 apply - |
156 apply - |
157 apply(perm_strict_simp) |
157 apply(perm_strict_simp) |
158 apply(rule a1) |
158 apply(rule a1) |
159 apply(rule_tac p="-p" in permute_boolE) |
159 apply(drule_tac p="p" in permute_boolI) |
160 apply(perm_strict_simp add: permute_minus_cancel) |
160 apply(perm_strict_simp add: permute_minus_cancel) |
161 apply(assumption) |
161 apply(assumption) |
162 apply(rule_tac p="-p" in permute_boolE) |
162 apply(rotate_tac 1) |
|
163 apply(drule_tac p="p" in permute_boolI) |
163 apply(perm_strict_simp add: permute_minus_cancel) |
164 apply(perm_strict_simp add: permute_minus_cancel) |
164 apply(assumption) |
165 apply(assumption) |
165 done |
166 done |
166 next |
167 next |
167 case (t_App \<Gamma> t1 T1 T2 t2 p c) |
168 case (t_App \<Gamma> t1 T1 T2 t2 p c) |
168 then show ?case |
169 then show ?case |
169 apply - |
170 apply - |
170 apply(perm_strict_simp) |
171 apply(perm_strict_simp) |
171 apply(rule_tac ?T1.0="p \<bullet> T1" in a2) |
172 apply(rule a2) |
172 apply(rule_tac p="-p" in permute_boolE) |
173 apply(drule_tac p="p" in permute_boolI) |
173 apply(perm_strict_simp add: permute_minus_cancel) |
174 apply(perm_strict_simp add: permute_minus_cancel) |
174 apply(assumption) |
175 apply(assumption) |
175 apply(assumption) |
176 apply(assumption) |
176 apply(rule_tac p="-p" in permute_boolE) |
177 apply(rotate_tac 2) |
|
178 apply(drule_tac p="p" in permute_boolI) |
177 apply(perm_strict_simp add: permute_minus_cancel) |
179 apply(perm_strict_simp add: permute_minus_cancel) |
178 apply(assumption) |
180 apply(assumption) |
179 apply(assumption) |
181 apply(assumption) |
180 done |
182 done |
181 next |
183 next |
183 then show ?case |
185 then show ?case |
184 apply - |
186 apply - |
185 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> |
187 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> |
186 supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q") |
188 supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q") |
187 apply(erule exE) |
189 apply(erule exE) |
188 apply(rule_tac t="p \<bullet> \<Gamma>" and s="q \<bullet> p \<bullet> \<Gamma>" in subst) |
190 apply(rule_tac t="p \<bullet> \<Gamma>" and s="(q + p) \<bullet> \<Gamma>" in subst) |
|
191 apply(simp only: permute_plus) |
189 apply(rule supp_perm_eq) |
192 apply(rule supp_perm_eq) |
190 apply(simp add: supp_Pair fresh_star_union) |
193 apply(simp add: supp_Pair fresh_star_union) |
191 apply(rule_tac t="p \<bullet> Lam x t" and s="q \<bullet> p \<bullet> Lam x t" in subst) |
194 apply(rule_tac t="p \<bullet> Lam x t" and s="(q + p) \<bullet> Lam x t" in subst) |
|
195 apply(simp only: permute_plus) |
192 apply(rule supp_perm_eq) |
196 apply(rule supp_perm_eq) |
193 apply(simp add: supp_Pair fresh_star_union) |
197 apply(simp add: supp_Pair fresh_star_union) |
194 apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and s="q \<bullet> p \<bullet> (T1 \<rightarrow> T2)" in subst) |
198 apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst) |
|
199 apply(simp only: permute_plus) |
195 apply(rule supp_perm_eq) |
200 apply(rule supp_perm_eq) |
196 apply(simp add: supp_Pair fresh_star_union) |
201 apply(simp add: supp_Pair fresh_star_union) |
197 apply(simp add: eqvts) |
202 apply(simp (no_asm) only: eqvts) |
198 apply(rule a3) |
203 apply(rule a3) |
|
204 apply(simp only: eqvts permute_plus) |
199 apply(simp add: fresh_star_def) |
205 apply(simp add: fresh_star_def) |
200 apply(rule_tac p="-q" in permute_boolE) |
206 apply(drule_tac p="q + p" in permute_boolI) |
201 apply(perm_strict_simp add: permute_minus_cancel) |
207 apply(perm_strict_simp add: permute_minus_cancel) |
202 apply(rule_tac p="-p" in permute_boolE) |
208 apply(assumption) |
203 apply(perm_strict_simp add: permute_minus_cancel) |
209 apply(rotate_tac 1) |
204 apply(assumption) |
210 apply(drule_tac p="q + p" in permute_boolI) |
205 apply(rule_tac p="-q" in permute_boolE) |
|
206 apply(perm_strict_simp add: permute_minus_cancel) |
|
207 apply(rule_tac p="-p" in permute_boolE) |
|
208 apply(perm_strict_simp add: permute_minus_cancel) |
211 apply(perm_strict_simp add: permute_minus_cancel) |
209 apply(assumption) |
212 apply(assumption) |
210 apply(drule_tac x="d" in meta_spec) |
213 apply(drule_tac x="d" in meta_spec) |
211 apply(drule_tac x="q + p" in meta_spec) |
214 apply(drule_tac x="q + p" in meta_spec) |
212 apply(simp) |
215 apply(perm_strict_simp add: permute_minus_cancel) |
|
216 apply(assumption) |
213 apply(rule at_set_avoiding2) |
217 apply(rule at_set_avoiding2) |
214 apply(simp add: finite_supp) |
218 apply(simp add: finite_supp) |
215 apply(simp add: finite_supp) |
219 apply(simp add: finite_supp) |
216 apply(simp add: finite_supp) |
220 apply(simp add: finite_supp) |
217 apply(rule_tac p="-p" in permute_boolE) |
221 apply(rule_tac p="-p" in permute_boolE) |
218 apply(perm_strict_simp add: permute_minus_cancel) |
222 apply(perm_strict_simp add: permute_minus_cancel) |
219 (* supplied by the user *) |
223 (* supplied by the user *) |
220 apply(simp add: fresh_star_prod) |
224 apply(simp add: fresh_star_prod) |
221 apply(simp add: fresh_star_def) |
225 apply(simp add: fresh_star_def) |
222 |
226 sorry |
223 |
227 qed |
224 done |
228 then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" . |
225 (* HERE *) |
229 then show "P c \<Gamma> t T" by simp |
|
230 qed |
226 |
231 |
227 |
232 |
228 |
233 |
229 |
234 |
230 |
235 |
412 apply(subst if_not_P) |
417 apply(subst if_not_P) |
413 apply(auto) |
418 apply(auto) |
414 done |
419 done |
415 *) |
420 *) |
416 |
421 |
|
422 ML {* |
|
423 fun mk_avoids ctxt params name set = |
|
424 let |
|
425 val (_, ctxt') = ProofContext.add_fixes |
|
426 (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt; |
|
427 fun mk s = |
|
428 let |
|
429 val t = Syntax.read_term ctxt' s; |
|
430 val t' = list_abs_free (params, t) |> |
|
431 funpow (length params) (fn Abs (_, _, t) => t) |
|
432 in (t', HOLogic.dest_setT (fastype_of t)) end |
|
433 handle TERM _ => |
|
434 error ("Expression " ^ quote s ^ " to be avoided in case " ^ |
|
435 quote name ^ " is not a set type"); |
|
436 fun add_set p [] = [p] |
|
437 | add_set (t, T) ((u, U) :: ps) = |
|
438 if T = U then |
|
439 let val S = HOLogic.mk_setT T |
|
440 in (Const (@{const_name sup}, S --> S --> S) $ u $ t, T) :: ps |
|
441 end |
|
442 else (u, U) :: add_set (t, T) ps |
|
443 in |
|
444 (mk #> add_set) set |
|
445 end; |
|
446 *} |
|
447 |
|
448 |
|
449 ML {* |
|
450 writeln (commas (map (Syntax.string_of_term @{context} o fst) |
|
451 (mk_avoids @{context} [] "t_Var" "{x}" []))) |
|
452 *} |
|
453 |
417 |
454 |
418 ML {* |
455 ML {* |
419 |
456 |
420 fun prove_strong_ind (pred_name, avoids) ctxt = |
457 fun prove_strong_ind (pred_name, avoids) ctxt = |
421 Proof.theorem NONE (K I) [] ctxt |
458 Proof.theorem NONE (K I) [] ctxt |