author  blanchet 
Fri, 31 Aug 2012 15:04:03 +0200  
changeset 49048  4e0f0f98be02 
parent 49046  3c5eba97d93a 
child 49049  c81747d3e920 
permissions  rwrr 
49017  1 
(* Title: HOL/Codatatype/Tools/bnf_sugar.ML 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 
Copyright 2012 

4 

5 
Sugar on top of a BNF. 

6 
*) 

7 

8 
signature BNF_SUGAR = 

9 
sig 

10 
end; 

11 

12 
structure BNF_Sugar : BNF_SUGAR = 

13 
struct 

14 

15 
open BNF_Util 

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

17 
open BNF_Sugar_Tactics 
49017  18 

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

19 
val is_N = "is_"; 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

20 

49025  21 
val case_congN = "case_cong" 
22 
val case_discsN = "case_discs" 

23 
val casesN = "cases" 

24 
val ctr_selsN = "ctr_sels" 

25 
val disc_disjointN = "disc_disjoint" 

49027  26 
val disc_exhaustN = "disc_exhaust" 
27 
val discsN = "discs" 

49025  28 
val distinctN = "distinct" 
29 
val selsN = "sels" 

30 
val splitN = "split" 

31 
val split_asmN = "split_asm" 

32 
val weak_case_cong_thmsN = "weak_case_cong" 

49019  33 

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

34 
val default_name = @{binding _}; 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

35 

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

36 
fun mk_half_pairss' _ [] = [] 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

37 
 mk_half_pairss' pad (y :: ys) = 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

38 
pad @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: pad) ys); 
49027  39 

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

40 
fun mk_half_pairss ys = mk_half_pairss' [[]] ys; 
49027  41 

49032  42 
val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; 
43 

49043  44 
fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
49032  45 

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

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

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

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

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

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

51 

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

52 
fun prepare_sugar prep_term (((raw_ctrs, raw_caseof), raw_disc_names), sel_namess) no_defs_lthy = 
49017  53 
let 
49019  54 
(* TODO: sanity checks on arguments *) 
49017  55 

49025  56 
(* TODO: normalize types of constructors w.r.t. each other *) 
57 

58 
val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; 

59 
val caseof0 = prep_term no_defs_lthy raw_caseof; 

49017  60 

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

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

62 
map2 (fn ctr => fn disc => 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

63 
if Binding.eq_name (disc, default_name) then 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

64 
Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr))) 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

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

66 
disc) ctrs0 raw_disc_names; 
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

67 

49025  68 
val n = length ctrs0; 
69 
val ks = 1 upto n; 

49022  70 

49025  71 
val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0))); 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

72 
val b = Binding.qualified_name T_name; 
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

73 

49025  74 
val (As, B) = 
75 
no_defs_lthy 

76 
> mk_TFrees (length As0) 

77 
> the_single o fst o mk_TFrees 1; 

78 

79 
fun mk_undef T Ts = Const (@{const_name undefined}, Ts > T); 

80 

81 
fun mk_ctr Ts ctr = 

49028  82 
let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in 
49025  83 
Term.subst_atomic_types (Ts0 ~~ Ts) ctr 
84 
end; 

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

85 

49028  86 
fun mk_caseof Ts T = 
87 
let val (binders, body) = strip_type (fastype_of caseof0) in 

88 
Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0 

49022  89 
end; 
90 

49025  91 
val T = Type (T_name, As); 
92 
val ctrs = map (mk_ctr As) ctrs0; 

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

94 

49028  95 
val ms = map length ctr_Tss; 
96 

97 
val caseofB = mk_caseof As B; 

49025  98 
val caseofB_Ts = map (fn Ts => Ts > B) ctr_Tss; 
99 

49043  100 
fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs); 
101 

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

49025  103 
mk_Freess "x" ctr_Tss 
104 
>> mk_Freess "y" ctr_Tss 

105 
>> mk_Frees "f" caseofB_Ts 

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

107 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T 
49032  108 
>> yield_singleton (mk_Frees "w") T 
49043  109 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; 
110 

111 
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

112 

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

49032  115 

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

118 

119 
val eta_fs = map2 eta_expand_caseof_arg xss xfs; 

120 
val eta_gs = map2 eta_expand_caseof_arg xss xgs; 

121 

122 
val caseofB_fs = Term.list_comb (caseofB, eta_fs); 

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

123 

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

49022  126 

49032  127 
fun mk_sel_caseof_args k xs x T = 
49025  128 
map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks; 
129 

130 
fun disc_spec b exist_xs_v_eq_ctr = 

49032  131 
mk_Trueprop_eq (Free (Binding.name_of b, T > HOLogic.boolT) $ v, exist_xs_v_eq_ctr); 
49025  132 

49028  133 
fun sel_spec b x xs k = 
49025  134 
let val T' = fastype_of x in 
49032  135 
mk_Trueprop_eq (Free (Binding.name_of b, T > T') $ v, 
136 
Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) 

49022  137 
end; 
138 

49028  139 
val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) = 
49022  140 
no_defs_lthy 
49025  141 
> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr => 
49022  142 
Specification.definition (SOME (b, NONE, NoSyn), 
49025  143 
((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs 
49028  144 
>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k => 
49025  145 
apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x => 
49022  146 
Specification.definition (SOME (b, NONE, NoSyn), 
49028  147 
((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks 
49022  148 
> `Local_Theory.restore; 
149 

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

152 

49028  153 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
154 
val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss; 

155 

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

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

49025  158 

49028  159 
fun mk_disc_or_sel Ts t = 
160 
Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t; 

161 

162 
val discs = map (mk_disc_or_sel As) discs0; 

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

49025  164 

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

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

167 
val goal_exhaust = 
49032  168 
let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in 
49025  169 
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

170 
end; 
49019  171 

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

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

174 
fun mk_goal _ _ [] [] = [] 
49025  175 
 mk_goal xctr yctr xs ys = 
49034
b77e1910af8a
make parallel list indexing possible for inject theorems
blanchet
parents:
49033
diff
changeset

176 
[mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), 
b77e1910af8a
make parallel list indexing possible for inject theorems
blanchet
parents:
49033
diff
changeset

177 
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))]; 
49017  178 
in 
49034
b77e1910af8a
make parallel list indexing possible for inject theorems
blanchet
parents:
49033
diff
changeset

179 
map4 mk_goal xctrs yctrs xss yss 
49017  180 
end; 
181 

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

182 
val goal_half_distinctss = 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

183 
map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs); 
49019  184 

49043  185 
val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs; 
49025  186 

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

187 
val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases]; 
49019  188 

189 
fun after_qed thmss lthy = 

190 
let 

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

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

192 
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); 
49019  193 

49043  194 
val inject_thms = flat inject_thmss; 
195 

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

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

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

200 
end; 

201 

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

202 
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

203 

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

204 
val distinct_thmsss = 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

205 
map2 (map2 append) (Library.chop_groups n half_distinct_thmss) 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

206 
(transpose (Library.chop_groups n other_half_distinct_thmss)); 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

207 
val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss); 
49019  208 

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

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

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

211 
val goal = 
49022  212 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', 
49029  213 
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

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

215 
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

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

217 

49030  218 
val sel_thmss = 
49025  219 
let 
49028  220 
fun mk_thm k xs goal_case case_thm x sel_def = 
49025  221 
let 
222 
val T = fastype_of x; 

223 
val cTs = 

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

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

49032  226 
val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T); 
49025  227 
in 
228 
Local_Defs.fold lthy [sel_def] 

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

230 
end; 

49028  231 
fun mk_thms k xs goal_case case_thm sel_defs = 
232 
map2 (mk_thm k xs goal_case case_thm) xs sel_defs; 

49025  233 
in 
49030  234 
map5 mk_thms ks xss goal_cases case_thms sel_defss 
49025  235 
end; 
236 

49030  237 
val discD_thms = map (fn def => def RS iffD1) disc_defs; 
49028  238 
val discI_thms = 
49030  239 
map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; 
49028  240 
val not_disc_thms = 
49030  241 
map2 (fn m => fn def => funpow m (fn thm => allI RS thm) 
242 
(Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) 

49028  243 
ms disc_defs; 
244 

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

245 
val disc_thmss = 
49027  246 
let 
49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

247 
fun mk_thm discI _ [] = refl RS discI 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

248 
 mk_thm _ not_disc [distinct] = distinct RS not_disc; 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

249 
fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss; 
49027  250 
in 
49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

251 
map3 mk_thms discI_thms not_disc_thms (transpose distinct_thmsss) 
49027  252 
end; 
49025  253 

49028  254 
val disc_disjoint_thms = 
255 
let 

256 
fun mk_goal ((_, disc), (_, disc')) = 

49029  257 
Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), 
258 
HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)))); 

49028  259 
fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); 
260 

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

261 
val bundles = ms ~~ discD_thms ~~ discs; 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

262 
val half_pairss = mk_half_pairss bundles; 
49028  263 

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

264 
val goal_halvess = map (map mk_goal) half_pairss; 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

265 
val half_thmss = 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

266 
map3 (fn [] => K (K []) 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

267 
 [(((m, discD), _), _)] => fn disc_thm => fn [goal] => 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

268 
[prove (mk_half_disc_disjoint_tac m discD disc_thm) goal]) 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

269 
half_pairss (flat (transpose disc_thmss)) goal_halvess; 
49028  270 

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

271 
val goal_other_halvess = map (map (mk_goal o swap)) half_pairss; 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

272 
val other_half_thmss = 
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

273 
map2 (map2 (prove o mk_other_half_disc_disjoint_tac)) half_thmss goal_other_halvess; 
49028  274 
in 
49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49046
diff
changeset

275 
interleave (flat half_thmss) (flat other_half_thmss) 
49028  276 
end; 
49025  277 

49029  278 
val disc_exhaust_thm = 
279 
let 

280 
fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)]; 

281 
val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); 

282 
in 

283 
Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) 

284 
end; 

49025  285 

49030  286 
val ctr_sel_thms = 
287 
let 

288 
fun mk_goal ctr disc sels = 

289 
Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), 

49032  290 
mk_Trueprop_eq ((null sels ? swap) 
291 
(Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)))); 

49030  292 
val goals = map3 mk_goal ctrs discs selss; 
293 
in 

294 
map4 (fn goal => fn m => fn discD => fn sel_thms => 

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

296 
mk_ctr_sel_tac ctxt m discD sel_thms)) 

297 
goals ms discD_thms sel_thmss 

298 
end; 

49025  299 

49031  300 
val case_disc_thm = 
301 
let 

302 
fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); 

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

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

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

306 
(disc $ v) $ mk_core f sels $ mk_rhs discs fs selss; 

49043  307 
val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); 
49031  308 
in 
309 
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 

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

310 
mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss sel_thmss) 
49031  311 
> singleton (Proof_Context.export names_lthy lthy) 
312 
end; 

49025  313 

49033  314 
val (case_cong_thm, weak_case_cong_thm) = 
49032  315 
let 
316 
fun mk_prem xctr xs f g = 

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

317 
fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), 
49032  318 
mk_Trueprop_eq (f, g))); 
49033  319 

320 
val v_eq_w = mk_Trueprop_eq (v, w); 

49043  321 
val caseof_fs = mk_caseofB_term eta_fs; 
322 
val caseof_gs = mk_caseofB_term eta_gs; 

49032  323 

324 
val goal = 

49033  325 
Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs, 
326 
mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w)); 

327 
val goal_weak = 

328 
Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w)); 

49032  329 
in 
49033  330 
(Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 
331 
mk_case_cong_tac ctxt exhaust_thm' case_thms), 

332 
Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) 

333 
> pairself (singleton (Proof_Context.export names_lthy lthy)) 

49032  334 
end; 
49025  335 

49044  336 
val (split_thm, split_asm_thm) = 
49043  337 
let 
49044  338 
fun mk_conjunct xctr xs f_xs = 
49043  339 
list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); 
49044  340 
fun mk_disjunct xctr xs f_xs = 
341 
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr), 

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

343 

344 
val lhs = q $ (mk_caseofB_term eta_fs $ v); 

345 

49043  346 
val goal = 
49044  347 
mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); 
348 
val goal_asm = 

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

350 
(map3 mk_disjunct xctrs xss xfs))); 

351 

352 
val split_thm = 

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

354 
mk_split_tac ctxt exhaust_thm' case_thms inject_thms distinct_thms) 

355 
> singleton (Proof_Context.export names_lthy lthy) 

356 
val split_asm_thm = 

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

358 
mk_split_asm_tac ctxt split_thm) 

359 
> singleton (Proof_Context.export names_lthy lthy) 

49043  360 
in 
49044  361 
(split_thm, split_asm_thm) 
49043  362 
end; 
49025  363 

49043  364 
(* TODO: case syntax *) 
365 
(* TODO: attributes (simp, case_names, etc.) *) 

49025  366 

49019  367 
fun note thmN thms = 
368 
snd o Local_Theory.note 

369 
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms); 

370 
in 

371 
lthy 

49025  372 
> note case_congN [case_cong_thm] 
49031  373 
> note case_discsN [case_disc_thm] 
49025  374 
> note casesN case_thms 
375 
> note ctr_selsN ctr_sel_thms 

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

376 
> note discsN (flat disc_thmss) 
49025  377 
> note disc_disjointN disc_disjoint_thms 
49029  378 
> note disc_exhaustN [disc_exhaust_thm] 
49043  379 
> note distinctN distinct_thms 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

380 
> note exhaustN [exhaust_thm] 
49043  381 
> note injectN inject_thms 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

382 
> note nchotomyN [nchotomy_thm] 
49030  383 
> note selsN (flat sel_thmss) 
49043  384 
> note splitN [split_thm] 
385 
> note split_asmN [split_asm_thm] 

49033  386 
> note weak_case_cong_thmsN [weak_case_cong_thm] 
49019  387 
end; 
49017  388 
in 
49025  389 
(goals, after_qed, lthy') 
49017  390 
end; 
391 

392 
val parse_binding_list = Parse.$$$ "["  Parse.list Parse.binding  Parse.$$$ "]"; 

393 

49019  394 
val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) => 
395 
Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo 

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

396 
prepare_sugar Syntax.read_term; 
49017  397 

398 
val _ = 

399 
Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF" 

49023  400 
(((Parse.$$$ "["  Parse.list Parse.term  Parse.$$$ "]")  Parse.term  
401 
parse_binding_list  (Parse.$$$ "["  Parse.list parse_binding_list  Parse.$$$ "]")) 

402 
>> bnf_sugar_cmd); 

49017  403 

404 
end; 