equal
deleted
inserted
replaced
54 in |
54 in |
55 filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths |
55 filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths |
56 end |
56 end |
57 *} |
57 *} |
58 |
58 |
59 (* An induction for a single relation is "R x y \<Longrightarrow> P x y" |
|
60 but for multiple relations is "(R1 x y \<longrightarrow> P x y) \<and> (R2 a b \<longrightarrow> P2 a b)" *) |
|
61 ML {* |
|
62 fun rel_indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct |
|
63 *} |
|
64 |
|
65 ML {* |
59 ML {* |
66 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt = |
60 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt = |
67 let |
61 let |
68 val tys = map (domain_type o fastype_of) alphas; |
62 val tys = map (domain_type o fastype_of) alphas; |
69 val names = Datatype_Prop.make_tnames tys; |
63 val names = Datatype_Prop.make_tnames tys; |
78 val trm_gls = map mk_conjl trm_gl_lists; |
72 val trm_gls = map mk_conjl trm_gl_lists; |
79 val pgls = map |
73 val pgls = map |
80 (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) |
74 (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) |
81 ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr)) |
75 ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr)) |
82 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls); |
76 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls); |
83 fun tac {context,...} = (rel_indtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
77 fun tac {context,...} = (rtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
84 TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1 |
78 TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1 |
85 val th_loc = Goal.prove ctxt'' [] [] gl tac |
79 val th_loc = Goal.prove ctxt'' [] [] gl tac |
86 val ths_loc = HOLogic.conj_elims th_loc |
80 val ths_loc = HOLogic.conj_elims th_loc |
87 val ths = Variable.export ctxt'' ctxt ths_loc |
81 val ths = Variable.export ctxt'' ctxt ths_loc |
88 in |
82 in |