author  blanchet 
Thu, 27 Sep 2012 18:39:17 +0200  
changeset 49622  a93f976c3307 
parent 49619  0e248756147a 
child 49633  5b5450bc544c 
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 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

10 
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

11 
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

12 

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

15 

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

17 

49199  18 
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

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

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

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

49074  27 
structure BNF_Wrap : BNF_WRAP = 
49017  28 
struct 
29 

30 
open BNF_Util 

49074  31 
open BNF_Wrap_Tactics 
49017  32 

49223  33 
val isN = "is_"; 
34 
val unN = "un_"; 

35 
fun mk_unN 1 1 suf = unN ^ suf 

36 
 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

37 

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

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

40 
val case_convN = "case_conv"; 
49118  41 
val collapseN = "collapse"; 
49122  42 
val disc_excludeN = "disc_exclude"; 
49054  43 
val disc_exhaustN = "disc_exhaust"; 
44 
val discsN = "discs"; 

45 
val distinctN = "distinct"; 

49075  46 
val exhaustN = "exhaust"; 
49486  47 
val expandN = "expand"; 
49075  48 
val injectN = "inject"; 
49 
val nchotomyN = "nchotomy"; 

49054  50 
val selsN = "sels"; 
51 
val splitN = "split"; 

52 
val split_asmN = "split_asm"; 

53 
val weak_case_cong_thmsN = "weak_case_cong"; 

49019  54 

49336  55 
val std_binding = @{binding _}; 
49300  56 

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

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

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

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

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

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

62 

49056  63 
fun pad_list x n xs = xs @ replicate (n  length xs) x; 
64 

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

66 

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

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

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

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

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

71 
fun mk_half_pairss p = mk_half_pairss' [[]] p; 
49027  72 

49486  73 
fun join_halves n half_xss other_half_xss = 
74 
let 

75 
val xsss = 

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

77 
(transpose (Library.chop_groups n other_half_xss)) 

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

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

79 
in (xs, xsss) end; 
49027  80 

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

81 
fun mk_undefined T = Const (@{const_name undefined}, T); 
49055  82 

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

85 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

49203  86 
end; 
87 

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

90 

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

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

94 
end; 

95 

49622  96 
fun name_of_ctr c = 
97 
(case head_of c of 

98 
Const (s, _) => s 

99 
 Free (s, _) => s 

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

101 

102 
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

103 

49437  104 
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
105 

49278  106 
fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case), 
49336  107 
(raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy = 
49017  108 
let 
49019  109 
(* TODO: sanity checks on arguments *) 
49113  110 
(* TODO: case syntax *) 
49025  111 

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

112 
val n = length raw_ctrs; 
49054  113 
val ks = 1 upto n; 
114 

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

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

117 
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

118 
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

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

120 
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

121 

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

123 
val data_b = Binding.qualified_name dataT_name; 
49498  124 
val data_b_name = Binding.name_of data_b; 
49055  125 

126 
val (As, B) = 

127 
no_defs_lthy 

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

128 
> mk_TFrees' (map Type.sort_of_atyp As0) 
49055  129 
> the_single o fst o mk_TFrees 1; 
130 

49300  131 
val dataT = Type (dataT_name, As); 
49055  132 
val ctrs = map (mk_ctr As) ctrs0; 
133 
val ctr_Tss = map (binder_types o fastype_of) ctrs; 

134 

135 
val ms = map length ctr_Tss; 

136 

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

137 
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

138 

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

139 
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

140 
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

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

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

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

145 
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

146 

49336  147 
val std_disc_binding = 
49498  148 
Binding.qualify false data_b_name 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

149 

49336  150 
val disc_bindings = 
151 
raw_disc_bindings' 

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

152 
> map4 (fn k => fn m => fn ctr => fn disc => 
49498  153 
Option.map (Binding.qualify false data_b_name) 
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

154 
(if Binding.eq_name (disc, Binding.empty) then 
49336  155 
if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr) 
156 
else if Binding.eq_name (disc, std_binding) then 

157 
SOME (std_disc_binding ctr) 

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

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

159 
SOME disc)) ks ms ctrs0; 
49056  160 

49336  161 
val no_discs = map is_none disc_bindings; 
49137  162 
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

163 

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

165 

49336  166 
val sel_bindingss = 
167 
pad_list [] n raw_sel_bindingss 

49056  168 
> map3 (fn ctr => fn m => map2 (fn l => fn sel => 
49498  169 
Binding.qualify false data_b_name 
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

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

172 
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

173 
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

174 

49536  175 
val casex = mk_case As B case0; 
49201  176 
val case_Ts = map (fn Ts => Ts > B) ctr_Tss; 
49043  177 

49498  178 
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

179 
mk_Freess' "x" ctr_Tss 
49025  180 
>> mk_Freess "y" ctr_Tss 
49201  181 
>> mk_Frees "f" case_Ts 
182 
>> mk_Frees "g" case_Ts 

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

49498  186 
val u = Free u'; 
187 
val v = Free v'; 

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

189 

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

49032  192 

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

195 

49437  196 
val eta_fs = map2 eta_expand_arg xss xfs; 
197 
val eta_gs = map2 eta_expand_arg xss xgs; 

49043  198 

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

201 

49486  202 
val ufcase = fcase $ u; 
203 
val vfcase = fcase $ v; 

204 
val vgcase = gcase $ v; 

205 

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

206 
fun mk_uu_eq () = HOLogic.mk_eq (u, u); 
49486  207 

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

208 
val uv_eq = mk_Trueprop_eq (u, v); 
49486  209 

210 
val exist_xs_u_eq_ctrs = 

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

49022  212 

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

215 

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

217 
HOLogic.mk_not 
49336  218 
(case nth disc_bindings (k  1) of 
49486  219 
NONE => nth exist_xs_u_eq_ctrs (k  1) 
220 
 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

221 

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

49278  224 
if no_dests then 
49486  225 
(true, [], [], [], [], [], [], [], [], [], no_defs_lthy) 
49278  226 
else 
227 
let 

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

49486  230 
fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr); 
49278  231 

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

49278  234 

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

235 
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

236 
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

237 
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

238 
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

239 
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

240 

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

241 
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

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

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

244 
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

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

246 
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

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

248 
 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

249 

49278  250 
fun sel_spec b proto_sels = 
251 
let 

252 
val _ = 

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

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

255 
" for constructor " ^ 

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

257 
 [] => ()) 

258 
val T = 

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

260 
[T] => T 

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

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

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

264 
in 

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

268 

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

271 
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

272 

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

275 
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

276 

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

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

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

283 

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

285 

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

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

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

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

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

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

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

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

49278  306 

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

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

49028  309 

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

49486  312 

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

49486  315 

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

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

49278  321 
end; 
49025  322 

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

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

328 
end; 
49019  329 

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

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

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

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

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

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

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

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

355 
fun after_qed thmss lthy = 

356 
let 

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

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

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

49438  360 
val inject_thms = flat inject_thmss; 
361 

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

364 
fun inst_thm t thm = 

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

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

367 

368 
val uexhaust_thm = inst_thm u exhaust_thm; 

49032  369 

49300  370 
val exhaust_cases = map base_name_of_ctr ctrs; 
371 

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

372 
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

373 

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

375 
join_halves n half_distinct_thmss other_half_distinct_thmss > `transpose; 
49019  376 

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

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

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

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

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

383 
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

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

385 

49484  386 
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

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

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

391 
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

392 
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

393 
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

394 
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); 
49281  395 

396 
fun has_undefined_rhs thm = 

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

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

399 
 _ => false); 

400 

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 
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; 
49281  402 

403 
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

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

405 
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

406 
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

407 
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

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

409 
> filter_out has_undefined_rhs; 
49278  410 

411 
fun mk_unique_disc_def () = 

412 
let 

413 
val m = the_single ms; 

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

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

419 
end; 

420 

421 
fun mk_alternate_disc_def k = 

422 
let 

423 
val goal = 

49486  424 
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3  k), 
425 
nth exist_xs_u_eq_ctrs (k  1)); 

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

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

49486  429 
(nth distinct_thms (2  k)) uexhaust_thm) 
49278  430 
> singleton (Proof_Context.export names_lthy lthy) 
431 
> Thm.close_derivation 

432 
end; 

49028  433 

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

436 

437 
val disc_defs' = 

438 
map2 (fn k => fn def => 

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

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

441 
else def) ks disc_defs; 

442 

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

444 
val discI_thms = 

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

446 
disc_defs'; 

447 
val not_discI_thms = 

448 
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

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

452 
val (disc_thmss', disc_thmss) = 

453 
let 

454 
fun mk_thm discI _ [] = refl RS discI 

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

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

457 
in 

458 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 

459 
end; 

460 

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

49028  462 

49486  463 
val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = 
464 
let 

465 
fun mk_goal [] = [] 

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

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

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

469 

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

471 

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

472 
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs)); 
49486  473 

474 
val half_goalss = map mk_goal half_pairss; 

475 
val half_thmss = 

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

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

478 
half_goalss half_pairss (flat disc_thmss'); 

49278  479 

49486  480 
val other_half_goalss = map (mk_goal o map swap) half_pairss; 
481 
val other_half_thmss = 

482 
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss 

483 
other_half_goalss; 

484 
in 

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

485 
join_halves n half_thmss other_half_thmss > `transpose 
49486  486 
>> has_alternate_disc_def ? K [] 
487 
end; 

49278  488 

49486  489 
val disc_exhaust_thm = 
490 
let 

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

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

493 
in 

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

495 
mk_disc_exhaust_tac n exhaust_thm discI_thms) 

496 
end; 

49028  497 

49486  498 
val (collapse_thms, collapse_thm_opts) = 
499 
let 

500 
fun mk_goal ctr udisc usels = 

501 
let 

502 
val prem = HOLogic.mk_Trueprop udisc; 

503 
val concl = 

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

505 
in 

506 
if prem aconv concl then NONE 

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

508 
end; 

509 
val goals = map3 mk_goal ctrs udiscs uselss; 

510 
in 

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

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

513 
mk_collapse_tac ctxt m discD sel_thms) 

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

515 
> `(map_filter I) 

516 
end; 

49025  517 

49486  518 
val expand_thms = 
519 
let 

520 
fun mk_prems k udisc usels vdisc vsels = 

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

522 
(if null usels then 

523 
[] 

524 
else 

525 
[Logic.list_implies 

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

527 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 

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

529 

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

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

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

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

533 

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

536 
in 

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

538 
mk_expand_tac ctxt n ms (inst_thm u disc_exhaust_thm) 

539 
(inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss 

540 
disc_exclude_thmsss')] 

541 
> Proof_Context.export names_lthy lthy 

542 
end; 

49278  543 

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

544 
val case_conv_thms = 
49486  545 
let 
546 
fun mk_body f usels = Term.list_comb (f, usels); 

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

548 
in 

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

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

550 
mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] 
49486  551 
> Proof_Context.export names_lthy lthy 
552 
end; 

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

553 
in 
49484  554 
(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

555 
[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

556 
end; 
49025  557 

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

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

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

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

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

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

49486  582 
val lhs = q $ ufcase; 
49044  583 

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

589 

590 
val split_thm = 

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

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

49043  598 
in 
49044  599 
(split_thm, split_asm_thm) 
49043  600 
end; 
49025  601 

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

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

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

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

608 
(case_convN, case_conv_thms, []), 
49300  609 
(collapseN, collapse_thms, simp_attrs), 
610 
(discsN, disc_thms, simp_attrs), 

611 
(disc_excludeN, disc_exclude_thms, []), 

612 
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), 

613 
(distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), 

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

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

619 
(splitN, [split_thm], []), 

620 
(split_asmN, [split_asm_thm], []), 

621 
(weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] 

622 
> filter_out (null o #2) 

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

49498  624 
((Binding.qualify true data_b_name (Binding.name thmN), attrs), [(thms, [])])); 
49300  625 

626 
val notes' = 

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

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

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

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

631 
sel_thmss), lthy > Local_Theory.notes (notes' @ notes) > snd) 
49019  632 
end; 
49017  633 
in 
49121  634 
(goalss, after_qed, lthy') 
49017  635 
end; 
636 

49199  637 
fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) => 
49111  638 
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

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

640 

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

643 
prepare_wrap_datatype Syntax.read_term; 

644 

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

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

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

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

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

649 

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

650 
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

651 
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

652 
val parse_bound_termss = parse_bracket_list parse_bound_terms; 
49017  653 

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

656 

49017  657 
val _ = 
49074  658 
Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype" 
49278  659 
((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

660 
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

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

664 
end; 