47 (* @end *) |
47 (* @end *) |
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 = Proof_Context.theory_of lthy |
52 val orules = map (Object_Logic.atomize_term lthy) rules |
53 val orules = map (Object_Logic.atomize_term thy) rules |
|
54 val defs = |
53 val defs = |
55 map (defs_aux lthy orules preds params) (preds ~~ arg_typess) |
54 map (defs_aux lthy orules preds params) (preds ~~ arg_typess) |
56 in |
55 in |
57 fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
56 fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
58 end |
57 end |
59 (* @end *) |
58 (* @end *) |
60 |
59 |
61 fun inst_spec ct = |
60 fun inst_spec ct = |
62 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
61 Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}; |
|
62 |
|
63 fun dtac ctxt thm = dresolve_tac ctxt [thm] |
|
64 fun rtac ctxt thm = resolve_tac ctxt [thm] |
63 |
65 |
64 (* @chunk induction_tac *) |
66 (* @chunk induction_tac *) |
65 fun induction_tac ctxt defs prems insts = |
67 fun induction_tac ctxt defs prems insts = |
66 EVERY1 [Object_Logic.full_atomize_tac ctxt, |
68 EVERY1 [Object_Logic.full_atomize_tac ctxt, |
67 cut_facts_tac prems, |
69 cut_facts_tac prems, |
68 rewrite_goal_tac ctxt defs, |
70 rewrite_goal_tac ctxt defs, |
69 EVERY' (map (dtac o inst_spec) insts), |
71 EVERY' (map (dtac ctxt o inst_spec) insts), |
70 assume_tac] |
72 assume_tac ctxt] |
71 (* @end *) |
73 (* @end *) |
72 |
74 |
73 (* @chunk induction_rules *) |
75 (* @chunk induction_rules *) |
74 fun inductions rules defs parnames preds Tss lthy1 = |
76 fun inductions rules defs parnames preds Tss lthy1 = |
75 let |
77 let |
76 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
78 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
77 |
79 |
78 val Ps = replicate (length preds) "P" |
80 val Ps = replicate (length preds) "P" |
79 val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2 |
81 val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2 |
80 |
82 |
81 val thy = Proof_Context.theory_of lthy3 |
|
82 |
|
83 val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss |
83 val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss |
84 val newpreds = map Free (newprednames ~~ Tss') |
84 val newpreds = map Free (newprednames ~~ Tss') |
85 val cnewpreds = map (cterm_of thy) newpreds |
85 val cnewpreds = map (Thm.cterm_of lthy3) newpreds |
86 val rules' = map (subst_free (preds ~~ newpreds)) rules |
86 val rules' = map (subst_free (preds ~~ newpreds)) rules |
87 |
87 |
88 fun prove_induction ((pred, newpred), Ts) = |
88 fun prove_induction ((pred, newpred), Ts) = |
89 let |
89 let |
90 val (newargnames, lthy4) = |
90 val (newargnames, lthy4) = |
108 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); |
108 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); |
109 |
109 |
110 |
110 |
111 (* @chunk subproof1 *) |
111 (* @chunk subproof1 *) |
112 fun subproof2 prem params2 prems2 = |
112 fun subproof2 prem params2 prems2 = |
113 SUBPROOF (fn {prems, ...} => |
113 SUBPROOF (fn {prems, context, ...} => |
114 let |
114 let |
115 val prem' = prems MRS prem; |
115 val prem' = prems MRS prem; |
116 val prem'' = |
116 val prem'' = |
117 case prop_of prem' of |
117 case Thm.prop_of prem' of |
118 _ $ (Const (@{const_name All}, _) $ _) => |
118 _ $ (Const (@{const_name All}, _) $ _) => |
119 prem' |> all_elims params2 |
119 prem' |> all_elims params2 |
120 |> imp_elims prems2 |
120 |> imp_elims prems2 |
121 | _ => prem'; |
121 | _ => prem'; |
122 in |
122 in |
123 rtac prem'' 1 |
123 rtac context prem'' 1 |
124 end) |
124 end) |
125 (* @end *) |
125 (* @end *) |
126 |
126 |
127 (* @chunk subproof2 *) |
127 (* @chunk subproof2 *) |
128 fun subproof1 rules preds i = |
128 fun subproof1 rules preds i = |
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 ctxt' (all_elims params1 (nth prems2 i))) 1 |
134 rtac ctxt' (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 ctxt, |
141 EVERY1 [Object_Logic.rulify_tac ctxt, |
142 rewrite_goal_tac ctxt defs, |
142 rewrite_goal_tac ctxt defs, |
143 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
143 REPEAT o (resolve_tac ctxt [@{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 *) |
148 fun introductions rules parnames preds defs lthy1 = |
148 fun introductions rules parnames preds defs lthy1 = |
192 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
192 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
193 (preds ~~ inducts)) #>> maps snd) |
193 (preds ~~ inducts)) #>> maps snd) |
194 |> snd |
194 |> snd |
195 end |
195 end |
196 (* @end *) |
196 (* @end *) |
197 |
197 val _ = Proof_Context.read_stmt |
198 (* @chunk read_specification *) |
198 (* @chunk read_specification *) |
199 fun read_specification' vars specs lthy = |
199 fun read_specification' vars specs lthy = |
200 let |
200 let |
201 val specs' = map (fn (a, s) => (a, [s])) specs |
201 val specs' = map (fn (a, s) => ((a, s), [],[])) specs |
202 val ((varst, specst), _) = |
202 val ((varst, specst),_) = |
203 Specification.read_specification vars specs' lthy |
203 Specification.read_multi_specs vars specs' lthy |
204 val specst' = map (apsnd the_single) specst |
|
205 in |
204 in |
206 (varst, specst') |
205 (varst, specst) |
207 end |
206 end |
208 (* @end *) |
207 (* @end *) |
209 |
208 |
210 (* @chunk add_inductive *) |
209 (* @chunk add_inductive *) |
211 fun add_inductive preds params specs lthy = |
210 fun add_inductive preds params specs lthy = |