author  blanchet 
Thu, 05 Dec 2013 14:35:58 +0100  
changeset 54635  30666a281ae3 
parent 54634  366297517091 
child 54691  506312c293f5 
permissions  rwrr 
54397  1 
(* Title: HOL/Tools/ctr_sugar.ML 
49017  2 
Author: Jasmin Blanchette, TU Muenchen 
54397  3 
Copyright 2012, 2013 
49017  4 

51797  5 
Wrapping existing freely generated type's constructors. 
49017  6 
*) 
7 

54006  8 
signature CTR_SUGAR = 
49017  9 
sig 
51840  10 
type ctr_sugar = 
51839  11 
{ctrs: term list, 
52375  12 
casex: term, 
51839  13 
discs: term list, 
51819  14 
selss: term list list, 
15 
exhaust: thm, 

52375  16 
nchotomy: thm, 
51819  17 
injects: thm list, 
18 
distincts: thm list, 

19 
case_thms: thm list, 

52375  20 
case_cong: thm, 
21 
weak_case_cong: thm, 

22 
split: thm, 

23 
split_asm: thm, 

51819  24 
disc_thmss: thm list list, 
25 
discIs: thm list, 

53475  26 
sel_thmss: thm list list, 
27 
disc_exhausts: thm list, 

53916  28 
sel_exhausts: thm list, 
53475  29 
collapses: thm list, 
30 
expands: thm list, 

53917  31 
sel_splits: thm list, 
32 
sel_split_asms: thm list, 

54491  33 
case_eq_ifs: thm list}; 
51809  34 

51840  35 
val morph_ctr_sugar: morphism > ctr_sugar > ctr_sugar 
54256  36 
val transfer_ctr_sugar: Proof.context > ctr_sugar > ctr_sugar 
53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

37 
val ctr_sugar_of: Proof.context > string > ctr_sugar option 
53906  38 
val ctr_sugars_of: Proof.context > ctr_sugar list 
54403  39 
val ctr_sugar_of_case: Proof.context > string > ctr_sugar option 
54399  40 
val register_ctr_sugar: string > ctr_sugar > local_theory > local_theory 
54400  41 
val register_ctr_sugar_global: string > ctr_sugar > theory > theory 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

42 

49633  43 
val rep_compat_prefix: string 
44 

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

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

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

47 

49203  48 
val mk_ctr: typ list > term > term 
53864
a48d4bd3faaa
use case rather than sequence of ifs in expansion
blanchet
parents:
53857
diff
changeset

49 
val mk_case: typ list > typ > term > term 
49484  50 
val mk_disc_or_sel: typ list > term > term 
49622  51 
val name_of_ctr: term > string 
51777
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

52 
val name_of_disc: term > string 
53888  53 
val dest_ctr: Proof.context > string > term > term * term list 
53870  54 
val dest_case: Proof.context > string > typ list > term > (term list * term list) option 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

55 

51781  56 
val wrap_free_constructors: ({prems: thm list, context: Proof.context} > tactic) list list > 
54626  57 
(((bool * (bool * bool)) * term list) * binding) * 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

58 
(binding list * (binding list list * (binding * term) list list)) > local_theory > 
51840  59 
ctr_sugar * local_theory 
54626  60 
val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser 
49286  61 
val parse_bound_term: (binding * string) parser 
49017  62 
end; 
63 

54006  64 
structure Ctr_Sugar : CTR_SUGAR = 
49017  65 
struct 
66 

54008
b15cfc2864de
refactoring  splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset

67 
open Ctr_Sugar_Util 
54006  68 
open Ctr_Sugar_Tactics 
54615
62fb5af93fe2
generalized datatype code generation code so that it works with oldstyle and newstyle (co)datatypes (as long as they are not local)
blanchet
parents:
54493
diff
changeset

69 
open Ctr_Sugar_Code 
49017  70 

51840  71 
type ctr_sugar = 
51839  72 
{ctrs: term list, 
52375  73 
casex: term, 
51839  74 
discs: term list, 
51819  75 
selss: term list list, 
76 
exhaust: thm, 

52375  77 
nchotomy: thm, 
51819  78 
injects: thm list, 
79 
distincts: thm list, 

80 
case_thms: thm list, 

52375  81 
case_cong: thm, 
82 
weak_case_cong: thm, 

83 
split: thm, 

84 
split_asm: thm, 

51819  85 
disc_thmss: thm list list, 
86 
discIs: thm list, 

53475  87 
sel_thmss: thm list list, 
88 
disc_exhausts: thm list, 

53916  89 
sel_exhausts: thm list, 
53475  90 
collapses: thm list, 
91 
expands: thm list, 

53917  92 
sel_splits: thm list, 
93 
sel_split_asms: thm list, 

54491  94 
case_eq_ifs: thm list}; 
51809  95 

53906  96 
fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar, 
97 
{ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) = 

98 
ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2; 

99 

52375  100 
fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, 
53475  101 
case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss, 
54491  102 
disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} = 
51839  103 
{ctrs = map (Morphism.term phi) ctrs, 
52375  104 
casex = Morphism.term phi casex, 
51839  105 
discs = map (Morphism.term phi) discs, 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

106 
selss = map (map (Morphism.term phi)) selss, 
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

107 
exhaust = Morphism.thm phi exhaust, 
52375  108 
nchotomy = Morphism.thm phi nchotomy, 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

109 
injects = map (Morphism.thm phi) injects, 
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

110 
distincts = map (Morphism.thm phi) distincts, 
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

111 
case_thms = map (Morphism.thm phi) case_thms, 
52375  112 
case_cong = Morphism.thm phi case_cong, 
113 
weak_case_cong = Morphism.thm phi weak_case_cong, 

114 
split = Morphism.thm phi split, 

115 
split_asm = Morphism.thm phi split_asm, 

51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

116 
disc_thmss = map (map (Morphism.thm phi)) disc_thmss, 
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

117 
discIs = map (Morphism.thm phi) discIs, 
53475  118 
sel_thmss = map (map (Morphism.thm phi)) sel_thmss, 
119 
disc_exhausts = map (Morphism.thm phi) disc_exhausts, 

53916  120 
sel_exhausts = map (Morphism.thm phi) sel_exhausts, 
53475  121 
collapses = map (Morphism.thm phi) collapses, 
122 
expands = map (Morphism.thm phi) expands, 

53917  123 
sel_splits = map (Morphism.thm phi) sel_splits, 
124 
sel_split_asms = map (Morphism.thm phi) sel_split_asms, 

54491  125 
case_eq_ifs = map (Morphism.thm phi) case_eq_ifs}; 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

126 

53906  127 
val transfer_ctr_sugar = 
128 
morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of; 

53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

129 

8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

130 
structure Data = Generic_Data 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

131 
( 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

132 
type T = ctr_sugar Symtab.table; 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

133 
val empty = Symtab.empty; 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

134 
val extend = I; 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

135 
val merge = Symtab.merge eq_ctr_sugar; 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

136 
); 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

137 

8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

138 
fun ctr_sugar_of ctxt = 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

139 
Symtab.lookup (Data.get (Context.Proof ctxt)) 
53906  140 
#> Option.map (transfer_ctr_sugar ctxt); 
141 

142 
fun ctr_sugars_of ctxt = 

143 
Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) []; 

53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

144 

54403  145 
fun ctr_sugar_of_case ctxt s = 
146 
find_first (fn {casex = Const (s', _), ...} => s' = s  _ => false) (ctr_sugars_of ctxt); 

147 

53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

148 
fun register_ctr_sugar key ctr_sugar = 
54285
578371ba74cc
reverted 3e1d230f1c00  pervasiveness is useful, cf. Coinductive_Nat in the AFP
blanchet
parents:
54265
diff
changeset

149 
Local_Theory.declaration {syntax = false, pervasive = true} 
53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

150 
(fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar))); 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

151 

54400  152 
fun register_ctr_sugar_global key ctr_sugar = 
153 
Context.theory_map (Data.map (Symtab.default (key, ctr_sugar))); 

154 

49633  155 
val rep_compat_prefix = "new"; 
156 

49223  157 
val isN = "is_"; 
158 
val unN = "un_"; 

159 
fun mk_unN 1 1 suf = unN ^ suf 

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

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

161 

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

162 
val caseN = "case"; 
49054  163 
val case_congN = "case_cong"; 
54491  164 
val case_eq_ifN = "case_eq_if"; 
49118  165 
val collapseN = "collapse"; 
49122  166 
val disc_excludeN = "disc_exclude"; 
49054  167 
val disc_exhaustN = "disc_exhaust"; 
53694  168 
val discN = "disc"; 
53700  169 
val discIN = "discI"; 
49054  170 
val distinctN = "distinct"; 
49075  171 
val exhaustN = "exhaust"; 
49486  172 
val expandN = "expand"; 
49075  173 
val injectN = "inject"; 
174 
val nchotomyN = "nchotomy"; 

53694  175 
val selN = "sel"; 
53916  176 
val sel_exhaustN = "sel_exhaust"; 
53917  177 
val sel_splitN = "sel_split"; 
178 
val sel_split_asmN = "sel_split_asm"; 

49054  179 
val splitN = "split"; 
49633  180 
val splitsN = "splits"; 
49054  181 
val split_asmN = "split_asm"; 
182 
val weak_case_cong_thmsN = "weak_case_cong"; 

49019  183 

53700  184 
val cong_attrs = @{attributes [cong]}; 
53836  185 
val dest_attrs = @{attributes [dest]}; 
53700  186 
val safe_elim_attrs = @{attributes [elim!]}; 
187 
val iff_attrs = @{attributes [iff]}; 

54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54008
diff
changeset

188 
val inductsimp_attrs = @{attributes [induct_simp]}; 
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54008
diff
changeset

189 
val nitpicksimp_attrs = @{attributes [nitpick_simp]}; 
49300  190 
val simp_attrs = @{attributes [simp]}; 
54151  191 
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; 
192 
val code_nitpicksimp_simp_attrs = code_nitpicksimp_attrs @ simp_attrs; 

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

193 

53040  194 
fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys); 
49258
84f13469d7f0
allow same selector name for several constructors
blanchet
parents:
49257
diff
changeset

195 

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

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

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

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

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

200 
fun mk_half_pairss p = mk_half_pairss' [[]] p; 
49027  201 

49486  202 
fun join_halves n half_xss other_half_xss = 
203 
let 

204 
val xsss = 

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

206 
(transpose (Library.chop_groups n other_half_xss)) 

49668  207 
val xs = splice (flat half_xss) (flat other_half_xss); 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

208 
in (xs, xsss) end; 
49027  209 

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

210 
fun mk_undefined T = Const (@{const_name undefined}, T); 
49055  211 

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

54435
4a655e62ad34
fixed type variable confusion in 'datatype_new_compat'
blanchet
parents:
54422
diff
changeset

214 
subst_nonatomic_types (Ts0 ~~ Ts) t 
49203  215 
end; 
216 

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

54435
4a655e62ad34
fixed type variable confusion in 'datatype_new_compat'
blanchet
parents:
54422
diff
changeset

219 
subst_nonatomic_types ((body, T) :: (Ts0 ~~ Ts)) t 
49536  220 
end; 
221 

53864
a48d4bd3faaa
use case rather than sequence of ifs in expansion
blanchet
parents:
53857
diff
changeset

222 
fun mk_disc_or_sel Ts t = 
54435
4a655e62ad34
fixed type variable confusion in 'datatype_new_compat'
blanchet
parents:
54422
diff
changeset

223 
subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t; 
53864
a48d4bd3faaa
use case rather than sequence of ifs in expansion
blanchet
parents:
53857
diff
changeset

224 

51777
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

225 
fun name_of_const what t = 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

226 
(case head_of t of 
49622  227 
Const (s, _) => s 
228 
 Free (s, _) => s 

51777
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

229 
 _ => error ("Cannot extract name of " ^ what)); 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

230 

48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

231 
val name_of_ctr = name_of_const "constructor"; 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

232 

48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

233 
val notN = "not_"; 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

234 
val eqN = "eq_"; 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

235 
val neqN = "neq_"; 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

236 

48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

237 
fun name_of_disc t = 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

238 
(case head_of t of 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

239 
Abs (_, _, @{const Not} $ (t' $ Bound 0)) => 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

240 
Long_Name.map_base_name (prefix notN) (name_of_disc t') 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

241 
 Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') => 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

242 
Long_Name.map_base_name (prefix eqN) (name_of_disc t') 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

243 
 Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) => 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

244 
Long_Name.map_base_name (prefix neqN) (name_of_disc t') 
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51771
diff
changeset

245 
 t' => name_of_const "destructor" t'); 
49622  246 

247 
val base_name_of_ctr = Long_Name.base_name o name_of_ctr; 

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

248 

53888  249 
fun dest_ctr ctxt s t = 
250 
let 

251 
val (f, args) = Term.strip_comb t; 

252 
in 

253 
(case ctr_sugar_of ctxt s of 

254 
SOME {ctrs, ...} => 

255 
(case find_first (can (fo_match ctxt f)) ctrs of 

256 
SOME f' => (f', args) 

257 
 NONE => raise Fail "dest_ctr") 

258 
 NONE => raise Fail "dest_ctr") 

259 
end; 

260 

53870  261 
fun dest_case ctxt s Ts t = 
262 
(case Term.strip_comb t of 

263 
(Const (c, _), args as _ :: _) => 

264 
(case ctr_sugar_of ctxt s of 

265 
SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} => 

266 
if case_name = c then 

53924  267 
let val n = length discs0 in 
268 
if n < length args then 

269 
let 

270 
val (branches, obj :: leftovers) = chop n args; 

271 
val discs = map (mk_disc_or_sel Ts) discs0; 

272 
val selss = map (map (mk_disc_or_sel Ts)) selss0; 

273 
val conds = map (rapp obj) discs; 

274 
val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss; 

275 
val branches' = map2 (curry Term.betapplys) branches branch_argss; 

276 
in 

277 
SOME (conds, branches') 

278 
end 

279 
else 

280 
NONE 

53870  281 
end 
282 
else 

283 
NONE 

284 
 _ => NONE) 

285 
 _ => NONE); 

286 

49437  287 
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
288 

54626  289 
fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs), 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

290 
raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy = 
49017  291 
let 
49019  292 
(* TODO: sanity checks on arguments *) 
49025  293 

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

294 
val n = length raw_ctrs; 
49054  295 
val ks = 1 upto n; 
296 

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

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

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

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

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

302 

53908  303 
val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0)); 
304 
val fc_b_name = Long_Name.base_name fcT_name; 

305 
val fc_b = Binding.name fc_b_name; 

49055  306 

49633  307 
fun qualify mandatory = 
53908  308 
Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix); 
49633  309 

54386  310 
fun dest_TFree_or_TVar (TFree sS) = sS 
53268
de1dc709f9d4
handle type class annotations on (co)datatype parameters gracefully
blanchet
parents:
53210
diff
changeset

311 
 dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S) 
de1dc709f9d4
handle type class annotations on (co)datatype parameters gracefully
blanchet
parents:
53210
diff
changeset

312 
 dest_TFree_or_TVar _ = error "Invalid type argument"; 
52965
0cd62cb233e0
handle both TVars and TFrees  necessary for 'wrap_free_constructors'
blanchet
parents:
52963
diff
changeset

313 

53268
de1dc709f9d4
handle type class annotations on (co)datatype parameters gracefully
blanchet
parents:
53210
diff
changeset

314 
val (unsorted_As, B) = 
49055  315 
no_defs_lthy 
53268
de1dc709f9d4
handle type class annotations on (co)datatype parameters gracefully
blanchet
parents:
53210
diff
changeset

316 
> variant_tfrees (map (fst o dest_TFree_or_TVar) As0) 
49055  317 
> the_single o fst o mk_TFrees 1; 
318 

53268
de1dc709f9d4
handle type class annotations on (co)datatype parameters gracefully
blanchet
parents:
53210
diff
changeset

319 
val As = map2 (resort_tfree o snd o dest_TFree_or_TVar) As0 unsorted_As; 
de1dc709f9d4
handle type class annotations on (co)datatype parameters gracefully
blanchet
parents:
53210
diff
changeset

320 

53908  321 
val fcT = Type (fcT_name, As); 
49055  322 
val ctrs = map (mk_ctr As) ctrs0; 
323 
val ctr_Tss = map (binder_types o fastype_of) ctrs; 

324 

325 
val ms = map length ctr_Tss; 

326 

51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

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

328 

53925  329 
fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k  1))); 
51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

330 
fun can_rely_on_disc k = 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

331 
can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2)); 
53925  332 
fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3  k)); 
51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

333 

22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

334 
fun is_disc_binding_valid b = 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

335 
not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding)); 
51787
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51781
diff
changeset

336 

52322  337 
val standard_disc_binding = Binding.name o prefix isN o base_name_of_ctr; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

338 

49336  339 
val disc_bindings = 
340 
raw_disc_bindings' 

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

341 
> map4 (fn k => fn m => fn ctr => fn disc => 
51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

342 
qualify false 
51787
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51781
diff
changeset

343 
(if Binding.is_empty disc then 
51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

344 
if should_omit_disc_binding k then disc else standard_disc_binding ctr 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

345 
else if Binding.eq_name (disc, equal_binding) then 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

346 
if m = 0 then disc 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

347 
else error "Cannot use \"=\" syntax for discriminating nonnullary constructor" 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

348 
else if Binding.eq_name (disc, standard_binding) then 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

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

350 
else 
51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

351 
disc)) ks ms ctrs0; 
49056  352 

51787
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51781
diff
changeset

353 
fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr; 
49120
7f8e69fc6ac9
smarter "*" syntax  fallback on "_" if "*" is impossible
blanchet
parents:
49119
diff
changeset

354 

49336  355 
val sel_bindingss = 
356 
pad_list [] n raw_sel_bindingss 

49056  357 
> map3 (fn ctr => fn m => map2 (fn l => fn sel => 
49633  358 
qualify false 
51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

359 
(if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then 
51787
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51781
diff
changeset

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

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

362 
sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms; 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

363 

49201  364 
val case_Ts = map (fn Ts => Ts > B) ctr_Tss; 
49043  365 

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

366 
val ((((((((xss, xss'), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) = no_defs_lthy > 
49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

367 
mk_Freess' "x" ctr_Tss 
49025  368 
>> mk_Freess "y" ctr_Tss 
49201  369 
>> mk_Frees "f" case_Ts 
370 
>> mk_Frees "g" case_Ts 

53908  371 
>> (apfst (map (rpair fcT)) oo Variable.variant_fixes) [fc_b_name, fc_b_name ^ "'"] 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

372 
>> mk_Frees "z" [B] 
49043  373 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; 
374 

49498  375 
val u = Free u'; 
376 
val v = Free v'; 

49463  377 
val q = Free (fst p', mk_pred1T B); 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

378 

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

49032  381 

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

384 

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

385 
(* TODO: Etaexpension is for compatibility with the old datatype package (but it also provides 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

386 
nicer names). Consider removing. *) 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

387 
val eta_fs = map2 eta_expand_arg xss xfs; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

388 
val eta_gs = map2 eta_expand_arg xss xgs; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

389 

2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

390 
val case_binding = 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

391 
qualify false 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

392 
(if Binding.is_empty raw_case_binding orelse 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

393 
Binding.eq_name (raw_case_binding, standard_binding) then 
54493
5b34a5b93ec2
use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'
blanchet
parents:
54491
diff
changeset

394 
Binding.prefix_name (caseN ^ "_") fc_b 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

395 
else 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

396 
raw_case_binding); 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

397 

2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

398 
fun mk_case_disj xctr xf xs = 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

399 
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf))); 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

400 

53925  401 
val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]] 
402 
(Const (@{const_name The}, (B > HOLogic.boolT) > B) $ 

403 
Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss))); 

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

404 

2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

405 
val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy 
54155  406 
> Local_Theory.define ((case_binding, NoSyn), 
407 
((Binding.conceal (Thm.def_binding case_binding), []), case_rhs)) 

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

408 
> `Local_Theory.restore; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

409 

2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

410 
val phi = Proof_Context.export_morphism lthy lthy'; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

411 

2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

412 
val case_def = Morphism.thm phi raw_case_def; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

413 

2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

414 
val case0 = Morphism.term phi raw_case; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

415 
val casex = mk_case As B case0; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

416 

51759
587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

417 
val fcase = Term.list_comb (casex, fs); 
587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

418 

587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

419 
val ufcase = fcase $ u; 
587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

420 
val vfcase = fcase $ v; 
587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

421 

587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

422 
val eta_fcase = Term.list_comb (casex, eta_fs); 
587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

423 
val eta_gcase = Term.list_comb (casex, eta_gs); 
49020
f379cf5d71bd
more work on BNF sugar  up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset

424 

51759
587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

425 
val eta_ufcase = eta_fcase $ u; 
587bba425430
etacontracted weak congruence rules (like in the old package)
blanchet
parents:
51757
diff
changeset

426 
val eta_vgcase = eta_gcase $ v; 
49486  427 

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

428 
fun mk_uu_eq () = HOLogic.mk_eq (u, u); 
49486  429 

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

430 
val uv_eq = mk_Trueprop_eq (u, v); 
49486  431 

432 
val exist_xs_u_eq_ctrs = 

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

49022  434 

51743  435 
val unique_disc_no_def = TrueI; (*arbitrary marker*) 
436 
val alternate_disc_no_def = FalseE; (*arbitrary marker*) 

437 

49486  438 
fun alternate_disc_lhs get_udisc k = 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

439 
HOLogic.mk_not 
51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

440 
(let val b = nth disc_bindings (k  1) in 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

441 
if is_disc_binding_valid b then get_udisc b (k  1) else nth exist_xs_u_eq_ctrs (k  1) 
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

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

443 

53917  444 
val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') = 
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52968
diff
changeset

445 
if no_discs_sels then 
53917  446 
(true, [], [], [], [], [], lthy) 
49278  447 
else 
448 
let 

53908  449 
fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT); 
49025  450 

54634
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

451 
fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr); 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

452 

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

49278  455 

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

456 
fun mk_sel_case_args b proto_sels T = 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

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

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

459 
NONE => 
49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

460 
(case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k  1))) b of 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

461 
NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T) 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

462 
 SOME t => t > Type.constraint (Ts > T) > Syntax.check_term lthy) 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

463 
 SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks; 
49258
84f13469d7f0
allow same selector name for several constructors
blanchet
parents:
49257
diff
changeset

464 

54634
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

465 
fun sel_spec b proto_sels = 
49278  466 
let 
467 
val _ = 

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

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

470 
" for constructor " ^ 

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

471 
quote (Syntax.string_of_term lthy (nth ctrs (k  1)))) 
49278  472 
 [] => ()) 
473 
val T = 

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

475 
[T] => T 

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

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

477 
quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. " 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

478 
^ quote (Syntax.string_of_typ lthy T'))); 
49278  479 
in 
54634
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

480 
mk_Trueprop_eq (Free (Binding.name_of b, fcT > T) $ u, 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

481 
Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u) 
49278  482 
end; 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

483 

49336  484 
val sel_bindings = flat sel_bindingss; 
485 
val uniq_sel_bindings = distinct Binding.eq_name sel_bindings; 

486 
val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings); 

49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

487 

49336  488 
val sel_binding_index = 
489 
if all_sels_distinct then 1 upto length sel_bindings 

490 
else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings; 

49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

491 

036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

492 
val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss); 
49300  493 
val sel_infos = 
49336  494 
AList.group (op =) (sel_binding_index ~~ proto_sels) 
49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

495 
> sort (int_ord o pairself fst) 
49336  496 
> map snd > curry (op ~~) uniq_sel_bindings; 
497 
val sel_bindings = map fst sel_infos; 

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

498 

49336  499 
fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss; 
49258
84f13469d7f0
allow same selector name for several constructors
blanchet
parents:
49257
diff
changeset

500 

49278  501 
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

502 
lthy 
51809  503 
> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b => 
54634
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

504 
if Binding.is_empty b then 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

505 
if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

506 
else pair (alternate_disc k, alternate_disc_no_def) 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

507 
else if Binding.eq_name (b, equal_binding) then 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

508 
pair (Term.lambda u exist_xs_u_eq_ctr, refl) 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

509 
else 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

510 
Specification.definition (SOME (b, NONE, NoSyn), 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

511 
((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd) 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

512 
ks exist_xs_u_eq_ctrs disc_bindings 
49278  513 
>> apfst split_list o fold_map (fn (b, proto_sels) => 
54634
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

514 
Specification.definition (SOME (b, NONE, NoSyn), 
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

515 
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos 
49278  516 
> `Local_Theory.restore; 
49022  517 

49278  518 
val phi = Proof_Context.export_morphism lthy lthy'; 
49025  519 

49278  520 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
49281  521 
val sel_defs = map (Morphism.thm phi) raw_sel_defs; 
522 
val sel_defss = unflat_selss sel_defs; 

49278  523 

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

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

49028  526 

49278  527 
val discs = map (mk_disc_or_sel As) discs0; 
528 
val selss = map (map (mk_disc_or_sel As)) selss0; 

529 
in 

53917  530 
(all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') 
49278  531 
end; 
49025  532 

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

49458  535 
val exhaust_goal = 
49486  536 
let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in 
537 
fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss)) 

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

538 
end; 
49019  539 

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

542 
fun mk_goal _ _ [] [] = [] 
49025  543 
 mk_goal xctr yctr xs ys = 
49121  544 
[fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), 
545 
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; 

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

547 
map4 mk_goal xctrs yctrs xss yss 
49017  548 
end; 
549 

49484  550 
val half_distinct_goalss = 
49121  551 
let 
49203  552 
fun mk_goal ((xs, xc), (xs', xc')) = 
49121  553 
fold_rev Logic.all (xs @ xs') 
49203  554 
(HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc')))); 
49121  555 
in 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

556 
map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs))) 
49121  557 
end; 
49019  558 

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

559 
val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss; 
49019  560 

561 
fun after_qed thmss lthy = 

562 
let 

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

563 
val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss)); 
49019  564 

49438  565 
val inject_thms = flat inject_thmss; 
566 

53210
7219c61796c0
simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
blanchet
parents:
53040
diff
changeset

567 
val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As); 
49486  568 

569 
fun inst_thm t thm = 

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

53210
7219c61796c0
simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
blanchet
parents:
53040
diff
changeset

571 
(Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm)); 
49486  572 

573 
val uexhaust_thm = inst_thm u exhaust_thm; 

49032  574 

49300  575 
val exhaust_cases = map base_name_of_ctr ctrs; 
576 

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

577 
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

578 

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

580 
join_halves n half_distinct_thmss other_half_distinct_thmss > `transpose; 
49019  581 

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

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

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

584 
val goal = 
49486  585 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u', 
586 
Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs)); 

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

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

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

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

591 

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

592 
val case_thms = 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

593 
let 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

594 
val goals = 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

595 
map3 (fn xctr => fn xf => fn xs => 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

596 
fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

597 
in 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

598 
map4 (fn k => fn goal => fn injects => fn distinctss => 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

599 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

600 
mk_case_tac ctxt n k case_def injects distinctss) 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

601 
> Thm.close_derivation) 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

602 
ks goals inject_thmss distinct_thmsss 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

603 
end; 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

604 

53917  605 
val (case_cong_thm, weak_case_cong_thm) = 
606 
let 

607 
fun mk_prem xctr xs xf xg = 

608 
fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr), 

609 
mk_Trueprop_eq (xf, xg))); 

610 

611 
val goal = 

612 
Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs, 

613 
mk_Trueprop_eq (eta_ufcase, eta_vgcase)); 

614 
val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); 

615 
in 

616 
(Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms), 

617 
Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1))) 

618 
> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy)) 

619 
end; 

620 

621 
val split_lhs = q $ ufcase; 

622 

623 
fun mk_split_conjunct xctr xs f_xs = 

624 
list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs)); 

625 
fun mk_split_disjunct xctr xs f_xs = 

626 
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), 

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

628 

629 
fun mk_split_goal xctrs xss xfs = 

630 
mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj 

631 
(map3 mk_split_conjunct xctrs xss xfs)); 

632 
fun mk_split_asm_goal xctrs xss xfs = 

633 
mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj 

634 
(map3 mk_split_disjunct xctrs xss xfs))); 

635 

636 
fun prove_split selss goal = 

637 
Goal.prove_sorry lthy [] [] goal (fn _ => 

638 
mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss) 

639 
> Thm.close_derivation 

640 
> singleton (Proof_Context.export names_lthy lthy); 

641 

642 
fun prove_split_asm asm_goal split_thm = 

643 
Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} => 

644 
mk_split_asm_tac ctxt split_thm) 

645 
> Thm.close_derivation 

646 
> singleton (Proof_Context.export names_lthy lthy); 

647 

648 
val (split_thm, split_asm_thm) = 

649 
let 

650 
val goal = mk_split_goal xctrs xss xfs; 

651 
val asm_goal = mk_split_asm_goal xctrs xss xfs; 

652 

653 
val thm = prove_split (replicate n []) goal; 

654 
val asm_thm = prove_split_asm asm_goal thm; 

655 
in 

656 
(thm, asm_thm) 

657 
end; 

658 

53704  659 
val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms, 
53916  660 
disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, 
54491  661 
safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) = 
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52968
diff
changeset

662 
if no_discs_sels then 
53917  663 
([], [], [], [], [], [], [], [], [], [], [], [], [], [], []) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

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

665 
let 
53917  666 
val udiscs = map (rapp u) discs; 
667 
val uselss = map (map (rapp u)) selss; 

668 
val usel_ctrs = map2 (curry Term.list_comb) ctrs uselss; 

669 
val usel_fs = map2 (curry Term.list_comb) fs uselss; 

670 

671 
val vdiscs = map (rapp v) discs; 

672 
val vselss = map (map (rapp v)) selss; 

673 

49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

674 
fun make_sel_thm xs' case_thm sel_def = 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

675 
zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs') 
54634
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

676 
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); 
49281  677 

53704  678 
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; 
679 

49281  680 
fun has_undefined_rhs thm = 
681 
(case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of 

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

683 
 _ => false); 

684 

685 
val all_sel_thms = 

49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

686 
(if all_sels_distinct andalso forall null sel_defaultss then 
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

687 
flat sel_thmss 
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

688 
else 
49364
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

689 
map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs 
838b5e8ede73
allow default values to refer to selector arguments  this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet
parents:
49336
diff
changeset

690 
(xss' ~~ case_thms)) 
49285
036b833b99aa
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
blanchet
parents:
49281
diff
changeset

691 
> filter_out has_undefined_rhs; 
49278  692 

693 
fun mk_unique_disc_def () = 

694 
let 

695 
val m = the_single ms; 

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

696 
val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs); 
49278  697 
in 
51551  698 
Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm) 
49692  699 
> Thm.close_derivation 
49278  700 
> singleton (Proof_Context.export names_lthy lthy) 
701 
end; 

702 

703 
fun mk_alternate_disc_def k = 

704 
let 

705 
val goal = 

49486  706 
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3  k), 
707 
nth exist_xs_u_eq_ctrs (k  1)); 

49278  708 
in 
51551  709 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
54634
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

710 
mk_alternate_disc_def_tac ctxt k (nth disc_defs (2  k)) 
49486  711 
(nth distinct_thms (2  k)) uexhaust_thm) 
49692  712 
> Thm.close_derivation 
49278  713 
> singleton (Proof_Context.export names_lthy lthy) 
714 
end; 

49028  715 

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

718 

719 
val disc_defs' = 

720 
map2 (fn k => fn def => 

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

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

54634
366297517091
reverted 141cb34744de and e78e7df36690  better provide nicer "etaexpanded" definitions for discriminators and selectors, since users might want to unfold them
blanchet
parents:
54626
diff
changeset

723 
else def) ks disc_defs; 
49278  724 

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

726 
val discI_thms = 

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

728 
disc_defs'; 

729 
val not_discI_thms = 

730 
map2 (fn m => fn def => funpow m (fn thm => allI RS thm) 

49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49500
diff
changeset

731 
(unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) 
49278  732 
ms disc_defs'; 
733 

734 
val (disc_thmss', disc_thmss) = 

735 
let 

736 
fun mk_thm discI _ [] = refl RS discI 

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

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

739 
in 

740 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 

741 
end; 

742 

53704  743 
val nontriv_disc_thms = 
744 
flat (map2 (fn b => if is_disc_binding_valid b then I else K []) 

745 
disc_bindings disc_thmss); 

746 

747 
fun is_discI_boring b = 

748 
(n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding); 

749 

750 
val nontriv_discI_thms = 

751 
flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings 

752 
discI_thms); 

49028  753 

49486  754 
val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = 
755 
let 

756 
fun mk_goal [] = [] 

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

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

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

760 

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

761 
fun prove tac goal = 
51551  762 
Goal.prove_sorry lthy [] [] goal (K tac) 
49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

763 
> Thm.close_derivation; 
49486  764 

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

765 
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs)); 
49486  766 

767 
val half_goalss = map mk_goal half_pairss; 

768 
val half_thmss = 

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

51798  770 
fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal]) 
49486  771 
half_goalss half_pairss (flat disc_thmss'); 
49278  772 

49486  773 
val other_half_goalss = map (mk_goal o map swap) half_pairss; 
774 
val other_half_thmss = 

775 
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss 

776 
other_half_goalss; 

777 
in 

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

778 
join_halves n half_thmss other_half_thmss > `transpose 
49486  779 
>> has_alternate_disc_def ? K [] 
780 
end; 

49278  781 

49486  782 
val disc_exhaust_thm = 
783 
let 

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

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

786 
in 

51551  787 
Goal.prove_sorry lthy [] [] goal (fn _ => 
49486  788 
mk_disc_exhaust_tac n exhaust_thm discI_thms) 
49667
44d85dc8ca08
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
traytel
parents:
49633
diff
changeset

789 
> Thm.close_derivation 
49486  790 
end; 
49028  791 

53740  792 
val (safe_collapse_thms, all_collapse_thms) = 
49486  793 
let 
54008
b15cfc2864de
refactoring  splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset

794 
fun mk_goal m udisc usel_ctr = 
49486  795 
let 
796 
val prem = HOLogic.mk_Trueprop udisc; 

53916  797 
val concl = mk_Trueprop_eq ((usel_ctr, u) > m = 0 ? swap); 
49486  798 
in 
53740  799 
(prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl))) 
49486  800 
end; 
54008
b15cfc2864de
refactoring  splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset

801 
val (trivs, goals) = map3 mk_goal ms udiscs usel_ctrs > split_list; 
53740  802 
val thms = 
803 
map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal => 

804 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 

805 
mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac) 

806 
> Thm.close_derivation 

807 
> not triv ? perhaps (try (fn thm => refl RS thm))) 

808 
ms discD_thms sel_thmss trivs goals; 

49486  809 
in 
53740  810 
(map_filter (fn (true, _) => NONE  (false, thm) => SOME thm) (trivs ~~ thms), 
811 
thms) 

49486  812 
end; 
49025  813 

53916  814 
val swapped_all_collapse_thms = 
815 
map2 (fn m => fn thm => if m = 0 then thm else thm RS sym) ms all_collapse_thms; 

816 

817 
val sel_exhaust_thm = 

818 
let 

819 
fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)]; 

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

821 
in 

822 
Goal.prove_sorry lthy [] [] goal (fn _ => 

823 
mk_sel_exhaust_tac n disc_exhaust_thm swapped_all_collapse_thms) 

824 
> Thm.close_derivation 

825 
end; 

826 

53919  827 
val expand_thm = 
49486  828 
let 
829 
fun mk_prems k udisc usels vdisc vsels = 

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

831 
(if null usels then 

832 
[] 

833 
else 

834 
[Logic.list_implies 

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

836 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 

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

838 

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

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

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

841 
(map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq); 
49486  842 
val uncollapse_thms = 
53740  843 
map2 (fn thm => fn [] => thm  _ => thm RS sym) all_collapse_thms uselss; 
49486  844 
in 
53919  845 
Goal.prove_sorry lthy [] [] goal (fn _ => 
846 
mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm) 

847 
(inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss 

848 
disc_exclude_thmsss') 

849 
> Thm.close_derivation 

850 
> singleton (Proof_Context.export names_lthy lthy) 

49486  851 
end; 
49278  852 

53917  853 
val (sel_split_thm, sel_split_asm_thm) = 
854 
let 

855 
val zss = map (K []) xss; 

856 
val goal = mk_split_goal usel_ctrs zss usel_fs; 

857 
val asm_goal = mk_split_asm_goal usel_ctrs zss usel_fs; 

858 

859 
val thm = prove_split sel_thmss goal; 

860 
val asm_thm = prove_split_asm asm_goal thm; 

861 
in 

862 
(thm, asm_thm) 

863 
end; 

864 

54491  865 
val case_eq_if_thm = 
49486  866 
let 
53917  867 
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs); 
49486  868 
in 
53919  869 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
54491  870 
mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss) 
53919  871 
> Thm.close_derivation 
872 
> singleton (Proof_Context.export names_lthy lthy) 

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

874 
in 
53704  875 
(all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, 
53916  876 
nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm], 
53919  877 
all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm], 
54491  878 
[sel_split_asm_thm], [case_eq_if_thm]) 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

879 
end; 
49025  880 

49437  881 
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); 
53908  882 
val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name)); 
49300  883 

54151  884 
val anonymous_notes = 
885 
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs), 

886 
(map (fn th => th RS @{thm eq_False[THEN iffD2]} 

887 
handle THM _ => th RS @{thm eq_True[THEN iffD2]}) nontriv_disc_thms, 

888 
code_nitpicksimp_attrs)] 

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

890 

49052  891 
val notes = 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54008
diff
changeset

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

893 
(case_congN, [case_cong_thm], []), 
54491  894 
(case_eq_ifN, case_eq_if_thms, []), 
53740  895 
(collapseN, safe_collapse_thms, simp_attrs), 
53704  896 
(discN, nontriv_disc_thms, simp_attrs), 
53700  897 
(discIN, nontriv_discI_thms, []), 
53836  898 
(disc_excludeN, disc_exclude_thms, dest_attrs), 
49300  899 
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54008
diff
changeset

900 
(distinctN, distinct_thms, simp_attrs @ inductsimp_attrs), 
49300  901 
(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]), 
49486  902 
(expandN, expand_thms, []), 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54008
diff
changeset

903 
(injectN, inject_thms, iff_attrs @ inductsimp_attrs), 
49300  904 
(nchotomyN, [nchotomy_thm], []), 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54008
diff
changeset

905 
(selN, all_sel_thms, code_nitpicksimp_simp_attrs), 
53916  906 
(sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]), 
53917  907 
(sel_splitN, sel_split_thms, []), 
908 
(sel_split_asmN, sel_split_asm_thms, []), 

49300  909 
(splitN, [split_thm], []), 
910 
(split_asmN, [split_asm_thm], []), 

49633  911 
(splitsN, [split_thm, split_asm_thm], []), 
49300  912 
(weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] 
913 
> filter_out (null o #2) 

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

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

53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

917 
val ctr_sugar = 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

918 
{ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm, 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

919 
nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms, 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

920 
case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm, 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

921 
split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss, 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

922 
discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms, 
53916  923 
sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms, 
53917  924 
sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms, 
54491  925 
case_eq_ifs = case_eq_if_thms}; 
49019  926 
in 
53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

927 
(ctr_sugar, 
51819  928 
lthy 
929 
> not rep_compat ? 

54615
62fb5af93fe2
generalized datatype code generation code so that it works with oldstyle and newstyle (co)datatypes (as long as they are not local)
blanchet
parents:
54493
diff
changeset

930 
Local_Theory.declaration {syntax = false, pervasive = true} 
62fb5af93fe2
generalized datatype code generation code so that it works with oldstyle and newstyle (co)datatypes (as long as they are not local)
blanchet
parents:
54493
diff
changeset

931 
(fn phi => Case_Translation.register 
62fb5af93fe2
generalized datatype code generation code so that it works with oldstyle and newstyle (co)datatypes (as long as they are not local)
blanchet
parents:
54493
diff
changeset

932 
(Morphism.term phi casex) (map (Morphism.term phi) ctrs)) 
54626  933 
> (not no_code andalso null (Thm.hyps_of (hd case_thms))) 
54617
1183bd511980
don't try to register code equations in a locale with assumptions
blanchet
parents:
54615
diff
changeset

934 
? Local_Theory.background_theory 
54635
30666a281ae3
proper code generation for discriminators/selectors
blanchet
parents:
54634
diff
changeset

935 
(fold (fold Code.del_eqn) [disc_defs, sel_defs] 
30666a281ae3
proper code generation for discriminators/selectors
blanchet
parents:
54634
diff
changeset

936 
#> add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms 
30666a281ae3
proper code generation for discriminators/selectors
blanchet
parents:
54634
diff
changeset

937 
case_thms) 
30666a281ae3
proper code generation for discriminators/selectors
blanchet
parents:
54634
diff
changeset

938 
> Local_Theory.notes (anonymous_notes @ notes) > snd 
30666a281ae3
proper code generation for discriminators/selectors
blanchet
parents:
54634
diff
changeset

939 
> register_ctr_sugar fcT_name ctr_sugar) 
49019  940 
end; 
49017  941 
in 
49121  942 
(goalss, after_qed, lthy') 
49017  943 
end; 
944 

51781  945 
fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) => 
51551  946 
map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss 
51781  947 
> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I); 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

948 

51781  949 
val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) => 
49297  950 
Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo 
51781  951 
prepare_wrap_free_constructors Syntax.read_term; 
49297  952 

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

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

51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

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

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

957 

51790
22517d04d20b
more intuitive syntax for equalitystyle discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset

958 
val parse_bound_term = (parse_binding  @{keyword ":"})  Parse.term; 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

959 
val parse_bound_terms = parse_bracket_list parse_bound_term; 
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

960 
val parse_bound_termss = parse_bracket_list parse_bound_terms; 
49017  961 

52823  962 
val parse_wrap_free_constructors_options = 
54626  963 
Scan.optional (@{keyword "("}  Parse.list1 
964 
(Parse.reserved "no_discs_sels" >> K 0  Parse.reserved "no_code" >> K 1  

965 
Parse.reserved "rep_compat" >> K 2)  @{keyword ")"} 

966 
>> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2)))) 

967 
(false, (false, false)); 

49278  968 

49017  969 
val _ = 
51781  970 
Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"} 
51797  971 
"wrap an existing freely generated type's constructors" 
52823  972 
((parse_wrap_free_constructors_options  (@{keyword "["}  Parse.list Parse.term  
973 
@{keyword "]"})  

52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

974 
parse_binding  Scan.optional (parse_bindings  Scan.optional (parse_bindingss  
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

975 
Scan.optional parse_bound_termss []) ([], [])) ([], ([], []))) 
51781  976 
>> wrap_free_constructors_cmd); 
49017  977 

978 
end; 