author  blanchet 
Wed, 26 Sep 2012 10:01:00 +0200  
changeset 49594  55e798614c45 
parent 49591  91b228e26348 
child 49618  29be73b789f9 
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 

49437  16 
val base_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 
49278  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 

49300  96 
fun base_name_of_ctr c = 
97 
Long_Name.base_name (case head_of c of 

98 
Const (s, _) => s 

99 
 Free (s, _) => s 

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

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

101 

49437  102 
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
103 

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

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

110 
val n = length raw_ctrs; 
49054  111 
val ks = 1 upto n; 
112 

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

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

115 
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

116 
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

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

118 
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

119 

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

121 
val data_b = Binding.qualified_name dataT_name; 
49498  122 
val data_b_name = Binding.name_of data_b; 
49055  123 

124 
val (As, B) = 

125 
no_defs_lthy 

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

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

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

132 

133 
val ms = map length ctr_Tss; 

134 

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

135 
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

136 

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

137 
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

138 
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

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

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

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

143 
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

144 

49336  145 
val std_disc_binding = 
49498  146 
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

147 

49336  148 
val disc_bindings = 
149 
raw_disc_bindings' 

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

150 
> map4 (fn k => fn m => fn ctr => fn disc => 
49498  151 
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

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

155 
SOME (std_disc_binding ctr) 

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

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

157 
SOME disc)) ks ms ctrs0; 
49056  158 

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

161 

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

163 

49336  164 
val sel_bindingss = 
165 
pad_list [] n raw_sel_bindingss 

49056  166 
> map3 (fn ctr => fn m => map2 (fn l => fn sel => 
49498  167 
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

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

170 
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

171 
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

172 

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

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

177 
mk_Freess' "x" ctr_Tss 
49025  178 
>> mk_Freess "y" ctr_Tss 
49201  179 
>> mk_Frees "f" case_Ts 
180 
>> mk_Frees "g" case_Ts 

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

49498  184 
val u = Free u'; 
185 
val v = Free v'; 

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

187 

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

49032  190 

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

193 

49437  194 
val eta_fs = map2 eta_expand_arg xss xfs; 
195 
val eta_gs = map2 eta_expand_arg xss xgs; 

49043  196 

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

199 

49486  200 
val ufcase = fcase $ u; 
201 
val vfcase = fcase $ v; 

202 
val vgcase = gcase $ v; 

203 

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

204 
fun mk_uu_eq () = HOLogic.mk_eq (u, u); 
49486  205 

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

206 
val uv_eq = mk_Trueprop_eq (u, v); 
49486  207 

208 
val exist_xs_u_eq_ctrs = 

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

49022  210 

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

213 

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

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

219 

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

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

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

49486  228 
fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr); 
49278  229 

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

49278  232 

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

233 
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

234 
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

235 
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

236 
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

237 
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

238 

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

239 
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

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

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

242 
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

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

244 
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

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

246 
 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

247 

49278  248 
fun sel_spec b proto_sels = 
249 
let 

250 
val _ = 

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

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

253 
" for constructor " ^ 

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

255 
 [] => ()) 

256 
val T = 

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

258 
[T] => T 

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

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

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

262 
in 

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

266 

49336  267 
val sel_bindings = flat sel_bindingss; 
268 
val uniq_sel_bindings = distinct Binding.eq_name sel_bindings; 

269 
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

270 

49336  271 
val sel_binding_index = 
272 
if all_sels_distinct then 1 upto length sel_bindings 

273 
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

274 

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

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

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

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

281 

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

283 

49278  284 
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = 
285 
no_defs_lthy 

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

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

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

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

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

49278  299 
val phi = Proof_Context.export_morphism lthy lthy'; 
49025  300 

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

49278  304 

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

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

49028  307 

49278  308 
val discs = map (mk_disc_or_sel As) discs0; 
309 
val selss = map (map (mk_disc_or_sel As)) selss0; 

49486  310 

49500  311 
val udiscs = map (rapp u) discs; 
312 
val uselss = map (map (rapp u)) selss; 

49486  313 

49500  314 
val vdiscs = map (rapp v) discs; 
315 
val vselss = map (map (rapp v)) selss; 

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

49278  319 
end; 
49025  320 

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

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

326 
end; 
49019  327 

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

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

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

335 
map4 mk_goal xctrs yctrs xss yss 
49017  336 
end; 
337 

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

344 
map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs))) 
49121  345 
end; 
49019  346 

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

49484  351 
val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal]; 
49019  352 

353 
fun after_qed thmss lthy = 

354 
let 

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

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

356 
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); 
49019  357 

49438  358 
val inject_thms = flat inject_thmss; 
359 

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

362 
fun inst_thm t thm = 

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

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

365 

366 
val uexhaust_thm = inst_thm u exhaust_thm; 

49032  367 

49300  368 
val exhaust_cases = map base_name_of_ctr ctrs; 
369 

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

370 
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

371 

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

373 
join_halves n half_distinct_thmss other_half_distinct_thmss > `transpose; 
49019  374 

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

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

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

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

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

381 
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

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

383 

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

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

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

389 
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

390 
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

391 
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

392 
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); 
49281  393 

394 
fun has_undefined_rhs thm = 

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

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

397 
 _ => false); 

398 

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

399 
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; 
49281  400 

401 
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

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

403 
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

404 
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

405 
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

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

407 
> filter_out has_undefined_rhs; 
49278  408 

409 
fun mk_unique_disc_def () = 

410 
let 

411 
val m = the_single ms; 

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

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

417 
end; 

418 

419 
fun mk_alternate_disc_def k = 

420 
let 

421 
val goal = 

49486  422 
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3  k), 
423 
nth exist_xs_u_eq_ctrs (k  1)); 

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

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

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

430 
end; 

49028  431 

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

434 

435 
val disc_defs' = 

436 
map2 (fn k => fn def => 

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

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

439 
else def) ks disc_defs; 

440 

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

442 
val discI_thms = 

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

444 
disc_defs'; 

445 
val not_discI_thms = 

446 
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

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

450 
val (disc_thmss', disc_thmss) = 

451 
let 

452 
fun mk_thm discI _ [] = refl RS discI 

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

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

455 
in 

456 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 

457 
end; 

458 

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

49028  460 

49486  461 
val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = 
462 
let 

463 
fun mk_goal [] = [] 

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

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

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

467 

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

469 

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

470 
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs)); 
49486  471 

472 
val half_goalss = map mk_goal half_pairss; 

473 
val half_thmss = 

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

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

476 
half_goalss half_pairss (flat disc_thmss'); 

49278  477 

49486  478 
val other_half_goalss = map (mk_goal o map swap) half_pairss; 
479 
val other_half_thmss = 

480 
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss 

481 
other_half_goalss; 

482 
in 

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

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

49278  486 

49486  487 
val disc_exhaust_thm = 
488 
let 

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

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

491 
in 

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

493 
mk_disc_exhaust_tac n exhaust_thm discI_thms) 

494 
end; 

49028  495 

49486  496 
val (collapse_thms, collapse_thm_opts) = 
497 
let 

498 
fun mk_goal ctr udisc usels = 

499 
let 

500 
val prem = HOLogic.mk_Trueprop udisc; 

501 
val concl = 

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

503 
in 

504 
if prem aconv concl then NONE 

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

506 
end; 

507 
val goals = map3 mk_goal ctrs udiscs uselss; 

508 
in 

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

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

511 
mk_collapse_tac ctxt m discD sel_thms) 

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

513 
> `(map_filter I) 

514 
end; 

49025  515 

49486  516 
val expand_thms = 
517 
let 

518 
fun mk_prems k udisc usels vdisc vsels = 

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

520 
(if null usels then 

521 
[] 

522 
else 

523 
[Logic.list_implies 

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

525 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 

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

527 

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

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

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

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

531 

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

534 
in 

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

536 
mk_expand_tac ctxt n ms (inst_thm u disc_exhaust_thm) 

537 
(inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss 

538 
disc_exclude_thmsss')] 

539 
> Proof_Context.export names_lthy lthy 

540 
end; 

49278  541 

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

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

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

546 
in 

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

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

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

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

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

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

554 
end; 
49025  555 

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

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

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

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

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

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

49486  580 
val lhs = q $ ufcase; 
49044  581 

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

587 

588 
val split_thm = 

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

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

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

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

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

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

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

606 
(case_convN, case_conv_thms, []), 
49300  607 
(collapseN, collapse_thms, simp_attrs), 
608 
(discsN, disc_thms, simp_attrs), 

609 
(disc_excludeN, disc_exclude_thms, []), 

610 
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), 

611 
(distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), 

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

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

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

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

619 
(weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] 

620 
> filter_out (null o #2) 

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

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

624 
val notes' = 

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

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

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

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

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

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

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

638 

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

641 
prepare_wrap_datatype Syntax.read_term; 

642 

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

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

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

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

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

647 

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

648 
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

649 
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

650 
val parse_bound_termss = parse_bracket_list parse_bound_terms; 
49017  651 

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

654 

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

658 
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

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

662 
end; 