32
|
1 |
(* @chunk SIMPLE_INDUCTIVE_PACKAGE *)
|
|
2 |
signature SIMPLE_INDUCTIVE_PACKAGE =
|
|
3 |
sig
|
|
4 |
val add_inductive_i:
|
76
|
5 |
((Binding.binding * typ) * mixfix) list -> (*{predicates}*)
|
|
6 |
(Binding.binding * typ) list -> (*{parameters}*)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
7 |
((Binding.binding * Attrib.src list) * term) list -> (*{rules}*)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
local_theory -> local_theory
|
32
|
9 |
val add_inductive:
|
76
|
10 |
(Binding.binding * string option * mixfix) list -> (*{predicates}*)
|
|
11 |
(Binding.binding * string option * mixfix) list -> (*{parameters}*)
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
12 |
(Attrib.binding * string) list -> (*{rules}*)
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
local_theory -> local_theory
|
32
|
14 |
end;
|
|
15 |
(* @end *)
|
|
16 |
|
|
17 |
structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
|
|
18 |
struct
|
|
19 |
|
111
|
20 |
fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
|
111
|
22 |
(* @chunk definitions *)
|
|
23 |
fun define_aux s ((binding, syn), (attr, trm)) lthy =
|
|
24 |
let
|
|
25 |
val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy
|
|
26 |
in
|
|
27 |
(thm, lthy)
|
|
28 |
end
|
|
29 |
|
|
30 |
fun DEFINITION params' rules preds preds' Tss lthy =
|
|
31 |
let
|
|
32 |
val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules
|
|
33 |
in
|
|
34 |
fold_map (fn ((((R, _), syn), pred), Ts) =>
|
|
35 |
let
|
|
36 |
val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts))
|
|
37 |
|
|
38 |
val t0 = list_comb (pred, zs);
|
|
39 |
val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0;
|
|
40 |
val t2 = fold_rev mk_all preds' t1;
|
|
41 |
val t3 = fold_rev lambda (params' @ zs) t2;
|
|
42 |
in
|
|
43 |
define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
|
|
44 |
end) (preds ~~ preds' ~~ Tss) lthy
|
|
45 |
end
|
|
46 |
(* @end *)
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
fun inst_spec ct =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
51 |
val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
52 |
val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp});
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
|
111
|
54 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
(* @chunk induction_rules *)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
fun INDUCTION rules preds' Tss defs lthy1 lthy2 =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
let
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss);
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
val rules'' = map (subst_free (preds' ~~ Ps)) rules;
|
32
|
62 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
fun prove_indrule ((R, P), Ts) =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
let
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
val zs = map Free (znames ~~ Ts)
|
32
|
67 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
val prem = HOLogic.mk_Trueprop (list_comb (R, zs))
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs)))
|
32
|
70 |
in
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
Goal.prove lthy4 [] [prem] goal
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
(fn {prems, ...} => EVERY1
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
([ObjectLogic.full_atomize_tac,
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
cut_facts_tac prems,
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
75 |
K (rewrite_goals_tac defs)] @
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
map (fn ct => dtac (inst_spec ct)) cPs @
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
77 |
[assume_tac])) |>
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
78 |
singleton (ProofContext.export lthy4 lthy1)
|
32
|
79 |
end;
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
80 |
in
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
81 |
map prove_indrule (preds' ~~ Ps ~~ Tss)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
82 |
end
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
83 |
(* @end *)
|
32
|
84 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
85 |
(* @chunk intro_rules *)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
86 |
fun INTROS rules preds' defs lthy1 lthy2 =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
87 |
let
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
88 |
fun prove_intro (i, r) =
|
32
|
89 |
Goal.prove lthy2 [] [] r
|
|
90 |
(fn {prems, context = ctxt} => EVERY
|
|
91 |
[ObjectLogic.rulify_tac 1,
|
|
92 |
rewrite_goals_tac defs,
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
93 |
REPEAT (resolve_tac [@{thm allI},@{thm impI}] 1),
|
32
|
94 |
SUBPROOF (fn {params, prems, context = ctxt', ...} =>
|
|
95 |
let
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
96 |
val (prems1, prems2) = chop (length prems - length rules) prems;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
97 |
val (params1, params2) = chop (length params - length preds') params;
|
32
|
98 |
in
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
99 |
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
100 |
THEN
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
EVERY1 (map (fn prem =>
|
32
|
102 |
SUBPROOF (fn {prems = prems', concl, ...} =>
|
|
103 |
let
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
|
32
|
105 |
val prem' = prems' MRS prem;
|
|
106 |
val prem'' = case prop_of prem' of
|
|
107 |
_ $ (Const (@{const_name All}, _) $ _) =>
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
108 |
prem' |> all_elims params2
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
109 |
|> imp_elims prems2
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
| _ => prem';
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
in rtac prem'' 1 end) ctxt') prems1)
|
32
|
112 |
end) ctxt 1]) |>
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
113 |
singleton (ProofContext.export lthy2 lthy1)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
114 |
in
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
115 |
map_index prove_intro rules
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
end
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
117 |
(* @end *)
|
32
|
118 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
119 |
(* @chunk add_inductive_i *)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
120 |
fun add_inductive_i preds params specs lthy =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
121 |
let
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
122 |
val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
123 |
val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
val Tss = map (binder_types o fastype_of) preds';
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
val (ass,rules) = split_list specs;
|
32
|
126 |
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
127 |
val (defs, lthy1) = DEFINITION params' rules preds preds' Tss lthy
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
129 |
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
130 |
val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
131 |
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
132 |
val intros = INTROS rules preds' defs lthy1 lthy2
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
133 |
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
134 |
val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds);
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
135 |
val case_names = map (Binding.base_name o fst o fst) specs
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
136 |
in
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
137 |
lthy1
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
138 |
|> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
139 |
((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros))
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
140 |
|-> (fn intross => LocalTheory.note Thm.theoremK
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
141 |
((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intross))
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
142 |
|>> snd
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
143 |
||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
144 |
((Binding.qualify (Binding.base_name R) (Binding.name "induct"),
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
145 |
[Attrib.internal (K (RuleCases.case_names case_names)),
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
Attrib.internal (K (RuleCases.consumes 1)),
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
148 |
(preds ~~ inducts)) #>> maps snd)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
|> snd
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
150 |
end
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
151 |
(* @end *)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
152 |
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
153 |
(* @chunk add_inductive *)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
154 |
fun read_specification' vars specs lthy =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
155 |
let
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
156 |
val specs' = map (fn (a, s) => [(a, [s])]) specs
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
157 |
val ((varst, specst), _) = Specification.read_specification vars specs' lthy
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
158 |
val specst' = map (apsnd the_single) specst
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
159 |
in
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
160 |
(varst, specst')
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
161 |
end
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
163 |
fun add_inductive preds params specs lthy =
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
164 |
let
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
165 |
val (vars, specs') = read_specification' (preds @ params) specs lthy;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
166 |
val (preds', params') = chop (length preds) vars;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
167 |
val params'' = map fst params'
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
168 |
in
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
169 |
add_inductive_i preds' params'' specs' lthy
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
170 |
end;
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
171 |
(* @end *)
|
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
172 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
173 |
(* @chunk syntax *)
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
174 |
val parser =
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
175 |
OuterParse.opt_target --
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
176 |
OuterParse.fixes --
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
177 |
OuterParse.for_fixes --
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
178 |
Scan.optional
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
179 |
(OuterParse.$$$ "where" |--
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
180 |
OuterParse.!!!
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
181 |
(OuterParse.enum1 "|"
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
182 |
(SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
|
32
|
183 |
|
|
184 |
val ind_decl =
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
185 |
parser >>
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
(fn (((loc, preds), params), specs) =>
|
110
12533bb49615
recovered old version of simple_induct; split the main function into small functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
Toplevel.local_theory loc (add_inductive preds params specs))
|
32
|
188 |
|
|
189 |
val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
190 |
OuterKeyword.thy_decl ind_decl;
|
32
|
191 |
(* @end *)
|
|
192 |
|
|
193 |
end;
|