equal
deleted
inserted
replaced
12 |
12 |
13 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
13 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
14 term list -> typ list -> thm list |
14 term list -> typ list -> thm list |
15 |
15 |
16 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
16 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
17 thm list -> (thm list * thm list) |
17 thm list -> thm list |
18 |
18 |
19 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
19 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
20 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
20 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
21 |
21 |
22 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
22 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
313 |
313 |
314 |
314 |
315 |
315 |
316 (** produces the alpha_eq_iff simplification rules **) |
316 (** produces the alpha_eq_iff simplification rules **) |
317 |
317 |
318 (* in case a theorem is of the form (C.. = C..), it will be |
318 (* in case a theorem is of the form (Rel Const Const), it will be |
319 rewritten to ((C.. = C..) = True) *) |
319 rewritten to ((Rel Const = Const) = True) |
|
320 *) |
320 fun mk_simp_rule thm = |
321 fun mk_simp_rule thm = |
321 case (prop_of thm) of |
322 case (prop_of thm) of |
322 @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm] |
323 @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} |
323 | _ => thm |
324 | _ => thm |
324 |
325 |
325 fun alpha_eq_iff_tac dist_inj intros elims = |
326 fun alpha_eq_iff_tac dist_inj intros elims = |
326 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE' |
327 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE' |
327 (rtac @{thm iffI} THEN' |
328 (rtac @{thm iffI} THEN' |
345 val goals = map mk_alpha_eq_iff_goal thms_imp; |
346 val goals = map mk_alpha_eq_iff_goal thms_imp; |
346 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
347 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
347 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
348 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
348 in |
349 in |
349 Variable.export ctxt' ctxt thms |
350 Variable.export ctxt' ctxt thms |
350 |> `(map mk_simp_rule) |
351 |> map mk_simp_rule |
351 end |
352 end |
352 |
353 |
353 |
354 |
354 (** proof by induction over the alpha-definitions **) |
355 (** proof by induction over the alpha-definitions **) |
355 |
356 |