18 thm lam.perm_simps |
18 thm lam.perm_simps |
19 thm lam.eq_iff |
19 thm lam.eq_iff |
20 thm lam.fv_bn_eqvt |
20 thm lam.fv_bn_eqvt |
21 thm lam.size_eqvt |
21 thm lam.size_eqvt |
22 |
22 |
23 ML {* |
|
24 fun mk_cplus p q = Thm.capply (Thm.capply @{cterm "plus::perm \<Rightarrow> perm \<Rightarrow> perm"} p) q |
|
25 |
|
26 fun mk_cminus p = Thm.capply @{cterm "uminus::perm \<Rightarrow> perm"} p |
|
27 |
|
28 |
|
29 fun minus_permute_intro_tac p = |
|
30 rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}) |
|
31 |
|
32 fun minus_permute_elim p thm = |
|
33 thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) |
|
34 *} |
|
35 |
|
36 ML {* |
|
37 fun real_head_of (@{term Trueprop} $ t) = real_head_of t |
|
38 | real_head_of (Const ("==>", _) $ _ $ t) = real_head_of t |
|
39 | real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t |
|
40 | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t |
|
41 | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t |
|
42 | real_head_of t = head_of t |
|
43 *} |
|
44 |
|
45 ML {* |
|
46 fun mk_vc_compat (avoid, avoid_trm) prems concl_args params = |
|
47 let |
|
48 val vc_goal = concl_args |
|
49 |> HOLogic.mk_tuple |
|
50 |> mk_fresh_star avoid_trm |
|
51 |> HOLogic.mk_Trueprop |
|
52 |> (curry Logic.list_implies) prems |
|
53 |> (curry list_all_free) params |
|
54 val finite_goal = avoid_trm |
|
55 |> mk_finite |
|
56 |> HOLogic.mk_Trueprop |
|
57 |> (curry Logic.list_implies) prems |
|
58 |> (curry list_all_free) params |
|
59 in |
|
60 if null avoid then [] else [vc_goal, finite_goal] |
|
61 end |
|
62 *} |
|
63 |
|
64 ML {* |
|
65 fun map_term prop f trm = |
|
66 if prop trm |
|
67 then f trm |
|
68 else case trm of |
|
69 (t1 $ t2) => map_term prop f t1 $ map_term prop f t2 |
|
70 | Abs (x, T, t) => Abs (x, T, map_term prop f t) |
|
71 | _ => trm |
|
72 *} |
|
73 |
|
74 ML {* |
|
75 fun add_p_c p (c, c_ty) trm = |
|
76 let |
|
77 val (P, args) = strip_comb trm |
|
78 val (P_name, P_ty) = dest_Free P |
|
79 val (ty_args, bool) = strip_type P_ty |
|
80 val args' = map (mk_perm p) args |
|
81 in |
|
82 list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |
|
83 |> (fn t => HOLogic.all_const c_ty $ lambda c t ) |
|
84 |> (fn t => HOLogic.all_const @{typ perm} $ lambda p t) |
|
85 end |
|
86 *} |
|
87 |
|
88 ML {* |
|
89 fun induct_forall_const T = Const ("HOL.induct_forall", (T --> @{typ bool}) --> @{typ bool}) |
|
90 fun mk_induct_forall (a, T) t = induct_forall_const T $ Abs (a, T, t) |
|
91 *} |
|
92 |
|
93 ML {* |
|
94 fun add_c_prop qnt Ps (c, c_name, c_ty) trm = |
|
95 let |
|
96 fun add t = |
|
97 let |
|
98 val (P, args) = strip_comb t |
|
99 val (P_name, P_ty) = dest_Free P |
|
100 val (ty_args, bool) = strip_type P_ty |
|
101 val args' = args |
|
102 |> qnt ? map (incr_boundvars 1) |
|
103 in |
|
104 list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |
|
105 |> qnt ? mk_induct_forall (c_name, c_ty) |
|
106 end |
|
107 in |
|
108 map_term (member (op =) Ps o head_of) add trm |
|
109 end |
|
110 *} |
|
111 |
|
112 ML {* |
|
113 fun prep_prem Ps c_name c_ty (avoid, avoid_trm) (params, prems, concl) = |
|
114 let |
|
115 val prems' = prems |
|
116 |> map (incr_boundvars 1) |
|
117 |> map (add_c_prop true Ps (Bound 0, c_name, c_ty)) |
|
118 |
|
119 val avoid_trm' = avoid_trm |
|
120 |> (curry list_abs_free) (params @ [(c_name, c_ty)]) |
|
121 |> strip_abs_body |
|
122 |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |
|
123 |> HOLogic.mk_Trueprop |
|
124 |
|
125 val prems'' = |
|
126 if null avoid |
|
127 then prems' |
|
128 else avoid_trm' :: prems' |
|
129 |
|
130 val concl' = concl |
|
131 |> incr_boundvars 1 |
|
132 |> add_c_prop false Ps (Bound 0, c_name, c_ty) |
|
133 in |
|
134 mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' |
|
135 end |
|
136 *} |
|
137 |
|
138 |
|
139 ML {* |
|
140 fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2) |
|
141 | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2) |
|
142 | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2) |
|
143 | same_name _ = false |
|
144 *} |
|
145 |
|
146 ML {* |
|
147 fun map7 _ [] [] [] [] [] [] [] = [] |
|
148 | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = |
|
149 f x y z u v r s :: map7 f xs ys zs us vs rs ss |
|
150 *} |
|
151 |
|
152 ML {* |
|
153 (* local abbreviations *) |
|
154 fun eqvt_stac ctxt = Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel} [] |
|
155 fun eqvt_srule ctxt = Nominal_Permeq.eqvt_strict_rule ctxt @{thms permute_minus_cancel} [] |
|
156 *} |
|
157 |
|
158 ML {* |
|
159 val all_elims = |
|
160 let |
|
161 fun spec' ct = Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec} |
|
162 in |
|
163 fold (fn ct => fn th => th RS spec' ct) |
|
164 end |
|
165 *} |
|
166 |
|
167 ML {* |
|
168 fun helper_tac flag prm p ctxt = |
|
169 Subgoal.SUBPROOF (fn {context, prems, ...} => |
|
170 let |
|
171 val prems' = prems |
|
172 |> map (minus_permute_elim p) |
|
173 |> map (eqvt_srule context) |
|
174 |
|
175 val prm' = (prems' MRS prm) |
|
176 |> flag ? (all_elims [p]) |
|
177 |> flag ? (eqvt_srule context) |
|
178 |
|
179 val _ = tracing ("prm':" ^ @{make_string} prm') |
|
180 in |
|
181 print_tac "start helper" |
|
182 THEN asm_full_simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def})) 1 |
|
183 THEN print_tac "final helper" |
|
184 end) ctxt |
|
185 *} |
|
186 |
|
187 ML {* |
|
188 fun non_binder_tac prem intr_cvars Ps ctxt = |
|
189 Subgoal.SUBPROOF (fn {context, params, prems, ...} => |
|
190 let |
|
191 val thy = ProofContext.theory_of context |
|
192 val (prms, p, _) = split_last2 (map snd params) |
|
193 val prm_tys = map (fastype_of o term_of) prms |
|
194 val cperms = map (cterm_of thy o perm_const) prm_tys |
|
195 val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms |
|
196 val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem |
|
197 |
|
198 (* for inductive-premises*) |
|
199 fun tac1 prm = helper_tac true prm p context |
|
200 |
|
201 (* for non-inductive premises *) |
|
202 fun tac2 prm = |
|
203 EVERY' [ minus_permute_intro_tac p, |
|
204 eqvt_stac context, |
|
205 helper_tac false prm p context ] |
|
206 |
|
207 fun select prm (t, i) = |
|
208 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i |
|
209 in |
|
210 EVERY1 [eqvt_stac ctxt, rtac prem', RANGE (map (SUBGOAL o select) prems) ] |
|
211 end) ctxt |
|
212 *} |
|
213 |
|
214 |
|
215 ML {* |
|
216 fun fresh_thm ctxt user_thm p c concl_args avoid_trm = |
|
217 let |
|
218 val conj1 = |
|
219 mk_fresh_star (mk_perm (Bound 0) (mk_perm p avoid_trm)) c |
|
220 val conj2 = |
|
221 mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) concl_args))) (Bound 0) |
|
222 val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2)) |
|
223 |> HOLogic.mk_Trueprop |
|
224 |
|
225 val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ |
|
226 @{thms fresh_star_Pair fresh_star_permute_iff} |
|
227 val simp = asm_full_simp_tac (HOL_ss addsimps ss) |
|
228 in |
|
229 Goal.prove ctxt [] [] fresh_goal |
|
230 (K (HEADGOAL (rtac @{thm at_set_avoiding2} |
|
231 THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp]))) |
|
232 end |
|
233 *} |
|
234 |
|
235 ML {* |
|
236 val supp_perm_eq' = |
|
237 @{lemma "supp (p \<bullet> x) \<sharp>* q ==> p \<bullet> x == (q + p) \<bullet> x" by (simp add: supp_perm_eq)} |
|
238 val fresh_star_plus = |
|
239 @{lemma "(q \<bullet> (p \<bullet> x)) \<sharp>* c ==> ((q + p) \<bullet> x) \<sharp>* c" by (simp add: permute_plus)} |
|
240 *} |
|
241 |
|
242 ML {* |
|
243 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt = |
|
244 Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => |
|
245 let |
|
246 val thy = ProofContext.theory_of ctxt |
|
247 val (prms, p, c) = split_last2 (map snd params) |
|
248 val prm_trms = map term_of prms |
|
249 val prm_tys = map fastype_of prm_trms |
|
250 |
|
251 val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm |
|
252 val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args |
|
253 |
|
254 val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm |
|
255 |> map (full_simplify (HOL_ss addsimps (@{thm fresh_star_Pair}::prems))) |
|
256 |
|
257 val fthm = fresh_thm ctxt user_thm' (term_of p) (term_of c) concl_args' avoid_trm' |
|
258 |
|
259 val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result |
|
260 (K (EVERY1 [etac @{thm exE}, |
|
261 full_simp_tac (HOL_basic_ss addsimps @{thms supp_Pair fresh_star_Un}), |
|
262 REPEAT o etac @{thm conjE}, |
|
263 dtac fresh_star_plus, |
|
264 REPEAT o dtac supp_perm_eq'])) [fthm] ctxt |
|
265 |
|
266 val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) |
|
267 fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt |
|
268 |
|
269 val cperms = map (cterm_of thy o perm_const) prm_tys |
|
270 val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms |
|
271 val prem' = cterm_instantiate (intr_cvars ~~ qp_prms) prem |
|
272 |
|
273 val fprop' = eqvt_srule ctxt' fprop |
|
274 val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop']) |
|
275 |
|
276 (* for inductive-premises*) |
|
277 fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' |
|
278 |
|
279 (* for non-inductive premises *) |
|
280 fun tac2 prm = |
|
281 EVERY' [ minus_permute_intro_tac (mk_cplus q p), |
|
282 eqvt_stac ctxt, |
|
283 helper_tac false prm (mk_cplus q p) ctxt' ] |
|
284 |
|
285 fun select prm (t, i) = |
|
286 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i |
|
287 |
|
288 val _ = tracing ("fthm:\n" ^ @{make_string} fthm) |
|
289 val _ = tracing ("fr_eqs:\n" ^ cat_lines (map @{make_string} fresh_eqs)) |
|
290 val _ = tracing ("fprop:\n" ^ @{make_string} fprop) |
|
291 val _ = tracing ("fprop':\n" ^ @{make_string} fprop') |
|
292 val _ = tracing ("fperm:\n" ^ @{make_string} q) |
|
293 val _ = tracing ("prem':\n" ^ @{make_string} prem') |
|
294 |
|
295 val side_thm = Goal.prove ctxt' [] [] (term_of concl) |
|
296 (fn {context, ...} => |
|
297 EVERY1 [ CONVERSION (expand_conv_bot context), |
|
298 eqvt_stac context, |
|
299 rtac prem', |
|
300 RANGE (tac_fresh :: map (SUBGOAL o select) prems), |
|
301 K (print_tac "GOAL") ]) |
|
302 |> singleton (ProofContext.export ctxt' ctxt) |
|
303 in |
|
304 rtac side_thm 1 |
|
305 end) ctxt |
|
306 *} |
|
307 |
|
308 ML {* |
|
309 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = |
|
310 let |
|
311 val tac1 = non_binder_tac prem intr_cvars Ps ctxt |
|
312 val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt |
|
313 in |
|
314 EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ] |
|
315 end |
|
316 *} |
|
317 |
|
318 ML {* |
|
319 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args |
|
320 {prems, context} = |
|
321 let |
|
322 val cases_tac = |
|
323 map7 (case_tac context Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args |
|
324 in |
|
325 EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ] |
|
326 end |
|
327 *} |
|
328 |
|
329 ML {* |
|
330 val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp} |
|
331 *} |
|
332 |
|
333 ML {* Local_Theory.note *} |
|
334 |
|
335 ML {* |
|
336 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt = |
|
337 let |
|
338 val thy = ProofContext.theory_of ctxt |
|
339 val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt |
|
340 |
|
341 val (ind_prems, ind_concl) = raw_induct' |
|
342 |> prop_of |
|
343 |> Logic.strip_horn |
|
344 |>> map strip_full_horn |
|
345 val params = map (fn (x, _, _) => x) ind_prems |
|
346 val param_trms = (map o map) Free params |
|
347 |
|
348 val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs |
|
349 val intr_vars = (map o map) fst intr_vars_tys |
|
350 val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms |
|
351 val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys |
|
352 |
|
353 val (intr_prems, intr_concls) = intrs |
|
354 |> map prop_of |
|
355 |> map2 subst_Vars intr_vars_substs |
|
356 |> map Logic.strip_horn |
|
357 |> split_list |
|
358 |
|
359 val intr_concls_args = map (snd o strip_comb o HOLogic.dest_Trueprop) intr_concls |
|
360 |
|
361 val avoid_trms = avoids |
|
362 |> (map o map) (setify ctxt') |
|
363 |> map fold_union |
|
364 |
|
365 val vc_compat_goals = |
|
366 map4 mk_vc_compat (avoids ~~ avoid_trms) intr_prems intr_concls_args params |
|
367 |
|
368 val ([c_name, a, p], ctxt'') = Variable.variant_fixes ["c", "'a", "p"] ctxt' |
|
369 val c_ty = TFree (a, @{sort fs}) |
|
370 val c = Free (c_name, c_ty) |
|
371 val p = Free (p, @{typ perm}) |
|
372 |
|
373 val (preconds, ind_concls) = ind_concl |
|
374 |> HOLogic.dest_Trueprop |
|
375 |> HOLogic.dest_conj |
|
376 |> map HOLogic.dest_imp |
|
377 |> split_list |
|
378 |
|
379 val Ps = map (fst o strip_comb) ind_concls |
|
380 |
|
381 val ind_concl' = ind_concls |
|
382 |> map (add_p_c p (c, c_ty)) |
|
383 |> (curry (op ~~)) preconds |
|
384 |> map HOLogic.mk_imp |
|
385 |> fold_conj |
|
386 |> HOLogic.mk_Trueprop |
|
387 |
|
388 val ind_prems' = ind_prems |
|
389 |> map2 (prep_prem Ps c_name c_ty) (avoids ~~ avoid_trms) |
|
390 |
|
391 fun after_qed ctxt_outside user_thms ctxt = |
|
392 let |
|
393 val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' |
|
394 (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |
|
395 |> singleton (ProofContext.export ctxt ctxt_outside) |
|
396 |> Datatype_Aux.split_conj_thm |
|
397 |> map (fn thm => thm RS normalise) |
|
398 |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify})) |
|
399 |> map (Drule.rotate_prems (length ind_prems')) |
|
400 |> map zero_var_indexes |
|
401 |
|
402 val qualified_thm_name = pred_names |
|
403 |> map Long_Name.base_name |
|
404 |> space_implode "_" |
|
405 |> (fn s => Binding.qualify false s (Binding.name "strong_induct")) |
|
406 |
|
407 val attrs = |
|
408 [ Attrib.internal (K (Rule_Cases.consumes 1)), |
|
409 Attrib.internal (K (Rule_Cases.case_names rule_names)) ] |
|
410 val _ = tracing ("RESULTS\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) strong_ind_thms)) |
|
411 val _ = tracing ("rule_names: " ^ commas rule_names) |
|
412 val _ = tracing ("pred_names: " ^ commas pred_names) |
|
413 in |
|
414 ctxt |
|
415 |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms) |
|
416 |> snd |
|
417 end |
|
418 in |
|
419 Proof.theorem NONE (after_qed ctxt) ((map o map) (rpair []) vc_compat_goals) ctxt'' |
|
420 end |
|
421 *} |
|
422 |
|
423 ML {* |
|
424 fun prove_strong_inductive_cmd (pred_name, avoids) ctxt = |
|
425 let |
|
426 val thy = ProofContext.theory_of ctxt; |
|
427 val ({names, ...}, {raw_induct, intrs, ...}) = |
|
428 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name); |
|
429 |
|
430 val rule_names = |
|
431 hd names |
|
432 |> the o Induct.lookup_inductP ctxt |
|
433 |> fst o Rule_Cases.get |
|
434 |> map fst |
|
435 |
|
436 val _ = (case duplicates (op = o pairself fst) avoids of |
|
437 [] => () |
|
438 | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs))) |
|
439 |
|
440 val _ = (case subtract (op =) rule_names (map fst avoids) of |
|
441 [] => () |
|
442 | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)) |
|
443 |
|
444 val avoids_ordered = order_default (op =) [] rule_names avoids |
|
445 |
|
446 fun read_avoids avoid_trms intr = |
|
447 let |
|
448 (* fixme hack *) |
|
449 val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt |
|
450 val trms = map (term_of o snd) ctrms |
|
451 val ctxt'' = fold Variable.declare_term trms ctxt' |
|
452 in |
|
453 map (Syntax.read_term ctxt'') avoid_trms |
|
454 end |
|
455 |
|
456 val avoid_trms = map2 read_avoids avoids_ordered intrs |
|
457 in |
|
458 prove_strong_inductive names rule_names avoid_trms raw_induct intrs ctxt |
|
459 end |
|
460 *} |
|
461 |
|
462 ML {* |
|
463 (* outer syntax *) |
|
464 local |
|
465 structure P = Parse; |
|
466 structure S = Scan |
|
467 |
|
468 val _ = Keyword.keyword "avoids" |
|
469 |
|
470 val single_avoid_parser = |
|
471 P.name -- (P.$$$ ":" |-- P.and_list1 P.term) |
|
472 |
|
473 val avoids_parser = |
|
474 S.optional (P.$$$ "avoids" |-- P.enum1 "|" single_avoid_parser) [] |
|
475 |
|
476 val main_parser = P.xname -- avoids_parser |
|
477 in |
|
478 val _ = |
|
479 Outer_Syntax.local_theory_to_proof "nominal_inductive" |
|
480 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
|
481 Keyword.thy_goal (main_parser >> prove_strong_inductive_cmd) |
|
482 end |
|
483 *} |
|
484 |
|
485 inductive |
|
486 Acc :: "('a::pt \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
|
487 where |
|
488 AccI: "(\<And>y. R y x \<Longrightarrow> Acc R y) \<Longrightarrow> Acc R x" |
|
489 |
|
490 (* |
|
491 equivariance Acc |
|
492 *) |
|
493 |
|
494 lemma Acc_eqvt [eqvt]: |
|
495 fixes p::"perm" |
|
496 assumes a: "Acc R x" |
|
497 shows "Acc (p \<bullet> R) (p \<bullet> x)" |
|
498 using a |
|
499 apply(induct) |
|
500 apply(rule AccI) |
|
501 apply(rotate_tac 1) |
|
502 apply(drule_tac x="-p \<bullet> y" in meta_spec) |
|
503 apply(simp) |
|
504 apply(drule meta_mp) |
|
505 apply(rule_tac p="p" in permute_boolE) |
|
506 apply(perm_simp add: permute_minus_cancel) |
|
507 apply(assumption) |
|
508 apply(assumption) |
|
509 done |
|
510 |
|
511 |
|
512 nominal_inductive Acc . |
|
513 |
|
514 thm Acc.strong_induct |
|
515 |
23 |
516 section {* Typing *} |
24 section {* Typing *} |
517 |
25 |
518 nominal_datatype ty = |
26 nominal_datatype ty = |
519 TVar string |
27 TVar string |