58 |
58 |
59 |
59 |
60 (* @chunk induction_rules *) |
60 (* @chunk induction_rules *) |
61 fun INDUCTION rules preds' Tss defs lthy1 lthy2 = |
61 fun INDUCTION rules preds' Tss defs lthy1 lthy2 = |
62 let |
62 let |
63 val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2; |
63 val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2; |
64 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss); |
64 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss); |
65 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
65 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
66 val rules'' = map (subst_free (preds' ~~ Ps)) rules; |
66 val rules'' = map (subst_free (preds' ~~ Ps)) rules; |
67 |
67 |
68 fun prove_indrule ((R, P), Ts) = |
68 fun prove_indrule ((R, P), Ts) = |
69 let |
69 let |
70 val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
70 val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
71 val zs = map Free (znames ~~ Ts) |
71 val zs = map Free (znames ~~ Ts) |
72 |
72 |
73 val prem = HOLogic.mk_Trueprop (list_comb (R, zs)) |
73 val prem = HOLogic.mk_Trueprop (list_comb (R, zs)) |
74 val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs))) |
74 val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs))) |
75 in |
75 in |
76 Goal.prove lthy4 [] [prem] goal |
76 Goal.prove lthy4 [] [prem] goal |
77 (fn {prems, ...} => EVERY1 |
77 (fn {prems, ...} => EVERY1 |
78 ([ObjectLogic.full_atomize_tac, |
78 ([ObjectLogic.full_atomize_tac, |
79 cut_facts_tac prems, |
79 cut_facts_tac prems, |
80 K (rewrite_goals_tac defs)] @ |
80 K (rewrite_goals_tac defs)] @ |
81 map (fn ct => dtac (inst_spec ct)) cPs @ |
81 map (fn ct => dtac (inst_spec ct)) cPs @ |
82 [assume_tac])) |> |
82 [assume_tac])) |> |
83 singleton (ProofContext.export lthy4 lthy1) |
83 singleton (ProofContext.export lthy4 lthy1) |
84 end; |
84 end; |
85 in |
85 in |
86 map prove_indrule (preds' ~~ Ps ~~ Tss) |
86 map prove_indrule (preds' ~~ Ps ~~ Tss) |
87 end |
87 end |
88 (* @end *) |
88 (* @end *) |
89 |
89 |
90 (* @chunk intro_rules *) |
90 (* @chunk intro_rules *) |
91 fun INTROS rules preds' defs lthy1 lthy2 = |
91 fun INTROS rules preds' defs lthy1 lthy2 = |
92 let |
92 let |
121 end |
121 end |
122 (* @end *) |
122 (* @end *) |
123 |
123 |
124 (* @chunk add_inductive_i *) |
124 (* @chunk add_inductive_i *) |
125 fun add_inductive_i preds params specs lthy = |
125 fun add_inductive_i preds params specs lthy = |
126 let |
126 let |
127 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
127 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
128 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds; |
128 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds; |
129 val Tss = map (binder_types o fastype_of) preds'; |
129 val Tss = map (binder_types o fastype_of) preds'; |
130 val (ass,rules) = split_list specs; |
130 val (ass,rules) = split_list specs; |
131 |
131 |
132 val (defs, lthy1) = definitions params' rules preds preds' Tss lthy |
132 val (defs, lthy1) = definitions params' rules preds preds' Tss lthy |
133 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
133 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
134 |
134 |
135 val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 |
135 val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 |
136 |
136 |
137 val intros = INTROS rules preds' defs lthy1 lthy2 |
137 val intros = INTROS rules preds' defs lthy1 lthy2 |
138 |
138 |
139 val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds); |
139 val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds); |
140 val case_names = map (Binding.base_name o fst o fst) specs |
140 val case_names = map (Binding.base_name o fst o fst) specs |
141 in |
141 in |
142 lthy1 |
142 lthy1 |
143 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
143 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
144 ((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros)) |
144 ((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros)) |
145 |-> (fn intross => LocalTheory.note Thm.theoremK |
145 |-> (fn intross => LocalTheory.note Thm.theoremK |
146 ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intross)) |
146 ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intross)) |
150 [Attrib.internal (K (RuleCases.case_names case_names)), |
150 [Attrib.internal (K (RuleCases.case_names case_names)), |
151 Attrib.internal (K (RuleCases.consumes 1)), |
151 Attrib.internal (K (RuleCases.consumes 1)), |
152 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
152 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
153 (preds ~~ inducts)) #>> maps snd) |
153 (preds ~~ inducts)) #>> maps snd) |
154 |> snd |
154 |> snd |
155 end |
155 end |
156 (* @end *) |
156 (* @end *) |
157 |
157 |
158 (* @chunk read_specification *) |
158 (* @chunk read_specification *) |
159 fun read_specification' vars specs lthy = |
159 fun read_specification' vars specs lthy = |
160 let |
160 let |