author  blanchet 
Tue, 04 Sep 2012 13:02:31 +0200  
changeset 49118  b815fa776b91 
parent 49117  000deee4913e 
child 49119  1f605c36869c 
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 
49111  10 
val wrap: ({prems: thm list, context: Proof.context} > tactic) list list > 
11 
(term list * term) * (binding list * binding list list) > Proof.context > local_theory 

49017  12 
end; 
13 

49074  14 
structure BNF_Wrap : BNF_WRAP = 
49017  15 
struct 
16 

17 
open BNF_Util 

49074  18 
open BNF_Wrap_Tactics 
49017  19 

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

20 
val is_N = "is_"; 
49054  21 
val un_N = "un_"; 
22 
fun mk_un_N 1 1 suf = un_N ^ suf 

23 
 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

24 

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

26 
val case_eqN = "case_eq"; 
49054  27 
val casesN = "cases"; 
49118  28 
val collapseN = "collapse"; 
49054  29 
val disc_exclusN = "disc_exclus"; 
30 
val disc_exhaustN = "disc_exhaust"; 

31 
val discsN = "discs"; 

32 
val distinctN = "distinct"; 

49075  33 
val exhaustN = "exhaust"; 
34 
val injectN = "inject"; 

35 
val nchotomyN = "nchotomy"; 

49054  36 
val selsN = "sels"; 
37 
val splitN = "split"; 

38 
val split_asmN = "split_asm"; 

39 
val weak_case_cong_thmsN = "weak_case_cong"; 

49019  40 

49114  41 
val no_name = @{binding "*"}; 
49046
3c5eba97d93a
allow default names for selectors via wildcard (_) + fix wrong index (k)
blanchet
parents:
49045
diff
changeset

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

43 

49056  44 
fun pad_list x n xs = xs @ replicate (n  length xs) x; 
45 

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

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

49027  49 

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

50 
fun mk_half_pairss ys = mk_half_pairss' [[]] ys; 
49027  51 

49032  52 
val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; 
53 

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

49043  56 
fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
49032  57 

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

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

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

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

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

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

63 

49074  64 
fun prepare_wrap prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess)) 
49054  65 
no_defs_lthy = 
49017  66 
let 
49019  67 
(* TODO: sanity checks on arguments *) 
49113  68 
(* TODO: attributes (simp, case_names, etc.) *) 
69 
(* TODO: case syntax *) 

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

49025  71 

72 
val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; 

73 
val caseof0 = prep_term no_defs_lthy raw_caseof; 

49017  74 

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

77 

49055  78 
val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0))); 
79 
val b = Binding.qualified_name T_name; 

80 

81 
val (As, B) = 

82 
no_defs_lthy 

83 
> mk_TFrees (length As0) 

84 
> the_single o fst o mk_TFrees 1; 

85 

86 
fun mk_ctr Ts ctr = 

87 
let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in 

88 
Term.subst_atomic_types (Ts0 ~~ Ts) ctr 

89 
end; 

90 

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 

95 
val ms = map length ctr_Tss; 

96 

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

97 
val disc_names = 
49056  98 
pad_list default_name n raw_disc_names 
99 
> map2 (fn ctr => fn disc => 

49114  100 
if Binding.eq_name (disc, no_name) then 
101 
NONE 

102 
else if Binding.eq_name (disc, default_name) then 

103 
SOME (Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr)))) 

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

104 
else 
49114  105 
SOME disc) ctrs0; 
49056  106 

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

107 
val no_discs = map is_none disc_names; 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

108 

49054  109 
val sel_namess = 
49056  110 
pad_list [] n raw_sel_namess 
111 
> map3 (fn ctr => fn m => map2 (fn l => fn sel => 

112 
if Binding.eq_name (sel, default_name) then 

113 
Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr))) 

114 
else 

115 
sel) (1 upto m) o pad_list default_name m) ctrs0 ms; 

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

116 

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

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

49022  120 
end; 
121 

49028  122 
val caseofB = mk_caseof As B; 
49025  123 
val caseofB_Ts = map (fn Ts => Ts > B) ctr_Tss; 
124 

49043  125 
fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs); 
126 

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

49025  128 
mk_Freess "x" ctr_Tss 
129 
>> mk_Freess "y" ctr_Tss 

130 
>> mk_Frees "f" caseofB_Ts 

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

132 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T 
49032  133 
>> yield_singleton (mk_Frees "w") T 
49043  134 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; 
135 

136 
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

137 

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

49032  140 

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

143 

144 
val eta_fs = map2 eta_expand_caseof_arg xss xfs; 

145 
val eta_gs = map2 eta_expand_caseof_arg xss xgs; 

146 

147 
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

148 

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

49022  151 

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

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

155 
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

156 

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

157 
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

158 

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

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

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

161 
(case nth disc_names i of NONE => nth exist_xs_v_eq_ctrs i  SOME b => disc_free b $ v); 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

162 

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

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

164 
if n = 2 then Term.lambda v (not_other_disc_lhs (2  k)) else error "Cannot use \"*\" here" 
49025  165 

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

49022  170 
end; 
171 

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

172 
val missing_disc_def = TrueI; (* marker *) 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

173 

49114  174 
val (((raw_discs, raw_disc_defs), (raw_selss, raw_sel_defss)), (lthy', lthy)) = 
49022  175 
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

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

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

178 
if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl) 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

179 
else pair (not_other_disc k, missing_disc_def) 
49114  180 
 SOME b => Specification.definition (SOME (b, NONE, NoSyn), 
181 
((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) 

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

182 
ks ms exist_xs_v_eq_ctrs disc_names 
49114  183 
>> apfst split_list o fold_map3 (fn bs => fn xs => fn k => apfst split_list o 
184 
fold_map2 (fn b => fn x => Specification.definition (SOME (b, NONE, NoSyn), 

185 
((Thm.def_binding b, []), sel_spec b x xs k)) #>> apsnd snd) bs xs) sel_namess xss ks 

49022  186 
> `Local_Theory.restore; 
187 

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

190 

49028  191 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
192 
val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss; 

193 

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

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

49025  196 

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

199 

200 
val discs = map (mk_disc_or_sel As) discs0; 

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

49025  202 

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

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

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

208 
end; 
49019  209 

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

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

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

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

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

217 
map4 mk_goal xctrs yctrs xss yss 
49017  218 
end; 
219 

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

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

221 
map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs); 
49019  222 

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

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

225 
val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases]; 
49019  226 

227 
fun after_qed thmss lthy = 

228 
let 

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

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

230 
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); 
49019  231 

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

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

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

236 
end; 

237 

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

238 
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

239 

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

241 
map2 (map2 append) (Library.chop_groups n half_distinct_thmss) 
49052  242 
(transpose (Library.chop_groups n other_half_distinct_thmss)) 
243 
> `transpose; 

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

244 
val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss); 
49019  245 

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

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

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

248 
val goal = 
49022  249 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', 
49029  250 
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

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

252 
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

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

254 

49030  255 
val sel_thmss = 
49025  256 
let 
49028  257 
fun mk_thm k xs goal_case case_thm x sel_def = 
49025  258 
let 
259 
val T = fastype_of x; 

260 
val cTs = 

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

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

49032  263 
val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T); 
49025  264 
in 
265 
Local_Defs.fold lthy [sel_def] 

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

267 
end; 

49028  268 
fun mk_thms k xs goal_case case_thm sel_defs = 
269 
map2 (mk_thm k xs goal_case case_thm) xs sel_defs; 

49025  270 
in 
49030  271 
map5 mk_thms ks xss goal_cases case_thms sel_defss 
49025  272 
end; 
273 

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

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

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

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

277 
mk_Trueprop_eq (Morphism.term phi (not_other_disc_lhs (2  k)), 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

278 
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

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

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

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

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

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

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

285 

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

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

287 
exists (fn def => Thm.eq_thm_prop (def, missing_disc_def)) disc_defs; 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

288 

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

289 
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

290 
map2 (fn k => fn def => 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

291 
if Thm.eq_thm_prop (def, missing_disc_def) then not_other_disc_def k else def) 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

292 
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

293 

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

294 
val discD_thms = map (fn def => def RS iffD1) disc_defs'; 
49028  295 
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

296 
map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs'; 
49028  297 
val not_disc_thms = 
49030  298 
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

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

300 
ms disc_defs'; 
49028  301 

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

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

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

306 
fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss; 
49027  307 
in 
49114  308 
map3 mk_thms discI_thms not_disc_thms distinct_thmsss' > `transpose 
49027  309 
end; 
49025  310 

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

311 
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

312 

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

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

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

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

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

318 
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

319 
 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

320 
 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

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

322 
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

323 
fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); 
49028  324 

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

325 
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

326 
val half_pairss = mk_half_pairss bundles; 
49028  327 

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

328 
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

329 
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

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

331 
[prove (mk_half_disc_exclus_tac m discD disc_thm) goal]) 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

332 
goal_halvess half_pairss (flat disc_thmss'); 
49028  333 

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

334 
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

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

336 
map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess; 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

338 
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

339 
end; 
49025  340 

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

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

342 
if has_not_other_disc_def orelse forall I no_discs then 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

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

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

346 
fun mk_prem disc = mk_imp_p [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

347 
val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); 
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

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

350 
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

351 
end; 
49025  352 

49118  353 
val collapse_thms = 
49030  354 
let 
355 
fun mk_goal ctr disc sels = 

49114  356 
let 
357 
val prem = HOLogic.mk_Trueprop (betapply (disc, v)); 

358 
val concl = 

359 
mk_Trueprop_eq ((null sels ? swap) 

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

361 
in 

362 
if prem aconv concl then NONE 

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

364 
end; 

49030  365 
val goals = map3 mk_goal ctrs discs selss; 
366 
in 

49114  367 
map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => 
49030  368 
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => 
49118  369 
mk_collapse_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals 
49114  370 
> map_filter I 
49030  371 
end; 
49025  372 

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

373 
val case_eq_thm = 
49031  374 
let 
375 
fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); 

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

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

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

49114  379 
betapply (disc, v) $ mk_core f sels $ mk_rhs discs fs selss; 
49043  380 
val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); 
49031  381 
in 
382 
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

383 
mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) 
49031  384 
> singleton (Proof_Context.export names_lthy lthy) 
385 
end; 

49025  386 

49033  387 
val (case_cong_thm, weak_case_cong_thm) = 
49032  388 
let 
389 
fun mk_prem xctr xs f g = 

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

390 
fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), 
49032  391 
mk_Trueprop_eq (f, g))); 
49033  392 

393 
val v_eq_w = mk_Trueprop_eq (v, w); 

49043  394 
val caseof_fs = mk_caseofB_term eta_fs; 
395 
val caseof_gs = mk_caseofB_term eta_gs; 

49032  396 

397 
val goal = 

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

400 
val goal_weak = 

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

49032  402 
in 
49049  403 
(Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms), 
49033  404 
Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) 
405 
> pairself (singleton (Proof_Context.export names_lthy lthy)) 

49032  406 
end; 
49025  407 

49044  408 
val (split_thm, split_asm_thm) = 
49043  409 
let 
49044  410 
fun mk_conjunct xctr xs f_xs = 
49043  411 
list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs)); 
49044  412 
fun mk_disjunct xctr xs f_xs = 
413 
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr), 

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

415 

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

417 

49043  418 
val goal = 
49044  419 
mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); 
420 
val goal_asm = 

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

422 
(map3 mk_disjunct xctrs xss xfs))); 

423 

424 
val split_thm = 

49049  425 
Skip_Proof.prove lthy [] [] goal 
49052  426 
(fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss) 
49044  427 
> singleton (Proof_Context.export names_lthy lthy) 
428 
val split_asm_thm = 

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

430 
mk_split_asm_tac ctxt split_thm) 

431 
> singleton (Proof_Context.export names_lthy lthy) 

49043  432 
in 
49044  433 
(split_thm, split_asm_thm) 
49043  434 
end; 
49025  435 

49052  436 
val notes = 
437 
[(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

438 
(case_eqN, [case_eq_thm]), 
49052  439 
(casesN, case_thms), 
49118  440 
(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

441 
(discsN, disc_thms), 
49053  442 
(disc_exclusN, disc_exclus_thms), 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

443 
(disc_exhaustN, disc_exhaust_thms), 
49052  444 
(distinctN, distinct_thms), 
445 
(exhaustN, [exhaust_thm]), 

446 
(injectN, (flat inject_thmss)), 

447 
(nchotomyN, [nchotomy_thm]), 

448 
(selsN, (flat sel_thmss)), 

449 
(splitN, [split_thm]), 

450 
(split_asmN, [split_asm_thm]), 

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

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

49019  455 
in 
49052  456 
lthy > Local_Theory.notes notes > snd 
49019  457 
end; 
49017  458 
in 
49025  459 
(goals, after_qed, lthy') 
49017  460 
end; 
461 

49111  462 
fun wrap tacss = (fn (goalss, after_qed, lthy) => 
463 
map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss 

464 
> (fn thms => after_qed thms lthy)) oo 

465 
prepare_wrap (singleton o Type_Infer_Context.infer_types) 

466 

49114  467 
val parse_bindings = Parse.$$$ "["  Parse.list Parse.binding  Parse.$$$ "]"; 
49057  468 
val parse_bindingss = Parse.$$$ "["  Parse.list parse_bindings  Parse.$$$ "]"; 
49017  469 

49074  470 
val wrap_data_cmd = (fn (goalss, after_qed, lthy) => 
49019  471 
Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo 
49074  472 
prepare_wrap Syntax.read_term; 
49017  473 

474 
val _ = 

49074  475 
Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype" 
49023  476 
(((Parse.$$$ "["  Parse.list Parse.term  Parse.$$$ "]")  Parse.term  
49057  477 
Scan.optional (parse_bindings  Scan.optional parse_bindingss []) ([], [])) 
49074  478 
>> wrap_data_cmd); 
49017  479 

480 
end; 