author  traytel 
Sun, 30 Sep 2012 12:08:16 +0200  
changeset 49667  44d85dc8ca08 
parent 49633  5b5450bc544c 
child 49668  0209087a14d0 
permissions  rwrr 
49509
163914705f8d
renamed toplevel theory from "Codatatype" to "BNF"
blanchet
parents:
49504
diff
changeset

1 
(* Title: HOL/BNF/Tools/bnf_wrap.ML 
49017  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2012 

4 

49074  5 
Wrapping existing datatypes. 
49017  6 
*) 
7 

49074  8 
signature BNF_WRAP = 
49017  9 
sig 
49633  10 
val rep_compat_prefix: string 
11 

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

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

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

14 

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

17 

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

19 

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

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

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

49074  29 
structure BNF_Wrap : BNF_WRAP = 
49017  30 
struct 
31 

32 
open BNF_Util 

49074  33 
open BNF_Wrap_Tactics 
49017  34 

49633  35 
val rep_compat_prefix = "new"; 
36 

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

39 
fun mk_unN 1 1 suf = unN ^ suf 

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

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

41 

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

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

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

49 
val distinctN = "distinct"; 

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

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

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

49019  59 

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

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

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

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

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

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

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

67 

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

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

71 

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

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

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

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

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

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

49486  78 
fun join_halves n half_xss other_half_xss = 
79 
let 

80 
val xsss = 

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

82 
(transpose (Library.chop_groups n other_half_xss)) 

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

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

84 
in (xs, xsss) end; 
49027  85 

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

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

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

90 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

49203  91 
end; 
92 

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

95 

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

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

99 
end; 

100 

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

103 
Const (s, _) => s 

104 
 Free (s, _) => s 

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

106 

107 
val base_name_of_ctr = Long_Name.base_name o name_of_ctr; 

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

108 

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

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

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

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

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

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

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

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

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

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

126 

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

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

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

133 
(rep_compat ? Binding.qualify false rep_compat_prefix); 

134 

49055  135 
val (As, B) = 
136 
no_defs_lthy 

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

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

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

143 

144 
val ms = map length ctr_Tss; 

145 

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

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

147 

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

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

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

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

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

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

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

155 

49633  156 
val std_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

157 

49336  158 
val disc_bindings = 
159 
raw_disc_bindings' 

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

160 
> map4 (fn k => fn m => fn ctr => fn disc => 
49633  161 
Option.map (qualify false) 
49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49364
diff
changeset

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

165 
SOME (std_disc_binding ctr) 

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

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

167 
SOME disc)) ks ms ctrs0; 
49056  168 

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

171 

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

173 

49336  174 
val sel_bindingss = 
175 
pad_list [] n raw_sel_bindingss 

49056  176 
> map3 (fn ctr => fn m => map2 (fn l => fn sel => 
49633  177 
qualify false 
49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49364
diff
changeset

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

180 
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

181 
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

182 

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

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

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

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

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

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

197 

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

49032  200 

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

203 

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

49043  206 

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

209 

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

212 
val vgcase = gcase $ v; 

213 

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

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

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

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

218 
val exist_xs_u_eq_ctrs = 

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

49022  220 

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

223 

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

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

229 

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

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

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

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

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

49278  242 

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

244 
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

245 
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

246 
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

247 
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

248 

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

249 
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

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

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

252 
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

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

254 
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

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

256 
 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

257 

49278  258 
fun sel_spec b proto_sels = 
259 
let 

260 
val _ = 

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

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

263 
" for constructor " ^ 

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

265 
 [] => ()) 

266 
val T = 

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

268 
[T] => T 

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

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

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

272 
in 

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

276 

49336  277 
val sel_bindings = flat sel_bindingss; 
278 
val uniq_sel_bindings = distinct Binding.eq_name sel_bindings; 

279 
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

280 

49336  281 
val sel_binding_index = 
282 
if all_sels_distinct then 1 upto length sel_bindings 

283 
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

284 

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

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

288 
> sort (int_ord o pairself fst) 
49336  289 
> map snd > curry (op ~~) uniq_sel_bindings; 
290 
val sel_bindings = map fst sel_infos; 

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

291 

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

293 

49278  294 
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = 
295 
no_defs_lthy 

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

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

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

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

49300  306 
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos 
49278  307 
> `Local_Theory.restore; 
49022  308 

49278  309 
val phi = Proof_Context.export_morphism lthy lthy'; 
49025  310 

49278  311 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
49281  312 
val sel_defs = map (Morphism.thm phi) raw_sel_defs; 
313 
val sel_defss = unflat_selss sel_defs; 

49278  314 

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

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

49028  317 

49278  318 
val discs = map (mk_disc_or_sel As) discs0; 
319 
val selss = map (map (mk_disc_or_sel As)) selss0; 

49486  320 

49500  321 
val udiscs = map (rapp u) discs; 
322 
val uselss = map (map (rapp u)) selss; 

49486  323 

49500  324 
val vdiscs = map (rapp v) discs; 
325 
val vselss = map (map (rapp v)) selss; 

49278  326 
in 
49486  327 
(all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs, 
328 
sel_defss, lthy') 

49278  329 
end; 
49025  330 

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

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

336 
end; 
49019  337 

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

340 
fun mk_goal _ _ [] [] = [] 
49025  341 
 mk_goal xctr yctr xs ys = 
49121  342 
[fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), 
343 
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; 

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

345 
map4 mk_goal xctrs yctrs xss yss 
49017  346 
end; 
347 

49484  348 
val half_distinct_goalss = 
49121  349 
let 
49203  350 
fun mk_goal ((xs, xc), (xs', xc')) = 
49121  351 
fold_rev Logic.all (xs @ xs') 
49203  352 
(HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc')))); 
49121  353 
in 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

354 
map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs))) 
49121  355 
end; 
49019  356 

49458  357 
val cases_goal = 
49121  358 
map3 (fn xs => fn xctr => fn xf => 
49201  359 
fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs; 
49025  360 

49484  361 
val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal]; 
49019  362 

363 
fun after_qed thmss lthy = 

364 
let 

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

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

366 
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); 
49019  367 

49438  368 
val inject_thms = flat inject_thmss; 
369 

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

372 
fun inst_thm t thm = 

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

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

375 

376 
val uexhaust_thm = inst_thm u exhaust_thm; 

49032  377 

49300  378 
val exhaust_cases = map base_name_of_ctr ctrs; 
379 

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

380 
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

381 

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

383 
join_halves n half_distinct_thmss other_half_distinct_thmss > `transpose; 
49019  384 

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

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

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

387 
val goal = 
49486  388 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u', 
389 
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

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

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

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

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

394 

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

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

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

400 
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

401 
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

402 
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

403 
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); 
49281  404 

405 
fun has_undefined_rhs thm = 

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

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

408 
 _ => false); 

409 

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

410 
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; 
49281  411 

412 
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

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

414 
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

415 
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

416 
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

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

418 
> filter_out has_undefined_rhs; 
49278  419 

420 
fun mk_unique_disc_def () = 

421 
let 

422 
val m = the_single ms; 

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

423 
val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs); 
49278  424 
in 
49486  425 
Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm) 
49278  426 
> singleton (Proof_Context.export names_lthy lthy) 
427 
> Thm.close_derivation 

428 
end; 

429 

430 
fun mk_alternate_disc_def k = 

431 
let 

432 
val goal = 

49486  433 
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3  k), 
434 
nth exist_xs_u_eq_ctrs (k  1)); 

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

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

49486  438 
(nth distinct_thms (2  k)) uexhaust_thm) 
49278  439 
> singleton (Proof_Context.export names_lthy lthy) 
440 
> Thm.close_derivation 

441 
end; 

49028  442 

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

445 

446 
val disc_defs' = 

447 
map2 (fn k => fn def => 

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

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

450 
else def) ks disc_defs; 

451 

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

453 
val discI_thms = 

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

455 
disc_defs'; 

456 
val not_discI_thms = 

457 
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

458 
(unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) 
49278  459 
ms disc_defs'; 
460 

461 
val (disc_thmss', disc_thmss) = 

462 
let 

463 
fun mk_thm discI _ [] = refl RS discI 

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

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

466 
in 

467 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 

468 
end; 

469 

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

49028  471 

49486  472 
val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = 
473 
let 

474 
fun mk_goal [] = [] 

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

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

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

478 

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

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

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

481 
> Thm.close_derivation; 
49486  482 

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

483 
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs)); 
49486  484 

485 
val half_goalss = map mk_goal half_pairss; 

486 
val half_thmss = 

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

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

489 
half_goalss half_pairss (flat disc_thmss'); 

49278  490 

49486  491 
val other_half_goalss = map (mk_goal o map swap) half_pairss; 
492 
val other_half_thmss = 

493 
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss 

494 
other_half_goalss; 

495 
in 

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

496 
join_halves n half_thmss other_half_thmss > `transpose 
49486  497 
>> has_alternate_disc_def ? K [] 
498 
end; 

49278  499 

49486  500 
val disc_exhaust_thm = 
501 
let 

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

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

504 
in 

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

506 
mk_disc_exhaust_tac n exhaust_thm discI_thms) 

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

507 
> Thm.close_derivation 
49486  508 
end; 
49028  509 

49486  510 
val (collapse_thms, collapse_thm_opts) = 
511 
let 

512 
fun mk_goal ctr udisc usels = 

513 
let 

514 
val prem = HOLogic.mk_Trueprop udisc; 

515 
val concl = 

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

517 
in 

518 
if prem aconv concl then NONE 

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

520 
end; 

521 
val goals = map3 mk_goal ctrs udiscs uselss; 

522 
in 

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

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

525 
mk_collapse_tac ctxt m discD sel_thms) 

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

526 
> Thm.close_derivation 
49486  527 
> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals 
528 
> `(map_filter I) 

529 
end; 

49025  530 

49486  531 
val expand_thms = 
532 
let 

533 
fun mk_prems k udisc usels vdisc vsels = 

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

535 
(if null usels then 

536 
[] 

537 
else 

538 
[Logic.list_implies 

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

540 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 

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

542 

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

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

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

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

546 

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

549 
in 

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

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

551 
mk_expand_tac n ms (inst_thm u disc_exhaust_thm) 
49486  552 
(inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss 
553 
disc_exclude_thmsss')] 

554 
> Proof_Context.export names_lthy lthy 

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

555 
> map Thm.close_derivation 
49486  556 
end; 
49278  557 

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

558 
val case_conv_thms = 
49486  559 
let 
560 
fun mk_body f usels = Term.list_comb (f, usels); 

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

562 
in 

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

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

564 
mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] 
49486  565 
> Proof_Context.export names_lthy lthy 
49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

566 
> map Thm.close_derivation 
49486  567 
end; 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

568 
in 
49484  569 
(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

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

571 
end; 
49025  572 

49033  573 
val (case_cong_thm, weak_case_cong_thm) = 
49032  574 
let 
575 
fun mk_prem xctr xs f g = 

49486  576 
fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr), 
49032  577 
mk_Trueprop_eq (f, g))); 
49033  578 

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

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

582 
val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); 
49032  583 
in 
49486  584 
(Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms), 
49458  585 
Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1))) 
49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

586 
> pairself (singleton (Proof_Context.export names_lthy lthy) #> Thm.close_derivation) 
49032  587 
end; 
49025  588 

49044  589 
val (split_thm, split_asm_thm) = 
49043  590 
let 
49044  591 
fun mk_conjunct xctr xs f_xs = 
49486  592 
list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs)); 
49044  593 
fun mk_disjunct xctr xs f_xs = 
49486  594 
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), 
49044  595 
HOLogic.mk_not (q $ f_xs))); 
596 

49486  597 
val lhs = q $ ufcase; 
49044  598 

49043  599 
val goal = 
49044  600 
mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); 
49458  601 
val asm_goal = 
49044  602 
mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj 
603 
(map3 mk_disjunct xctrs xss xfs))); 

604 

605 
val split_thm = 

49049  606 
Skip_Proof.prove lthy [] [] goal 
49486  607 
(fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss) 
49044  608 
> singleton (Proof_Context.export names_lthy lthy) 
49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

609 
> Thm.close_derivation; 
49044  610 
val split_asm_thm = 
49458  611 
Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} => 
49044  612 
mk_split_asm_tac ctxt split_thm) 
613 
> singleton (Proof_Context.export names_lthy lthy) 

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

614 
> Thm.close_derivation; 
49043  615 
in 
49044  616 
(split_thm, split_asm_thm) 
49043  617 
end; 
49025  618 

49437  619 
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); 
49300  620 
val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name)); 
621 

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

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

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

625 
(case_convN, case_conv_thms, []), 
49300  626 
(collapseN, collapse_thms, simp_attrs), 
627 
(discsN, disc_thms, simp_attrs), 

628 
(disc_excludeN, disc_exclude_thms, []), 

629 
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), 

630 
(distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), 

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

49486  632 
(expandN, expand_thms, []), 
49438  633 
(injectN, inject_thms, iff_attrs @ induct_simp_attrs), 
49300  634 
(nchotomyN, [nchotomy_thm], []), 
635 
(selsN, all_sel_thms, simp_attrs), 

636 
(splitN, [split_thm], []), 

637 
(split_asmN, [split_asm_thm], []), 

49633  638 
(splitsN, [split_thm, split_asm_thm], []), 
49300  639 
(weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] 
640 
> filter_out (null o #2) 

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

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

644 
val notes' = 

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

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

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

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

649 
sel_thmss), lthy > Local_Theory.notes (notes' @ notes) > snd) 
49019  650 
end; 
49017  651 
in 
49121  652 
(goalss, after_qed, lthy') 
49017  653 
end; 
654 

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

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

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

658 

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

661 
prepare_wrap_datatype Syntax.read_term; 

662 

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

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

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

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

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

667 

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

668 
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

669 
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

670 
val parse_bound_termss = parse_bracket_list parse_bound_terms; 
49017  671 

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

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

49278  676 

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

680 
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

681 
Scan.optional parse_bound_termss []) ([], [])) ([], ([], []))) 
49199  682 
>> wrap_datatype_cmd); 
49017  683 

684 
end; 