author  blanchet 
Fri, 21 Sep 2012 02:19:44 +0200  
changeset 49486  64cc57c0d0fe 
parent 49484  0194a18f80cf 
child 49498  acc583e14167 
permissions  rwrr 
49074  1 
(* Title: HOL/Codatatype/Tools/bnf_wrap.ML 
49017  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2012 

4 

49074  5 
Wrapping existing datatypes. 
49017  6 
*) 
7 

49074  8 
signature BNF_WRAP = 
49017  9 
sig 
49121  10 
val mk_half_pairss: 'a list > ('a * 'a) list list 
49203  11 
val mk_ctr: typ list > term > term 
49484  12 
val mk_disc_or_sel: typ list > term > term 
49437  13 
val base_name_of_ctr: term > string 
49199  14 
val wrap_datatype: ({prems: thm list, context: Proof.context} > tactic) list list > 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

15 
((bool * term list) * term) * 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

16 
(binding list * (binding list list * (binding * term) list list)) > local_theory > 
49484  17 
(term list * term list list * thm list * thm list * thm list * thm list list * thm list * 
18 
thm list list) * local_theory 

49278  19 
val parse_wrap_options: bool parser 
49286  20 
val parse_bound_term: (binding * string) parser 
49017  21 
end; 
22 

49074  23 
structure BNF_Wrap : BNF_WRAP = 
49017  24 
struct 
25 

26 
open BNF_Util 

49074  27 
open BNF_Wrap_Tactics 
49017  28 

49223  29 
val isN = "is_"; 
30 
val unN = "un_"; 

31 
fun mk_unN 1 1 suf = unN ^ suf 

32 
 mk_unN _ l suf = unN ^ suf ^ string_of_int l; 

49046
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

33 

49054  34 
val case_congN = "case_cong"; 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

35 
val case_eqN = "case_eq"; 
49054  36 
val casesN = "cases"; 
49118  37 
val collapseN = "collapse"; 
49122  38 
val disc_excludeN = "disc_exclude"; 
49054  39 
val disc_exhaustN = "disc_exhaust"; 
40 
val discsN = "discs"; 

41 
val distinctN = "distinct"; 

49075  42 
val exhaustN = "exhaust"; 
49486  43 
val expandN = "expand"; 
49075  44 
val injectN = "inject"; 
45 
val nchotomyN = "nchotomy"; 

49054  46 
val selsN = "sels"; 
47 
val splitN = "split"; 

48 
val split_asmN = "split_asm"; 

49 
val weak_case_cong_thmsN = "weak_case_cong"; 

49019  50 

49336  51 
val std_binding = @{binding _}; 
49300  52 

53 
val induct_simp_attrs = @{attributes [induct_simp]}; 

54 
val cong_attrs = @{attributes [cong]}; 

55 
val iff_attrs = @{attributes [iff]}; 

56 
val safe_elim_attrs = @{attributes [elim!]}; 

57 
val simp_attrs = @{attributes [simp]}; 

49046
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

58 

49056  59 
fun pad_list x n xs = xs @ replicate (n  length xs) x; 
60 

49259  61 
fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys))); 
49258
84f13469d7f0
allow same selector name for several constructors
blanchet
parents:
49257
diff
changeset

62 

49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

63 
fun mk_half_pairss' _ [] = [] 
49486  64 
 mk_half_pairss' indent (x :: xs) = 
65 
indent @ fold_rev (cons o single o pair x) xs (mk_half_pairss' ([] :: indent) xs); 

66 

67 
fun mk_half_pairss xs = mk_half_pairss' [[]] xs; 

49027  68 

49486  69 
fun join_halves n half_xss other_half_xss = 
70 
let 

71 
val xsss = 

72 
map2 (map2 append) (Library.chop_groups n half_xss) 

73 
(transpose (Library.chop_groups n other_half_xss)) 

74 
val xs = interleave (flat half_xss) (flat other_half_xss); 

75 
in (xs, xsss > `transpose) end; 

49027  76 

49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

77 
fun mk_undefined T = Const (@{const_name undefined}, T); 
49055  78 

49203  79 
fun mk_ctr Ts ctr = 
80 
let val Type (_, Ts0) = body_type (fastype_of ctr) in 

81 
Term.subst_atomic_types (Ts0 ~~ Ts) ctr 

82 
end; 

83 

49484  84 
fun mk_disc_or_sel Ts t = 
85 
Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t; 

86 

49300  87 
fun base_name_of_ctr c = 
88 
Long_Name.base_name (case head_of c of 

89 
Const (s, _) => s 

90 
 Free (s, _) => s 

91 
 _ => error "Cannot extract name of constructor"); 

49046
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

92 

49486  93 
fun rap u t = betapply (t, u); 
94 

49437  95 
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
96 

49278  97 
fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case), 
49336  98 
(raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy = 
49017  99 
let 
49019  100 
(* TODO: sanity checks on arguments *) 
49113  101 
(* TODO: case syntax *) 
49025  102 

49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

103 
val n = length raw_ctrs; 
49054  104 
val ks = 1 upto n; 
105 

49121  106 
val _ = if n > 0 then () else error "No constructors specified"; 
107 

49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

108 
val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

109 
val case0 = prep_term no_defs_lthy raw_case; 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

110 
val sel_defaultss = 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

111 
pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss); 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

112 

49300  113 
val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0)); 
49302
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

114 
val data_b = Binding.qualified_name dataT_name; 
49055  115 

116 
val (As, B) = 

117 
no_defs_lthy 

49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

118 
> mk_TFrees' (map Type.sort_of_atyp As0) 
49055  119 
> the_single o fst o mk_TFrees 1; 
120 

49300  121 
val dataT = Type (dataT_name, As); 
49055  122 
val ctrs = map (mk_ctr As) ctrs0; 
123 
val ctr_Tss = map (binder_types o fastype_of) ctrs; 

124 

125 
val ms = map length ctr_Tss; 

126 

49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49364
diff
changeset

127 
val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

128 

49174
41790d616f63
by default, only generate one discriminator for a twovalue datatype
blanchet
parents:
49157
diff
changeset

129 
fun can_really_rely_on_disc k = 
49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49364
diff
changeset

130 
not (Binding.eq_name (nth raw_disc_bindings' (k  1), Binding.empty)) orelse 
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49364
diff
changeset

131 
nth ms (k  1) = 0; 
49174
41790d616f63
by default, only generate one discriminator for a twovalue datatype
blanchet
parents:
49157
diff
changeset

132 
fun can_rely_on_disc k = 
41790d616f63
by default, only generate one discriminator for a twovalue datatype
blanchet
parents:
49157
diff
changeset

133 
can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2)); 
49336  134 
fun can_omit_disc_binding k m = 
49174
41790d616f63
by default, only generate one discriminator for a twovalue datatype
blanchet
parents:
49157
diff
changeset

135 
n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3  k)); 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

136 

49336  137 
val std_disc_binding = 
49302
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

138 
Binding.qualify false (Binding.name_of data_b) o Binding.name o prefix isN o base_name_of_ctr; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

139 

49336  140 
val disc_bindings = 
141 
raw_disc_bindings' 

49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

142 
> map4 (fn k => fn m => fn ctr => fn disc => 
49302
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

143 
Option.map (Binding.qualify false (Binding.name_of data_b)) 
49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49364
diff
changeset

144 
(if Binding.eq_name (disc, Binding.empty) then 
49336  145 
if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr) 
146 
else if Binding.eq_name (disc, std_binding) then 

147 
SOME (std_disc_binding ctr) 

49302
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

148 
else 
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

149 
SOME disc)) ks ms ctrs0; 
49056  150 

49336  151 
val no_discs = map is_none disc_bindings; 
49137  152 
val no_discs_at_all = forall I no_discs; 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

153 

49336  154 
fun std_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

155 

49336  156 
val sel_bindingss = 
157 
pad_list [] n raw_sel_bindingss 

49056  158 
> map3 (fn ctr => fn m => map2 (fn l => fn sel => 
49302
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

159 
Binding.qualify false (Binding.name_of data_b) 
49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49364
diff
changeset

160 
(if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then 
49336  161 
std_sel_binding m l ctr 
49302
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

162 
else 
49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49364
diff
changeset

163 
sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms; 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

164 

49130
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

165 
fun mk_case Ts T = 
49121  166 
let 
49336  167 
val (bindings, body) = strip_type (fastype_of case0) 
168 
val Type (_, Ts0) = List.last bindings 

49130
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

169 
in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) case0 end; 
49022  170 

49201  171 
val casex = mk_case As B; 
172 
val case_Ts = map (fn Ts => Ts > B) ctr_Tss; 

49043  173 

49486  174 
val ((((((((xss, xss'), yss), fs), gs), (u, u')), v), (p, p')), names_lthy) = no_defs_lthy > 
49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

175 
mk_Freess' "x" ctr_Tss 
49025  176 
>> mk_Freess "y" ctr_Tss 
49201  177 
>> mk_Frees "f" case_Ts 
178 
>> mk_Frees "g" case_Ts 

49486  179 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "u") dataT 
180 
>> yield_singleton (mk_Frees "v") dataT 

49043  181 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; 
182 

49463  183 
val q = Free (fst p', mk_pred1T B); 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

184 

49025  185 
val xctrs = map2 (curry Term.list_comb) ctrs xss; 
186 
val yctrs = map2 (curry Term.list_comb) ctrs yss; 

49032  187 

49043  188 
val xfs = map2 (curry Term.list_comb) fs xss; 
189 
val xgs = map2 (curry Term.list_comb) gs xss; 

190 

49437  191 
val eta_fs = map2 eta_expand_arg xss xfs; 
192 
val eta_gs = map2 eta_expand_arg xss xgs; 

49043  193 

49201  194 
val fcase = Term.list_comb (casex, eta_fs); 
195 
val gcase = Term.list_comb (casex, eta_gs); 

49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

196 

49486  197 
val ufcase = fcase $ u; 
198 
val vfcase = fcase $ v; 

199 
val vgcase = gcase $ v; 

200 

201 
fun mk_u_eq_u () = HOLogic.mk_eq (u, u); 

202 

203 
val u_eq_v = mk_Trueprop_eq (u, v); 

204 

205 
val exist_xs_u_eq_ctrs = 

206 
map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss; 

49022  207 

49278  208 
val unique_disc_no_def = TrueI; (*arbitrary marker*) 
209 
val alternate_disc_no_def = FalseE; (*arbitrary marker*) 

49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

210 

49486  211 
fun alternate_disc_lhs get_udisc k = 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

212 
HOLogic.mk_not 
49336  213 
(case nth disc_bindings (k  1) of 
49486  214 
NONE => nth exist_xs_u_eq_ctrs (k  1) 
215 
 SOME b => get_udisc b (k  1)); 

49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

216 

49486  217 
val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs, 
218 
sel_defss, lthy') = 

49278  219 
if no_dests then 
49486  220 
(true, [], [], [], [], [], [], [], [], [], no_defs_lthy) 
49278  221 
else 
222 
let 

49463  223 
fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT); 
49025  224 

49486  225 
fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr); 
49278  226 

49486  227 
fun alternate_disc k = Term.lambda u (alternate_disc_lhs (K o rap u o disc_free) (3  k)); 
49278  228 

49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

229 
fun mk_default T t = 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

230 
let 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

231 
val Ts0 = map TFree (Term.add_tfreesT (fastype_of t) []); 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

232 
val Ts = map TFree (Term.add_tfreesT T []); 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

233 
in Term.subst_atomic_types (Ts0 ~~ Ts) t end; 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

234 

49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

235 
fun mk_sel_case_args b proto_sels T = 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

236 
map2 (fn Ts => fn k => 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

237 
(case AList.lookup (op =) proto_sels k of 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

238 
NONE => 
49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

239 
(case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k  1))) b of 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

240 
NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T) 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

241 
 SOME t => mk_default (Ts > T) t) 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

242 
 SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks; 
49258
84f13469d7f0
allow same selector name for several constructors
blanchet
parents:
49257
diff
changeset

243 

49278  244 
fun sel_spec b proto_sels = 
245 
let 

246 
val _ = 

247 
(case duplicates (op =) (map fst proto_sels) of 

248 
k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^ 

249 
" for constructor " ^ 

250 
quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k  1)))) 

251 
 [] => ()) 

252 
val T = 

253 
(case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of 

254 
[T] => T 

255 
 T :: T' :: _ => error ("Inconsistent range type for selector " ^ 

256 
quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ 

257 
" vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T'))); 

258 
in 

49486  259 
mk_Trueprop_eq (Free (Binding.name_of b, dataT > T) $ u, 
260 
Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ u) 

49278  261 
end; 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

262 

49336  263 
val sel_bindings = flat sel_bindingss; 
264 
val uniq_sel_bindings = distinct Binding.eq_name sel_bindings; 

265 
val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings); 

49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

266 

49336  267 
val sel_binding_index = 
268 
if all_sels_distinct then 1 upto length sel_bindings 

269 
else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings; 

49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

270 

036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

271 
val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss); 
49300  272 
val sel_infos = 
49336  273 
AList.group (op =) (sel_binding_index ~~ proto_sels) 
49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

274 
> sort (int_ord o pairself fst) 
49336  275 
> map snd > curry (op ~~) uniq_sel_bindings; 
276 
val sel_bindings = map fst sel_infos; 

49258
84f13469d7f0
allow same selector name for several constructors
blanchet
parents:
49257
diff
changeset

277 

49336  278 
fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss; 
49258
84f13469d7f0
allow same selector name for several constructors
blanchet
parents:
49257
diff
changeset

279 

49278  280 
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = 
281 
no_defs_lthy 

49486  282 
> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => 
49278  283 
fn NONE => 
49486  284 
if n = 1 then pair (Term.lambda u (mk_u_eq_u ()), unique_disc_no_def) 
285 
else if m = 0 then pair (Term.lambda u exist_xs_u_eq_ctr, refl) 

49278  286 
else pair (alternate_disc k, alternate_disc_no_def) 
287 
 SOME b => Specification.definition (SOME (b, NONE, NoSyn), 

49486  288 
((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd) 
289 
ks ms exist_xs_u_eq_ctrs disc_bindings 

49278  290 
>> apfst split_list o fold_map (fn (b, proto_sels) => 
291 
Specification.definition (SOME (b, NONE, NoSyn), 

49300  292 
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos 
49278  293 
> `Local_Theory.restore; 
49022  294 

49278  295 
val phi = Proof_Context.export_morphism lthy lthy'; 
49025  296 

49278  297 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
49281  298 
val sel_defs = map (Morphism.thm phi) raw_sel_defs; 
299 
val sel_defss = unflat_selss sel_defs; 

49278  300 

301 
val discs0 = map (Morphism.term phi) raw_discs; 

302 
val selss0 = unflat_selss (map (Morphism.term phi) raw_sels); 

49028  303 

49278  304 
val discs = map (mk_disc_or_sel As) discs0; 
305 
val selss = map (map (mk_disc_or_sel As)) selss0; 

49486  306 

307 
val udiscs = map (rap u) discs; 

308 
val uselss = map (map (rap u)) selss; 

309 

310 
val vdiscs = map (rap v) discs; 

311 
val vselss = map (map (rap v)) selss; 

49278  312 
in 
49486  313 
(all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs, 
314 
sel_defss, lthy') 

49278  315 
end; 
49025  316 

49032  317 
fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); 
49029  318 

49458  319 
val exhaust_goal = 
49486  320 
let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in 
321 
fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss)) 

49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

322 
end; 
49019  323 

49484  324 
val inject_goalss = 
49017  325 
let 
49034
b77e1910af8a
make parallel list indexing possible for inject theorems
blanchet
parents:
49033
diff
changeset

326 
fun mk_goal _ _ [] [] = [] 
49025  327 
 mk_goal xctr yctr xs ys = 
49121  328 
[fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), 
329 
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; 

49017  330 
in 
49034
b77e1910af8a
make parallel list indexing possible for inject theorems
blanchet
parents:
49033
diff
changeset

331 
map4 mk_goal xctrs yctrs xss yss 
49017  332 
end; 
333 

49484  334 
val half_distinct_goalss = 
49121  335 
let 
49203  336 
fun mk_goal ((xs, xc), (xs', xc')) = 
49121  337 
fold_rev Logic.all (xs @ xs') 
49203  338 
(HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc')))); 
49121  339 
in 
340 
map (map mk_goal) (mk_half_pairss (xss ~~ xctrs)) 

341 
end; 

49019  342 

49458  343 
val cases_goal = 
49121  344 
map3 (fn xs => fn xctr => fn xf => 
49201  345 
fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs; 
49025  346 

49484  347 
val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal]; 
49019  348 

349 
fun after_qed thmss lthy = 

350 
let 

49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

351 
val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) = 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

352 
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); 
49019  353 

49438  354 
val inject_thms = flat inject_thmss; 
355 

49486  356 
val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As); 
357 

358 
fun inst_thm t thm = 

359 
Drule.instantiate' [] [SOME (certify lthy t)] 

360 
(Thm.instantiate (Tinst, []) (Drule.zero_var_indexes thm)); 

361 

362 
val uexhaust_thm = inst_thm u exhaust_thm; 

49032  363 

49300  364 
val exhaust_cases = map base_name_of_ctr ctrs; 
365 

49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

366 
val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss; 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

367 

49486  368 
val (distinct_thms, (distinct_thmsss', distinct_thmsss)) = 
369 
join_halves n half_distinct_thmss other_half_distinct_thmss; 

49019  370 

49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

371 
val nchotomy_thm = 
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

372 
let 
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

373 
val goal = 
49486  374 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u', 
375 
Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs)); 

49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

376 
in 
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

377 
Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) 
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

378 
end; 
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

379 

49484  380 
val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, 
49486  381 
disc_exhaust_thms, collapse_thms, expand_thms, case_eq_thms) = 
49278  382 
if no_dests then 
49486  383 
([], [], [], [], [], [], [], [], [], []) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

384 
else 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

385 
let 
49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

386 
fun make_sel_thm xs' case_thm sel_def = 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

387 
zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs') 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

388 
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); 
49281  389 

390 
fun has_undefined_rhs thm = 

391 
(case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of 

392 
Const (@{const_name undefined}, _) => true 

393 
 _ => false); 

394 

49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

395 
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; 
49281  396 

397 
val all_sel_thms = 

49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

398 
(if all_sels_distinct andalso forall null sel_defaultss then 
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

399 
flat sel_thmss 
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

400 
else 
49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

401 
map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

402 
(xss' ~~ case_thms)) 
49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

403 
> filter_out has_undefined_rhs; 
49278  404 

405 
fun mk_unique_disc_def () = 

406 
let 

407 
val m = the_single ms; 

49486  408 
val goal = mk_Trueprop_eq (mk_u_eq_u (), the_single exist_xs_u_eq_ctrs); 
49278  409 
in 
49486  410 
Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm) 
49278  411 
> singleton (Proof_Context.export names_lthy lthy) 
412 
> Thm.close_derivation 

413 
end; 

414 

415 
fun mk_alternate_disc_def k = 

416 
let 

417 
val goal = 

49486  418 
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3  k), 
419 
nth exist_xs_u_eq_ctrs (k  1)); 

49278  420 
in 
421 
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 

422 
mk_alternate_disc_def_tac ctxt k (nth disc_defs (2  k)) 

49486  423 
(nth distinct_thms (2  k)) uexhaust_thm) 
49278  424 
> singleton (Proof_Context.export names_lthy lthy) 
425 
> Thm.close_derivation 

426 
end; 

49028  427 

49278  428 
val has_alternate_disc_def = 
429 
exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs; 

430 

431 
val disc_defs' = 

432 
map2 (fn k => fn def => 

433 
if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def () 

434 
else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k 

435 
else def) ks disc_defs; 

436 

437 
val discD_thms = map (fn def => def RS iffD1) disc_defs'; 

438 
val discI_thms = 

439 
map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms 

440 
disc_defs'; 

441 
val not_discI_thms = 

442 
map2 (fn m => fn def => funpow m (fn thm => allI RS thm) 

49463  443 
(unfold_defs lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) 
49278  444 
ms disc_defs'; 
445 

446 
val (disc_thmss', disc_thmss) = 

447 
let 

448 
fun mk_thm discI _ [] = refl RS discI 

449 
 mk_thm _ not_discI [distinct] = distinct RS not_discI; 

450 
fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss; 

451 
in 

452 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 

453 
end; 

454 

455 
val disc_thms = flat (map2 (fn true => K []  false => I) no_discs disc_thmss); 

49028  456 

49486  457 
val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = 
458 
let 

459 
fun mk_goal [] = [] 

460 
 mk_goal [((_, udisc), (_, udisc'))] = 

461 
[Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc, 

462 
HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))]; 

463 

464 
fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); 

465 

466 
val infos = ms ~~ discD_thms ~~ udiscs; 

467 
val half_pairss = mk_half_pairss infos; 

468 

469 
val half_goalss = map mk_goal half_pairss; 

470 
val half_thmss = 

471 
map3 (fn [] => K (K [])  [goal] => fn [(((m, discD), _), _)] => 

472 
fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal]) 

473 
half_goalss half_pairss (flat disc_thmss'); 

49278  474 

49486  475 
val other_half_goalss = map (mk_goal o map swap) half_pairss; 
476 
val other_half_thmss = 

477 
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss 

478 
other_half_goalss; 

479 
in 

480 
join_halves n half_thmss other_half_thmss 

481 
>> has_alternate_disc_def ? K [] 

482 
end; 

49278  483 

49486  484 
val disc_exhaust_thm = 
485 
let 

486 
fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc]; 

487 
val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs)); 

488 
in 

489 
Skip_Proof.prove lthy [] [] goal (fn _ => 

490 
mk_disc_exhaust_tac n exhaust_thm discI_thms) 

491 
end; 

49028  492 

49278  493 
val disc_exhaust_thms = 
49486  494 
if has_alternate_disc_def orelse no_discs_at_all then [] else [disc_exhaust_thm]; 
495 

496 
val (collapse_thms, collapse_thm_opts) = 

497 
let 

498 
fun mk_goal ctr udisc usels = 

499 
let 

500 
val prem = HOLogic.mk_Trueprop udisc; 

501 
val concl = 

502 
mk_Trueprop_eq ((null usels ? swap) (Term.list_comb (ctr, usels), u)); 

503 
in 

504 
if prem aconv concl then NONE 

505 
else SOME (Logic.all u (Logic.mk_implies (prem, concl))) 

506 
end; 

507 
val goals = map3 mk_goal ctrs udiscs uselss; 

508 
in 

509 
map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => 

510 
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 

511 
mk_collapse_tac ctxt m discD sel_thms) 

512 
> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals 

513 
> `(map_filter I) 

514 
end; 

49025  515 

49486  516 
val expand_thms = 
517 
let 

518 
fun mk_prems k udisc usels vdisc vsels = 

519 
(if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @ 

520 
(if null usels then 

521 
[] 

522 
else 

523 
[Logic.list_implies 

524 
(if n = 1 then [] else map HOLogic.mk_Trueprop [udisc, vdisc], 

525 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 

526 
(map2 (curry HOLogic.mk_eq) usels vsels)))]); 

527 

528 
val uncollapse_thms = 

529 
map (fn NONE => Drule.dummy_thm  SOME thm => thm RS sym) collapse_thm_opts; 

530 

531 
val goal = 

532 
Library.foldr Logic.list_implies 

533 
(map5 mk_prems ks udiscs uselss vdiscs vselss, u_eq_v); 

534 
in 

535 
[Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 

536 
mk_expand_tac ctxt n ms (inst_thm u disc_exhaust_thm) 

537 
(inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss 

538 
disc_exclude_thmsss')] 

539 
> Proof_Context.export names_lthy lthy 

540 
end; 

49278  541 

542 
val case_eq_thms = 

49486  543 
let 
544 
fun mk_body f usels = Term.list_comb (f, usels); 

545 
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss)); 

546 
in 

547 
[Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 

548 
mk_case_eq_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] 

549 
> Proof_Context.export names_lthy lthy 

550 
end; 

49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

551 
in 
49484  552 
(all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, 
49486  553 
disc_exhaust_thms, collapse_thms, expand_thms, case_eq_thms) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

554 
end; 
49025  555 

49033  556 
val (case_cong_thm, weak_case_cong_thm) = 
49032  557 
let 
558 
fun mk_prem xctr xs f g = 

49486  559 
fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr), 
49032  560 
mk_Trueprop_eq (f, g))); 
49033  561 

49032  562 
val goal = 
49486  563 
Logic.list_implies (u_eq_v :: map4 mk_prem xctrs xss fs gs, 
564 
mk_Trueprop_eq (ufcase, vgcase)); 

565 
val weak_goal = Logic.mk_implies (u_eq_v, mk_Trueprop_eq (ufcase, vfcase)); 

49032  566 
in 
49486  567 
(Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms), 
49458  568 
Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1))) 
49033  569 
> pairself (singleton (Proof_Context.export names_lthy lthy)) 
49032  570 
end; 
49025  571 

49044  572 
val (split_thm, split_asm_thm) = 
49043  573 
let 
49044  574 
fun mk_conjunct xctr xs f_xs = 
49486  575 
list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs)); 
49044  576 
fun mk_disjunct xctr xs f_xs = 
49486  577 
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), 
49044  578 
HOLogic.mk_not (q $ f_xs))); 
579 

49486  580 
val lhs = q $ ufcase; 
49044  581 

49043  582 
val goal = 
49044  583 
mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); 
49458  584 
val asm_goal = 
49044  585 
mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj 
586 
(map3 mk_disjunct xctrs xss xfs))); 

587 

588 
val split_thm = 

49049  589 
Skip_Proof.prove lthy [] [] goal 
49486  590 
(fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss) 
49044  591 
> singleton (Proof_Context.export names_lthy lthy) 
592 
val split_asm_thm = 

49458  593 
Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} => 
49044  594 
mk_split_asm_tac ctxt split_thm) 
595 
> singleton (Proof_Context.export names_lthy lthy) 

49043  596 
in 
49044  597 
(split_thm, split_asm_thm) 
49043  598 
end; 
49025  599 

49437  600 
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); 
49300  601 
val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name)); 
602 

49052  603 
val notes = 
49300  604 
[(case_congN, [case_cong_thm], []), 
605 
(case_eqN, case_eq_thms, []), 

606 
(casesN, case_thms, simp_attrs), 

607 
(collapseN, collapse_thms, simp_attrs), 

608 
(discsN, disc_thms, simp_attrs), 

609 
(disc_excludeN, disc_exclude_thms, []), 

610 
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), 

611 
(distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), 

612 
(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]), 

49486  613 
(expandN, expand_thms, []), 
49438  614 
(injectN, inject_thms, iff_attrs @ induct_simp_attrs), 
49300  615 
(nchotomyN, [nchotomy_thm], []), 
616 
(selsN, all_sel_thms, simp_attrs), 

617 
(splitN, [split_thm], []), 

618 
(split_asmN, [split_asm_thm], []), 

619 
(weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] 

620 
> filter_out (null o #2) 

621 
> map (fn (thmN, thms, attrs) => 

49302
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

622 
((Binding.qualify true (Binding.name_of data_b) (Binding.name thmN), attrs), 
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

623 
[(thms, [])])); 
49300  624 

625 
val notes' = 

626 
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)] 

627 
> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); 

49019  628 
in 
49484  629 
((discs, selss, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms, sel_thmss), 
49438  630 
lthy > Local_Theory.notes (notes' @ notes) > snd) 
49019  631 
end; 
49017  632 
in 
49121  633 
(goalss, after_qed, lthy') 
49017  634 
end; 
635 

49199  636 
fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) => 
49111  637 
map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

638 
> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I); 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

639 

49297  640 
val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) => 
641 
Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo 

642 
prepare_wrap_datatype Syntax.read_term; 

643 

49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

644 
fun parse_bracket_list parser = @{keyword "["}  Parse.list parser  @{keyword "]"}; 
49111  645 

49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

646 
val parse_bindings = parse_bracket_list Parse.binding; 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

647 
val parse_bindingss = parse_bracket_list parse_bindings; 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

648 

52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

649 
val parse_bound_term = (Parse.binding  @{keyword ":"})  Parse.term; 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

650 
val parse_bound_terms = parse_bracket_list parse_bound_term; 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

651 
val parse_bound_termss = parse_bracket_list parse_bound_terms; 
49017  652 

49278  653 
val parse_wrap_options = 
654 
Scan.optional (@{keyword "("}  (@{keyword "no_dests"} >> K true)  @{keyword ")"}) false; 

655 

49017  656 
val _ = 
49074  657 
Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype" 
49278  658 
((parse_wrap_options  (@{keyword "["}  Parse.list Parse.term  @{keyword "]"})  
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

659 
Parse.term  Scan.optional (parse_bindings  Scan.optional (parse_bindingss  
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

660 
Scan.optional parse_bound_termss []) ([], [])) ([], ([], []))) 
49199  661 
>> wrap_datatype_cmd); 
49017  662 

663 
end; 