author  blanchet 
Thu, 11 Sep 2014 20:01:29 +0200  
changeset 58317  21fac057681e 
parent 58289  eb93bc67d361 
child 58335  a5a3b576fcfb 
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 
58191  10 
val code_plugin: string 
11 

51840  12 
type ctr_sugar = 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

13 
{T: typ, 
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

14 
ctrs: term list, 
52375  15 
casex: term, 
51839  16 
discs: term list, 
51819  17 
selss: term list list, 
18 
exhaust: thm, 

52375  19 
nchotomy: thm, 
51819  20 
injects: thm list, 
21 
distincts: thm list, 

22 
case_thms: thm list, 

52375  23 
case_cong: thm, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

24 
case_cong_weak: thm, 
52375  25 
split: thm, 
26 
split_asm: thm, 

56858  27 
disc_defs: thm list, 
51819  28 
disc_thmss: thm list list, 
29 
discIs: thm list, 

56858  30 
sel_defs: thm list, 
53475  31 
sel_thmss: thm list list, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

32 
distinct_discsss: thm list list list, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

33 
exhaust_discs: thm list, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

34 
exhaust_sels: thm list, 
53475  35 
collapses: thm list, 
36 
expands: thm list, 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

37 
split_sels: thm list, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

38 
split_sel_asms: thm list, 
54491  39 
case_eq_ifs: thm list}; 
51809  40 

51840  41 
val morph_ctr_sugar: morphism > ctr_sugar > ctr_sugar 
58115  42 
val transfer_ctr_sugar: theory > ctr_sugar > ctr_sugar 
53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

43 
val ctr_sugar_of: Proof.context > string > ctr_sugar option 
58116  44 
val ctr_sugar_of_global: theory > string > ctr_sugar option 
53906  45 
val ctr_sugars_of: Proof.context > ctr_sugar list 
58116  46 
val ctr_sugars_of_global: theory > ctr_sugar list 
54403  47 
val ctr_sugar_of_case: Proof.context > string > ctr_sugar option 
58116  48 
val ctr_sugar_of_case_global: theory > string > ctr_sugar option 
58186  49 
val ctr_sugar_interpretation: string > (ctr_sugar > theory > theory) > 
58177
166131276380
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
blanchet
parents:
58176
diff
changeset

50 
(ctr_sugar > local_theory > local_theory) > theory > theory 
58188  51 
val interpret_ctr_sugar: (string > bool) > ctr_sugar > local_theory > local_theory 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

52 
val register_ctr_sugar_raw: ctr_sugar > local_theory > local_theory 
58188  53 
val register_ctr_sugar: (string > bool) > ctr_sugar > local_theory > local_theory 
54 
val default_register_ctr_sugar_global: (string > bool) > ctr_sugar > theory > theory 

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

55 

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

56 
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

57 
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

58 

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

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

63 
val name_of_disc: term > string 
53888  64 
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

65 
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

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

67 

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

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

69 

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

70 
val disc_of_ctr_spec: ('c, 'a) ctr_spec > binding 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

71 
val ctr_of_ctr_spec: ('c, 'a) ctr_spec > 'c 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

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

73 

58191  74 
type ctr_options = (string > bool) * bool 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

75 

57830
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

76 
val fake_local_theory_for_sel_defaults: (binding * typ) list > Proof.context > Proof.context 
55468
98b25c51e9e5
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents:
55464
diff
changeset

77 
val free_constructors: ({prems: thm list, context: Proof.context} > tactic) list list > 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

78 
((ctr_options * binding) * (term, binding) ctr_spec list) * term list > local_theory > 
51840  79 
ctr_sugar * local_theory 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

80 
val default_ctr_options: ctr_options 
49286  81 
val parse_bound_term: (binding * string) parser 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

82 
val parse_ctr_options: ctr_options parser 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

83 
val parse_ctr_spec: 'c parser > 'a parser > ('c, 'a) ctr_spec parser 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

84 
val parse_sel_default_eqs: string list parser 
49017  85 
end; 
86 

54006  87 
structure Ctr_Sugar : CTR_SUGAR = 
49017  88 
struct 
89 

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

90 
open Ctr_Sugar_Util 
54006  91 
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

92 
open Ctr_Sugar_Code 
49017  93 

58191  94 
val code_plugin = "code" 
95 

51840  96 
type ctr_sugar = 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

97 
{T: typ, 
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

98 
ctrs: term list, 
52375  99 
casex: term, 
51839  100 
discs: term list, 
51819  101 
selss: term list list, 
102 
exhaust: thm, 

52375  103 
nchotomy: thm, 
51819  104 
injects: thm list, 
105 
distincts: thm list, 

106 
case_thms: thm list, 

52375  107 
case_cong: thm, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

108 
case_cong_weak: thm, 
52375  109 
split: thm, 
110 
split_asm: thm, 

56858  111 
disc_defs: thm list, 
51819  112 
disc_thmss: thm list list, 
113 
discIs: thm list, 

56858  114 
sel_defs: thm list, 
53475  115 
sel_thmss: thm list list, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

116 
distinct_discsss: thm list list list, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

117 
exhaust_discs: thm list, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

118 
exhaust_sels: thm list, 
53475  119 
collapses: thm list, 
120 
expands: thm list, 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

121 
split_sels: thm list, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

122 
split_sel_asms: thm list, 
54491  123 
case_eq_ifs: thm list}; 
51809  124 

58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

125 
fun morph_ctr_sugar phi {T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

126 
case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

127 
sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

128 
split_sel_asms, case_eq_ifs} = 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

129 
{T = Morphism.typ phi T, 
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

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

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

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

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

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

138 
case_thms = map (Morphism.thm phi) case_thms, 
52375  139 
case_cong = Morphism.thm phi case_cong, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

140 
case_cong_weak = Morphism.thm phi case_cong_weak, 
52375  141 
split = Morphism.thm phi split, 
142 
split_asm = Morphism.thm phi split_asm, 

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

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

145 
discIs = map (Morphism.thm phi) discIs, 
56858  146 
sel_defs = map (Morphism.thm phi) sel_defs, 
53475  147 
sel_thmss = map (map (Morphism.thm phi)) sel_thmss, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

148 
distinct_discsss = map (map (map (Morphism.thm phi))) distinct_discsss, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

149 
exhaust_discs = map (Morphism.thm phi) exhaust_discs, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

150 
exhaust_sels = map (Morphism.thm phi) exhaust_sels, 
53475  151 
collapses = map (Morphism.thm phi) collapses, 
152 
expands = map (Morphism.thm phi) expands, 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

153 
split_sels = map (Morphism.thm phi) split_sels, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

154 
split_sel_asms = map (Morphism.thm phi) split_sel_asms, 
54491  155 
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

156 

58115  157 
val transfer_ctr_sugar = morph_ctr_sugar o Morphism.transfer_morphism; 
53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53864
diff
changeset

158 

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

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

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

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

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

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

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

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

166 

58116  167 
fun ctr_sugar_of_generic context = 
168 
Option.map (transfer_ctr_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context); 

169 

170 
fun ctr_sugars_of_generic context = 

171 
Symtab.fold (cons o transfer_ctr_sugar (Context.theory_of context) o snd) (Data.get context) []; 

53906  172 

58116  173 
fun ctr_sugar_of_case_generic context s = 
174 
find_first (fn {casex = Const (s', _), ...} => s' = s  _ => false) 

175 
(ctr_sugars_of_generic context); 

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

176 

58116  177 
val ctr_sugar_of = ctr_sugar_of_generic o Context.Proof; 
178 
val ctr_sugar_of_global = ctr_sugar_of_generic o Context.Theory; 

179 

180 
val ctr_sugars_of = ctr_sugars_of_generic o Context.Proof; 

181 
val ctr_sugars_of_global = ctr_sugars_of_generic o Context.Theory; 

182 

183 
val ctr_sugar_of_case = ctr_sugar_of_case_generic o Context.Proof; 

184 
val ctr_sugar_of_case_global = ctr_sugar_of_case_generic o Context.Theory; 

54403  185 

58177
166131276380
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
blanchet
parents:
58176
diff
changeset

186 
structure Ctr_Sugar_Interpretation = Local_Interpretation 
56345  187 
( 
188 
type T = ctr_sugar; 

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

190 
); 

191 

58185  192 
fun with_transfer_ctr_sugar g ctr_sugar thy = g (transfer_ctr_sugar 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

193 

58186  194 
fun ctr_sugar_interpretation name = 
195 
Ctr_Sugar_Interpretation.interpretation name o with_transfer_ctr_sugar; 

56345  196 

58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

197 
val interpret_ctr_sugar = Ctr_Sugar_Interpretation.data; 
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

198 

d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

199 
fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) = 
54285
578371ba74cc
reverted 3e1d230f1c00  pervasiveness is useful, cf. Coinductive_Nat in the AFP
blanchet
parents:
54265
diff
changeset

200 
Local_Theory.declaration {syntax = false, pervasive = true} 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

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

202 

58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

203 
fun register_ctr_sugar plugins ctr_sugar = 
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

204 
register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar plugins ctr_sugar; 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

205 

58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

206 
fun default_register_ctr_sugar_global plugins (ctr_sugar as {T = Type (s, _), ...}) thy = 
56345  207 
let val tab = Data.get (Context.Theory thy) in 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

208 
if Symtab.defined tab s then 
56345  209 
thy 
210 
else 

211 
thy 

58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

212 
> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab)) 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

213 
> Ctr_Sugar_Interpretation.data_global plugins ctr_sugar 
56345  214 
end; 
54400  215 

49223  216 
val isN = "is_"; 
217 
val unN = "un_"; 

57629
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

218 
val notN = "not_"; 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

219 

49223  220 
fun mk_unN 1 1 suf = unN ^ suf 
221 
 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

222 

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

223 
val caseN = "case"; 
49054  224 
val case_congN = "case_cong"; 
54491  225 
val case_eq_ifN = "case_eq_if"; 
49118  226 
val collapseN = "collapse"; 
53694  227 
val discN = "disc"; 
53700  228 
val discIN = "discI"; 
49054  229 
val distinctN = "distinct"; 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

230 
val distinct_discN = "distinct_disc"; 
49075  231 
val exhaustN = "exhaust"; 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

232 
val exhaust_discN = "exhaust_disc"; 
49486  233 
val expandN = "expand"; 
49075  234 
val injectN = "inject"; 
235 
val nchotomyN = "nchotomy"; 

53694  236 
val selN = "sel"; 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

237 
val exhaust_selN = "exhaust_sel"; 
49054  238 
val splitN = "split"; 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

239 
val split_asmN = "split_asm"; 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

240 
val split_selN = "split_sel"; 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

241 
val split_sel_asmN = "split_sel_asm"; 
49633  242 
val splitsN = "splits"; 
57984
cbe9a16f8e11
added collection theorem for consistency and convenience
blanchet
parents:
57983
diff
changeset

243 
val split_selsN = "split_sels"; 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

244 
val case_cong_weak_thmsN = "case_cong_weak"; 
49019  245 

53700  246 
val cong_attrs = @{attributes [cong]}; 
53836  247 
val dest_attrs = @{attributes [dest]}; 
53700  248 
val safe_elim_attrs = @{attributes [elim!]}; 
249 
val iff_attrs = @{attributes [iff]}; 

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

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

251 
val nitpicksimp_attrs = @{attributes [nitpick_simp]}; 
49300  252 
val simp_attrs = @{attributes [simp]}; 
54151  253 
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; 
254 
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

255 

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

256 
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

257 

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

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

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

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

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

262 
fun mk_half_pairss p = mk_half_pairss' [[]] p; 
49027  263 

49486  264 
fun join_halves n half_xss other_half_xss = 
55342  265 
(splice (flat half_xss) (flat other_half_xss), 
266 
map2 (map2 append) (Library.chop_groups n half_xss) 

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

49027  268 

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

269 
fun mk_undefined T = Const (@{const_name undefined}, T); 
49055  270 

49500  271 
fun mk_ctr Ts t = 
272 
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

273 
subst_nonatomic_types (Ts0 ~~ Ts) t 
49203  274 
end; 
275 

49536  276 
fun mk_case Ts T t = 
277 
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

278 
subst_nonatomic_types ((body, T) :: (Ts0 ~~ Ts)) t 
49536  279 
end; 
280 

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

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

282 
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

283 

58284
f9b6af3017fd
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
blanchet
parents:
58256
diff
changeset

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

285 

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

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

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

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

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

290 
 Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') => 
57260
8747af0d1012
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
blanchet
parents:
57200
diff
changeset

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

292 
 Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) => 
57260
8747af0d1012
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
blanchet
parents:
57200
diff
changeset

293 
Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t') 
58289  294 
 t' => name_of_const "discriminator" (perhaps (try domain_type)) t'); 
49622  295 

296 
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

297 

53888  298 
fun dest_ctr ctxt s t = 
55342  299 
let val (f, args) = Term.strip_comb t in 
53888  300 
(case ctr_sugar_of ctxt s of 
301 
SOME {ctrs, ...} => 

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

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

304 
 NONE => raise Fail "dest_ctr") 

305 
 NONE => raise Fail "dest_ctr") 

306 
end; 

307 

53870  308 
fun dest_case ctxt s Ts t = 
309 
(case Term.strip_comb t of 

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

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

312 
SOME (ctr_sugar as {casex = Const (case_name, _), discs = discs0, selss = selss0, ...}) => 
53870  313 
if case_name = c then 
53924  314 
let val n = length discs0 in 
315 
if n < length args then 

316 
let 

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

318 
val discs = map (mk_disc_or_sel Ts) discs0; 

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

320 
val conds = map (rapp obj) discs; 

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

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

323 
in 

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

324 
SOME (ctr_sugar, conds, branches') 
53924  325 
end 
326 
else 

327 
NONE 

53870  328 
end 
329 
else 

330 
NONE 

331 
 _ => NONE) 

332 
 _ => NONE); 

333 

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

334 
fun const_or_free_name (Const (s, _)) = Long_Name.base_name s 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

335 
 const_or_free_name (Free (s, _)) = s 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

336 
 const_or_free_name t = raise TERM ("const_or_free_name", [t]) 
49437  337 

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

338 
fun extract_sel_default ctxt t = 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

339 
let 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

340 
fun malformed () = 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

341 
error ("Malformed selector default value equation: " ^ Syntax.string_of_term ctxt t); 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

342 

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

343 
val ((sel, (ctr, vars)), rhs) = 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

344 
fst (Term.replace_dummy_patterns (Syntax.check_term ctxt t) 0) 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

345 
> HOLogic.dest_eq 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

346 
>> (Term.dest_comb 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

347 
#>> const_or_free_name 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

348 
##> (Term.strip_comb #>> (Term.dest_Const #> fst))) 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

349 
handle TERM _ => malformed (); 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

350 
in 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

351 
if forall (is_Free orf is_Var) vars andalso not (has_duplicates (op aconv) vars) then 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

352 
((ctr, sel), fold_rev Term.lambda vars rhs) 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

353 
else 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

354 
malformed () 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

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

356 

57830
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

357 
(* Ideally, we would enrich the context with constants rather than free variables. *) 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

358 
fun fake_local_theory_for_sel_defaults sel_bTs = 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

359 
Proof_Context.allow_dummies 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

360 
#> Proof_Context.add_fixes (map (fn (b, T) => (b, SOME T, NoSyn)) sel_bTs) 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

361 
#> snd; 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

362 

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

363 
type ('c, 'a) ctr_spec = (binding * 'c) * 'a list; 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

364 

aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

365 
fun disc_of_ctr_spec ((disc, _), _) = disc; 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

366 
fun ctr_of_ctr_spec ((_, ctr), _) = ctr; 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

367 
fun args_of_ctr_spec (_, args) = args; 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

368 

58191  369 
fun prepare_free_constructors prep_term ((((plugins, discs_sels), raw_case_binding), ctr_specs), 
370 
sel_default_eqs) no_defs_lthy = 

49017  371 
let 
49019  372 
(* TODO: sanity checks on arguments *) 
49025  373 

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

374 
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

375 
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

376 
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

377 

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

378 
val n = length raw_ctrs; 
49054  379 
val ks = 1 upto n; 
380 

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

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

383 
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

384 

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

387 
val fc_b = Binding.name fc_b_name; 

49055  388 

55410  389 
fun qualify mandatory = Binding.qualify mandatory fc_b_name; 
49633  390 

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

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

393 
> variant_tfrees (map (fst o dest_TFree_or_TVar) As0) 
49055  394 
> the_single o fst o mk_TFrees 1; 
395 

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

397 

53908  398 
val fcT = Type (fcT_name, As); 
49055  399 
val ctrs = map (mk_ctr As) ctrs0; 
400 
val ctr_Tss = map (binder_types o fastype_of) ctrs; 

401 

402 
val ms = map length ctr_Tss; 

403 

57091  404 
fun can_definitely_rely_on_disc k = 
405 
not (Binding.is_empty (nth raw_disc_bindings (k  1))) orelse nth ms (k  1) = 0; 

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

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

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

409 

57090
0224caba67ca
use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
blanchet
parents:
57038
diff
changeset

410 
val equal_binding = @{binding "="}; 
0224caba67ca
use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
blanchet
parents:
57038
diff
changeset

411 

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

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

413 
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

414 

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

416 

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

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

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

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

421 
(if Binding.is_empty disc then 
57091  422 
if m = 0 then equal_binding 
423 
else if should_omit_disc_binding k then disc 

57090
0224caba67ca
use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
blanchet
parents:
57038
diff
changeset

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

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

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

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

428 
disc)) ks ms ctrs0; 
49056  429 

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

430 
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

431 

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

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

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

436 
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

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

438 
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

439 

49201  440 
val case_Ts = map (fn Ts => Ts > B) ctr_Tss; 
49043  441 

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

442 
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

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

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

445 
>> mk_Freess' "x" ctr_Tss 
49025  446 
>> mk_Freess "y" ctr_Tss 
49201  447 
>> mk_Frees "f" case_Ts 
448 
>> mk_Frees "g" case_Ts 

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

450 
>> mk_Frees "z" [B] 
49043  451 
>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; 
452 

49498  453 
val u = Free u'; 
454 
val v = Free v'; 

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

456 

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

49032  459 

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

462 

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

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

464 
nicer names). Consider removing. *) 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

465 
val eta_fs = map2 (fold_rev Term.lambda) xss xfs; 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

466 
val eta_gs = map2 (fold_rev Term.lambda) xss xgs; 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52965
diff
changeset

467 

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

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

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

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

471 
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

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

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

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

475 

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

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

477 
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

478 

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

481 
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

482 

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

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

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

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

487 

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

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

489 

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

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

491 

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

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

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

494 

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

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

496 

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

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

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

499 

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

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

501 
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

502 

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

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

504 
val eta_vgcase = eta_gcase $ v; 
49486  505 

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

506 
fun mk_uu_eq () = HOLogic.mk_eq (u, u); 
49486  507 

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

508 
val uv_eq = mk_Trueprop_eq (u, v); 
49486  509 

510 
val exist_xs_u_eq_ctrs = 

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

49022  512 

51743  513 
val unique_disc_no_def = TrueI; (*arbitrary marker*) 
514 
val alternate_disc_no_def = FalseE; (*arbitrary marker*) 

515 

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

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

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

519 
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

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

521 

57094
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset

522 
val no_discs_sels = 
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset

523 
not discs_sels andalso 
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset

524 
forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

525 
null sel_default_eqs; 
57094
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset

526 

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

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

529 
(true, [], [], [], [], [], lthy') 
49278  530 
else 
531 
let 

57830
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

532 
val all_sel_bindings = flat sel_bindingss; 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

533 
val num_all_sel_bindings = length all_sel_bindings; 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

534 
val uniq_sel_bindings = distinct Binding.eq_name all_sel_bindings; 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

535 
val all_sels_distinct = (length uniq_sel_bindings = num_all_sel_bindings); 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

536 

aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

537 
val sel_binding_index = 
57830
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

538 
if all_sels_distinct then 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

539 
1 upto num_all_sel_bindings 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

540 
else 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

541 
map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings; 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

542 

57830
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

543 
val all_proto_sels = flat (map3 (fn k => fn xs => map (pair k o pair xs)) ks xss xss); 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

544 
val sel_infos = 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

545 
AList.group (op =) (sel_binding_index ~~ all_proto_sels) 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

546 
> sort (int_ord o pairself fst) 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

547 
> map snd > curry (op ~~) uniq_sel_bindings; 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

548 
val sel_bindings = map fst sel_infos; 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

549 

aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

550 
val sel_defaults = 
57830
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

551 
if null sel_default_eqs then 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

552 
[] 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

553 
else 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

554 
let 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

555 
val sel_Ts = map (curry (op >) fcT o fastype_of o snd o snd o hd o snd) sel_infos; 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

556 
val fake_lthy = 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

557 
fake_local_theory_for_sel_defaults (sel_bindings ~~ sel_Ts) no_defs_lthy; 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

558 
in 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

559 
map (extract_sel_default fake_lthy o prep_term fake_lthy) sel_default_eqs 
2d0f0d6fdf3e
correctly resolve selector names in default value equations
blanchet
parents:
57633
diff
changeset

560 
end; 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

561 

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

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

564 
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

565 

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

49278  568 

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

569 
fun mk_sel_case_args b proto_sels T = 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

570 
map3 (fn Const (c, _) => fn Ts => fn k => 
49280
52413dc96326
allow default values for selectors in lowlevel "wrap_data" command
blanchet
parents:
49278
diff
changeset

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

572 
NONE => 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

573 
(case filter (curry (op =) (c, Binding.name_of b) o fst) sel_defaults of 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

574 
[] => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T) 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

575 
 [(_, t)] => t 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

576 
 _ => error "Multiple default values for selector/constructor pair") 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

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

578 

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

579 
fun sel_spec b proto_sels = 
49278  580 
let 
581 
val _ = 

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

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

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

584 
" for constructor " ^ quote (Syntax.string_of_term lthy (nth ctrs (k  1)))) 
49278  585 
 [] => ()) 
586 
val T = 

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

588 
[T] => T 

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

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

590 
quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

591 
" vs. " ^ quote (Syntax.string_of_typ lthy T'))); 
49278  592 
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

593 
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

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

596 

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

598 

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

600 
lthy 
51809  601 
> 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

602 
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

603 
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

604 
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

605 
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

606 
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

607 
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

608 
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

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

610 
ks exist_xs_u_eq_ctrs disc_bindings 
49278  611 
>> 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

612 
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

613 
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos 
49278  614 
> `Local_Theory.restore; 
49022  615 

49278  616 
val phi = Proof_Context.export_morphism lthy lthy'; 
49025  617 

49278  618 
val disc_defs = map (Morphism.thm phi) raw_disc_defs; 
49281  619 
val sel_defs = map (Morphism.thm phi) raw_sel_defs; 
620 
val sel_defss = unflat_selss sel_defs; 

49278  621 

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

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

49028  624 

49278  625 
val discs = map (mk_disc_or_sel As) discs0; 
626 
val selss = map (map (mk_disc_or_sel As)) selss0; 

627 
in 

53917  628 
(all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') 
49278  629 
end; 
49025  630 

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

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

634 
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

635 
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

636 
end; 
49019  637 

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

640 
fun mk_goal _ _ [] [] = [] 
49025  641 
 mk_goal xctr yctr xs ys = 
49121  642 
[fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), 
643 
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; 

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

645 
map4 mk_goal xctrs yctrs xss yss 
49017  646 
end; 
647 

49484  648 
val half_distinct_goalss = 
49121  649 
let 
49203  650 
fun mk_goal ((xs, xc), (xs', xc')) = 
49121  651 
fold_rev Logic.all (xs @ xs') 
49203  652 
(HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc')))); 
49121  653 
in 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset

654 
map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs))) 
49121  655 
end; 
49019  656 

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

657 
val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss; 
49019  658 

57633  659 
fun after_qed ([exhaust_thm] :: thmss) lthy = 
49019  660 
let 
57633  661 
val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss >> `flat; 
49438  662 

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

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

665 
fun inst_thm t thm = 

666 
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

667 
(Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm)); 
49486  668 

669 
val uexhaust_thm = inst_thm u exhaust_thm; 

49032  670 

49300  671 
val exhaust_cases = map base_name_of_ctr ctrs; 
672 

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

673 
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

674 

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

676 
join_halves n half_distinct_thmss other_half_distinct_thmss > `transpose; 
49019  677 

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

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

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

680 
val goal = 
49486  681 
HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u', 
682 
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

683 
in 
51551  684 
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

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

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

687 

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

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

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

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

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

692 
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

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

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

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

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

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

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

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

700 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

701 
val (case_cong_thm, case_cong_weak_thm) = 
53917  702 
let 
703 
fun mk_prem xctr xs xf xg = 

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

705 
mk_Trueprop_eq (xf, xg))); 

706 

707 
val goal = 

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

709 
mk_Trueprop_eq (eta_ufcase, eta_vgcase)); 

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

711 
in 

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

713 
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

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

715 
Thm.close_derivation) 
53917  716 
end; 
717 

718 
val split_lhs = q $ ufcase; 

719 

720 
fun mk_split_conjunct xctr xs f_xs = 

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

722 
fun mk_split_disjunct xctr xs f_xs = 

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

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

725 

726 
fun mk_split_goal xctrs xss xfs = 

727 
mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj 

728 
(map3 mk_split_conjunct xctrs xss xfs)); 

729 
fun mk_split_asm_goal xctrs xss xfs = 

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

731 
(map3 mk_split_disjunct xctrs xss xfs))); 

732 

733 
fun prove_split selss goal = 

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

735 
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

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

737 
> Thm.close_derivation; 
53917  738 

739 
fun prove_split_asm asm_goal split_thm = 

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

741 
mk_split_asm_tac ctxt split_thm) 

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

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

743 
> Thm.close_derivation; 
53917  744 

745 
val (split_thm, split_asm_thm) = 

746 
let 

747 
val goal = mk_split_goal xctrs xss xfs; 

748 
val asm_goal = mk_split_asm_goal xctrs xss xfs; 

749 

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

751 
val asm_thm = prove_split_asm asm_goal thm; 

752 
in 

753 
(thm, asm_thm) 

754 
end; 

755 

56858  756 
val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

757 
discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

758 
exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

759 
expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms) = 
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52968
diff
changeset

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

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

763 
let 
53917  764 
val udiscs = map (rapp u) discs; 
765 
val uselss = map (map (rapp u)) selss; 

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

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

768 

769 
val vdiscs = map (rapp v) discs; 

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

771 

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

772 
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

773 
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

774 
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); 
49281  775 

53704  776 
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; 
777 

49281  778 
fun has_undefined_rhs thm = 
779 
(case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of 

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

781 
 _ => false); 

782 

783 
val all_sel_thms = 

57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

784 
(if all_sels_distinct andalso null sel_default_eqs then 
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

785 
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

786 
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

787 
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

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

789 
> filter_out has_undefined_rhs; 
49278  790 

791 
fun mk_unique_disc_def () = 

792 
let 

793 
val m = the_single ms; 

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

794 
val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs); 
49278  795 
in 
51551  796 
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

797 
> singleton (Proof_Context.export names_lthy lthy) 
49692  798 
> Thm.close_derivation 
49278  799 
end; 
800 

801 
fun mk_alternate_disc_def k = 

802 
let 

803 
val goal = 

49486  804 
mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3  k), 
805 
nth exist_xs_u_eq_ctrs (k  1)); 

49278  806 
in 
51551  807 
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

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

810 
> singleton (Proof_Context.export names_lthy lthy) 
49692  811 
> Thm.close_derivation 
49278  812 
end; 
49028  813 

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

816 

817 
val disc_defs' = 

818 
map2 (fn k => fn def => 

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

820 
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

821 
else def) ks disc_defs; 
49278  822 

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

824 
val discI_thms = 

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

826 
disc_defs'; 

827 
val not_discI_thms = 

828 
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

829 
(unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) 
49278  830 
ms disc_defs'; 
831 

832 
val (disc_thmss', disc_thmss) = 

833 
let 

834 
fun mk_thm discI _ [] = refl RS discI 

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

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

837 
in 

838 
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' > `transpose 

839 
end; 

840 

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

53704  843 

844 
fun is_discI_boring b = 

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

846 

847 
val nontriv_discI_thms = 

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

849 
discI_thms); 

49028  850 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

851 
val (distinct_disc_thms, (distinct_disc_thmsss', distinct_disc_thmsss)) = 
49486  852 
let 
853 
fun mk_goal [] = [] 

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

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

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

857 

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

858 
fun prove tac goal = 
51551  859 
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

860 
> Thm.close_derivation; 
49486  861 

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

862 
val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs)); 
49486  863 

864 
val half_goalss = map mk_goal half_pairss; 

865 
val half_thmss = 

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

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

867 
fn disc_thm => [prove (mk_half_distinct_disc_tac lthy m discD disc_thm) goal]) 
49486  868 
half_goalss half_pairss (flat disc_thmss'); 
49278  869 

49486  870 
val other_half_goalss = map (mk_goal o map swap) half_pairss; 
871 
val other_half_thmss = 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

872 
map2 (map2 (prove o mk_other_half_distinct_disc_tac)) half_thmss 
49486  873 
other_half_goalss; 
874 
in 

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

875 
join_halves n half_thmss other_half_thmss > `transpose 
49486  876 
>> has_alternate_disc_def ? K [] 
877 
end; 

49278  878 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

879 
val exhaust_disc_thm = 
49486  880 
let 
881 
fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc]; 

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

883 
in 

51551  884 
Goal.prove_sorry lthy [] [] goal (fn _ => 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

885 
mk_exhaust_disc_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

886 
> Thm.close_derivation 
49486  887 
end; 
49028  888 

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

891 
fun mk_goal m udisc usel_ctr = 
49486  892 
let 
893 
val prem = HOLogic.mk_Trueprop udisc; 

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

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

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

902 
mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac) 

903 
> Thm.close_derivation 

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

905 
ms discD_thms sel_thmss trivs goals; 

49486  906 
in 
53740  907 
(map_filter (fn (true, _) => NONE  (false, thm) => SOME thm) (trivs ~~ thms), 
908 
thms) 

49486  909 
end; 
49025  910 

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

913 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

914 
val exhaust_sel_thm = 
53916  915 
let 
916 
fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)]; 

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

918 
in 

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

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

920 
mk_exhaust_sel_tac n exhaust_disc_thm swapped_all_collapse_thms) 
53916  921 
> Thm.close_derivation 
922 
end; 

923 

53919  924 
val expand_thm = 
49486  925 
let 
926 
fun mk_prems k udisc usels vdisc vsels = 

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

928 
(if null usels then 

929 
[] 

930 
else 

931 
[Logic.list_implies 

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

933 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 

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

935 

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

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

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

938 
(map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq); 
49486  939 
val uncollapse_thms = 
53740  940 
map2 (fn thm => fn [] => thm  _ => thm RS sym) all_collapse_thms uselss; 
49486  941 
in 
53919  942 
Goal.prove_sorry lthy [] [] goal (fn _ => 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

943 
mk_expand_tac lthy n ms (inst_thm u exhaust_disc_thm) 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

944 
(inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

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

946 
> singleton (Proof_Context.export names_lthy lthy) 
53919  947 
> Thm.close_derivation 
49486  948 
end; 
49278  949 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

950 
val (split_sel_thm, split_sel_asm_thm) = 
53917  951 
let 
952 
val zss = map (K []) xss; 

953 
val goal = mk_split_goal usel_ctrs zss usel_fs; 

954 
val asm_goal = mk_split_asm_goal usel_ctrs zss usel_fs; 

955 

956 
val thm = prove_split sel_thmss goal; 

957 
val asm_thm = prove_split_asm asm_goal thm; 

958 
in 

959 
(thm, asm_thm) 

960 
end; 

961 

54491  962 
val case_eq_if_thm = 
49486  963 
let 
53917  964 
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs); 
49486  965 
in 
53919  966 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
54491  967 
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

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

971 
in 
56858  972 
(sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

973 
discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

974 
[exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

975 
[expand_thm], [split_sel_thm], [split_sel_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

976 
end; 
49025  977 

49437  978 
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); 
53908  979 
val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name)); 
49300  980 

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

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

984 

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

55464  987 
(flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)] 
54151  988 
> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); 
989 

49052  990 
val notes = 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

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

992 
(case_congN, [case_cong_thm], []), 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

993 
(case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs), 
54491  994 
(case_eq_ifN, case_eq_if_thms, []), 
58151
414deb2ef328
take out 'x = C' of the simplifier for unit types
blanchet
parents:
58116
diff
changeset

995 
(collapseN, safe_collapse_thms, if ms = [0] then [] else simp_attrs), 
55464  996 
(discN, flat nontriv_disc_thmss, simp_attrs), 
53700  997 
(discIN, nontriv_discI_thms, []), 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54008
diff
changeset

998 
(distinctN, distinct_thms, simp_attrs @ inductsimp_attrs), 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

999 
(distinct_discN, distinct_disc_thms, dest_attrs), 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1000 
(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]), 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1001 
(exhaust_discN, exhaust_disc_thms, [exhaust_case_names_attr]), 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1002 
(exhaust_selN, exhaust_sel_thms, [exhaust_case_names_attr]), 
49486  1003 
(expandN, expand_thms, []), 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54008
diff
changeset

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

1006 
(selN, all_sel_thms, code_nitpicksimp_simp_attrs), 
57985  1007 
(splitN, [split_thm], []), 
1008 
(split_asmN, [split_asm_thm], []), 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1009 
(split_selN, split_sel_thms, []), 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1010 
(split_sel_asmN, split_sel_asm_thms, []), 
57985  1011 
(split_selsN, split_sel_thms @ split_sel_asm_thms, []), 
1012 
(splitsN, [split_thm, split_asm_thm], [])] 

49300  1013 
> filter_out (null o #2) 
1014 
> map (fn (thmN, thms, attrs) => 

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

57629
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1017 
val (noted, lthy') = 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1018 
lthy 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1019 
> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1020 
> fold (Spec_Rules.add Spec_Rules.Equational) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1021 
(AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms)) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1022 
> fold (Spec_Rules.add Spec_Rules.Equational) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1023 
(filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss)) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1024 
> Local_Theory.declaration {syntax = false, pervasive = true} 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1025 
(fn phi => Case_Translation.register 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1026 
(Morphism.term phi casex) (map (Morphism.term phi) ctrs)) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1027 
> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs]) 
58191  1028 
> plugins code_plugin ? 
57629
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1029 
Local_Theory.declaration {syntax = false, pervasive = false} 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1030 
(fn phi => Context.mapping 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1031 
(add_ctr_code fcT_name (map (Morphism.typ phi) As) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1032 
(map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1033 
(Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms)) 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1034 
I) 
57633  1035 
> Local_Theory.notes (anonymous_notes @ notes) 
58317  1036 
(* for "datatype_realizer.ML": *) 
57633  1037 
>> name_noted_thms fcT_name exhaustN; 
57629
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1038 

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

1039 
val ctr_sugar = 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58186
diff
changeset

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

1041 
nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1042 
case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm, 
56858  1043 
split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs, 
1044 
disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss, 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1045 
distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1046 
exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57882
diff
changeset

1047 
split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms, 
57629
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1048 
case_eq_ifs = case_eq_if_thms} 
e88b5f59cade
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
blanchet
parents:
57260
diff
changeset

1049 
> morph_ctr_sugar (substitute_noted_thm noted); 
49019  1050 
in 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

1051 
(ctr_sugar, lthy' > register_ctr_sugar plugins ctr_sugar) 
49019  1052 
end; 
49017  1053 
in 
49121  1054 
(goalss, after_qed, lthy') 
49017  1055 
end; 
1056 

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

1057 
fun free_constructors tacss = (fn (goalss, after_qed, lthy) => 
51551  1058 
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

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

1060 

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

1061 
val free_constructors_cmd = (fn (goalss, after_qed, lthy) => 
49297  1062 
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

1063 
prepare_free_constructors Syntax.read_term; 
49297  1064 

57091  1065 
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

1066 

58224  1067 
type ctr_options = (string > bool) * bool; 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

1068 

58224  1069 
val default_ctr_options = (K true, false) : ctr_options; 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

1070 

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

1071 
val parse_ctr_options = 
54626  1072 
Scan.optional (@{keyword "("}  Parse.list1 
58191  1073 
(parse_plugins >> (apfst o K)  Parse.reserved "discs_sels" >> (apsnd o K o K true))  
55410  1074 
@{keyword ")"} 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

1075 
>> (fn fs => fold I fs default_ctr_options)) 
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset

1076 
default_ctr_options; 
49278  1077 

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

1078 
fun parse_ctr_spec parse_ctr parse_arg = 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

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

1080 

57091  1081 
val parse_ctr_specs = Parse.enum1 "" (parse_ctr_spec Parse.term Parse.binding); 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

1082 
val parse_sel_default_eqs = Scan.optional (@{keyword "where"}  Parse.enum1 "" Parse.prop) []; 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1083 

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

1085 
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

1086 
"register an existing freely generated type's constructors" 
57091  1087 
(parse_ctr_options  Parse.binding  @{keyword "for"}  parse_ctr_specs 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57094
diff
changeset

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

1089 
>> free_constructors_cmd); 
49017  1090 

58256
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58234
diff
changeset

1091 
val _ = Theory.setup Ctr_Sugar_Interpretation.init; 
56522
f54003750e7d
don't forget to init Interpretation and transfer theorems in the interpretation hook
kuncar
parents:
56376
diff
changeset

1092 

49017  1093 
end; 