author | wenzelm |
Mon, 01 Jun 2015 13:35:16 +0200 | |
changeset 60328 | 9c94e6a30d29 |
parent 59498 | 50b60f501b05 |
child 62082 | 614ef6d7a6b6 |
permissions | -rw-r--r-- |
58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58179
diff
changeset
|
1 |
(* Title: HOL/Tools/Old_Datatype/old_size.ML |
43084
946c8e171ffd
more precise authorship, reflecting my own ignorance and hg annotate
krauss
parents:
42361
diff
changeset
|
2 |
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen |
24710 | 3 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
4 |
Size functions for old-style datatypes. |
24710 | 5 |
*) |
6 |
||
58179 | 7 |
structure Old_Size: sig end = |
24710 | 8 |
struct |
9 |
||
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35064
diff
changeset
|
10 |
fun plus (t1, t2) = Const (@{const_name Groups.plus}, |
24710 | 11 |
HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; |
12 |
||
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
13 |
fun size_of_type f g h (T as Type (s, Ts)) = |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
14 |
(case f s of |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
15 |
SOME t => SOME t |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
16 |
| NONE => (case g s of |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
17 |
SOME size_name => |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
18 |
SOME (list_comb (Const (size_name, |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
19 |
map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT), |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
20 |
map (size_of_type' f g h) Ts)) |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
21 |
| NONE => NONE)) |
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56639
diff
changeset
|
22 |
| size_of_type _ _ h (TFree (s, _)) = h s |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
23 |
and size_of_type' f g h T = (case size_of_type f g h T of |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
24 |
NONE => Abs ("x", T, HOLogic.zero) |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
25 |
| SOME t => t); |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
26 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
27 |
fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) = |
58179 | 28 |
is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
29 |
| is_poly _ _ = true; |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
30 |
|
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
31 |
fun constrs_of thy name = |
24710 | 32 |
let |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
33 |
val {descr, index, ...} = Old_Datatype_Data.the_info thy name |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
34 |
val SOME (_, _, constrs) = AList.lookup op = descr index |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
35 |
in constrs end; |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
36 |
|
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
37 |
val app = curry (list_comb o swap); |
24710 | 38 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
39 |
fun prove_size_thms (info : Old_Datatype_Aux.info) new_type_names thy = |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
40 |
let |
45822 | 41 |
val {descr, rec_names, rec_rewrites, induct, ...} = info; |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
42 |
val l = length new_type_names; |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
43 |
val descr' = List.take (descr, l); |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
44 |
val tycos = map (#1 o snd) descr'; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
45 |
in |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
46 |
if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
47 |
(* nothing to do -- the "size" function is already defined *) |
24710 | 48 |
thy |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
49 |
else |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
50 |
let |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
51 |
val recTs = Old_Datatype_Aux.get_rec_types descr; |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
52 |
val (recTs1, recTs2) = chop l recTs; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
53 |
val (_, (_, paramdts, _)) :: _ = descr; |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
54 |
val paramTs = map (Old_Datatype_Aux.typ_of_dtyp descr) paramdts; |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
55 |
val ((param_size_fs, param_size_fTs), f_names) = paramTs |> |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
56 |
map (fn T as TFree (s, _) => |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
57 |
let |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
58 |
val name = "f" ^ unprefix "'" s; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
59 |
val U = T --> HOLogic.natT |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
60 |
in |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
61 |
(((s, Free (name, U)), U), name) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
62 |
end) |> split_list |>> split_list; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
63 |
val param_size = AList.lookup op = param_size_fs; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
64 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
65 |
val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |> |
58179 | 66 |
map_filter (Option.map (fst o snd) o BNF_LFP_Size.size_of_global thy) |> flat; |
67 |
val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy; |
|
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
68 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
69 |
val (((size_names, size_fns), def_names), def_names') = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
70 |
recTs1 |> map (fn T as Type (s, _) => |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
71 |
let |
56846
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56651
diff
changeset
|
72 |
val s' = "size_" ^ Long_Name.base_name s; |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
73 |
val s'' = Sign.full_bname thy s'; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
74 |
in |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
75 |
(s'', |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
76 |
(list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT), |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
77 |
map snd param_size_fs), |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
78 |
(s' ^ "_def", s' ^ "_overloaded_def"))) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
79 |
end) |> split_list ||>> split_list ||>> split_list; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
80 |
val overloaded_size_fns = map HOLogic.size_const recTs1; |
24710 | 81 |
|
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
82 |
(* instantiation for primrec combinator *) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
83 |
fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
84 |
let |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
85 |
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs; |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
86 |
val k = length (filter Old_Datatype_Aux.is_rec_type cargs); |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
87 |
val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) => |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
88 |
if Old_Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1) |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
89 |
else |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
90 |
(if b andalso is_poly thy dt' then |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
91 |
case size_of_type (K NONE) extra_size size_ofp T of |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
92 |
NONE => us | SOME sz => sz $ Bound j :: us |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
93 |
else us, i, j + 1)) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
94 |
(cargs ~~ cargs' ~~ Ts) ([], 0, k); |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
95 |
val t = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
96 |
if null ts andalso (not b orelse not (exists (is_poly thy) cargs')) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
97 |
then HOLogic.zero |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
98 |
else foldl1 plus (ts @ [HOLogic.Suc_zero]) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
99 |
in |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
100 |
fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
101 |
end; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
102 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
103 |
val fs = maps (fn (_, (name, _, constrs)) => |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
104 |
map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
105 |
val fs' = maps (fn (n, (name, _, constrs)) => |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
106 |
map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
107 |
val fTs = map fastype_of fs; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
108 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
109 |
val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) => |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
110 |
Const (rec_name, fTs @ [T] ---> HOLogic.natT)) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
111 |
(recTs ~~ rec_names)); |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
112 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
113 |
fun define_overloaded (def_name, eq) lthy = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
114 |
let |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
115 |
val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
116 |
val (thm, lthy') = lthy |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
117 |
|> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
118 |
|-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm); |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
119 |
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
120 |
val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
121 |
in (thm', lthy') end; |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
122 |
|
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
123 |
val ((size_def_thms, size_def_thms'), thy') = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
124 |
thy |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
125 |
|> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
126 |
param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
127 |
(size_names ~~ recTs1)) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
128 |
|> Global_Theory.add_defs false |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
129 |
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs))) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
130 |
(map Binding.name def_names ~~ (size_fns ~~ rec_combs1))) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
131 |
||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size]) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
132 |
||>> fold_map define_overloaded |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
133 |
(def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1)) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58381
diff
changeset
|
134 |
||> Class.prove_instantiation_instance (fn ctxt => Class.intro_classes_tac ctxt []) |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
135 |
||> Local_Theory.exit_global; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
136 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
137 |
val ctxt = Proof_Context.init_global thy'; |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
138 |
|
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
139 |
val simpset1 = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
140 |
put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} :: |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
141 |
size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
142 |
val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2); |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
143 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56639
diff
changeset
|
144 |
fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) = |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
145 |
HOLogic.mk_eq (app fs r $ Free p, |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
146 |
the (size_of_type tab extra_size size_ofp T) $ Free p); |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
147 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
148 |
fun prove_unfolded_size_eqs size_ofp fs = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
149 |
if null recTs2 then [] |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
150 |
else Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs [] |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
151 |
(HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (replicate l @{term True} @ |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
152 |
map (mk_unfolded_size_eq (AList.lookup op = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
153 |
(new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
154 |
(xs ~~ recTs2 ~~ rec_combs2)))) |
60328 | 155 |
(fn _ => (Old_Datatype_Aux.ind_tac ctxt induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
156 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
157 |
val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
158 |
val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
159 |
|
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
160 |
(* characteristic equations for size functions *) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
161 |
fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
162 |
let |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
163 |
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs; |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
164 |
val tnames = Name.variant_list f_names (Old_Datatype_Prop.make_tnames Ts); |
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56639
diff
changeset
|
165 |
val ts = map_filter (fn (sT as (_, T), dt) => |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
166 |
Option.map (fn sz => sz $ Free sT) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
167 |
(if p dt then size_of_type size_of extra_size size_ofp T |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
168 |
else NONE)) (tnames ~~ Ts ~~ cargs) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
169 |
in |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
170 |
HOLogic.mk_Trueprop (HOLogic.mk_eq |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
171 |
(size_const $ list_comb (Const (cname, Ts ---> T), |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
172 |
map2 (curry Free) tnames Ts), |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
173 |
if null ts then HOLogic.zero |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
174 |
else foldl1 plus (ts @ [HOLogic.Suc_zero]))) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
175 |
end; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
176 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
177 |
val simpset2 = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
178 |
put_simpset HOL_basic_ss ctxt |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
179 |
addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1); |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
180 |
val simpset3 = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
181 |
put_simpset HOL_basic_ss ctxt |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
182 |
addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2); |
24710 | 183 |
|
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
184 |
fun prove_size_eqs p size_fns size_ofp simpset = |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
185 |
maps (fn (((_, (_, _, constrs)), size_const), T) => |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
186 |
map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] [] |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
187 |
(gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns)) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
188 |
size_ofp size_const T constr) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
189 |
(fn _ => simp_tac simpset 1))) constrs) |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
190 |
(descr' ~~ size_fns ~~ recTs1); |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
191 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
192 |
val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @ |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
193 |
prove_size_eqs Old_Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3; |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
194 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
195 |
val ([(_, size_thms)], thy'') = thy' |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
196 |
|> Global_Theory.note_thmss "" |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
197 |
[((Binding.name "size", |
57964 | 198 |
[Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}, |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
199 |
Thm.declaration_attribute (fn thm => |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
200 |
Context.mapping (Code.add_default_eqn thm) I)]), |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
201 |
[(size_eqns, [])])]; |
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
202 |
|
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
203 |
in |
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56639
diff
changeset
|
204 |
fold2 (fn new_type_name => fn size_name => |
56651 | 205 |
BNF_LFP_Size.register_size_global new_type_name size_name size_thms []) |
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56639
diff
changeset
|
206 |
new_type_names size_names thy'' |
56639
c9d6b581bd3b
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
blanchet
parents:
56375
diff
changeset
|
207 |
end |
24710 | 208 |
end; |
209 |
||
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56639
diff
changeset
|
210 |
fun add_size_thms _ (new_type_names as name :: _) thy = |
24710 | 211 |
let |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
212 |
val info as {descr, ...} = Old_Datatype_Data.the_info thy name; |
56375
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
56239
diff
changeset
|
213 |
val prefix = space_implode "_" (map Long_Name.base_name new_type_names); |
24710 | 214 |
val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
215 |
Old_Datatype_Aux.is_rec_type dt andalso |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57964
diff
changeset
|
216 |
not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr |
45701 | 217 |
in |
218 |
if no_size then thy |
|
24710 | 219 |
else |
220 |
thy |
|
24714
1618c2ac1b74
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24711
diff
changeset
|
221 |
|> Sign.add_path prefix |
25679
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
222 |
|> prove_size_thms info new_type_names |
b77f797b528a
size functions for nested datatypes are now expressed using
berghofe
parents:
25569
diff
changeset
|
223 |
|> Sign.restore_naming thy |
24710 | 224 |
end; |
225 |
||
58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58179
diff
changeset
|
226 |
val _ = Theory.setup (Old_Datatype_Data.interpretation add_size_thms); |
24710 | 227 |
|
29866
6e93ae65c678
Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
blanchet
parents:
29863
diff
changeset
|
228 |
end; |