author | blanchet |
Mon, 01 Sep 2014 16:17:46 +0200 | |
changeset 58111 | 82db9ad610b9 |
parent 56254 | a2dd9200854d |
child 58112 | 8081087096ad |
permissions | -rw-r--r-- |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/inductive_realizer.ML |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
2 |
Author: Stefan Berghofer, TU Muenchen |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
3 |
|
36043 | 4 |
Program extraction from proofs involving inductive predicates: |
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28965
diff
changeset
|
5 |
Realizers for induction and elimination rules. |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
6 |
*) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
7 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
8 |
signature INDUCTIVE_REALIZER = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
9 |
sig |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
10 |
val add_ind_realizers: string -> string list -> theory -> theory |
18708 | 11 |
val setup: theory -> theory |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
12 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
13 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
14 |
structure InductiveRealizer : INDUCTIVE_REALIZER = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
15 |
struct |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
16 |
|
22606
962f824c2df9
- Tried to make name_of_thm more robust against changes of the
berghofe
parents:
22596
diff
changeset
|
17 |
fun name_of_thm thm = |
28800 | 18 |
(case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I) |
28814 | 19 |
[Thm.proof_of thm] [] of |
28800 | 20 |
[name] => name |
55235 | 21 |
| _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm])); |
22271 | 22 |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
23 |
fun prf_of thm = |
44060 | 24 |
Reconstruct.proof_of thm |
25 |
|> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)]; (* FIXME *) |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
26 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
27 |
fun subsets [] = [[]] |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
28 |
| subsets (x::xs) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
29 |
let val ys = subsets xs |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
30 |
in ys @ map (cons x) ys end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
31 |
|
22271 | 32 |
val pred_of = fst o dest_Const o head_of; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
33 |
|
56245 | 34 |
fun strip_all' used names (Const (@{const_name Pure.all}, _) $ Abs (s, T, t)) = |
22271 | 35 |
let val (s', names') = (case names of |
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42375
diff
changeset
|
36 |
[] => (singleton (Name.variant_list used) s, []) |
22271 | 37 |
| name :: names' => (name, names')) |
38 |
in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end |
|
56245 | 39 |
| strip_all' used names ((t as Const (@{const_name Pure.imp}, _) $ P) $ Q) = |
22271 | 40 |
t $ strip_all' used names Q |
41 |
| strip_all' _ _ t = t; |
|
42 |
||
29281 | 43 |
fun strip_all t = strip_all' (Term.add_free_names t []) [] t; |
22271 | 44 |
|
56245 | 45 |
fun strip_one name |
46 |
(Const (@{const_name Pure.all}, _) $ Abs (s, T, Const (@{const_name Pure.imp}, _) $ P $ Q)) = |
|
22271 | 47 |
(subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q)) |
56245 | 48 |
| strip_one _ (Const (@{const_name Pure.imp}, _) $ P $ Q) = (P, Q); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
49 |
|
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
50 |
fun relevant_vars prop = fold (fn ((a, i), T) => fn vs => |
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
51 |
(case strip_type T of |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
52 |
(_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
53 |
| _ => vs)) (Term.add_vars prop []) []; |
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
54 |
|
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
55 |
val attach_typeS = map_types (map_atyps |
56254 | 56 |
(fn TFree (s, []) => TFree (s, @{sort type}) |
57 |
| TVar (ixn, []) => TVar (ixn, @{sort type}) |
|
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
58 |
| T => T)); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
59 |
|
22271 | 60 |
fun dt_of_intrs thy vs nparms intrs = |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
61 |
let |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
62 |
val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []); |
22271 | 63 |
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop |
64 |
(Logic.strip_imp_concl (prop_of (hd intrs)))); |
|
33957 | 65 |
val params = map dest_Var (take nparms ts); |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
66 |
val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs)); |
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
67 |
fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)), |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset
|
68 |
map (Logic.unvarifyT_global o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @ |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
69 |
filter_out (equal Extraction.nullT) (map |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset
|
70 |
(Logic.unvarifyT_global o Extraction.etype_of thy vs []) (prems_of intr)), |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
71 |
NoSyn); |
45839
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset
|
72 |
in |
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset
|
73 |
((tname, map (rpair dummyS) (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs), NoSyn), |
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset
|
74 |
map constr_of_intr intrs) |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
75 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
76 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
77 |
fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
78 |
|
22271 | 79 |
(** turn "P" into "%r x. realizes r (P x)" **) |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
80 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
81 |
fun gen_rvar vs (t as Var ((a, 0), T)) = |
22271 | 82 |
if body_type T <> HOLogic.boolT then t else |
83 |
let |
|
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
84 |
val U = TVar (("'" ^ a, 0), []) |
22271 | 85 |
val Ts = binder_types T; |
86 |
val i = length Ts; |
|
87 |
val xs = map (pair "x") Ts; |
|
88 |
val u = list_comb (t, map Bound (i - 1 downto 0)) |
|
89 |
in |
|
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
90 |
if member (op =) vs a then |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
91 |
fold_rev Term.abs (("r", U) :: xs) (mk_rlz U $ Bound i $ u) |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
92 |
else |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
93 |
fold_rev Term.abs xs (mk_rlz Extraction.nullT $ Extraction.nullt $ u) |
22271 | 94 |
end |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
95 |
| gen_rvar _ t = t; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
96 |
|
22271 | 97 |
fun mk_realizes_eqn n vs nparms intrs = |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
98 |
let |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
99 |
val intr = map_types Type.strip_sorts (prop_of (hd intrs)); |
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
100 |
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr); |
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
101 |
val iTs = rev (Term.add_tvars intr []); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
102 |
val Tvs = map TVar iTs; |
22271 | 103 |
val (h as Const (s, T), us) = strip_comb concl; |
104 |
val params = List.take (us, nparms); |
|
105 |
val elTs = List.drop (binder_types T, nparms); |
|
106 |
val predT = elTs ---> HOLogic.boolT; |
|
107 |
val used = map (fst o fst o dest_Var) params; |
|
108 |
val xs = map (Var o apfst (rpair 0)) |
|
109 |
(Name.variant_list used (replicate (length elTs) "x") ~~ elTs); |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
110 |
val rT = if n then Extraction.nullT |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
111 |
else Type (space_implode "_" (s ^ "T" :: vs), |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
112 |
map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs); |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
113 |
val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT); |
22271 | 114 |
val S = list_comb (h, params @ xs); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
115 |
val rvs = relevant_vars S; |
33040 | 116 |
val vs' = subtract (op =) vs (map fst rvs); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
117 |
val rname = space_implode "_" (s ^ "R" :: vs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
118 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
119 |
fun mk_Tprem n v = |
17485 | 120 |
let val T = (the o AList.lookup (op =) rvs) v |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
121 |
in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
122 |
Extraction.mk_typ (if n then Extraction.nullT |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
123 |
else TVar (("'" ^ v, 0), []))) |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
124 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
125 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
126 |
val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs; |
22271 | 127 |
val ts = map (gen_rvar vs) params; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
128 |
val argTs = map fastype_of ts; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
129 |
|
22271 | 130 |
in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S, |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
131 |
Extraction.mk_typ rT)), |
22271 | 132 |
(prems, (mk_rlz rT $ r $ S, |
133 |
if n then list_comb (Const (rname, argTs ---> predT), ts @ xs) |
|
134 |
else list_comb (Const (rname, argTs @ [rT] ---> predT), ts @ [r] @ xs)))) |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
135 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
136 |
|
22271 | 137 |
fun fun_of_prem thy rsets vs params rule ivs intr = |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
138 |
let |
42361 | 139 |
val ctxt = Proof_Context.init_global thy |
22271 | 140 |
val args = map (Free o apfst fst o dest_Var) ivs; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
141 |
val args' = map (Free o apfst fst) |
33040 | 142 |
(subtract (op =) params (Term.add_vars (prop_of intr) [])); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
143 |
val rule' = strip_all rule; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
144 |
val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule'); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
145 |
val used = map (fst o dest_Free) args; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
146 |
|
29271
1d685baea08e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29265
diff
changeset
|
147 |
val is_rec = exists_Const (fn (c, _) => member (op =) rsets c); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
148 |
|
56245 | 149 |
fun is_meta (Const (@{const_name Pure.all}, _) $ Abs (s, _, P)) = is_meta P |
150 |
| is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q |
|
35364 | 151 |
| is_meta (Const (@{const_name Trueprop}, _) $ t) = |
152 |
(case head_of t of |
|
153 |
Const (s, _) => can (Inductive.the_inductive ctxt) s |
|
154 |
| _ => true) |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
155 |
| is_meta _ = false; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
156 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
157 |
fun fun_of ts rts args used (prem :: prems) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
158 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
159 |
val T = Extraction.etype_of thy vs [] prem; |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19806
diff
changeset
|
160 |
val [x, r] = Name.variant_list used ["x", "r"] |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
161 |
in if T = Extraction.nullT |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
162 |
then fun_of ts rts args used prems |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
163 |
else if is_rec prem then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
164 |
if is_meta prem then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
165 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
166 |
val prem' :: prems' = prems; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
167 |
val U = Extraction.etype_of thy vs [] prem'; |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
168 |
in |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
169 |
if U = Extraction.nullT |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
170 |
then fun_of (Free (x, T) :: ts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
171 |
(Free (r, binder_types T ---> HOLogic.unitT) :: rts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
172 |
(Free (x, T) :: args) (x :: r :: used) prems' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
173 |
else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
174 |
(Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
175 |
end |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
176 |
else |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
177 |
(case strip_type T of |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37236
diff
changeset
|
178 |
(Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) => |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
179 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
180 |
val fx = Free (x, Ts ---> T1); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
181 |
val fr = Free (r, Ts ---> T2); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
182 |
val bs = map Bound (length Ts - 1 downto 0); |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
183 |
val t = |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
184 |
fold_rev (Term.abs o pair "z") Ts |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
185 |
(HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs))); |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
186 |
in fun_of (fx :: ts) (fr :: rts) (t::args) (x :: r :: used) prems end |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
187 |
| (Ts, U) => fun_of (Free (x, T) :: ts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
188 |
(Free (r, binder_types T ---> HOLogic.unitT) :: rts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
189 |
(Free (x, T) :: args) (x :: r :: used) prems) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
190 |
else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
191 |
(x :: used) prems |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
192 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
193 |
| fun_of ts rts args used [] = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
194 |
let val xs = rev (rts @ ts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
195 |
in if conclT = Extraction.nullT |
44241 | 196 |
then fold_rev (absfree o dest_Free) xs HOLogic.unit |
197 |
else fold_rev (absfree o dest_Free) xs |
|
198 |
(list_comb |
|
199 |
(Free ("r" ^ Long_Name.base_name (name_of_thm intr), |
|
200 |
map fastype_of (rev args) ---> conclT), rev args)) |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
201 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
202 |
|
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset
|
203 |
in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
204 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
205 |
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
206 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
207 |
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); |
31986 | 208 |
val premss = map_filter (fn (s, rs) => if member (op =) rsets s then |
209 |
SOME (rs, map (fn (_, r) => nth (prems_of raw_induct) |
|
210 |
(find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss; |
|
22271 | 211 |
val fs = maps (fn ((intrs, prems), dummy) => |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
212 |
let |
22271 | 213 |
val fs = map (fn (rule, (ivs, intr)) => |
214 |
fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs) |
|
35364 | 215 |
in |
216 |
if dummy then Const (@{const_name default}, |
|
217 |
HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs |
|
22271 | 218 |
else fs |
219 |
end) (premss ~~ dummies); |
|
16861 | 220 |
val frees = fold Term.add_frees fs []; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
221 |
val Ts = map fastype_of fs; |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
222 |
fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr) |
22271 | 223 |
in |
224 |
fst (fold_map (fn concl => fn names => |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
225 |
let val T = Extraction.etype_of thy vs [] concl |
22271 | 226 |
in if T = Extraction.nullT then (Extraction.nullt, names) else |
227 |
let |
|
228 |
val Type ("fun", [U, _]) = T; |
|
229 |
val a :: names' = names |
|
44241 | 230 |
in |
231 |
(fold_rev absfree (("x", U) :: map_filter (fn intr => |
|
232 |
Option.map (pair (name_of_fn intr)) |
|
233 |
(AList.lookup (op =) frees (name_of_fn intr))) intrs) |
|
234 |
(list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names') |
|
22271 | 235 |
end |
236 |
end) concls rec_names) |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
237 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
238 |
|
45839
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset
|
239 |
fun add_dummy name dname (x as (_, ((s, vs, mx), cs))) = |
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset
|
240 |
if Binding.eq_name (name, s) |
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset
|
241 |
then (true, ((s, vs, mx), (dname, [HOLogic.unitT], NoSyn) :: cs)) |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
242 |
else x; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
243 |
|
18314 | 244 |
fun add_dummies f [] _ thy = |
245 |
(([], NONE), thy) |
|
246 |
| add_dummies f dts used thy = |
|
247 |
thy |
|
248 |
|> f (map snd dts) |
|
30345 | 249 |
|-> (fn dtinfo => pair (map fst dts, SOME dtinfo)) |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33957
diff
changeset
|
250 |
handle Datatype_Aux.Datatype_Empty name' => |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
251 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
252 |
val name = Long_Name.base_name name'; |
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42375
diff
changeset
|
253 |
val dname = singleton (Name.variant_list used) "Dummy"; |
18314 | 254 |
in |
255 |
thy |
|
30345 | 256 |
|> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used) |
14888
99ac3eb0f84e
add_dummies no longer uses transform_error but handles specific
berghofe
parents:
13928
diff
changeset
|
257 |
end; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
258 |
|
22271 | 259 |
fun mk_realizer thy vs (name, rule, rrule, rlz, rt) = |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
260 |
let |
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset
|
261 |
val rvs = map fst (relevant_vars (prop_of rule)); |
16861 | 262 |
val xs = rev (Term.add_vars (prop_of rule) []); |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
263 |
val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs); |
16861 | 264 |
val rlzvs = rev (Term.add_vars (prop_of rrule) []); |
17485 | 265 |
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; |
22271 | 266 |
val rs = map Var (subtract (op = o pairself fst) xs rlzvs); |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
267 |
val rlz' = fold_rev Logic.all rs (prop_of rrule) |
22271 | 268 |
in (name, (vs, |
33338 | 269 |
if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt, |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
270 |
Extraction.abs_corr_shyps thy rule vs vs2 |
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
271 |
(ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz) |
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
272 |
(fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule))))) |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
273 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
274 |
|
24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset
|
275 |
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x)); |
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset
|
276 |
|
33244 | 277 |
fun add_ind_realizer rsets intrs induct raw_induct elims vs thy = |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
278 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
279 |
val qualifier = Long_Name.qualifier (name_of_thm induct); |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37678
diff
changeset
|
280 |
val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts"); |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
281 |
val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
282 |
val ar = length vs + length iTs; |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31668
diff
changeset
|
283 |
val params = Inductive.params_of raw_induct; |
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31668
diff
changeset
|
284 |
val arities = Inductive.arities_of raw_induct; |
22271 | 285 |
val nparms = length params; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
286 |
val params' = map dest_Var params; |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31668
diff
changeset
|
287 |
val rss = Inductive.partition_rules raw_induct intrs; |
22271 | 288 |
val rss' = map (fn (((s, rs), (_, arity)), elim) => |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31668
diff
changeset
|
289 |
(s, (Inductive.infer_intro_vars elim arity rs ~~ rs))) |
22790
e1cff9268177
Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents:
22606
diff
changeset
|
290 |
(rss ~~ arities ~~ elims); |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
291 |
val (prfx, _) = split_last (Long_Name.explode (fst (hd rss))); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
292 |
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets; |
16123 | 293 |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
294 |
val thy1 = thy |> |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24157
diff
changeset
|
295 |
Sign.root_path |> |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
296 |
Sign.add_path (Long_Name.implode prfx); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
297 |
val (ty_eqs, rlz_eqs) = split_list |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
298 |
(map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
299 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
300 |
val thy1' = thy1 |> |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
301 |
Sign.add_types_global |
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
302 |
(map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |> |
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
303 |
Extraction.add_typeof_eqns_i ty_eqs; |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
304 |
val dts = map_filter (fn (s, rs) => if member (op =) rsets s then |
22271 | 305 |
SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
306 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
307 |
(** datatype representing computational content of inductive set **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
308 |
|
31783
cfbe9609ceb1
add_datatypes does not yield particular rules any longer
haftmann
parents:
31781
diff
changeset
|
309 |
val ((dummies, some_dt_names), thy2) = |
18008 | 310 |
thy1 |
45701 | 311 |
|> add_dummies (Datatype.add_datatype {strict = false, quiet = false}) |
312 |
(map (pair false) dts) [] |
|
18314 | 313 |
||> Extraction.add_typeof_eqns_i ty_eqs |
314 |
||> Extraction.add_realizes_eqns_i rlz_eqs; |
|
31783
cfbe9609ceb1
add_datatypes does not yield particular rules any longer
haftmann
parents:
31781
diff
changeset
|
315 |
val dt_names = these some_dt_names; |
58111 | 316 |
val case_thms = map (#case_rewrites o Datatype_Data.the_info thy2) dt_names; |
45701 | 317 |
val rec_thms = |
318 |
if null dt_names then [] |
|
58111 | 319 |
else #rec_rewrites (Datatype_Data.the_info thy2 (hd dt_names)); |
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18929
diff
changeset
|
320 |
val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o |
31781
861e675f01e6
add_datatype interface yields type names and less rules
haftmann
parents:
31723
diff
changeset
|
321 |
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms); |
31458 | 322 |
val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) => |
323 |
if member (op =) rsets s then |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
324 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
325 |
val (d :: dummies') = dummies; |
19473 | 326 |
val (recs1, recs2) = chop (length rs) (if d then tl recs else recs) |
31458 | 327 |
in (map (head_of o hd o rev o snd o strip_comb o fst o |
328 |
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies')) |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
329 |
end |
31458 | 330 |
else (replicate (length rs) Extraction.nullt, (recs, dummies))) |
31781
861e675f01e6
add_datatype interface yields type names and less rules
haftmann
parents:
31723
diff
changeset
|
331 |
rss (rec_thms, dummies); |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
332 |
val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
333 |
(Extraction.realizes_of thy2 vs |
22271 | 334 |
(if c = Extraction.nullt then c else list_comb (c, map Var (rev |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
335 |
(subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))) |
32952 | 336 |
(maps snd rss ~~ flat constrss); |
30345 | 337 |
val (rlzpreds, rlzpreds') = |
338 |
rintrs |> map (fn rintr => |
|
22271 | 339 |
let |
30345 | 340 |
val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)); |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
341 |
val s' = Long_Name.base_name s; |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset
|
342 |
val T' = Logic.unvarifyT_global T; |
30345 | 343 |
in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) |
344 |
|> distinct (op = o pairself (#1 o #1)) |
|
345 |
|> map (apfst (apfst (apfst Binding.name))) |
|
346 |
|> split_list; |
|
347 |
||
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset
|
348 |
val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT_global T)) |
22271 | 349 |
(List.take (snd (strip_comb |
350 |
(HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms)); |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
351 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
352 |
(** realizability predicate **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
353 |
|
22271 | 354 |
val (ind_info, thy3') = thy2 |> |
33726
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
355 |
Inductive.add_inductive_global |
33669 | 356 |
{quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false, |
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47060
diff
changeset
|
357 |
no_elim = false, no_ind = false, skip_mono = false} |
22271 | 358 |
rlzpreds rlzparams (map (fn (rintr, intr) => |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
359 |
((Binding.name (Long_Name.base_name (name_of_thm intr)), []), |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset
|
360 |
subst_atomic rlzpreds' (Logic.unvarify_global rintr))) |
22271 | 361 |
(rintrs ~~ maps snd rss)) [] ||> |
30435
e62d6ecab6ad
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
wenzelm
parents:
30364
diff
changeset
|
362 |
Sign.root_path; |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37678
diff
changeset
|
363 |
val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
364 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
365 |
(** realizer for induction rule **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
366 |
|
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
367 |
val Ps = map_filter (fn _ $ M $ P => if member (op =) rsets (pred_of M) then |
15531 | 368 |
SOME (fst (fst (dest_Var (head_of P)))) else NONE) |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
369 |
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
370 |
|
33244 | 371 |
fun add_ind_realizer Ps thy = |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
372 |
let |
24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset
|
373 |
val vs' = rename (map (pairself (fst o fst o dest_Var)) |
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset
|
374 |
(params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop |
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset
|
375 |
(hd (prems_of (hd inducts))))), nparms))) vs; |
22271 | 376 |
val rs = indrule_realizer thy induct raw_induct rsets params' |
24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset
|
377 |
(vs' @ Ps) rec_names rss' intrs dummies; |
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset
|
378 |
val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r |
22271 | 379 |
(prop_of ind)) (rs ~~ inducts); |
29281 | 380 |
val used = fold Term.add_free_names rlzs []; |
22271 | 381 |
val rnames = Name.variant_list used (replicate (length inducts) "r"); |
382 |
val rnames' = Name.variant_list |
|
383 |
(used @ rnames) (replicate (length intrs) "s"); |
|
384 |
val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) => |
|
385 |
let |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset
|
386 |
val (P, Q) = strip_one name (Logic.unvarify_global rlz); |
22271 | 387 |
val Q' = strip_all' [] rnames' Q |
388 |
in |
|
389 |
(Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q') |
|
390 |
end) (rlzs ~~ rnames); |
|
391 |
val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map |
|
392 |
(fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs')); |
|
37136 | 393 |
val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms); |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
394 |
val thm = Goal.prove_global thy [] |
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
395 |
(map attach_typeS prems) (attach_typeS concl) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
396 |
(fn {context = ctxt, prems} => EVERY |
22271 | 397 |
[rtac (#raw_induct ind_info) 1, |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
398 |
rewrite_goals_tac ctxt rews, |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
399 |
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
400 |
[K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt, |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
401 |
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37678
diff
changeset
|
402 |
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_" |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
403 |
(Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy; |
22271 | 404 |
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33957
diff
changeset
|
405 |
(Datatype_Aux.split_conj_thm thm'); |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37678
diff
changeset
|
406 |
val ([thms'], thy'') = Global_Theory.add_thmss |
30435
e62d6ecab6ad
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
wenzelm
parents:
30364
diff
changeset
|
407 |
[((Binding.qualified_name (space_implode "_" |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
408 |
(Long_Name.qualify qualifier "inducts" :: vs' @ Ps @ |
29579 | 409 |
["correctness"])), thms), [])] thy'; |
22271 | 410 |
val realizers = inducts ~~ thms' ~~ rlzs ~~ rs; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
411 |
in |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
412 |
Extraction.add_realizers_i |
22271 | 413 |
(map (fn (((ind, corr), rlz), r) => |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
414 |
mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r)) |
22271 | 415 |
realizers @ (case realizers of |
416 |
[(((ind, corr), rlz), r)] => |
|
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
417 |
[mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct", |
22271 | 418 |
ind, corr, rlz, r)] |
419 |
| _ => [])) thy'' |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
420 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
421 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
422 |
(** realizer for elimination rules **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
423 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
424 |
val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o |
31781
861e675f01e6
add_datatype interface yields type names and less rules
haftmann
parents:
31723
diff
changeset
|
425 |
HOLogic.dest_Trueprop o prop_of o hd) case_thms; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
426 |
|
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset
|
427 |
fun add_elim_realizer Ps |
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset
|
428 |
(((((elim, elimR), intrs), case_thms), case_name), dummy) thy = |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
429 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
430 |
val (prem :: prems) = prems_of elim; |
22271 | 431 |
fun reorder1 (p, (_, intr)) = |
33244 | 432 |
fold (fn ((s, _), T) => Logic.all (Free (s, T))) |
433 |
(subtract (op =) params' (Term.add_vars (prop_of intr) [])) |
|
434 |
(strip_all p); |
|
22271 | 435 |
fun reorder2 ((ivs, intr), i) = |
33040 | 436 |
let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) []) |
33244 | 437 |
in fold (lambda o Var) fs (list_comb (Bound (i + length ivs), ivs)) end; |
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset
|
438 |
val p = Logic.list_implies |
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset
|
439 |
(map reorder1 (prems ~~ intrs) @ [prem], concl_of elim); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
440 |
val T' = Extraction.etype_of thy (vs @ Ps) [] p; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
441 |
val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T'; |
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset
|
442 |
val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim); |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
443 |
val r = |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
444 |
if null Ps then Extraction.nullt |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
445 |
else |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
446 |
fold_rev (Term.abs o pair "x") Ts |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
447 |
(list_comb (Const (case_name, T), |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
448 |
(if dummy then |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
449 |
[Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))] |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
450 |
else []) @ |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
451 |
map reorder2 (intrs ~~ (length prems - 1 downto 0)) @ |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset
|
452 |
[Bound (length prems)])); |
22271 | 453 |
val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim); |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
454 |
val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz)); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
455 |
val rews = map mk_meta_eq case_thms; |
22271 | 456 |
val thm = Goal.prove_global thy [] |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset
|
457 |
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset
|
458 |
(fn {context = ctxt, prems, ...} => EVERY |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset
|
459 |
[cut_tac (hd prems) 1, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset
|
460 |
etac elimR 1, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset
|
461 |
ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)), |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
462 |
rewrite_goals_tac ctxt rews, |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
463 |
REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN' |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset
|
464 |
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37678
diff
changeset
|
465 |
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_" |
29579 | 466 |
(name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
467 |
in |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
468 |
Extraction.add_realizers_i |
22271 | 469 |
[mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy' |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
470 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
471 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
472 |
(** add realizers to theory **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
473 |
|
33244 | 474 |
val thy4 = fold add_ind_realizer (subsets Ps) thy3; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
475 |
val thy5 = Extraction.add_realizers_i |
22271 | 476 |
(map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) => |
477 |
(name_of_thm rule, rule, rrule, rlz, |
|
33040 | 478 |
list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) [])))))) |
32952 | 479 |
(maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4; |
480 |
val elimps = map_filter (fn ((s, intrs), p) => |
|
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
481 |
if member (op =) rsets s then SOME (p, intrs) else NONE) |
22271 | 482 |
(rss' ~~ (elims ~~ #elims ind_info)); |
33244 | 483 |
val thy6 = |
484 |
fold (fn p as (((((elim, _), _), _), _), _) => |
|
485 |
add_elim_realizer [] p #> |
|
486 |
add_elim_realizer [fst (fst (dest_Var (HOLogic.dest_Trueprop (concl_of elim))))] p) |
|
487 |
(elimps ~~ case_thms ~~ case_names ~~ dummies) thy5; |
|
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
488 |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24157
diff
changeset
|
489 |
in Sign.restore_naming thy thy6 end; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
490 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
491 |
fun add_ind_realizers name rsets thy = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
492 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
493 |
val (_, {intrs, induct, raw_induct, elims, ...}) = |
42361 | 494 |
Inductive.the_inductive (Proof_Context.init_global thy) name; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
495 |
val vss = sort (int_ord o pairself length) |
22271 | 496 |
(subsets (map fst (relevant_vars (concl_of (hd intrs))))) |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
497 |
in |
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset
|
498 |
fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
499 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
500 |
|
20897 | 501 |
fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
502 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
503 |
fun err () = error "ind_realizer: bad rule"; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
504 |
val sets = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
505 |
(case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of |
22271 | 506 |
[_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))] |
507 |
| xs => map (pred_of o fst o HOLogic.dest_imp) xs) |
|
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
46708
diff
changeset
|
508 |
handle TERM _ => err () | List.Empty => err (); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
509 |
in |
18728 | 510 |
add_ind_realizers (hd sets) |
511 |
(case arg of |
|
15531 | 512 |
NONE => sets | SOME NONE => [] |
33040 | 513 |
| SOME (SOME sets') => subtract (op =) sets' sets) |
20897 | 514 |
end I); |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
515 |
|
18708 | 516 |
val setup = |
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
517 |
Attrib.setup @{binding ind_realizer} |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
518 |
((Scan.option (Scan.lift (Args.$$$ "irrelevant") |-- |
55954 | 519 |
Scan.option (Scan.lift (Args.colon) |-- |
55958
4ec984df4f45
more rigid const demands, based on educated guesses about the tools involved here;
wenzelm
parents:
55954
diff
changeset
|
520 |
Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib) |
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
521 |
"add realizers for inductive set"; |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
522 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
523 |
end; |
15706 | 524 |