|
1 (* @chunk SIMPLE_INDUCTIVE_PACKAGE *) |
|
2 signature SIMPLE_INDUCTIVE_PACKAGE = |
|
3 sig |
|
4 val add_inductive_i: |
|
5 ((Name.binding * typ) * mixfix) list -> (*{predicates}*) |
|
6 (Name.binding * typ) list -> (*{parameters}*) |
|
7 (Attrib.binding * term) list -> (*{rules}*) |
|
8 local_theory -> (thm list * thm list) * local_theory |
|
9 val add_inductive: |
|
10 (Name.binding * string option * mixfix) list -> (*{predicates}*) |
|
11 (Name.binding * string option * mixfix) list -> (*{parameters}*) |
|
12 (Attrib.binding * string) list -> (*{rules}*) |
|
13 local_theory -> (thm list * thm list) * local_theory |
|
14 end; |
|
15 (* @end *) |
|
16 |
|
17 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = |
|
18 struct |
|
19 |
|
20 fun add_inductive_i preds_syn params intrs lthy = |
|
21 let |
|
22 val params' = map (fn (p, T) => Free (Name.name_of p, T)) params; |
|
23 val preds = map (fn ((R, T), _) => |
|
24 list_comb (Free (Name.name_of R, T), params')) preds_syn; |
|
25 val Tss = map (binder_types o fastype_of) preds; |
|
26 |
|
27 (* making the definition *) |
|
28 |
|
29 val intrs' = map |
|
30 (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs; |
|
31 |
|
32 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P; |
|
33 |
|
34 val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) => |
|
35 let val zs = map Free (Variable.variant_frees lthy intrs' |
|
36 (map (pair "z") Ts)) |
|
37 in |
|
38 LocalTheory.define Thm.internalK |
|
39 ((R, syn), (Attrib.no_binding, fold_rev lambda (params' @ zs) |
|
40 (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp) |
|
41 intrs' (list_comb (pred, zs)))))) #>> snd #>> snd |
|
42 end) (preds_syn ~~ preds ~~ Tss) lthy; |
|
43 |
|
44 val (_, lthy2) = Variable.add_fixes (map (Name.name_of o fst) params) lthy1; |
|
45 |
|
46 |
|
47 (* proving the induction rules *) |
|
48 |
|
49 val (Pnames, lthy3) = |
|
50 Variable.variant_fixes (replicate (length preds) "P") lthy2; |
|
51 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) |
|
52 (Pnames ~~ Tss); |
|
53 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
|
54 val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs; |
|
55 |
|
56 fun inst_spec ct = Drule.instantiate' |
|
57 [SOME (ctyp_of_term ct)] [NONE, SOME ct] spec; |
|
58 |
|
59 fun prove_indrule ((R, P), Ts) = |
|
60 let |
|
61 val (znames, lthy4) = |
|
62 Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
|
63 val zs = map Free (znames ~~ Ts) |
|
64 in |
|
65 Goal.prove lthy4 [] |
|
66 [HOLogic.mk_Trueprop (list_comb (R, zs))] |
|
67 (Logic.list_implies (intrs'', |
|
68 HOLogic.mk_Trueprop (list_comb (P, zs)))) |
|
69 (fn {prems, ...} => EVERY |
|
70 ([ObjectLogic.full_atomize_tac 1, |
|
71 cut_facts_tac prems 1, |
|
72 rewrite_goals_tac defs] @ |
|
73 map (fn ct => dtac (inst_spec ct) 1) cPs @ |
|
74 [assume_tac 1])) |> |
|
75 singleton (ProofContext.export lthy4 lthy1) |
|
76 end; |
|
77 |
|
78 val indrules = map prove_indrule (preds ~~ Ps ~~ Tss); |
|
79 |
|
80 |
|
81 (* proving the introduction rules *) |
|
82 |
|
83 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
|
84 val imp_elims = fold (fn th => fn th' => [th', th] MRS mp); |
|
85 |
|
86 fun prove_intr (i, (_, r)) = |
|
87 Goal.prove lthy2 [] [] r |
|
88 (fn {prems, context = ctxt} => EVERY |
|
89 [ObjectLogic.rulify_tac 1, |
|
90 rewrite_goals_tac defs, |
|
91 REPEAT (resolve_tac [allI, impI] 1), |
|
92 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
|
93 let |
|
94 val (prems1, prems2) = |
|
95 chop (length prems - length intrs) prems; |
|
96 val (params1, params2) = |
|
97 chop (length params - length preds) params |
|
98 in |
|
99 rtac (ObjectLogic.rulify |
|
100 (all_elims params1 (nth prems2 i))) 1 THEN |
|
101 EVERY (map (fn prem => |
|
102 SUBPROOF (fn {prems = prems', concl, ...} => |
|
103 let |
|
104 val prem' = prems' MRS prem; |
|
105 val prem'' = case prop_of prem' of |
|
106 _ $ (Const (@{const_name All}, _) $ _) => |
|
107 prem' |> all_elims params2 |> |
|
108 imp_elims prems2 |
|
109 | _ => prem' |
|
110 in rtac prem'' 1 end) ctxt' 1) prems1) |
|
111 end) ctxt 1]) |> |
|
112 singleton (ProofContext.export lthy2 lthy1); |
|
113 |
|
114 val intr_ths = map_index prove_intr intrs; |
|
115 |
|
116 |
|
117 (* storing the theorems *) |
|
118 |
|
119 val mut_name = space_implode "_" (map (Name.name_of o fst o fst) preds_syn); |
|
120 val case_names = map (Name.name_of o fst o fst) intrs |
|
121 in |
|
122 lthy1 |> |
|
123 LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
|
124 ((Name.qualified mut_name a, atts), [([th], [])])) |
|
125 (intrs ~~ intr_ths)) |-> |
|
126 (fn intr_thss => LocalTheory.note Thm.theoremK |
|
127 ((Name.qualified mut_name (Name.binding "intros"), []), maps snd intr_thss)) |>> |
|
128 snd ||>> |
|
129 (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
|
130 ((Name.qualified (Name.name_of R) (Name.binding "induct"), |
|
131 [Attrib.internal (K (RuleCases.case_names case_names)), |
|
132 Attrib.internal (K (RuleCases.consumes 1)), |
|
133 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
|
134 (preds_syn ~~ indrules)) #>> maps snd) |
|
135 end; |
|
136 |
|
137 (* @chunk add_inductive *) |
|
138 fun add_inductive preds_syn params_syn intro_srcs lthy = |
|
139 let |
|
140 val ((vars, specs), _) = Specification.read_specification |
|
141 (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs) |
|
142 lthy; |
|
143 val (preds_syn', params_syn') = chop (length preds_syn) vars; |
|
144 val intrs = map (apsnd the_single) specs |
|
145 in |
|
146 add_inductive_i preds_syn' (map fst params_syn') intrs lthy |
|
147 end; |
|
148 (* @end *) |
|
149 |
|
150 |
|
151 (* outer syntax *) |
|
152 |
|
153 (* @chunk syntax *) |
|
154 local structure P = OuterParse and K = OuterKeyword in |
|
155 |
|
156 val ind_decl = |
|
157 P.opt_target -- |
|
158 P.fixes -- P.for_fixes -- |
|
159 Scan.optional (P.$$$ "where" |-- |
|
160 P.!!! (P.enum1 "|" (SpecParse.opt_thm_name ":" -- P.prop))) [] >> |
|
161 (fn (((loc, preds), params), specs) => |
|
162 Toplevel.local_theory loc (add_inductive preds params specs #> snd)); |
|
163 |
|
164 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
|
165 K.thy_decl ind_decl; |
|
166 |
|
167 end; |
|
168 (* @end *) |
|
169 |
|
170 end; |