48 |
48 |
49 (* @chunk definitions *) |
49 (* @chunk definitions *) |
50 fun definitions rules params preds prednames syns arg_typess lthy = |
50 fun definitions rules params preds prednames syns arg_typess lthy = |
51 let |
51 let |
52 val thy = ProofContext.theory_of lthy |
52 val thy = ProofContext.theory_of lthy |
53 val orules = map (ObjectLogic.atomize_term thy) rules |
53 val orules = map (Object_Logic.atomize_term thy) rules |
54 val defs = |
54 val defs = |
55 map (defs_aux lthy orules preds params) (preds ~~ arg_typess) |
55 map (defs_aux lthy orules preds params) (preds ~~ arg_typess) |
56 in |
56 in |
57 fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
57 fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
58 end |
58 end |
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 defs prems insts = |
66 EVERY1 [ObjectLogic.full_atomize_tac, |
66 EVERY1 [Object_Logic.full_atomize_tac, |
67 cut_facts_tac prems, |
67 cut_facts_tac prems, |
68 rewrite_goal_tac defs, |
68 rewrite_goal_tac 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 *) |
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 (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
134 rtac (Object_Logic.rulify (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 [ObjectLogic.rulify_tac, |
141 EVERY1 [Object_Logic.rulify_tac, |
142 rewrite_goal_tac defs, |
142 rewrite_goal_tac 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 |