author  blanchet 
Wed, 05 Sep 2012 11:11:26 +0200  
changeset 49150  881e573a619e 
parent 49148  93f281430e77 
child 49152  feb984727eec 
permissions  rwrr 
49074  1 
(* Title: HOL/Codatatype/Tools/bnf_wrap.ML 
49017  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2012 

4 

49074  5 
Wrapping existing datatypes. 
49017  6 
*) 
7 

49074  8 
signature BNF_WRAP = 
49017  9 
sig 
49129  10 
val no_binder: binding 
49121  11 
val mk_half_pairss: 'a list > ('a * 'a) list list 
12 
val wrap_data: ({prems: thm list, context: Proof.context} > tactic) list list > 

49119  13 
(term list * term) * (binding list * binding list list) > local_theory > local_theory 
49017  14 
end; 
15 

49074  16 
structure BNF_Wrap : BNF_WRAP = 
49017  17 
struct 
18 

19 
open BNF_Util 

49074  20 
open BNF_Wrap_Tactics 
49017  21 

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

22 
val is_N = "is_"; 
49054  23 
val un_N = "un_"; 
24 
fun mk_un_N 1 1 suf = un_N ^ suf 

25 
 mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; 

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

26 

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

28 
val case_eqN = "case_eq"; 
49054  29 
val casesN = "cases"; 
49118  30 
val collapseN = "collapse"; 
49122  31 
val disc_excludeN = "disc_exclude"; 
49054  32 
val disc_exhaustN = "disc_exhaust"; 
33 
val discsN = "discs"; 

34 
val distinctN = "distinct"; 

49075  35 
val exhaustN = "exhaust"; 
36 
val injectN = "inject"; 

37 
val nchotomyN = "nchotomy"; 

49054  38 
val selsN = "sels"; 
39 
val splitN = "split"; 

40 
val split_asmN = "split_asm"; 

41 
val weak_case_cong_thmsN = "weak_case_cong"; 

49019  42 

49139  43 
val no_binder = @{binding ""}; 
49129  44 
val fallback_binder = @{binding _}; 
49046
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

45 

49056  46 
fun pad_list x n xs = xs @ replicate (n  length xs) x; 
47 

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

48 
fun mk_half_pairss' _ [] = [] 
49056  49 
 mk_half_pairss' indent (y :: ys) = 
50 
indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys); 

49027  51 

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

52 
fun mk_half_pairss ys = mk_half_pairss' [[]] ys; 
49027  53 

49150  54 
(* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *) 
49055  55 
fun mk_undef T Ts = Const (@{const_name undefined}, Ts > T); 
56 

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

57 
fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
49032  58 

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

59 
fun name_of_ctr t = 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

60 
case head_of t of 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

61 
Const (s, _) => s 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

62 
 Free (s, _) => s 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

63 
 _ => error "Cannot extract name of constructor"; 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

64 

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

65 
fun prepare_wrap_data prep_term ((raw_ctrs, raw_case), (raw_disc_binders, raw_sel_binderss)) 
49054  66 
no_defs_lthy = 
49017  67 
let 
49019  68 
(* TODO: sanity checks on arguments *) 
49113  69 
(* TODO: attributes (simp, case_names, etc.) *) 
70 
(* TODO: case syntax *) 

71 
(* TODO: integration with function package ("size") *) 

49025  72 

73 
val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; 

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

74 
val case0 = prep_term no_defs_lthy raw_case; 
49017  75 

49054  76 
val n = length ctrs0; 
77 
val ks = 1 upto n; 

78 

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

81 
val Type (T_name, As0) = body_type (fastype_of (hd ctrs0)); 

49055  82 
val b = Binding.qualified_name T_name; 
83 

84 
val (As, B) = 

85 
no_defs_lthy 

86 
> mk_TFrees (length As0) 

87 
> the_single o fst o mk_TFrees 1; 

88 

89 
fun mk_ctr Ts ctr = 

49121  90 
let val Type (_, Ts0) = body_type (fastype_of ctr) in 
49055  91 
Term.subst_atomic_types (Ts0 ~~ Ts) ctr 
92 
end; 

93 

94 
val T = Type (T_name, As); 

95 
val ctrs = map (mk_ctr As) ctrs0; 

96 
val ctr_Tss = map (binder_types o fastype_of) ctrs; 

97 

98 
val ms = map length ctr_Tss; 

99 

49129  100 
val raw_disc_binders' = pad_list no_binder n raw_disc_binders; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

101 

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

102 
fun can_rely_on_disc i = 
49129  103 
not (Binding.eq_name (nth raw_disc_binders' i, no_binder)) orelse nth ms i = 0; 
104 
fun can_omit_disc_binder k m = 

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

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

106 

49129  107 
val fallback_disc_binder = Binding.name o prefix is_N o Long_Name.base_name o name_of_ctr; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

108 

49129  109 
val disc_binders = 
110 
raw_disc_binders' 

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

111 
> map4 (fn k => fn m => fn ctr => fn disc => 
49129  112 
if Binding.eq_name (disc, no_binder) then 
113 
if can_omit_disc_binder k m then NONE else SOME (fallback_disc_binder ctr) 

114 
else if Binding.eq_name (disc, fallback_binder) then 

115 
SOME (fallback_disc_binder ctr) 

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

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

117 
SOME disc) ks ms ctrs0; 
49056  118 

49129  119 
val no_discs = map is_none disc_binders; 
49137  120 
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

121 

49129  122 
fun fallback_sel_binder m l = Binding.name o mk_un_N m l o Long_Name.base_name o name_of_ctr; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

123 

49129  124 
val sel_binderss = 
125 
pad_list [] n raw_sel_binderss 

49056  126 
> map3 (fn ctr => fn m => map2 (fn l => fn sel => 
49129  127 
if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, fallback_binder) then 
128 
fallback_sel_binder m l ctr 

49056  129 
else 
49129  130 
sel) (1 upto m) o pad_list no_binder m) ctrs0 ms; 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

131 

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

132 
fun mk_case Ts T = 
49121  133 
let 
49130
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

134 
val (binders, body) = strip_type (fastype_of case0) 
49121  135 
val Type (_, Ts0) = List.last binders 
49130
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

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

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

138 
val caseB = mk_case As B; 
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

139 
val caseB_Ts = map (fn Ts => Ts > B) ctr_Tss; 
49025  140 

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

141 
fun mk_caseB_term eta_fs = Term.list_comb (caseB, eta_fs); 
49043  142 

143 
val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy > 

49025  144 
mk_Freess "x" ctr_Tss 
145 
>> mk_Freess "y" ctr_Tss 

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

146 
>> mk_Frees "f" caseB_Ts 
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

147 
>> mk_Frees "g" caseB_Ts 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

148 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T 
49032  149 
>> yield_singleton (mk_Frees "w") T 
49043  150 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; 
151 

152 
val q = Free (fst p', B > HOLogic.boolT); 

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

153 

49137  154 
fun mk_v_eq_v () = HOLogic.mk_eq (v, v); 
155 

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

49032  158 

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

161 

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

162 
val eta_fs = map2 eta_expand_case_arg xss xfs; 
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

163 
val eta_gs = map2 eta_expand_case_arg xss xgs; 
49043  164 

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

165 
val caseB_fs = Term.list_comb (caseB, eta_fs); 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

166 

49025  167 
val exist_xs_v_eq_ctrs = 
168 
map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; 

49022  169 

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

170 
fun mk_sel_case_args k xs x T = 
49025  171 
map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks; 
172 

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

173 
fun disc_free b = Free (Binding.name_of b, T > HOLogic.boolT); 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

174 

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

175 
fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr); 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

176 

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

178 
HOLogic.mk_not 
49129  179 
(case nth disc_binders i of NONE => nth exist_xs_v_eq_ctrs i  SOME b => disc_free b $ v); 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

180 

49137  181 
fun alternate_disc k = 
182 
if n = 2 then Term.lambda v (alternate_disc_lhs (2  k)) else error "Cannot use \"*\" here" 

49025  183 

49028  184 
fun sel_spec b x xs k = 
49025  185 
let val T' = fastype_of x in 
49032  186 
mk_Trueprop_eq (Free (Binding.name_of b, T > T') $ v, 
49130
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

187 
Term.list_comb (mk_case As T', mk_sel_case_args k xs x T') $ v) 
49022  188 
end; 
189 

49137  190 
val missing_unique_disc_def = TrueI; (*arbitrary marker*) 
191 
val missing_alternate_disc_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

192 

49114  193 
val (((raw_discs, raw_disc_defs), (raw_selss, raw_sel_defss)), (lthy', lthy)) = 
49022  194 
no_defs_lthy 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

195 
> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr => 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

196 
fn NONE => 
49137  197 
if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), missing_unique_disc_def) 
49136  198 
else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl) 
49137  199 
else pair (alternate_disc k, missing_alternate_disc_def) 
49114  200 
 SOME b => Specification.definition (SOME (b, NONE, NoSyn), 
201 
((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) 

49129  202 
ks ms exist_xs_v_eq_ctrs disc_binders 
49114  203 
>> apfst split_list o fold_map3 (fn bs => fn xs => fn k => apfst split_list o 
204 
fold_map2 (fn b => fn x => Specification.definition (SOME (b, NONE, NoSyn), 

49129  205 
((Thm.def_binding b, []), sel_spec b x xs k)) #>> apsnd snd) bs xs) sel_binderss xss ks 
49022  206 
> `Local_Theory.restore; 
207 

49025  208 
(*transforms defined frees into consts (and more)*) 
209 
val phi = Proof_Context.export_morphism lthy lthy'; 

210 

49028  211 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
212 
val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss; 

213 

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

215 
val selss0 = map (map (Morphism.term phi)) raw_selss; 

49025  216 

49028  217 
fun mk_disc_or_sel Ts t = 
49121  218 
Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t; 
49028  219 

220 
val discs = map (mk_disc_or_sel As) discs0; 

221 
val selss = map (map (mk_disc_or_sel As)) selss0; 

49025  222 

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

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

225 
val goal_exhaust = 
49032  226 
let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in 
49121  227 
fold_rev Logic.all [p, v] (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

228 
end; 
49019  229 

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

230 
val goal_injectss = 
49017  231 
let 
49034
b77e1910af8a
make parallel list indexing possible for inject theorems
blanchet
parents:
49033
diff
changeset

232 
fun mk_goal _ _ [] [] = [] 
49025  233 
 mk_goal xctr yctr xs ys = 
49121  234 
[fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), 
235 
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; 

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

237 
map4 mk_goal xctrs yctrs xss yss 
49017  238 
end; 
239 

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

240 
val goal_half_distinctss = 
49121  241 
let 
242 
fun mk_goal ((xs, t), (xs', t')) = 

243 
fold_rev Logic.all (xs @ xs') 

244 
(HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, t')))); 

245 
in 

246 
map (map mk_goal) (mk_half_pairss (xss ~~ xctrs)) 

247 
end; 

49019  248 

49121  249 
val goal_cases = 
250 
map3 (fn xs => fn xctr => fn xf => 

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

251 
fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (caseB_fs $ xctr, xf))) xss xctrs xfs; 
49025  252 

49121  253 
val goalss = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases]; 
49019  254 

255 
fun after_qed thmss lthy = 

256 
let 

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

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

258 
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); 
49019  259 

49032  260 
val exhaust_thm' = 
261 
let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in 

262 
Drule.instantiate' [] [SOME (certify lthy v)] 

263 
(Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm)) 

264 
end; 

265 

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

266 
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

267 

49052  268 
val (distinct_thmsss', distinct_thmsss) = 
49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

269 
map2 (map2 append) (Library.chop_groups n half_distinct_thmss) 
49052  270 
(transpose (Library.chop_groups n other_half_distinct_thmss)) 
271 
> `transpose; 

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

272 
val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss); 
49019  273 

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

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

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

276 
val goal = 
49022  277 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', 
49029  278 
Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

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

280 
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

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

282 

49030  283 
val sel_thmss = 
49025  284 
let 
49028  285 
fun mk_thm k xs goal_case case_thm x sel_def = 
49025  286 
let 
287 
val T = fastype_of x; 

288 
val cTs = 

289 
map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree) 

290 
(rev (Term.add_tfrees goal_case [])); 

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

291 
val cxs = map (certify lthy) (mk_sel_case_args k xs x T); 
49025  292 
in 
293 
Local_Defs.fold lthy [sel_def] 

294 
(Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm) 

295 
end; 

49028  296 
fun mk_thms k xs goal_case case_thm sel_defs = 
49140  297 
map2 (mk_thm k xs (strip_all_body goal_case) case_thm) xs sel_defs; 
49025  298 
in 
49030  299 
map5 mk_thms ks xss goal_cases case_thms sel_defss 
49025  300 
end; 
301 

49137  302 
fun mk_unique_disc_def k = 
303 
let 

304 
val m = the_single ms; 

305 
val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs); 

306 
in 

307 
Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm') 

308 
> singleton (Proof_Context.export names_lthy lthy) 

309 
> Thm.close_derivation 

310 
end; 

311 

312 
fun mk_alternate_disc_def k = 

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

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

314 
val goal = 
49137  315 
mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (2  k)), 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

316 
nth exist_xs_v_eq_ctrs (k  1)); 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

318 
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 
49148
93f281430e77
fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
blanchet
parents:
49140
diff
changeset

319 
mk_alternate_disc_def_tac ctxt k (nth disc_defs (2  k)) (nth distinct_thms (2  k)) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

321 
> singleton (Proof_Context.export names_lthy lthy) 
49125  322 
> Thm.close_derivation 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

324 

49137  325 
val has_alternate_disc_def = 
326 
exists (fn def => Thm.eq_thm_prop (def, missing_alternate_disc_def)) disc_defs; 

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

327 

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

328 
val disc_defs' = 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

329 
map2 (fn k => fn def => 
49137  330 
if Thm.eq_thm_prop (def, missing_unique_disc_def) then mk_unique_disc_def k 
331 
else if Thm.eq_thm_prop (def, missing_alternate_disc_def) then mk_alternate_disc_def k 

332 
else def) 

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

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

334 

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

335 
val discD_thms = map (fn def => def RS iffD1) disc_defs'; 
49028  336 
val discI_thms = 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

337 
map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs'; 
49137  338 
val not_discI_thms = 
49030  339 
map2 (fn m => fn def => funpow m (fn thm => allI RS thm) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

340 
(Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

341 
ms disc_defs'; 
49028  342 

49050  343 
val (disc_thmss', disc_thmss) = 
49027  344 
let 
49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

345 
fun mk_thm discI _ [] = refl RS discI 
49137  346 
 mk_thm _ not_discI [distinct] = distinct RS not_discI; 
347 
fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss; 

49027  348 
in 
49137  349 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 
49027  350 
end; 
49025  351 

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

352 
val disc_thms = flat (map2 (fn true => K []  false => I) no_discs disc_thmss); 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

353 

49122  354 
val disc_exclude_thms = 
49137  355 
if has_alternate_disc_def then 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

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

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

359 
fun mk_goal [] = [] 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

360 
 mk_goal [((_, true), (_, true))] = [] 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

361 
 mk_goal [(((_, disc), _), ((_, disc'), _))] = 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

362 
[Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)), 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

363 
HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))]; 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

364 
fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); 
49028  365 

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

366 
val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs; 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

367 
val half_pairss = mk_half_pairss bundles; 
49028  368 

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

369 
val goal_halvess = map mk_goal half_pairss; 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

371 
map3 (fn [] => K (K [])  [goal] => fn [((((m, discD), _), _), _)] => fn disc_thm => 
49122  372 
[prove (mk_half_disc_exclude_tac m discD disc_thm) goal]) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

373 
goal_halvess half_pairss (flat disc_thmss'); 
49028  374 

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

375 
val goal_other_halvess = map (mk_goal o map swap) half_pairss; 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

376 
val other_half_thmss = 
49122  377 
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss goal_other_halvess; 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

379 
interleave (flat half_thmss) (flat other_half_thmss) 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

380 
end; 
49025  381 

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

382 
val disc_exhaust_thms = 
49137  383 
if has_alternate_disc_def orelse no_discs_at_all then 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

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

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

387 
fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))]; 
49121  388 
val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs)); 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

390 
[Skip_Proof.prove lthy [] [] goal (fn _ => 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

391 
mk_disc_exhaust_tac n exhaust_thm discI_thms)] 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

392 
end; 
49025  393 

49118  394 
val collapse_thms = 
49030  395 
let 
396 
fun mk_goal ctr disc sels = 

49114  397 
let 
398 
val prem = HOLogic.mk_Trueprop (betapply (disc, v)); 

399 
val concl = 

400 
mk_Trueprop_eq ((null sels ? swap) 

401 
(Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)); 

402 
in 

403 
if prem aconv concl then NONE 

404 
else SOME (Logic.all v (Logic.mk_implies (prem, concl))) 

405 
end; 

49030  406 
val goals = map3 mk_goal ctrs discs selss; 
407 
in 

49114  408 
map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => 
49030  409 
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 
49137  410 
mk_collapse_tac ctxt m discD sel_thms) 
411 
> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals 

49114  412 
> map_filter I 
49030  413 
end; 
49025  414 

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

415 
val case_eq_thm = 
49031  416 
let 
417 
fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); 

418 
fun mk_rhs _ [f] [sels] = mk_core f sels 

419 
 mk_rhs (disc :: discs) (f :: fs) (sels :: selss) = 

420 
Const (@{const_name If}, HOLogic.boolT > B > B > B) $ 

49114  421 
betapply (disc, v) $ mk_core f sels $ mk_rhs discs fs selss; 
49130
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

422 
val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss); 
49031  423 
in 
424 
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 

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

425 
mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) 
49031  426 
> singleton (Proof_Context.export names_lthy lthy) 
427 
end; 

49025  428 

49033  429 
val (case_cong_thm, weak_case_cong_thm) = 
49032  430 
let 
431 
fun mk_prem xctr xs f g = 

49045
7d9631754bba
minor fixes (for compatibility with existing datatype package)
blanchet
parents:
49044
diff
changeset

432 
fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), 
49032  433 
mk_Trueprop_eq (f, g))); 
49033  434 

435 
val v_eq_w = mk_Trueprop_eq (v, w); 

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

436 
val case_fs = mk_caseB_term eta_fs; 
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

437 
val case_gs = mk_caseB_term eta_gs; 
49032  438 

439 
val goal = 

49033  440 
Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs, 
49130
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

441 
mk_Trueprop_eq (case_fs $ v, case_gs $ w)); 
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

442 
val goal_weak = Logic.mk_implies (v_eq_w, mk_Trueprop_eq (case_fs $ v, case_fs $ w)); 
49032  443 
in 
49049  444 
(Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms), 
49033  445 
Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) 
446 
> pairself (singleton (Proof_Context.export names_lthy lthy)) 

49032  447 
end; 
49025  448 

49044  449 
val (split_thm, split_asm_thm) = 
49043  450 
let 
49044  451 
fun mk_conjunct xctr xs f_xs = 
49043  452 
list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); 
49044  453 
fun mk_disjunct xctr xs f_xs = 
454 
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr), 

455 
HOLogic.mk_not (q $ f_xs))); 

456 

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

457 
val lhs = q $ (mk_caseB_term eta_fs $ v); 
49044  458 

49043  459 
val goal = 
49044  460 
mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); 
461 
val goal_asm = 

462 
mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj 

463 
(map3 mk_disjunct xctrs xss xfs))); 

464 

465 
val split_thm = 

49049  466 
Skip_Proof.prove lthy [] [] goal 
49052  467 
(fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss) 
49044  468 
> singleton (Proof_Context.export names_lthy lthy) 
469 
val split_asm_thm = 

470 
Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} => 

471 
mk_split_asm_tac ctxt split_thm) 

472 
> singleton (Proof_Context.export names_lthy lthy) 

49043  473 
in 
49044  474 
(split_thm, split_asm_thm) 
49043  475 
end; 
49025  476 

49052  477 
val notes = 
478 
[(case_congN, [case_cong_thm]), 

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

479 
(case_eqN, [case_eq_thm]), 
49052  480 
(casesN, case_thms), 
49118  481 
(collapseN, collapse_thms), 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

482 
(discsN, disc_thms), 
49122  483 
(disc_excludeN, disc_exclude_thms), 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

484 
(disc_exhaustN, disc_exhaust_thms), 
49052  485 
(distinctN, distinct_thms), 
486 
(exhaustN, [exhaust_thm]), 

49121  487 
(injectN, flat inject_thmss), 
49052  488 
(nchotomyN, [nchotomy_thm]), 
49121  489 
(selsN, flat sel_thmss), 
49052  490 
(splitN, [split_thm]), 
491 
(split_asmN, [split_asm_thm]), 

492 
(weak_case_cong_thmsN, [weak_case_cong_thm])] 

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

493 
> filter_out (null o snd) 
49052  494 
> map (fn (thmN, thms) => 
495 
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); 

49019  496 
in 
49052  497 
lthy > Local_Theory.notes notes > snd 
49019  498 
end; 
49017  499 
in 
49121  500 
(goalss, after_qed, lthy') 
49017  501 
end; 
502 

49121  503 
fun wrap_data tacss = (fn (goalss, after_qed, lthy) => 
49111  504 
map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss 
505 
> (fn thms => after_qed thms lthy)) oo 

49121  506 
prepare_wrap_data (K I) (* FIXME? (singleton o Type_Infer_Context.infer_types) *) 
49111  507 

49114  508 
val parse_bindings = Parse.$$$ "["  Parse.list Parse.binding  Parse.$$$ "]"; 
49057  509 
val parse_bindingss = Parse.$$$ "["  Parse.list parse_bindings  Parse.$$$ "]"; 
49017  510 

49074  511 
val wrap_data_cmd = (fn (goalss, after_qed, lthy) => 
49019  512 
Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo 
49121  513 
prepare_wrap_data Syntax.read_term; 
49017  514 

515 
val _ = 

49074  516 
Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype" 
49023  517 
(((Parse.$$$ "["  Parse.list Parse.term  Parse.$$$ "]")  Parse.term  
49057  518 
Scan.optional (parse_bindings  Scan.optional parse_bindingss []) ([], [])) 
49074  519 
>> wrap_data_cmd); 
49017  520 

521 
end; 