author  blanchet 
Fri, 08 Mar 2013 14:15:39 +0100  
changeset 51380  cac8c9a636b6 
parent 50214  67fb9a168d10 
child 51551  88d1d19fb74f 
permissions  rwrr 
49509
163914705f8d
renamed toplevel theory from "Codatatype" to "BNF"
blanchet
parents:
49504
diff
changeset

1 
(* Title: HOL/BNF/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 
49633  10 
val rep_compat_prefix: string 
11 

49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

12 
val mk_half_pairss: 'a list * 'a list > ('a * 'a) list list 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

13 
val join_halves: int > 'a list list > 'a list list > 'a list * 'a list list list 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

14 

49203  15 
val mk_ctr: typ list > term > term 
49484  16 
val mk_disc_or_sel: typ list > term > term 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

17 

49622  18 
val name_of_ctr: term > string 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

19 

49199  20 
val wrap_datatype: ({prems: thm list, context: Proof.context} > tactic) list list > 
49633  21 
(((bool * bool) * term list) * term) * 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

22 
(binding list * (binding list list * (binding * term) list list)) > local_theory > 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

23 
(term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list * 
49484  24 
thm list list) * local_theory 
49633  25 
val parse_wrap_options: (bool * bool) parser 
49286  26 
val parse_bound_term: (binding * string) parser 
49017  27 
end; 
28 

49074  29 
structure BNF_Wrap : BNF_WRAP = 
49017  30 
struct 
31 

32 
open BNF_Util 

49074  33 
open BNF_Wrap_Tactics 
49017  34 

49633  35 
val rep_compat_prefix = "new"; 
36 

49223  37 
val isN = "is_"; 
38 
val unN = "un_"; 

39 
fun mk_unN 1 1 suf = unN ^ suf 

40 
 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

41 

49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

42 
val caseN = "case"; 
49054  43 
val case_congN = "case_cong"; 
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

44 
val case_convN = "case_conv"; 
49118  45 
val collapseN = "collapse"; 
49122  46 
val disc_excludeN = "disc_exclude"; 
49054  47 
val disc_exhaustN = "disc_exhaust"; 
48 
val discsN = "discs"; 

49 
val distinctN = "distinct"; 

49075  50 
val exhaustN = "exhaust"; 
49486  51 
val expandN = "expand"; 
49075  52 
val injectN = "inject"; 
53 
val nchotomyN = "nchotomy"; 

49054  54 
val selsN = "sels"; 
55 
val splitN = "split"; 

49633  56 
val splitsN = "splits"; 
49054  57 
val split_asmN = "split_asm"; 
58 
val weak_case_cong_thmsN = "weak_case_cong"; 

49019  59 

49336  60 
val std_binding = @{binding _}; 
49300  61 

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

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

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

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

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

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

67 

49056  68 
fun pad_list x n xs = xs @ replicate (n  length xs) x; 
69 

49259  70 
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

71 

49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

72 
fun mk_half_pairss' _ ([], []) = [] 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

73 
 mk_half_pairss' indent (x :: xs, _ :: ys) = 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

74 
indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys)); 
49486  75 

49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

76 
fun mk_half_pairss p = mk_half_pairss' [[]] p; 
49027  77 

49486  78 
fun join_halves n half_xss other_half_xss = 
79 
let 

80 
val xsss = 

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

82 
(transpose (Library.chop_groups n other_half_xss)) 

49668  83 
val xs = splice (flat half_xss) (flat other_half_xss); 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

84 
in (xs, xsss) end; 
49027  85 

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

86 
fun mk_undefined T = Const (@{const_name undefined}, T); 
49055  87 

49500  88 
fun mk_ctr Ts t = 
89 
let val Type (_, Ts0) = body_type (fastype_of t) in 

90 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

49203  91 
end; 
92 

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

95 

49536  96 
fun mk_case Ts T t = 
97 
let val (Type (_, Ts0), body) = strip_type (fastype_of t) >> List.last in 

98 
Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t 

99 
end; 

100 

49622  101 
fun name_of_ctr c = 
102 
(case head_of c of 

103 
Const (s, _) => s 

104 
 Free (s, _) => s 

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

106 

107 
val base_name_of_ctr = Long_Name.base_name o name_of_ctr; 

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

108 

49437  109 
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
110 

49633  111 
fun prepare_wrap_datatype prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case), 
49336  112 
(raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy = 
49017  113 
let 
49019  114 
(* TODO: sanity checks on arguments *) 
49113  115 
(* TODO: case syntax *) 
49025  116 

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

117 
val n = length raw_ctrs; 
49054  118 
val ks = 1 upto n; 
119 

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

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

122 
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

123 
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

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

125 
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

126 

49300  127 
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

128 
val data_b = Binding.qualified_name dataT_name; 
49498  129 
val data_b_name = Binding.name_of data_b; 
49055  130 

49633  131 
fun qualify mandatory = 
132 
Binding.qualify mandatory data_b_name o 

133 
(rep_compat ? Binding.qualify false rep_compat_prefix); 

134 

49055  135 
val (As, B) = 
136 
no_defs_lthy 

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

137 
> mk_TFrees' (map Type.sort_of_atyp As0) 
49055  138 
> the_single o fst o mk_TFrees 1; 
139 

49300  140 
val dataT = Type (dataT_name, As); 
49055  141 
val ctrs = map (mk_ctr As) ctrs0; 
142 
val ctr_Tss = map (binder_types o fastype_of) ctrs; 

143 

144 
val ms = map length ctr_Tss; 

145 

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

146 
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

147 

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

148 
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

149 
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

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

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

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

154 
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

155 

49633  156 
val std_disc_binding = qualify false 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

157 

49336  158 
val disc_bindings = 
159 
raw_disc_bindings' 

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

160 
> map4 (fn k => fn m => fn ctr => fn disc => 
49633  161 
Option.map (qualify false) 
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

162 
(if Binding.eq_name (disc, Binding.empty) then 
49336  163 
if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr) 
164 
else if Binding.eq_name (disc, std_binding) then 

165 
SOME (std_disc_binding ctr) 

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

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

167 
SOME disc)) ks ms ctrs0; 
49056  168 

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

170 

49336  171 
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

172 

49336  173 
val sel_bindingss = 
174 
pad_list [] n raw_sel_bindingss 

49056  175 
> map3 (fn ctr => fn m => map2 (fn l => fn sel => 
49633  176 
qualify false 
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

177 
(if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then 
49336  178 
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

179 
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

180 
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

181 

49536  182 
val casex = mk_case As B case0; 
49201  183 
val case_Ts = map (fn Ts => Ts > B) ctr_Tss; 
49043  184 

49498  185 
val (((((((xss, xss'), yss), fs), gs), [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

186 
mk_Freess' "x" ctr_Tss 
49025  187 
>> mk_Freess "y" ctr_Tss 
49201  188 
>> mk_Frees "f" case_Ts 
189 
>> mk_Frees "g" case_Ts 

49498  190 
>> (apfst (map (rpair dataT)) oo Variable.variant_fixes) [data_b_name, data_b_name ^ "'"] 
49043  191 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; 
192 

49498  193 
val u = Free u'; 
194 
val v = Free v'; 

49463  195 
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

196 

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

49032  199 

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

202 

49437  203 
val eta_fs = map2 eta_expand_arg xss xfs; 
204 
val eta_gs = map2 eta_expand_arg xss xgs; 

49043  205 

49201  206 
val fcase = Term.list_comb (casex, eta_fs); 
207 
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

208 

49486  209 
val ufcase = fcase $ u; 
210 
val vfcase = fcase $ v; 

211 
val vgcase = gcase $ v; 

212 

49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

213 
fun mk_uu_eq () = HOLogic.mk_eq (u, u); 
49486  214 

49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

215 
val uv_eq = mk_Trueprop_eq (u, v); 
49486  216 

217 
val exist_xs_u_eq_ctrs = 

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

49022  219 

49278  220 
val unique_disc_no_def = TrueI; (*arbitrary marker*) 
221 
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

222 

49486  223 
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

224 
HOLogic.mk_not 
49336  225 
(case nth disc_bindings (k  1) of 
49486  226 
NONE => nth exist_xs_u_eq_ctrs (k  1) 
227 
 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

228 

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

49278  231 
if no_dests then 
49486  232 
(true, [], [], [], [], [], [], [], [], [], no_defs_lthy) 
49278  233 
else 
234 
let 

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

49486  237 
fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr); 
49278  238 

49500  239 
fun alternate_disc k = 
240 
Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3  k)); 

49278  241 

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

242 
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

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

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

245 
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

246 
(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

247 
NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T) 
51380  248 
 SOME t => t > Type.constraint (Ts > T) > Syntax.check_term no_defs_lthy) 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

249 
 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

250 

49278  251 
fun sel_spec b proto_sels = 
252 
let 

253 
val _ = 

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

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

256 
" for constructor " ^ 

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

258 
 [] => ()) 

259 
val T = 

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

261 
[T] => T 

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

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

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

265 
in 

49486  266 
mk_Trueprop_eq (Free (Binding.name_of b, dataT > T) $ u, 
49536  267 
Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u) 
49278  268 
end; 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

269 

49336  270 
val sel_bindings = flat sel_bindingss; 
271 
val uniq_sel_bindings = distinct Binding.eq_name sel_bindings; 

272 
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

273 

49336  274 
val sel_binding_index = 
275 
if all_sels_distinct then 1 upto length sel_bindings 

276 
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

277 

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

278 
val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss); 
49300  279 
val sel_infos = 
49336  280 
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

281 
> sort (int_ord o pairself fst) 
49336  282 
> map snd > curry (op ~~) uniq_sel_bindings; 
283 
val sel_bindings = map fst sel_infos; 

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

284 

49336  285 
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

286 

49278  287 
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = 
288 
no_defs_lthy 

49486  289 
> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => 
49278  290 
fn NONE => 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

291 
if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) 
49486  292 
else if m = 0 then pair (Term.lambda u exist_xs_u_eq_ctr, refl) 
49278  293 
else pair (alternate_disc k, alternate_disc_no_def) 
294 
 SOME b => Specification.definition (SOME (b, NONE, NoSyn), 

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

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

49300  299 
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos 
49278  300 
> `Local_Theory.restore; 
49022  301 

49278  302 
val phi = Proof_Context.export_morphism lthy lthy'; 
49025  303 

49278  304 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
49281  305 
val sel_defs = map (Morphism.thm phi) raw_sel_defs; 
306 
val sel_defss = unflat_selss sel_defs; 

49278  307 

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

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

49028  310 

49278  311 
val discs = map (mk_disc_or_sel As) discs0; 
312 
val selss = map (map (mk_disc_or_sel As)) selss0; 

49486  313 

49500  314 
val udiscs = map (rapp u) discs; 
315 
val uselss = map (map (rapp u)) selss; 

49486  316 

49500  317 
val vdiscs = map (rapp v) discs; 
318 
val vselss = map (map (rapp v)) selss; 

49278  319 
in 
49486  320 
(all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs, 
321 
sel_defss, lthy') 

49278  322 
end; 
49025  323 

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

49458  326 
val exhaust_goal = 
49486  327 
let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in 
328 
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

329 
end; 
49019  330 

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

333 
fun mk_goal _ _ [] [] = [] 
49025  334 
 mk_goal xctr yctr xs ys = 
49121  335 
[fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), 
336 
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; 

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

338 
map4 mk_goal xctrs yctrs xss yss 
49017  339 
end; 
340 

49484  341 
val half_distinct_goalss = 
49121  342 
let 
49203  343 
fun mk_goal ((xs, xc), (xs', xc')) = 
49121  344 
fold_rev Logic.all (xs @ xs') 
49203  345 
(HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc')))); 
49121  346 
in 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

347 
map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs))) 
49121  348 
end; 
49019  349 

49458  350 
val cases_goal = 
49121  351 
map3 (fn xs => fn xctr => fn xf => 
49201  352 
fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs; 
49025  353 

49484  354 
val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal]; 
49019  355 

356 
fun after_qed thmss lthy = 

357 
let 

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

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

359 
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); 
49019  360 

49438  361 
val inject_thms = flat inject_thmss; 
362 

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

365 
fun inst_thm t thm = 

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

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

368 

369 
val uexhaust_thm = inst_thm u exhaust_thm; 

49032  370 

49300  371 
val exhaust_cases = map base_name_of_ctr ctrs; 
372 

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

373 
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

374 

49486  375 
val (distinct_thms, (distinct_thmsss', distinct_thmsss)) = 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

376 
join_halves n half_distinct_thmss other_half_distinct_thmss > `transpose; 
49019  377 

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

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

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

380 
val goal = 
49486  381 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u', 
382 
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

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

384 
Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) 
49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

385 
> Thm.close_derivation 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

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

387 

49484  388 
val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, 
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

389 
disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) = 
49278  390 
if no_dests then 
49486  391 
([], [], [], [], [], [], [], [], [], []) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

393 
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

394 
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

395 
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

396 
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); 
49281  397 

398 
fun has_undefined_rhs thm = 

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

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

401 
 _ => false); 

402 

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

403 
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; 
49281  404 

405 
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

406 
(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

407 
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

408 
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

409 
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

410 
(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

411 
> filter_out has_undefined_rhs; 
49278  412 

413 
fun mk_unique_disc_def () = 

414 
let 

415 
val m = the_single ms; 

49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

416 
val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs); 
49278  417 
in 
49486  418 
Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm) 
49692  419 
> Thm.close_derivation 
49278  420 
> singleton (Proof_Context.export names_lthy lthy) 
421 
end; 

422 

423 
fun mk_alternate_disc_def k = 

424 
let 

425 
val goal = 

49486  426 
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3  k), 
427 
nth exist_xs_u_eq_ctrs (k  1)); 

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

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

49486  431 
(nth distinct_thms (2  k)) uexhaust_thm) 
49692  432 
> Thm.close_derivation 
49278  433 
> singleton (Proof_Context.export names_lthy lthy) 
434 
end; 

49028  435 

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

438 

439 
val disc_defs' = 

440 
map2 (fn k => fn def => 

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

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

443 
else def) ks disc_defs; 

444 

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

446 
val discI_thms = 

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

448 
disc_defs'; 

449 
val not_discI_thms = 

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

49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49500
diff
changeset

451 
(unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) 
49278  452 
ms disc_defs'; 
453 

454 
val (disc_thmss', disc_thmss) = 

455 
let 

456 
fun mk_thm discI _ [] = refl RS discI 

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

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

459 
in 

460 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 

461 
end; 

462 

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

49028  464 

49486  465 
val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = 
466 
let 

467 
fun mk_goal [] = [] 

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

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

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

471 

49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

472 
fun prove tac goal = 
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

473 
Skip_Proof.prove lthy [] [] goal (K tac) 
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

474 
> Thm.close_derivation; 
49486  475 

49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

476 
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs)); 
49486  477 

478 
val half_goalss = map mk_goal half_pairss; 

479 
val half_thmss = 

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

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

482 
half_goalss half_pairss (flat disc_thmss'); 

49278  483 

49486  484 
val other_half_goalss = map (mk_goal o map swap) half_pairss; 
485 
val other_half_thmss = 

486 
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss 

487 
other_half_goalss; 

488 
in 

49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

489 
join_halves n half_thmss other_half_thmss > `transpose 
49486  490 
>> has_alternate_disc_def ? K [] 
491 
end; 

49278  492 

49486  493 
val disc_exhaust_thm = 
494 
let 

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

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

497 
in 

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

499 
mk_disc_exhaust_tac n exhaust_thm discI_thms) 

49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

500 
> Thm.close_derivation 
49486  501 
end; 
49028  502 

49486  503 
val (collapse_thms, collapse_thm_opts) = 
504 
let 

505 
fun mk_goal ctr udisc usels = 

506 
let 

507 
val prem = HOLogic.mk_Trueprop udisc; 

508 
val concl = 

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

510 
in 

511 
if prem aconv concl then NONE 

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

513 
end; 

514 
val goals = map3 mk_goal ctrs udiscs uselss; 

515 
in 

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

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

518 
mk_collapse_tac ctxt m discD sel_thms) 

49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

519 
> Thm.close_derivation 
49486  520 
> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals 
521 
> `(map_filter I) 

522 
end; 

49025  523 

49486  524 
val expand_thms = 
525 
let 

526 
fun mk_prems k udisc usels vdisc vsels = 

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

528 
(if null usels then 

529 
[] 

530 
else 

531 
[Logic.list_implies 

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

533 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 

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

535 

49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

536 
val goal = 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

537 
Library.foldr Logic.list_implies 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

538 
(map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq); 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

539 

49486  540 
val uncollapse_thms = 
541 
map (fn NONE => Drule.dummy_thm  SOME thm => thm RS sym) collapse_thm_opts; 

542 
in 

49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

543 
[Skip_Proof.prove lthy [] [] goal (fn _ => 
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

544 
mk_expand_tac n ms (inst_thm u disc_exhaust_thm) 
49486  545 
(inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss 
546 
disc_exclude_thmsss')] 

49692  547 
> map Thm.close_derivation 
49486  548 
> Proof_Context.export names_lthy lthy 
549 
end; 

49278  550 

49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

551 
val case_conv_thms = 
49486  552 
let 
553 
fun mk_body f usels = Term.list_comb (f, usels); 

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

555 
in 

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

49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

557 
mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] 
49692  558 
> map Thm.close_derivation 
49486  559 
> Proof_Context.export names_lthy lthy 
560 
end; 

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

561 
in 
49484  562 
(all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, 
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

563 
[disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

564 
end; 
49025  565 

49033  566 
val (case_cong_thm, weak_case_cong_thm) = 
49032  567 
let 
568 
fun mk_prem xctr xs f g = 

49486  569 
fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr), 
49032  570 
mk_Trueprop_eq (f, g))); 
49033  571 

49032  572 
val goal = 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

573 
Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss fs gs, 
49486  574 
mk_Trueprop_eq (ufcase, vgcase)); 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

575 
val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); 
49032  576 
in 
49486  577 
(Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms), 
49458  578 
Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1))) 
49692  579 
> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy)) 
49032  580 
end; 
49025  581 

49044  582 
val (split_thm, split_asm_thm) = 
49043  583 
let 
49044  584 
fun mk_conjunct xctr xs f_xs = 
49486  585 
list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs)); 
49044  586 
fun mk_disjunct xctr xs f_xs = 
49486  587 
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), 
49044  588 
HOLogic.mk_not (q $ f_xs))); 
589 

49486  590 
val lhs = q $ ufcase; 
49044  591 

49043  592 
val goal = 
49044  593 
mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); 
49458  594 
val asm_goal = 
49044  595 
mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj 
596 
(map3 mk_disjunct xctrs xss xfs))); 

597 

598 
val split_thm = 

49049  599 
Skip_Proof.prove lthy [] [] goal 
49486  600 
(fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss) 
49692  601 
> Thm.close_derivation 
602 
> singleton (Proof_Context.export names_lthy lthy); 

49044  603 
val split_asm_thm = 
49458  604 
Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} => 
49044  605 
mk_split_asm_tac ctxt split_thm) 
49692  606 
> Thm.close_derivation 
607 
> singleton (Proof_Context.export names_lthy lthy); 

49043  608 
in 
49044  609 
(split_thm, split_asm_thm) 
49043  610 
end; 
49025  611 

49437  612 
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); 
49300  613 
val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name)); 
614 

49052  615 
val notes = 
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

616 
[(caseN, case_thms, simp_attrs), 
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

617 
(case_congN, [case_cong_thm], []), 
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49591
diff
changeset

618 
(case_convN, case_conv_thms, []), 
49300  619 
(collapseN, collapse_thms, simp_attrs), 
620 
(discsN, disc_thms, simp_attrs), 

621 
(disc_excludeN, disc_exclude_thms, []), 

622 
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), 

623 
(distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), 

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

49486  625 
(expandN, expand_thms, []), 
49438  626 
(injectN, inject_thms, iff_attrs @ induct_simp_attrs), 
49300  627 
(nchotomyN, [nchotomy_thm], []), 
628 
(selsN, all_sel_thms, simp_attrs), 

629 
(splitN, [split_thm], []), 

630 
(split_asmN, [split_asm_thm], []), 

49633  631 
(splitsN, [split_thm, split_asm_thm], []), 
49300  632 
(weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] 
633 
> filter_out (null o #2) 

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

49633  635 
((qualify true (Binding.name thmN), attrs), [(thms, [])])); 
49300  636 

637 
val notes' = 

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

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

49019  640 
in 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

641 
((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms, 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49586
diff
changeset

642 
sel_thmss), lthy > Local_Theory.notes (notes' @ notes) > snd) 
49019  643 
end; 
49017  644 
in 
49121  645 
(goalss, after_qed, lthy') 
49017  646 
end; 
647 

49199  648 
fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) => 
49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

649 
map2 (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])) goalss tacss 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

650 
> (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

651 

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

51380  654 
prepare_wrap_datatype Syntax.parse_term; 
49297  655 

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

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

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

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

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

660 

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

661 
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

662 
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

663 
val parse_bound_termss = parse_bracket_list parse_bound_terms; 
49017  664 

49278  665 
val parse_wrap_options = 
49633  666 
Scan.optional (@{keyword "("}  Parse.list1 ((@{keyword "no_dests"} >> K (true, false))  
667 
(@{keyword "rep_compat"} >> K (false, true)))  @{keyword ")"} 

668 
>> (pairself (exists I) o split_list)) (false, false); 

49278  669 

49017  670 
val _ = 
50214  671 
Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wrap an existing datatype" 
49278  672 
((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

673 
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

674 
Scan.optional parse_bound_termss []) ([], [])) ([], ([], []))) 
49199  675 
>> wrap_datatype_cmd); 
49017  676 

677 
end; 