16 (* @end *) |
16 (* @end *) |
17 |
17 |
18 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = |
18 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = |
19 struct |
19 struct |
20 |
20 |
21 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
21 (* @chunk make_definitions *) |
22 |
22 fun make_defs ((binding, syn), trm) lthy = |
23 (* @chunk definitions_aux *) |
|
24 fun definitions_aux ((binding, syn), trm) lthy = |
|
25 let |
23 let |
26 val ((_, (_, thm)), lthy) = |
24 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
27 LocalTheory.define Thm.internalK ((binding, syn), (Attrib.empty_binding, trm)) lthy |
25 val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy |
28 in |
26 in |
29 (thm, lthy) |
27 (thm, lthy) |
30 end |
28 end |
31 (* @end *) |
29 (* @end *) |
32 |
30 |
|
31 (* @chunk definitions_aux *) |
|
32 fun defs_aux lthy orules preds params (pred, arg_types) = |
|
33 let |
|
34 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
|
35 |
|
36 val fresh_args = |
|
37 arg_types |
|
38 |> map (pair "z") |
|
39 |> Variable.variant_frees lthy orules |
|
40 |> map Free |
|
41 in |
|
42 list_comb (pred, fresh_args) |
|
43 |> fold_rev (curry HOLogic.mk_imp) orules |
|
44 |> fold_rev mk_all preds |
|
45 |> fold_rev lambda (params @ fresh_args) |
|
46 end |
|
47 (* @end *) |
|
48 |
33 (* @chunk definitions *) |
49 (* @chunk definitions *) |
34 fun definitions params rules preds preds' Tss lthy = |
50 fun definitions rules params preds prednames syns arg_typess lthy = |
35 let |
51 let |
36 val thy = ProofContext.theory_of lthy |
52 val thy = ProofContext.theory_of lthy |
37 val rules' = map (ObjectLogic.atomize_term thy) rules |
53 val orules = map (ObjectLogic.atomize_term thy) rules |
38 in |
54 val defs = |
39 fold_map (fn ((((R, _), syn), pred), Ts) => |
55 map (defs_aux lthy orules preds params) (preds ~~ arg_typess) |
40 let |
56 in |
41 val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts)) |
57 fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
42 |
|
43 val t0 = list_comb (pred, zs); |
|
44 val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0; |
|
45 val t2 = fold_rev mk_all preds' t1; |
|
46 val t3 = fold_rev lambda (params @ zs) t2; |
|
47 in |
|
48 definitions_aux ((R, syn), t3) |
|
49 end) (preds ~~ preds' ~~ Tss) lthy |
|
50 end |
58 end |
51 (* @end *) |
59 (* @end *) |
52 |
60 |
53 fun inst_spec ct = |
61 fun inst_spec ct = |
54 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}; |
55 |
63 |
|
64 (* @chunk induction_tac *) |
|
65 fun induction_tac defs prems insts = |
|
66 EVERY1 [ObjectLogic.full_atomize_tac, |
|
67 cut_facts_tac prems, |
|
68 K (rewrite_goals_tac defs), |
|
69 EVERY' (map (dtac o inst_spec) insts), |
|
70 assume_tac] |
|
71 (* @end *) |
|
72 |
|
73 (* @chunk induction_rules *) |
|
74 fun inductions rules defs parnames preds Tss lthy1 = |
|
75 let |
|
76 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
|
77 |
|
78 val Ps = replicate (length preds) "P" |
|
79 val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2 |
|
80 |
|
81 val thy = ProofContext.theory_of lthy3 |
|
82 |
|
83 val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss |
|
84 val newpreds = map Free (newprednames ~~ Tss') |
|
85 val cnewpreds = map (cterm_of thy) newpreds |
|
86 val rules' = map (subst_free (preds ~~ newpreds)) rules |
|
87 |
|
88 fun prove_induction ((pred, newpred), Ts) = |
|
89 let |
|
90 val (newargnames, lthy4) = |
|
91 Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
|
92 val newargs = map Free (newargnames ~~ Ts) |
|
93 |
|
94 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
|
95 val goal = Logic.list_implies |
|
96 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
|
97 in |
|
98 Goal.prove lthy4 [] [prem] goal |
|
99 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
|
100 |> singleton (ProofContext.export lthy4 lthy1) |
|
101 end |
|
102 in |
|
103 map prove_induction (preds ~~ newpreds ~~ Tss) |
|
104 end |
|
105 (* @end *) |
|
106 |
56 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
107 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
57 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}); |
58 |
109 |
59 |
110 |
60 (* @chunk induction_rules *) |
111 (* @chunk subproof1 *) |
61 fun INDUCTION rules preds' Tss defs lthy1 lthy2 = |
112 fun subproof2 prem params2 prems2 = |
62 let |
113 SUBPROOF (fn {prems, ...} => |
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); |
|
65 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
|
66 val rules'' = map (subst_free (preds' ~~ Ps)) rules; |
|
67 |
|
68 fun prove_indrule ((R, P), Ts) = |
|
69 let |
114 let |
70 val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
115 val prem' = prems MRS prem; |
71 val zs = map Free (znames ~~ Ts) |
116 val prem'' = |
72 |
117 case prop_of prem' of |
73 val prem = HOLogic.mk_Trueprop (list_comb (R, zs)) |
118 _ $ (Const (@{const_name All}, _) $ _) => |
74 val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs))) |
119 prem' |> all_elims params2 |
|
120 |> imp_elims prems2 |
|
121 | _ => prem'; |
|
122 in |
|
123 rtac prem'' 1 |
|
124 end) |
|
125 (* @end *) |
|
126 |
|
127 (* @chunk subproof2 *) |
|
128 fun subproof1 rules preds i = |
|
129 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
|
130 let |
|
131 val (prems1, prems2) = chop (length prems - length rules) prems; |
|
132 val (params1, params2) = chop (length params - length preds) params; |
75 in |
133 in |
76 Goal.prove lthy4 [] [prem] goal |
134 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
77 (fn {prems, ...} => EVERY1 |
135 THEN |
78 ([ObjectLogic.full_atomize_tac, |
136 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
79 cut_facts_tac prems, |
137 end) |
80 K (rewrite_goals_tac defs)] @ |
|
81 map (fn ct => dtac (inst_spec ct)) cPs @ |
|
82 [assume_tac])) |> |
|
83 singleton (ProofContext.export lthy4 lthy1) |
|
84 end; |
|
85 in |
|
86 map prove_indrule (preds' ~~ Ps ~~ Tss) |
|
87 end |
|
88 (* @end *) |
138 (* @end *) |
89 |
139 |
90 (* @chunk intro_rules *) |
140 (* @chunk intro_rules *) |
91 fun INTROS rules preds' defs lthy1 lthy2 = |
141 fun INTROS rules parnames preds defs lthy1 = |
92 let |
142 let |
93 fun prove_intro (i, r) = |
143 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
94 Goal.prove lthy2 [] [] r |
144 |
95 (fn {prems, context = ctxt} => EVERY |
145 fun prove_intro (i, goal) = |
96 [ObjectLogic.rulify_tac 1, |
146 Goal.prove lthy2 [] [] goal |
97 rewrite_goals_tac defs, |
147 (fn {context = ctxt, ...} => |
98 REPEAT (resolve_tac [@{thm allI},@{thm impI}] 1), |
148 EVERY1 |
99 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
149 [ObjectLogic.rulify_tac, |
100 let |
150 K (rewrite_goals_tac defs), |
101 val (prems1, prems2) = chop (length prems - length rules) prems; |
151 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
102 val (params1, params2) = chop (length params - length preds') params; |
152 subproof1 rules preds i ctxt]) |
103 in |
153 |> singleton (ProofContext.export lthy2 lthy1) |
104 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
|
105 THEN |
|
106 EVERY1 (map (fn prem => |
|
107 SUBPROOF (fn {prems = prems', concl, ...} => |
|
108 let |
|
109 |
|
110 val prem' = prems' MRS prem; |
|
111 val prem'' = case prop_of prem' of |
|
112 _ $ (Const (@{const_name All}, _) $ _) => |
|
113 prem' |> all_elims params2 |
|
114 |> imp_elims prems2 |
|
115 | _ => prem'; |
|
116 in rtac prem'' 1 end) ctxt') prems1) |
|
117 end) ctxt 1]) |> |
|
118 singleton (ProofContext.export lthy2 lthy1) |
|
119 in |
154 in |
120 map_index prove_intro rules |
155 map_index prove_intro rules |
121 end |
156 end |
|
157 |
122 (* @end *) |
158 (* @end *) |
123 |
159 |
124 (* @chunk add_inductive_i *) |
160 (* @chunk add_inductive_i *) |
125 fun add_inductive_i preds params specs lthy = |
161 fun add_inductive_i preds params specs lthy = |
126 let |
162 let |
127 val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params; |
163 val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params; |
128 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds; |
164 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds; |
129 val Tss = map (binder_types o fastype_of) preds'; |
165 val Tss = map (binder_types o fastype_of) preds'; |
130 val (ass,rules) = split_list specs; |
166 val (ass,rules) = split_list specs; |
131 |
167 |
132 val (defs, lthy1) = definitions params' rules preds preds' Tss lthy |
168 val prednames = map (fst o fst) preds |
133 val (_, lthy2) = Variable.add_fixes (map (Binding.name_of o fst) params) lthy1; |
169 val syns = map snd preds |
|
170 val parnames = map (Binding.name_of o fst) params |
|
171 |
|
172 val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy; |
134 |
173 |
135 val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 |
174 val inducts = inductions rules defs parnames preds' Tss lthy1 |
136 |
175 |
137 val intros = INTROS rules preds' defs lthy1 lthy2 |
176 val intros = INTROS rules parnames preds' defs lthy1 |
138 |
177 |
139 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); |
178 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); |
140 val case_names = map (Binding.name_of o fst o fst) specs |
179 val case_names = map (Binding.name_of o fst o fst) specs |
141 in |
180 in |
142 lthy1 |
181 lthy1 |