60 |
60 |
61 fun inst_spec ct = |
61 fun inst_spec ct = |
62 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
62 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
63 |
63 |
64 (* @chunk induction_tac *) |
64 (* @chunk induction_tac *) |
65 fun induction_tac defs prems insts = |
65 fun induction_tac ctxt defs prems insts = |
66 EVERY1 [Object_Logic.full_atomize_tac, |
66 EVERY1 [Object_Logic.full_atomize_tac ctxt, |
67 cut_facts_tac prems, |
67 cut_facts_tac prems, |
68 rewrite_goal_tac defs, |
68 rewrite_goal_tac ctxt defs, |
69 EVERY' (map (dtac o inst_spec) insts), |
69 EVERY' (map (dtac o inst_spec) insts), |
70 assume_tac] |
70 assume_tac] |
71 (* @end *) |
71 (* @end *) |
72 |
72 |
73 (* @chunk induction_rules *) |
73 (* @chunk induction_rules *) |
94 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
94 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
95 val goal = Logic.list_implies |
95 val goal = Logic.list_implies |
96 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
96 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
97 in |
97 in |
98 Goal.prove lthy4 [] [prem] goal |
98 Goal.prove lthy4 [] [prem] goal |
99 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
99 (fn {prems, context, ...} => induction_tac context defs prems cnewpreds) |
100 |> singleton (Proof_Context.export lthy4 lthy1) |
100 |> singleton (Proof_Context.export lthy4 lthy1) |
101 end |
101 end |
102 in |
102 in |
103 map prove_induction (preds ~~ newpreds ~~ Tss) |
103 map prove_induction (preds ~~ newpreds ~~ Tss) |
104 end |
104 end |
129 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
129 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
130 let |
130 let |
131 val (prems1, prems2) = chop (length prems - length rules) prems; |
131 val (prems1, prems2) = chop (length prems - length rules) prems; |
132 val (params1, params2) = chop (length params - length preds) (map snd params); |
132 val (params1, params2) = chop (length params - length preds) (map snd params); |
133 in |
133 in |
134 rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 |
134 rtac (Object_Logic.rulify ctxt' (all_elims params1 (nth prems2 i))) 1 |
135 THEN |
135 THEN |
136 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
136 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
137 end) |
137 end) |
138 (* @end *) |
138 (* @end *) |
139 |
139 |
140 fun introductions_tac defs rules preds i ctxt = |
140 fun introductions_tac defs rules preds i ctxt = |
141 EVERY1 [Object_Logic.rulify_tac, |
141 EVERY1 [Object_Logic.rulify_tac ctxt, |
142 rewrite_goal_tac defs, |
142 rewrite_goal_tac ctxt defs, |
143 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
143 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
144 subproof1 rules preds i ctxt] |
144 subproof1 rules preds i ctxt] |
145 |
145 |
146 |
146 |
147 (* @chunk intro_rules *) |
147 (* @chunk intro_rules *) |