author  kuncar 
Thu, 10 Apr 2014 17:48:16 +0200  
changeset 56522  f54003750e7d 
parent 56376  5a93b8f928a2 
child 56523  2ae16e3d8b6d 
permissions  rwrr 
54701  1 
(* Title: HOL/Tools/Ctr_Sugar/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, 
54900  27 
disc_excludesss: thm list list list, 
53475  28 
disc_exhausts: thm list, 
53916  29 
sel_exhausts: thm list, 
53475  30 
collapses: thm list, 
31 
expands: thm list, 

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

54491  34 
case_eq_ifs: thm list}; 
51809  35 

51840  36 
val morph_ctr_sugar: morphism > ctr_sugar > ctr_sugar 
54256  37 
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

38 
val ctr_sugar_of: Proof.context > string > ctr_sugar option 
53906  39 
val ctr_sugars_of: Proof.context > ctr_sugar list 
54403  40 
val ctr_sugar_of_case: Proof.context > string > ctr_sugar option 
56345  41 
val ctr_sugar_interpretation: (ctr_sugar > theory > theory) > theory > theory 
54399  42 
val register_ctr_sugar: string > ctr_sugar > local_theory > local_theory 
55444
ec73f81e49e7
iteration n in the 'default' vs. 'update_new' vs. 'update' saga  'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents:
55410
diff
changeset

43 
val default_register_ctr_sugar_global: string > ctr_sugar > theory > theory 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

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 
54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54900
diff
changeset

54 
val dest_case: Proof.context > string > typ list > term > 
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54900
diff
changeset

55 
(ctr_sugar * term list * term list) option 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

56 

55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

57 
type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

58 

b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

59 
val disc_of_ctr_spec: ('c, 'a, 'v) ctr_spec > binding 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

60 
val ctr_of_ctr_spec: ('c, 'a, 'v) ctr_spec > 'c 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

61 
val args_of_ctr_spec: ('c, 'a, 'v) ctr_spec > 'a list 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

62 
val sel_defaults_of_ctr_spec: ('c, 'a, 'v) ctr_spec > (binding * 'v) list 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

63 

55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

64 
val free_constructors: ({prems: thm list, context: Proof.context} > tactic) list list > 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

65 
((bool * bool) * binding) * (term, binding, term) ctr_spec list > local_theory > 
51840  66 
ctr_sugar * local_theory 
49286  67 
val parse_bound_term: (binding * string) parser 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

68 
val parse_ctr_options: (bool * bool) parser 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

69 
val parse_ctr_spec: 'c parser > 'a parser > ('c, 'a, string) ctr_spec parser 
49017  70 
end; 
71 

54006  72 
structure Ctr_Sugar : CTR_SUGAR = 
49017  73 
struct 
74 

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

75 
open Ctr_Sugar_Util 
54006  76 
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

77 
open Ctr_Sugar_Code 
49017  78 

51840  79 
type ctr_sugar = 
51839  80 
{ctrs: term list, 
52375  81 
casex: term, 
51839  82 
discs: term list, 
51819  83 
selss: term list list, 
84 
exhaust: thm, 

52375  85 
nchotomy: thm, 
51819  86 
injects: thm list, 
87 
distincts: thm list, 

88 
case_thms: thm list, 

52375  89 
case_cong: thm, 
90 
weak_case_cong: thm, 

91 
split: thm, 

92 
split_asm: thm, 

51819  93 
disc_thmss: thm list list, 
94 
discIs: thm list, 

53475  95 
sel_thmss: thm list list, 
54900  96 
disc_excludesss: thm list list list, 
53475  97 
disc_exhausts: thm list, 
53916  98 
sel_exhausts: thm list, 
53475  99 
collapses: thm list, 
100 
expands: thm list, 

53917  101 
sel_splits: thm list, 
102 
sel_split_asms: thm list, 

54491  103 
case_eq_ifs: thm list}; 
51809  104 

52375  105 
fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, 
53475  106 
case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss, 
54900  107 
disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, 
108 
case_eq_ifs} = 

51839  109 
{ctrs = map (Morphism.term phi) ctrs, 
52375  110 
casex = Morphism.term phi casex, 
51839  111 
discs = map (Morphism.term phi) discs, 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

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

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

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

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

117 
case_thms = map (Morphism.thm phi) case_thms, 
52375  118 
case_cong = Morphism.thm phi case_cong, 
119 
weak_case_cong = Morphism.thm phi weak_case_cong, 

120 
split = Morphism.thm phi split, 

121 
split_asm = Morphism.thm phi split_asm, 

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

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

123 
discIs = map (Morphism.thm phi) discIs, 
53475  124 
sel_thmss = map (map (Morphism.thm phi)) sel_thmss, 
54900  125 
disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss, 
53475  126 
disc_exhausts = map (Morphism.thm phi) disc_exhausts, 
53916  127 
sel_exhausts = map (Morphism.thm phi) sel_exhausts, 
53475  128 
collapses = map (Morphism.thm phi) collapses, 
129 
expands = map (Morphism.thm phi) expands, 

53917  130 
sel_splits = map (Morphism.thm phi) sel_splits, 
131 
sel_split_asms = map (Morphism.thm phi) sel_split_asms, 

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

133 

53906  134 
val transfer_ctr_sugar = 
54740  135 
morph_ctr_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; 
53867
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 
structure Data = Generic_Data 
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

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

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

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

141 
val extend = I; 
55394
d5ebe055b599
more liberal merging of BNFs and constructor sugar
blanchet
parents:
55356
diff
changeset

142 
fun merge data : T = Symtab.merge (K true) data; 
53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

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

144 

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

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

146 
Symtab.lookup (Data.get (Context.Proof ctxt)) 
53906  147 
#> Option.map (transfer_ctr_sugar ctxt); 
148 

149 
fun ctr_sugars_of ctxt = 

150 
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

151 

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

154 

56345  155 
structure Ctr_Sugar_Interpretation = Interpretation 
156 
( 

157 
type T = ctr_sugar; 

158 
val eq: T * T > bool = op = o pairself #ctrs; 

159 
); 

160 

56376
5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56345
diff
changeset

161 
fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy = 
5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56345
diff
changeset

162 
thy 
5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56345
diff
changeset

163 
> Sign.root_path 
5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56345
diff
changeset

164 
> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1))))) 
56522
f54003750e7d
don't forget to init Interpretation and transfer theorems in the interpretation hook
kuncar
parents:
56376
diff
changeset

165 
> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy) 
56376
5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56345
diff
changeset

166 
> Sign.restore_naming thy; 
5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56345
diff
changeset

167 

5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56345
diff
changeset

168 
val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path; 
56345  169 

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

170 
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

171 
Local_Theory.declaration {syntax = false, pervasive = true} 
56345  172 
(fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar))) 
173 
#> Local_Theory.background_theory (Ctr_Sugar_Interpretation.data ctr_sugar); 

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

174 

56345  175 
fun default_register_ctr_sugar_global key ctr_sugar thy = 
176 
let val tab = Data.get (Context.Theory thy) in 

177 
if Symtab.defined tab key then 

178 
thy 

179 
else 

180 
thy 

181 
> Context.theory_map (Data.put (Symtab.update_new (key, ctr_sugar) tab)) 

182 
> Ctr_Sugar_Interpretation.data ctr_sugar 

183 
end; 

54400  184 

49223  185 
val isN = "is_"; 
186 
val unN = "un_"; 

187 
fun mk_unN 1 1 suf = unN ^ suf 

188 
 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

189 

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

190 
val caseN = "case"; 
49054  191 
val case_congN = "case_cong"; 
54491  192 
val case_eq_ifN = "case_eq_if"; 
49118  193 
val collapseN = "collapse"; 
49122  194 
val disc_excludeN = "disc_exclude"; 
49054  195 
val disc_exhaustN = "disc_exhaust"; 
53694  196 
val discN = "disc"; 
53700  197 
val discIN = "discI"; 
49054  198 
val distinctN = "distinct"; 
49075  199 
val exhaustN = "exhaust"; 
49486  200 
val expandN = "expand"; 
49075  201 
val injectN = "inject"; 
202 
val nchotomyN = "nchotomy"; 

53694  203 
val selN = "sel"; 
53916  204 
val sel_exhaustN = "sel_exhaust"; 
53917  205 
val sel_splitN = "sel_split"; 
206 
val sel_split_asmN = "sel_split_asm"; 

49054  207 
val splitN = "split"; 
49633  208 
val splitsN = "splits"; 
49054  209 
val split_asmN = "split_asm"; 
210 
val weak_case_cong_thmsN = "weak_case_cong"; 

49019  211 

53700  212 
val cong_attrs = @{attributes [cong]}; 
53836  213 
val dest_attrs = @{attributes [dest]}; 
53700  214 
val safe_elim_attrs = @{attributes [elim!]}; 
215 
val iff_attrs = @{attributes [iff]}; 

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

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

217 
val nitpicksimp_attrs = @{attributes [nitpick_simp]}; 
49300  218 
val simp_attrs = @{attributes [simp]}; 
54151  219 
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; 
220 
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

221 

55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55471
diff
changeset

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

223 

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

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

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

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

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

228 
fun mk_half_pairss p = mk_half_pairss' [[]] p; 
49027  229 

49486  230 
fun join_halves n half_xss other_half_xss = 
55342  231 
(splice (flat half_xss) (flat other_half_xss), 
232 
map2 (map2 append) (Library.chop_groups n half_xss) 

233 
(transpose (Library.chop_groups n other_half_xss))); 

49027  234 

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

235 
fun mk_undefined T = Const (@{const_name undefined}, T); 
49055  236 

49500  237 
fun mk_ctr Ts t = 
238 
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

239 
subst_nonatomic_types (Ts0 ~~ Ts) t 
49203  240 
end; 
241 

49536  242 
fun mk_case Ts T t = 
243 
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

244 
subst_nonatomic_types ((body, T) :: (Ts0 ~~ Ts)) t 
49536  245 
end; 
246 

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

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

248 
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

249 

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

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

251 
(case head_of t of 
49622  252 
Const (s, _) => s 
253 
 Free (s, _) => s 

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

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

255 

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

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

257 

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

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

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

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

261 

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

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

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

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

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

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

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

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

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

270 
 t' => name_of_const "destructor" t'); 
49622  271 

272 
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

273 

53888  274 
fun dest_ctr ctxt s t = 
55342  275 
let val (f, args) = Term.strip_comb t in 
53888  276 
(case ctr_sugar_of ctxt s of 
277 
SOME {ctrs, ...} => 

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

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

280 
 NONE => raise Fail "dest_ctr") 

281 
 NONE => raise Fail "dest_ctr") 

282 
end; 

283 

53870  284 
fun dest_case ctxt s Ts t = 
285 
(case Term.strip_comb t of 

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

287 
(case ctr_sugar_of ctxt s of 

54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54900
diff
changeset

288 
SOME (ctr_sugar as {casex = Const (case_name, _), discs = discs0, selss = selss0, ...}) => 
53870  289 
if case_name = c then 
53924  290 
let val n = length discs0 in 
291 
if n < length args then 

292 
let 

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

294 
val discs = map (mk_disc_or_sel Ts) discs0; 

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

296 
val conds = map (rapp obj) discs; 

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

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

299 
in 

54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54900
diff
changeset

300 
SOME (ctr_sugar, conds, branches') 
53924  301 
end 
302 
else 

303 
NONE 

53870  304 
end 
305 
else 

306 
NONE 

307 
 _ => NONE) 

308 
 _ => NONE); 

309 

49437  310 
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs; 
311 

55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

312 
type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

313 

b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

314 
fun disc_of_ctr_spec (((disc, _), _), _) = disc; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

315 
fun ctr_of_ctr_spec (((_, ctr), _), _) = ctr; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

316 
fun args_of_ctr_spec ((_, args), _) = args; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

317 
fun sel_defaults_of_ctr_spec (_, ds) = ds; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

318 

b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

319 
fun prepare_free_constructors prep_term (((no_discs_sels, no_code), raw_case_binding), ctr_specs) 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

320 
no_defs_lthy = 
49017  321 
let 
49019  322 
(* TODO: sanity checks on arguments *) 
49025  323 

55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

324 
val raw_ctrs = map ctr_of_ctr_spec ctr_specs; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

325 
val raw_disc_bindings = map disc_of_ctr_spec ctr_specs; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

326 
val raw_sel_bindingss = map args_of_ctr_spec ctr_specs; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

327 
val raw_sel_defaultss = map sel_defaults_of_ctr_spec ctr_specs; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

328 

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

329 
val n = length raw_ctrs; 
49054  330 
val ks = 1 upto n; 
331 

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

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

334 
val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; 
55470
46e6e1d91056
removed needless robustness (no longer needed thanks to new syntax)
blanchet
parents:
55469
diff
changeset

335 
val sel_defaultss = map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss; 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

336 

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

339 
val fc_b = Binding.name fc_b_name; 

49055  340 

55410  341 
fun qualify mandatory = Binding.qualify mandatory fc_b_name; 
49633  342 

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

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

345 
 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

346 

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

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

349 
> variant_tfrees (map (fst o dest_TFree_or_TVar) As0) 
49055  350 
> the_single o fst o mk_TFrees 1; 
351 

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

352 
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

353 

53908  354 
val fcT = Type (fcT_name, As); 
49055  355 
val ctrs = map (mk_ctr As) ctrs0; 
356 
val ctr_Tss = map (binder_types o fastype_of) ctrs; 

357 

358 
val ms = map length ctr_Tss; 

359 

55470
46e6e1d91056
removed needless robustness (no longer needed thanks to new syntax)
blanchet
parents:
55469
diff
changeset

360 
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

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

362 
can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2)); 
53925  363 
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

364 

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

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

366 
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

367 

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

369 

49336  370 
val disc_bindings = 
55470
46e6e1d91056
removed needless robustness (no longer needed thanks to new syntax)
blanchet
parents:
55469
diff
changeset

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

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

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

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

375 
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

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

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

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

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

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

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

382 
disc)) ks ms ctrs0; 
49056  383 

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

384 
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

385 

49336  386 
val sel_bindingss = 
55470
46e6e1d91056
removed needless robustness (no longer needed thanks to new syntax)
blanchet
parents:
55469
diff
changeset

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

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

390 
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

391 
else 
55470
46e6e1d91056
removed needless robustness (no longer needed thanks to new syntax)
blanchet
parents:
55469
diff
changeset

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

393 

49201  394 
val case_Ts = map (fn Ts => Ts > B) ctr_Tss; 
49043  395 

55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

396 
val (((((((([exh_y], (xss, xss')), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) = 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

397 
no_defs_lthy 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

398 
> mk_Frees "y" [fcT] (* for compatibility with "datatype_realizer.ML" *) 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

399 
>> mk_Freess' "x" ctr_Tss 
49025  400 
>> mk_Freess "y" ctr_Tss 
49201  401 
>> mk_Frees "f" case_Ts 
402 
>> mk_Frees "g" case_Ts 

53908  403 
>> (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

404 
>> mk_Frees "z" [B] 
49043  405 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; 
406 

49498  407 
val u = Free u'; 
408 
val v = Free v'; 

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

410 

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

49032  413 

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

416 

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

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

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

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

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

421 

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

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

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

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

425 
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

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

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

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

429 

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

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

431 
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

432 

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

435 
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

436 

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

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

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

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

441 

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

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

443 

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

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

445 

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

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

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

448 

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

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

450 

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

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

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

453 

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

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

455 
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

456 

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

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

458 
val eta_vgcase = eta_gcase $ v; 
49486  459 

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

460 
fun mk_uu_eq () = HOLogic.mk_eq (u, u); 
49486  461 

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

462 
val uv_eq = mk_Trueprop_eq (u, v); 
49486  463 

464 
val exist_xs_u_eq_ctrs = 

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

49022  466 

51743  467 
val unique_disc_no_def = TrueI; (*arbitrary marker*) 
468 
val alternate_disc_no_def = FalseE; (*arbitrary marker*) 

469 

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

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

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

473 
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

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

475 

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

477 
if no_discs_sels then 
55407
81f7e60755c3
use right local theory  shows up when 'no_discs_sels' is set
blanchet
parents:
55394
diff
changeset

478 
(true, [], [], [], [], [], lthy') 
49278  479 
else 
480 
let 

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

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

483 
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

484 

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

49278  487 

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

488 
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

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

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

491 
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

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

493 
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

494 
 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

495 
 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

496 

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

497 
fun sel_spec b proto_sels = 
49278  498 
let 
499 
val _ = 

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

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

502 
" for constructor " ^ 

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

503 
quote (Syntax.string_of_term lthy (nth ctrs (k  1)))) 
49278  504 
 [] => ()) 
505 
val T = 

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

507 
[T] => T 

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

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

509 
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

510 
^ quote (Syntax.string_of_typ lthy T'))); 
49278  511 
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

512 
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

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

515 

49336  516 
val sel_bindings = flat sel_bindingss; 
517 
val uniq_sel_bindings = distinct Binding.eq_name sel_bindings; 

518 
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

519 

49336  520 
val sel_binding_index = 
521 
if all_sels_distinct then 1 upto length sel_bindings 

522 
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

523 

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

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

527 
> sort (int_ord o pairself fst) 
49336  528 
> map snd > curry (op ~~) uniq_sel_bindings; 
529 
val sel_bindings = map fst sel_infos; 

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

530 

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

532 

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

534 
lthy 
51809  535 
> 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

536 
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

537 
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

538 
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

539 
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

540 
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

541 
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

542 
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

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

544 
ks exist_xs_u_eq_ctrs disc_bindings 
49278  545 
>> 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

546 
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

547 
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos 
49278  548 
> `Local_Theory.restore; 
49022  549 

49278  550 
val phi = Proof_Context.export_morphism lthy lthy'; 
49025  551 

49278  552 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
49281  553 
val sel_defs = map (Morphism.thm phi) raw_sel_defs; 
554 
val sel_defss = unflat_selss sel_defs; 

49278  555 

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

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

49028  558 

49278  559 
val discs = map (mk_disc_or_sel As) discs0; 
560 
val selss = map (map (mk_disc_or_sel As)) selss0; 

561 
in 

53917  562 
(all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') 
49278  563 
end; 
49025  564 

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

49458  567 
val exhaust_goal = 
55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

568 
let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (exh_y, xctr)]) in 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

569 
fold_rev Logic.all [p, exh_y] (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

570 
end; 
49019  571 

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

574 
fun mk_goal _ _ [] [] = [] 
49025  575 
 mk_goal xctr yctr xs ys = 
49121  576 
[fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), 
577 
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; 

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

579 
map4 mk_goal xctrs yctrs xss yss 
49017  580 
end; 
581 

49484  582 
val half_distinct_goalss = 
49121  583 
let 
49203  584 
fun mk_goal ((xs, xc), (xs', xc')) = 
49121  585 
fold_rev Logic.all (xs @ xs') 
49203  586 
(HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc')))); 
49121  587 
in 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

588 
map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs))) 
49121  589 
end; 
49019  590 

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

591 
val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss; 
49019  592 

593 
fun after_qed thmss lthy = 

594 
let 

55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

595 
val ([exhaust_thm0], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss)); 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

596 
(* for "datatype_realizer.ML": *) 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

597 
val exhaust_thm = 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

598 
Thm.name_derivation (fcT_name ^ Long_Name.separator ^ exhaustN) exhaust_thm0; 
49019  599 

49438  600 
val inject_thms = flat inject_thmss; 
601 

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

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

604 
fun inst_thm t thm = 

605 
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

606 
(Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm)); 
49486  607 

608 
val uexhaust_thm = inst_thm u exhaust_thm; 

49032  609 

49300  610 
val exhaust_cases = map base_name_of_ctr ctrs; 
611 

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

612 
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

613 

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

615 
join_halves n half_distinct_thmss other_half_distinct_thmss > `transpose; 
49019  616 

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

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

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

619 
val goal = 
49486  620 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u', 
621 
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

622 
in 
51551  623 
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

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

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

626 

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

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

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

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

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

631 
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

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

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

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

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

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

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

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

639 

53917  640 
val (case_cong_thm, weak_case_cong_thm) = 
641 
let 

642 
fun mk_prem xctr xs xf xg = 

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

644 
mk_Trueprop_eq (xf, xg))); 

645 

646 
val goal = 

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

648 
mk_Trueprop_eq (eta_ufcase, eta_vgcase)); 

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

650 
in 

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

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

55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

653 
> pairself (singleton (Proof_Context.export names_lthy lthy) #> 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

654 
Thm.close_derivation) 
53917  655 
end; 
656 

657 
val split_lhs = q $ ufcase; 

658 

659 
fun mk_split_conjunct xctr xs f_xs = 

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

661 
fun mk_split_disjunct xctr xs f_xs = 

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

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

664 

665 
fun mk_split_goal xctrs xss xfs = 

666 
mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj 

667 
(map3 mk_split_conjunct xctrs xss xfs)); 

668 
fun mk_split_asm_goal xctrs xss xfs = 

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

670 
(map3 mk_split_disjunct xctrs xss xfs))); 

671 

672 
fun prove_split selss goal = 

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

674 
mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss) 

55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

675 
> singleton (Proof_Context.export names_lthy lthy) 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

676 
> Thm.close_derivation; 
53917  677 

678 
fun prove_split_asm asm_goal split_thm = 

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

680 
mk_split_asm_tac ctxt split_thm) 

55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

681 
> singleton (Proof_Context.export names_lthy lthy) 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

682 
> Thm.close_derivation; 
53917  683 

684 
val (split_thm, split_asm_thm) = 

685 
let 

686 
val goal = mk_split_goal xctrs xss xfs; 

687 
val asm_goal = mk_split_asm_goal xctrs xss xfs; 

688 

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

690 
val asm_thm = prove_split_asm asm_goal thm; 

691 
in 

692 
(thm, asm_thm) 

693 
end; 

694 

55464  695 
val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms, 
696 
nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms, 

697 
sel_exhaust_thms, all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms, 

698 
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

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

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

702 
let 
53917  703 
val udiscs = map (rapp u) discs; 
704 
val uselss = map (map (rapp u)) selss; 

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

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

707 

708 
val vdiscs = map (rapp v) discs; 

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

710 

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

711 
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

712 
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

713 
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); 
49281  714 

53704  715 
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; 
716 

49281  717 
fun has_undefined_rhs thm = 
718 
(case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of 

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

720 
 _ => false); 

721 

722 
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

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

724 
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

725 
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

726 
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

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

728 
> filter_out has_undefined_rhs; 
49278  729 

730 
fun mk_unique_disc_def () = 

731 
let 

732 
val m = the_single ms; 

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

733 
val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs); 
49278  734 
in 
51551  735 
Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm) 
55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

736 
> singleton (Proof_Context.export names_lthy lthy) 
49692  737 
> Thm.close_derivation 
49278  738 
end; 
739 

740 
fun mk_alternate_disc_def k = 

741 
let 

742 
val goal = 

49486  743 
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3  k), 
744 
nth exist_xs_u_eq_ctrs (k  1)); 

49278  745 
in 
51551  746 
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

747 
mk_alternate_disc_def_tac ctxt k (nth disc_defs (2  k)) 
49486  748 
(nth distinct_thms (2  k)) uexhaust_thm) 
55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

749 
> singleton (Proof_Context.export names_lthy lthy) 
49692  750 
> Thm.close_derivation 
49278  751 
end; 
49028  752 

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

755 

756 
val disc_defs' = 

757 
map2 (fn k => fn def => 

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

759 
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

760 
else def) ks disc_defs; 
49278  761 

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

763 
val discI_thms = 

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

765 
disc_defs'; 

766 
val not_discI_thms = 

767 
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

768 
(unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) 
49278  769 
ms disc_defs'; 
770 

771 
val (disc_thmss', disc_thmss) = 

772 
let 

773 
fun mk_thm discI _ [] = refl RS discI 

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

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

776 
in 

777 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 

778 
end; 

779 

55464  780 
val nontriv_disc_thmss = 
781 
map2 (fn b => if is_disc_binding_valid b then I else K []) disc_bindings disc_thmss; 

53704  782 

783 
fun is_discI_boring b = 

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

785 

786 
val nontriv_discI_thms = 

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

788 
discI_thms); 

49028  789 

49486  790 
val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = 
791 
let 

792 
fun mk_goal [] = [] 

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

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

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

796 

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

797 
fun prove tac goal = 
51551  798 
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

799 
> Thm.close_derivation; 
49486  800 

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

801 
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs)); 
49486  802 

803 
val half_goalss = map mk_goal half_pairss; 

804 
val half_thmss = 

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

51798  806 
fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal]) 
49486  807 
half_goalss half_pairss (flat disc_thmss'); 
49278  808 

49486  809 
val other_half_goalss = map (mk_goal o map swap) half_pairss; 
810 
val other_half_thmss = 

811 
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss 

812 
other_half_goalss; 

813 
in 

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

814 
join_halves n half_thmss other_half_thmss > `transpose 
49486  815 
>> has_alternate_disc_def ? K [] 
816 
end; 

49278  817 

49486  818 
val disc_exhaust_thm = 
819 
let 

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

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

822 
in 

51551  823 
Goal.prove_sorry lthy [] [] goal (fn _ => 
49486  824 
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

825 
> Thm.close_derivation 
49486  826 
end; 
49028  827 

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

830 
fun mk_goal m udisc usel_ctr = 
49486  831 
let 
832 
val prem = HOLogic.mk_Trueprop udisc; 

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

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

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

841 
mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac) 

842 
> Thm.close_derivation 

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

844 
ms discD_thms sel_thmss trivs goals; 

49486  845 
in 
53740  846 
(map_filter (fn (true, _) => NONE  (false, thm) => SOME thm) (trivs ~~ thms), 
847 
thms) 

49486  848 
end; 
49025  849 

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

852 

853 
val sel_exhaust_thm = 

854 
let 

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

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

857 
in 

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

859 
mk_sel_exhaust_tac n disc_exhaust_thm swapped_all_collapse_thms) 

860 
> Thm.close_derivation 

861 
end; 

862 

53919  863 
val expand_thm = 
49486  864 
let 
865 
fun mk_prems k udisc usels vdisc vsels = 

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

867 
(if null usels then 

868 
[] 

869 
else 

870 
[Logic.list_implies 

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

872 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 

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

874 

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

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

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

877 
(map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq); 
49486  878 
val uncollapse_thms = 
53740  879 
map2 (fn thm => fn [] => thm  _ => thm RS sym) all_collapse_thms uselss; 
49486  880 
in 
53919  881 
Goal.prove_sorry lthy [] [] goal (fn _ => 
882 
mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm) 

883 
(inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss 

884 
disc_exclude_thmsss') 

55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

885 
> singleton (Proof_Context.export names_lthy lthy) 
53919  886 
> Thm.close_derivation 
49486  887 
end; 
49278  888 

53917  889 
val (sel_split_thm, sel_split_asm_thm) = 
890 
let 

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

892 
val goal = mk_split_goal usel_ctrs zss usel_fs; 

893 
val asm_goal = mk_split_asm_goal usel_ctrs zss usel_fs; 

894 

895 
val thm = prove_split sel_thmss goal; 

896 
val asm_thm = prove_split_asm asm_goal thm; 

897 
in 

898 
(thm, asm_thm) 

899 
end; 

900 

54491  901 
val case_eq_if_thm = 
49486  902 
let 
53917  903 
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs); 
49486  904 
in 
53919  905 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
54491  906 
mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss) 
55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55407
diff
changeset

907 
> singleton (Proof_Context.export names_lthy lthy) 
53919  908 
> Thm.close_derivation 
49486  909 
end; 
49116
3d520eec2746
allow pseudodefinition of is_Cons in terms of is_Nil (and similarly for other twoconstructor datatypes)
blanchet
parents:
49114
diff
changeset

910 
in 
55464  911 
(all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms, 
54900  912 
nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm], 
913 
[sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm], 

914 
[sel_split_thm], [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

915 
end; 
49025  916 

49437  917 
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); 
53908  918 
val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name)); 
49300  919 

55464  920 
val nontriv_disc_eq_thmss = 
921 
map (map (fn th => th RS @{thm eq_False[THEN iffD2]} 

922 
handle THM _ => th RS @{thm eq_True[THEN iffD2]})) nontriv_disc_thmss; 

923 

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

55464  926 
(flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)] 
54151  927 
> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); 
928 

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

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

931 
(case_congN, [case_cong_thm], []), 
54491  932 
(case_eq_ifN, case_eq_if_thms, []), 
53740  933 
(collapseN, safe_collapse_thms, simp_attrs), 
55464  934 
(discN, flat nontriv_disc_thmss, simp_attrs), 
53700  935 
(discIN, nontriv_discI_thms, []), 
53836  936 
(disc_excludeN, disc_exclude_thms, dest_attrs), 
49300  937 
(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

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

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

943 
(selN, all_sel_thms, code_nitpicksimp_simp_attrs), 
53916  944 
(sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]), 
53917  945 
(sel_splitN, sel_split_thms, []), 
946 
(sel_split_asmN, sel_split_asm_thms, []), 

49300  947 
(splitN, [split_thm], []), 
948 
(split_asmN, [split_asm_thm], []), 

49633  949 
(splitsN, [split_thm, split_asm_thm], []), 
49300  950 
(weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] 
951 
> filter_out (null o #2) 

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

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

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

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

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

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

958 
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

959 
split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss, 
54900  960 
discIs = discI_thms, sel_thmss = sel_thmss, disc_excludesss = disc_exclude_thmsss, 
961 
disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms, 

962 
collapses = all_collapse_thms, expands = expand_thms, sel_splits = sel_split_thms, 

963 
sel_split_asms = sel_split_asm_thms, case_eq_ifs = case_eq_if_thms}; 

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

965 
(ctr_sugar, 
51819  966 
lthy 
55464  967 
> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms) 
55471  968 
> fold (Spec_Rules.add Spec_Rules.Equational) 
55535
10194808430d
name derivations in 'primrec' for code extraction from proof terms
blanchet
parents:
55480
diff
changeset

969 
(AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms)) 
55471  970 
> fold (Spec_Rules.add Spec_Rules.Equational) 
971 
(filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss)) 

55410  972 
> Local_Theory.declaration {syntax = false, pervasive = true} 
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

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

974 
(Morphism.term phi casex) (map (Morphism.term phi) ctrs)) 
54691
506312c293f5
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
traytel
parents:
54635
diff
changeset

975 
> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs]) 
506312c293f5
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
traytel
parents:
54635
diff
changeset

976 
> not no_code ? 
506312c293f5
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
traytel
parents:
54635
diff
changeset

977 
Local_Theory.declaration {syntax = false, pervasive = false} 
506312c293f5
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
traytel
parents:
54635
diff
changeset

978 
(fn phi => Context.mapping 
506312c293f5
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
traytel
parents:
54635
diff
changeset

979 
(add_ctr_code fcT_name (map (Morphism.typ phi) As) 
506312c293f5
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
traytel
parents:
54635
diff
changeset

980 
(map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms) 
506312c293f5
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
traytel
parents:
54635
diff
changeset

981 
(Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms)) 
506312c293f5
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
traytel
parents:
54635
diff
changeset

982 
I) 
54635
30666a281ae3
proper code generation for discriminators/selectors
blanchet
parents:
54634
diff
changeset

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

984 
> register_ctr_sugar fcT_name ctr_sugar) 
49019  985 
end; 
49017  986 
in 
49121  987 
(goalss, after_qed, lthy') 
49017  988 
end; 
989 

55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

990 
fun free_constructors tacss = (fn (goalss, after_qed, lthy) => 
51551  991 
map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss 
55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

992 
> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I); 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

993 

55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

994 
val free_constructors_cmd = (fn (goalss, after_qed, lthy) => 
49297  995 
Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo 
55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

996 
prepare_free_constructors Syntax.read_term; 
49297  997 

55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

998 
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

999 

55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1000 
val parse_ctr_options = 
54626  1001 
Scan.optional (@{keyword "("}  Parse.list1 
55410  1002 
(Parse.reserved "no_discs_sels" >> K 0  Parse.reserved "no_code" >> K 1)  
1003 
@{keyword ")"} 

1004 
>> (fn js => (member (op =) js 0, member (op =) js 1))) 

1005 
(false, false); 

49278  1006 

55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1007 
val parse_defaults = 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1008 
@{keyword "("}  Parse.reserved "defaults"  Scan.repeat parse_bound_term  @{keyword ")"}; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1009 

b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1010 
fun parse_ctr_spec parse_ctr parse_arg = 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1011 
parse_opt_binding_colon  parse_ctr  Scan.repeat parse_arg  
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1012 
Scan.optional parse_defaults []; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1013 

b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1014 
val parse_ctr_specs = Parse.enum1 "" (parse_ctr_spec Parse.term parse_binding); 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1015 

49017  1016 
val _ = 
55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

1017 
Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"} 
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

1018 
"register an existing freely generated type's constructors" 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1019 
(parse_ctr_options  parse_binding  @{keyword "for"}  parse_ctr_specs 
55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

1020 
>> free_constructors_cmd); 
49017  1021 

56522
f54003750e7d
don't forget to init Interpretation and transfer theorems in the interpretation hook
kuncar
parents:
56376
diff
changeset

1022 
val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init); 
f54003750e7d
don't forget to init Interpretation and transfer theorems in the interpretation hook
kuncar
parents:
56376
diff
changeset

1023 

49017  1024 
end; 