author  blanchet 
Mon, 03 Mar 2014 12:48:20 +0100  
changeset 55869  54ddb003e128 
parent 55868  37b99986d435 
child 55871  a28817253b31 
permissions  rwrr 
55061  1 
(* Title: HOL/Tools/BNF/bnf_fp_def_sugar.ML 
49112  2 
Author: Jasmin Blanchette, TU Muenchen 
52349  3 
Copyright 2012, 2013 
49112  4 

49389  5 
Sugared datatype and codatatype constructions. 
49112  6 
*) 
7 

49636  8 
signature BNF_FP_DEF_SUGAR = 
49112  9 
sig 
51840  10 
type fp_sugar = 
51859  11 
{T: typ, 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

12 
X: typ, 
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

13 
fp: BNF_Util.fp_kind, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

14 
fp_res_index: int, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

15 
fp_res: BNF_FP_Util.fp_result, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

16 
pre_bnf: BNF_Def.bnf, 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

17 
absT_info: BNF_Comp.absT_info, 
52356  18 
nested_bnfs: BNF_Def.bnf list, 
53267
aad7d276b849
store nesting_bnfs in fp_sugar (required in "nested to mutual" reduction)
traytel
parents:
53266
diff
changeset

19 
nesting_bnfs: BNF_Def.bnf list, 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

20 
ctrXs_Tss: typ list list, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

21 
ctr_defs: thm list, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

22 
ctr_sugar: Ctr_Sugar.ctr_sugar, 
55863  23 
co_rec: term, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

24 
maps: thm list, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

25 
common_co_inducts: thm list, 
52343  26 
co_inducts: thm list, 
55863  27 
co_rec_thms: thm list, 
28 
disc_co_recs: thm list, 

29 
sel_co_recss: thm list list}; 

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

30 

51896  31 
val morph_fp_sugar: morphism > fp_sugar > fp_sugar 
54256  32 
val transfer_fp_sugar: Proof.context > fp_sugar > fp_sugar 
51896  33 
val fp_sugar_of: Proof.context > string > fp_sugar option 
53907  34 
val fp_sugars_of: Proof.context > fp_sugar list 
51852  35 

53106  36 
val co_induct_of: 'a list > 'a 
37 
val strong_co_induct_of: 'a list > 'a 

38 

52868  39 
val flat_corec_preds_predsss_gettersss: 'a list > 'a list list list > 'a list list list > 
40 
'a list 

51907  41 
val nesty_bnfs: Proof.context > typ list list list > typ list > BNF_Def.bnf list 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

42 

bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

43 
type lfp_sugar_thms = 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

44 
(thm list * thm * Args.src list) * (thm list list * Args.src list) 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

45 

54256  46 
val morph_lfp_sugar_thms: morphism > lfp_sugar_thms > lfp_sugar_thms 
47 
val transfer_lfp_sugar_thms: Proof.context > lfp_sugar_thms > lfp_sugar_thms 

48 

53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

49 
type gfp_sugar_thms = 
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

50 
((thm list * thm) list * Args.src list) 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

51 
* (thm list list * Args.src list) 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

52 
* (thm list list * Args.src list) 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

53 
* (thm list list * Args.src list) 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

54 
* (thm list list list * Args.src list) 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

55 

54256  56 
val morph_gfp_sugar_thms: morphism > gfp_sugar_thms > gfp_sugar_thms 
57 
val transfer_gfp_sugar_thms: Proof.context > gfp_sugar_thms > gfp_sugar_thms 

58 

55867  59 
val mk_co_recs_prelims: BNF_Util.fp_kind > typ list list list > typ list > typ list > 
60 
typ list > typ list > int list > int list list > term list > Proof.context > 

61 
(term list 

62 
* (typ list list * typ list list list list * term list list * term list list list list) option 

55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

63 
* (string * term list * term list list 
55867  64 
* ((term list list * term list list list) * typ list)) option) 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

65 
* Proof.context 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

66 
val repair_nullary_single_ctr: typ list list > typ list list 
55867  67 
val mk_corec_p_pred_types: typ list > int list > typ list list 
68 
val mk_corec_fun_arg_types: typ list list list > typ list > typ list > typ list > int list > 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

69 
int list list > term > 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

70 
typ list list 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

71 
* (typ list list list list * typ list list list * typ list list list list * typ list) 
55867  72 
val define_rec: 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

73 
(typ list list * typ list list list list * term list list * term list list list list) option > 
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

74 
(string > binding) > typ list > typ list > term list > term > Proof.context > 
55864  75 
(term * thm) * Proof.context 
55867  76 
val define_corec: 'a * term list * term list list 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

77 
* ((term list list * term list list list) * typ list) > (string > binding) > 'b list > 
55864  78 
typ list > term list > term > Proof.context > (term * thm) * local_theory 
55867  79 
val derive_induct_recs_thms_for_types: BNF_Def.bnf list > 
80 
('a * typ list list list list * term list list * 'b) option > thm > thm list > 

55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

81 
BNF_Def.bnf list > BNF_Def.bnf list > typ list > typ list > typ list > 
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

82 
typ list list list > thm list > thm list > thm list > term list list > thm list list > 
55864  83 
term list > thm list > Proof.context > lfp_sugar_thms 
55867  84 
val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list > 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

85 
string * term list * term list list * ((term list list * term list list list) * typ list) > 
55867  86 
thm > thm list > thm list > thm list > BNF_Def.bnf list > typ list > typ list > 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

87 
typ list > typ list list list > int list list > int list list > int list > thm list > 
55864  88 
thm list > (thm > thm) > thm list list > Ctr_Sugar.ctr_sugar list > term list > 
89 
thm list > (thm list > thm list) > local_theory > gfp_sugar_thms 

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

90 

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

91 
type co_datatype_spec = 
55699
1f9cc432ecd4
reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'
blanchet
parents:
55575
diff
changeset

92 
((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix) 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

93 
* ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

94 

55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

95 
val co_datatypes: BNF_Util.fp_kind > (mixfix list > binding list > binding list > 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

96 
binding list list > binding list > (string * sort) list > typ list * typ list list > 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

97 
BNF_Def.bnf list > BNF_Comp.absT_info list > local_theory > 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

98 
BNF_FP_Util.fp_result * local_theory) > 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

99 
(bool * bool) * co_datatype_spec list > 
49297  100 
local_theory > local_theory 
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

101 
val parse_co_datatype_cmd: BNF_Util.fp_kind > (mixfix list > binding list > binding list > 
51867  102 
binding list list > binding list > (string * sort) list > typ list * typ list list > 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

103 
BNF_Def.bnf list > BNF_Comp.absT_info list > local_theory > 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

104 
BNF_FP_Util.fp_result * local_theory) > 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
49302
diff
changeset

105 
(local_theory > local_theory) parser 
49112  106 
end; 
107 

49636  108 
structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = 
49112  109 
struct 
110 

54006  111 
open Ctr_Sugar 
55571  112 
open BNF_FP_Rec_Sugar_Util 
49119  113 
open BNF_Util 
53222  114 
open BNF_Comp 
49214
2a3cb4c71b87
construct the right iterator theorem in the recursive case
blanchet
parents:
49213
diff
changeset

115 
open BNF_Def 
51850
106afdf5806c
renamed a few FPrelated files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents:
51847
diff
changeset

116 
open BNF_FP_Util 
49636  117 
open BNF_FP_Def_Sugar_Tactics 
49119  118 

51788  119 
val EqN = "Eq_"; 
51777
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51769
diff
changeset

120 

51840  121 
type fp_sugar = 
51859  122 
{T: typ, 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

123 
X: typ, 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

124 
fp: fp_kind, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

125 
fp_res_index: int, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

126 
fp_res: fp_result, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

127 
pre_bnf: bnf, 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

128 
absT_info: absT_info, 
52356  129 
nested_bnfs: bnf list, 
53267
aad7d276b849
store nesting_bnfs in fp_sugar (required in "nested to mutual" reduction)
traytel
parents:
53266
diff
changeset

130 
nesting_bnfs: bnf list, 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

131 
ctrXs_Tss: typ list list, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

132 
ctr_defs: thm list, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

133 
ctr_sugar: Ctr_Sugar.ctr_sugar, 
55863  134 
co_rec: term, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

135 
maps: thm list, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

136 
common_co_inducts: thm list, 
52343  137 
co_inducts: thm list, 
55863  138 
co_rec_thms: thm list, 
139 
disc_co_recs: thm list, 

140 
sel_co_recss: thm list list}; 

52295  141 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

142 
fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs, 
55863  143 
nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, maps, common_co_inducts, co_inducts, 
144 
co_rec_thms, disc_co_recs, sel_co_recss} : fp_sugar) = 

55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

145 
{T = Morphism.typ phi T, 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

146 
X = Morphism.typ phi X, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

147 
fp = fp, 
53267
aad7d276b849
store nesting_bnfs in fp_sugar (required in "nested to mutual" reduction)
traytel
parents:
53266
diff
changeset

148 
fp_res = morph_fp_result phi fp_res, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

149 
fp_res_index = fp_res_index, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

150 
pre_bnf = morph_bnf phi pre_bnf, 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

151 
absT_info = morph_absT_info phi absT_info, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

152 
nested_bnfs = map (morph_bnf phi) nested_bnfs, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

153 
nesting_bnfs = map (morph_bnf phi) nesting_bnfs, 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

154 
ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

155 
ctr_defs = map (Morphism.thm phi) ctr_defs, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

156 
ctr_sugar = morph_ctr_sugar phi ctr_sugar, 
55863  157 
co_rec = Morphism.term phi co_rec, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

158 
maps = map (Morphism.thm phi) maps, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

159 
common_co_inducts = map (Morphism.thm phi) common_co_inducts, 
52343  160 
co_inducts = map (Morphism.thm phi) co_inducts, 
55863  161 
co_rec_thms = map (Morphism.thm phi) co_rec_thms, 
162 
disc_co_recs = map (Morphism.thm phi) disc_co_recs, 

163 
sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss}; 

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

164 

53907  165 
val transfer_fp_sugar = 
54740  166 
morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; 
53907  167 

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

168 
structure Data = Generic_Data 
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

169 
( 
51840  170 
type T = fp_sugar Symtab.table; 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

171 
val empty = Symtab.empty; 
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

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

173 
fun merge data : T = Symtab.merge (K true) data; 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

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

175 

53126
f4d2c64c7aa8
transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids nontrivial merges)
traytel
parents:
53106
diff
changeset

176 
fun fp_sugar_of ctxt = 
f4d2c64c7aa8
transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids nontrivial merges)
traytel
parents:
53106
diff
changeset

177 
Symtab.lookup (Data.get (Context.Proof ctxt)) 
53907  178 
#> Option.map (transfer_fp_sugar ctxt); 
179 

180 
fun fp_sugars_of ctxt = 

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

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

182 

53106  183 
fun co_induct_of (i :: _) = i; 
184 
fun strong_co_induct_of [_, s] = s; 

185 

53259  186 
(* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *) 
187 

51840  188 
fun register_fp_sugar key fp_sugar = 
54285
578371ba74cc
reverted 3e1d230f1c00  pervasiveness is useful, cf. Coinductive_Nat in the AFP
blanchet
parents:
54265
diff
changeset

189 
Local_Theory.declaration {syntax = false, pervasive = true} 
55444
ec73f81e49e7
iteration n in the 'default' vs. 'update_new' vs. 'update' saga  'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents:
55414
diff
changeset

190 
(fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar))); 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

191 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

192 
fun register_fp_sugars Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) 
55863  193 
ctrXs_Tsss ctr_defss ctr_sugars co_recs mapss common_co_inducts co_inductss co_rec_thmss 
194 
disc_co_recss sel_co_recsss lthy = 

51844  195 
(0, lthy) 
51859  196 
> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

197 
register_fp_sugar s {T = T, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

198 
pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs, 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

199 
nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, 
55863  200 
ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, maps = nth mapss kk, 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

201 
common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, 
55863  202 
co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk, 
203 
sel_co_recss = nth sel_co_recsss kk} 

52337  204 
lthy)) Ts 
51824  205 
> snd; 
206 

55342  207 
(* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A", 
208 
"x.x_A", "y.A"). *) 

49622  209 
fun quasi_unambiguous_case_names names = 
210 
let 

211 
val ps = map (`Long_Name.base_name) names; 

212 
val dups = Library.duplicates (op =) (map fst ps); 

213 
fun underscore s = 

214 
let val ss = space_explode Long_Name.separator s in 

215 
space_implode "_" (drop (length ss  2) ss) 

216 
end; 

217 
in 

218 
map (fn (base, full) => if member (op =) dups base then underscore full else base) ps 

219 
end; 

220 

52355  221 
val id_def = @{thm id_def}; 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

222 
val mp_conj = @{thm mp_conj}; 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

223 

55397
c2506f61fd26
generate 'fundec_cong' attribute for newstyle (co)datatypes
blanchet
parents:
55394
diff
changeset

224 
val fundefcong_attrs = @{attributes [fundef_cong]}; 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54107
diff
changeset

225 
val nitpicksimp_attrs = @{attributes [nitpick_simp]}; 
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54107
diff
changeset

226 
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; 
49300  227 
val simp_attrs = @{attributes [simp]}; 
228 

49297  229 
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)); 
49202
f493cd25737f
some work towards iterator and recursor properties
blanchet
parents:
49201
diff
changeset

230 

52868  231 
fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss); 
51829  232 

52868  233 
fun flat_corec_preds_predsss_gettersss [] [qss] [fss] = flat_corec_predss_getterss qss fss 
234 
 flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) = 

235 
p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss; 

51829  236 

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

237 
fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) = 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

238 
Abs ("x", T1, Abs ("y", T2, Var (x, T2 > T1 > T3) $ Bound 0 $ Bound 1)); 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

239 

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

240 
fun flip_rels lthy n thm = 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

241 
let 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

242 
val Rs = Term.add_vars (prop_of thm) []; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

243 
val Rs' = rev (drop (length Rs  n) Rs); 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

244 
val cRs = map (fn f => (certify lthy (Var f), certify lthy (mk_flip f))) Rs'; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

245 
in 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

246 
Drule.cterm_instantiate cRs thm 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

247 
end; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

248 

49536  249 
fun mk_ctor_or_dtor get_T Ts t = 
250 
let val Type (_, Ts0) = get_T (fastype_of t) in 

251 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

252 
end; 

253 

254 
val mk_ctor = mk_ctor_or_dtor range_type; 

255 
val mk_dtor = mk_ctor_or_dtor domain_type; 

256 

55867  257 
fun mk_xtor_co_recs thy fp fpTs Cs ts0 = 
51911
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

258 
let 
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

259 
val nn = length fpTs; 
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

260 
val (fpTs0, Cs0) = 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

261 
map ((fp = Greatest_FP ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) ts0 
51911
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

262 
> split_list; 
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

263 
val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs); 
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

264 
in 
52170
564be617ae84
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet
parents:
52169
diff
changeset

265 
map (Term.subst_TVars rho) ts0 
51911
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

266 
end; 
51827  267 

55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

268 
fun unzip_recT (Type (@{type_name prod}, _)) T = [T] 
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

269 
 unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts 
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

270 
 unzip_recT _ T = [T]; 
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

271 

53591  272 
fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] 
53901  273 
 unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts 
52871  274 
 unzip_corecT _ T = [T]; 
275 

52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

276 
fun liveness_of_fp_bnf n bnf = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

277 
(case T_of_bnf bnf of 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

278 
Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

279 
 _ => replicate n false); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

280 

55700  281 
fun cannot_merge_types fp = 
282 
error ("Mutually " ^ co_prefix fp ^ "recursive types must have the same type parameters"); 

52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

283 

55700  284 
fun merge_type_arg fp T T' = if T = T' then T else cannot_merge_types fp; 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

285 

55700  286 
fun merge_type_args fp (As, As') = 
287 
if length As = length As' then map2 (merge_type_arg fp) As As' else cannot_merge_types fp; 

52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

288 

ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

289 
fun reassoc_conjs thm = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

290 
reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]}) 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

291 
handle THM _ => thm; 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

292 

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

293 
type co_datatype_spec = 
55699
1f9cc432ecd4
reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'
blanchet
parents:
55575
diff
changeset

294 
((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix) 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

295 
* ((binding, binding * typ, term) ctr_spec * mixfix) list; 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

296 

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

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

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

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

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

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

302 
fun mixfixed_ctr_specs_of_spec (_, mx_ctr_specs) = mx_ctr_specs; 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

303 

ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

304 
fun add_nesty_bnf_names Us = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

305 
let 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

306 
fun add (Type (s, Ts)) ss = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

307 
let val (needs, ss') = fold_map add Ts ss in 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

308 
if exists I needs then (true, insert (op =) s ss') else (false, ss') 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

309 
end 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

310 
 add T ss = (member (op =) Us T, ss); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

311 
in snd oo add end; 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

312 

ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

313 
fun nesty_bnfs ctxt ctr_Tsss Us = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

314 
map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

315 

54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

316 
fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p; 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

317 

53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

318 
type lfp_sugar_thms = 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

319 
(thm list * thm * Args.src list) * (thm list list * Args.src list); 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

320 

55867  321 
fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) = 
54256  322 
((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs), 
55867  323 
(map (map (Morphism.thm phi)) recss, rec_attrs)) 
55095  324 
: lfp_sugar_thms; 
54256  325 

326 
val transfer_lfp_sugar_thms = 

54740  327 
morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; 
54256  328 

53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

329 
type gfp_sugar_thms = 
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

330 
((thm list * thm) list * Args.src list) 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

331 
* (thm list list * Args.src list) 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

332 
* (thm list list * Args.src list) 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

333 
* (thm list list * Args.src list) 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

334 
* (thm list list list * Args.src list); 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

335 

54256  336 
fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs), 
55867  337 
(corecss, corec_attrs), (disc_corecss, disc_rec_attrs), 
338 
(disc_corec_iffss, disc_rec_iff_attrs), (sel_corecsss, sel_rec_attrs)) = 

54256  339 
((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, 
340 
coinduct_attrs), 

55867  341 
(map (map (Morphism.thm phi)) corecss, corec_attrs), 
342 
(map (map (Morphism.thm phi)) disc_corecss, disc_rec_attrs), 

343 
(map (map (Morphism.thm phi)) disc_corec_iffss, disc_rec_iff_attrs), 

344 
(map (map (map (Morphism.thm phi))) sel_corecsss, sel_rec_attrs)) : gfp_sugar_thms; 

54256  345 

346 
val transfer_gfp_sugar_thms = 

54740  347 
morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; 
54256  348 

55867  349 
fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy = 
51832  350 
let 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

351 
val Css = map2 replicate ns Cs; 
55869  352 
val x_Tssss = 
55867  353 
map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T => 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

354 
map2 (map2 unzip_recT) 
55867  355 
ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T))) 
356 
absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts; 

51832  357 

55869  358 
val x_Tsss' = map (map flat_rec_arg_args) x_Tssss; 
359 
val f_Tss = map2 (map2 (curry (op >))) x_Tsss' Css; 

51832  360 

55869  361 
val ((fss, xssss), lthy) = 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

362 
lthy 
55869  363 
> mk_Freess "f" f_Tss 
364 
>> mk_Freessss "x" x_Tssss; 

51832  365 
in 
55869  366 
((f_Tss, x_Tssss, fss, xssss), lthy) 
51832  367 
end; 
368 

55867  369 
(*avoid "'a itself" arguments in corecursors*) 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

370 
fun repair_nullary_single_ctr [[]] = [[@{typ unit}]] 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

371 
 repair_nullary_single_ctr Tss = Tss; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

372 

55867  373 
fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts = 
51829  374 
let 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

375 
val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss; 
55869  376 
val g_absTs = map range_type fun_Ts; 
377 
val g_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss g_absTs); 

378 
val g_Tssss = map3 (fn C => map2 (map2 (map (curry (op >) C) oo unzip_corecT))) 

379 
Cs ctr_Tsss' g_Tsss; 

380 
val q_Tssss = map (map (map (fn [_] => []  [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss; 

52870  381 
in 
55869  382 
(q_Tssss, g_Tsss, g_Tssss, g_absTs) 
52870  383 
end; 
51829  384 

55867  385 
fun mk_corec_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n  1)) o mk_pred1T) ns Cs; 
52898  386 

55867  387 
fun mk_corec_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_corec = 
388 
(mk_corec_p_pred_types Cs ns, 

389 
mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss 

390 
(binder_fun_types (fastype_of dtor_corec))); 

51829  391 

55867  392 
fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy = 
393 
let 

394 
val p_Tss = mk_corec_p_pred_types Cs ns; 

51829  395 

55869  396 
val (q_Tssss, g_Tsss, g_Tssss, corec_types) = 
55867  397 
mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts; 
51831  398 

55869  399 
val (((((Free (x, _), cs), pss), qssss), gssss), lthy) = 
51829  400 
lthy 
55869  401 
> yield_singleton (mk_Frees "x") dummyT 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

402 
>> mk_Frees "a" Cs 
51829  403 
>> mk_Freess "p" p_Tss 
55869  404 
>> mk_Freessss "q" q_Tssss 
405 
>> mk_Freessss "g" g_Tssss; 

51831  406 

407 
val cpss = map2 (map o rapp) cs pss; 

51829  408 

52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

409 
fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

410 

55867  411 
fun build_dtor_corec_arg _ [] [cf] = cf 
412 
 build_dtor_corec_arg T [cq] [cf, cf'] = 

52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

413 
mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf) 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

414 
(build_sum_inj Inr_const (fastype_of cf', T) $ cf'); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

415 

55869  416 
val pgss = map3 flat_corec_preds_predsss_gettersss pss qssss gssss; 
417 
val cqssss = map2 (map o map o map o rapp) cs qssss; 

418 
val cgssss = map2 (map o map o map o rapp) cs gssss; 

419 
val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss; 

51831  420 
in 
55869  421 
((x, cs, cpss, ((pgss, cqgsss), corec_types)), lthy) 
51831  422 
end; 
51829  423 

55867  424 
fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy = 
51903  425 
let 
52169  426 
val thy = Proof_Context.theory_of lthy; 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

427 
val nn = length fpTs; 
52169  428 

55867  429 
val (xtor_co_rec_fun_Ts, xtor_co_recs) = 
430 
mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 > `(binder_fun_types o fastype_of o hd); 

51903  431 

55867  432 
val ((recs_args_types, corecs_args_types), lthy') = 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

433 
if fp = Least_FP then 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

434 
if nn = 1 andalso forall (forall (forall (not o exists_subtype_in fpTs))) ctr_Tsss then 
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

435 
((NONE, NONE), lthy) 
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

436 
else 
55867  437 
mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

438 
>> (rpair NONE o SOME) 
51903  439 
else 
55867  440 
mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

441 
>> (pair NONE o SOME); 
51903  442 
in 
55867  443 
((xtor_co_recs, recs_args_types, corecs_args_types), lthy') 
51903  444 
end; 
445 

55869  446 
fun mk_preds_getterss_join c cps absT abs cqgss = 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

447 
let 
55869  448 
val n = length cqgss; 
449 
val ts = map2 (mk_absumprod absT abs n) (1 upto n) cqgss; 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

450 
in 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

451 
Term.lambda c (mk_IfN absT cps ts) 
51900  452 
end; 
51886  453 

55867  454 
fun define_co_rec fp fpT Cs b rhs lthy0 = 
51897  455 
let 
52170
564be617ae84
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet
parents:
52169
diff
changeset

456 
val thy = Proof_Context.theory_of lthy0; 
564be617ae84
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet
parents:
52169
diff
changeset

457 

53569
b4db0ade27bd
conceal definitions of highlevel constructors and (co)iterators
traytel
parents:
53553
diff
changeset

458 
val maybe_conceal_def_binding = Thm.def_binding 
b4db0ade27bd
conceal definitions of highlevel constructors and (co)iterators
traytel
parents:
53553
diff
changeset

459 
#> Config.get lthy0 bnf_note_all = false ? Binding.conceal; 
b4db0ade27bd
conceal definitions of highlevel constructors and (co)iterators
traytel
parents:
53553
diff
changeset

460 

55864  461 
val ((cst, (_, def)), (lthy', lthy)) = lthy0 
462 
> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) 

52327  463 
> `Local_Theory.restore; 
464 

465 
val phi = Proof_Context.export_morphism lthy lthy'; 

466 

55869  467 
val cst' = mk_co_rec thy fp fpT Cs (Morphism.term phi cst); 
55864  468 
val def' = Morphism.thm phi def; 
52327  469 
in 
55864  470 
((cst', def'), lthy') 
52327  471 
end; 
472 

55867  473 
fun define_rec NONE _ _ _ _ _ = pair (Term.dummy, refl) 
474 
 define_rec (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_rec = 

55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

475 
let 
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

476 
val nn = length fpTs; 
55867  477 
val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec) 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

478 
>> map domain_type > domain_type; 
55864  479 
in 
55867  480 
define_co_rec Least_FP fpT Cs (mk_binding recN) 
481 
(fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec, 

482 
map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss => 

483 
mk_case_absumprod ctor_rec_absT rep fs 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

484 
(map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss)) 
55867  485 
ctor_rec_absTs reps fss xssss))) 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

486 
end; 
51897  487 

55869  488 
fun define_corec (_, cs, cpss, ((pgss, cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec = 
51897  489 
let 
51899  490 
val nn = length fpTs; 
55867  491 
val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec))); 
51897  492 
in 
55867  493 
define_co_rec Greatest_FP fpT Cs (mk_binding corecN) 
55869  494 
(fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec, 
495 
map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss))) 

52320  496 
end; 
51897  497 

55867  498 
fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

499 
nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses 
55864  500 
ctrss ctr_defss recs rec_defs lthy = 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

501 
let 
51827  502 
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; 
503 

51815  504 
val nn = length pre_bnfs; 
51827  505 
val ns = map length ctr_Tsss; 
506 
val mss = map (map length) ctr_Tsss; 

51815  507 

51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

508 
val pre_map_defs = map map_def_of_bnf pre_bnfs; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

509 
val pre_set_defss = map set_defs_of_bnf pre_bnfs; 
53329  510 
val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; 
511 
val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs; 

53290  512 
val nested_set_maps = maps set_map_of_bnf nested_bnfs; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

513 

51816  514 
val fp_b_names = map base_name_of_typ fpTs; 
51811  515 

51832  516 
val ((((ps, ps'), xsss), us'), names_lthy) = 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

517 
lthy 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

518 
> mk_Frees' "P" (map mk_pred1T fpTs) 
51827  519 
>> mk_Freesss "x" ctr_Tsss 
51816  520 
>> Variable.variant_fixes fp_b_names; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

521 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

522 
val us = map2 (curry Free) us' fpTs; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

523 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

524 
fun mk_sets_nested bnf = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

525 
let 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

526 
val Type (T_name, Us) = T_of_bnf bnf; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

527 
val lives = lives_of_bnf bnf; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

528 
val sets = sets_of_bnf bnf; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

529 
fun mk_set U = 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

530 
(case find_index (curry (op =) U) lives of 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

531 
~1 => Term.dummy 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

532 
 i => nth sets i); 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

533 
in 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

534 
(T_name, map mk_set Us) 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

535 
end; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

536 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

537 
val setss_nested = map mk_sets_nested nested_bnfs; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

538 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

539 
val (induct_thms, induct_thm) = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

540 
let 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

541 
fun mk_set Ts t = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

542 
let val Type (_, Ts0) = domain_type (fastype_of t) in 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

543 
Term.subst_atomic_types (Ts0 ~~ Ts) t 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

544 
end; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

545 

52310
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

546 
fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) = 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

547 
[([], (find_index (curry (op =) X) Xs + 1, x))] 
52310
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

548 
 mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) = 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

549 
(case AList.lookup (op =) setss_nested T_name of 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

550 
NONE => [] 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

551 
 SOME raw_sets0 => 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

552 
let 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

553 
val (Xs_Ts, (Ts, raw_sets)) = 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

554 
filter (exists_subtype_in Xs o fst) (Xs_Ts0 ~~ (Ts0 ~~ raw_sets0)) 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

555 
> split_list > split_list; 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

556 
val sets = map (mk_set Ts0) raw_sets; 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

557 
val (ys, names_lthy') = names_lthy > mk_Frees s Ts; 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

558 
val xysets = map (pair x) (ys ~~ sets); 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

559 
val ppremss = map2 (mk_raw_prem_prems names_lthy') ys Xs_Ts; 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

560 
in 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

561 
flat (map2 (map o apfst o cons) xysets ppremss) 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

562 
end) 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

563 
 mk_raw_prem_prems _ _ _ = []; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

564 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

565 
fun close_prem_prem xs t = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

566 
fold_rev Logic.all (map Free (drop (nn + length xs) 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

567 
(rev (Term.add_frees t (map dest_Free xs @ ps'))))) t; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

568 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

569 
fun mk_prem_prem xs (xysets, (j, x)) = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

570 
close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) => 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

571 
HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets, 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

572 
HOLogic.mk_Trueprop (nth ps (j  1) $ x))); 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

573 

52310
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

574 
fun mk_raw_prem phi ctr ctr_Ts ctrXs_Ts = 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

575 
let 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

576 
val (xs, names_lthy') = names_lthy > mk_Frees "x" ctr_Ts; 
52310
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

577 
val pprems = flat (map2 (mk_raw_prem_prems names_lthy') xs ctrXs_Ts); 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

578 
in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

579 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

580 
fun mk_prem (xs, raw_pprems, concl) = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

581 
fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl)); 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

582 

52310
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

583 
val raw_premss = map4 (map3 o mk_raw_prem) ps ctrss ctr_Tsss ctrXs_Tsss; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

584 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

585 
val goal = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

586 
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

587 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us))); 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

588 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

589 
val kksss = map (map (map (fst o snd) o #2)) raw_premss; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

590 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

591 
val ctor_induct' = ctor_induct OF (map2 mk_absumprodE fp_type_definitions mss); 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

592 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

593 
val thm = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

594 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

595 
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

596 
abs_inverses nested_set_maps pre_set_defss) 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

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

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

599 
> Thm.name_derivation (fst (dest_Type (hd fpTs)) ^ Long_Name.separator ^ 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55397
diff
changeset

600 
(if nn > 1 then space_implode "_" (tl fp_b_names) ^ Long_Name.separator else "") ^ 
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55397
diff
changeset

601 
inductN); 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

602 
in 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

603 
`(conj_dests nn) thm 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

604 
end; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

605 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

606 
val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); 
52305  607 
val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases)); 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

608 

52305  609 
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; 
610 

55867  611 
fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms = 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

612 
let 
55867  613 
val frecs = map (lists_bmoc fss) recs; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

614 

55867  615 
fun mk_goal fss frec xctr f xs fxs = 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

616 
fold_rev (fold_rev Logic.all) (xs :: fss) 
55867  617 
(mk_Trueprop_eq (frec $ xctr, Term.list_comb (f, fxs))); 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

618 

52302  619 
fun maybe_tick (T, U) u f = 
620 
if try (fst o HOLogic.dest_prodT) U = SOME T then 

621 
Term.lambda u (HOLogic.mk_prod (u, f $ u)) 

622 
else 

623 
f; 

51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

624 

55867  625 
fun build_rec (x as Free (_, T)) U = 
52368  626 
if T = U then 
627 
x 

628 
else 

52303
16d7708aba40
one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")
blanchet
parents:
52302
diff
changeset

629 
build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs 
55867  630 
(fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x; 
52301
7935e82a4ae4
simpler, more robust iterator goal construction code
blanchet
parents:
52300
diff
changeset

631 

55867  632 
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; 
633 
val goalss = map5 (map4 o mk_goal fss) frecs xctrss fss xsss fxsss; 

51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

634 

52305  635 
val tacss = 
55867  636 
map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs) 
637 
ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss; 

51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

638 

355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

639 
fun prove goal tac = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

640 
Goal.prove_sorry lthy [] [] goal (tac o #context) 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

641 
> Thm.close_derivation; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

642 
in 
52305  643 
map2 (map2 prove) goalss tacss 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

644 
end; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

645 

55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

646 
val rec_thmss = 
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

647 
(case rec_args_typess of 
55867  648 
SOME types => mk_rec_thmss types recs rec_defs ctor_rec_thms 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

649 
 NONE => replicate nn []); 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

650 
in 
52345  651 
((induct_thms, induct_thm, [induct_case_names_attr]), 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

652 
(rec_thmss, code_nitpicksimp_attrs @ simp_attrs)) 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

653 
end; 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

654 

55869  655 
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, 
656 
corecs_args_types as ((pgss, cqgsss), _)) 

55867  657 
dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

658 
mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) 
55864  659 
corecs corec_defs export_args lthy = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

660 
let 
55867  661 
fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = 
662 
iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; 

53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

663 

55867  664 
val ctor_dtor_corec_thms = map3 mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms; 
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

665 

51815  666 
val nn = length pre_bnfs; 
667 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

668 
val pre_map_defs = map map_def_of_bnf pre_bnfs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

669 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
53329  670 
val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; 
51830  671 
val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

672 

51816  673 
val fp_b_names = map base_name_of_typ fpTs; 
51811  674 

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

675 
val ctrss = map #ctrs ctr_sugars; 
7219c61796c0
simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
blanchet
parents:
53203
diff
changeset

676 
val discss = map #discs ctr_sugars; 
7219c61796c0
simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
blanchet
parents:
53203
diff
changeset

677 
val selsss = map #selss ctr_sugars; 
51840  678 
val exhausts = map #exhaust ctr_sugars; 
679 
val disc_thmsss = map #disc_thmss ctr_sugars; 

680 
val discIss = map #discIs ctr_sugars; 

681 
val sel_thmsss = map #sel_thmss ctr_sugars; 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

682 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

683 
val (((rs, us'), vs'), names_lthy) = 
52341  684 
lthy 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

685 
> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) 
51816  686 
>> Variable.variant_fixes fp_b_names 
687 
>> Variable.variant_fixes (map (suffix "'") fp_b_names); 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

688 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

689 
val us = map2 (curry Free) us' fpTs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

690 
val udiscss = map2 (map o rapp) us discss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

691 
val uselsss = map2 (map o map o rapp) us selsss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

692 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

693 
val vs = map2 (curry Free) vs' fpTs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

694 
val vdiscss = map2 (map o rapp) vs discss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

695 
val vselsss = map2 (map o map o rapp) vs selsss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

696 

52345  697 
val coinduct_thms_pairs = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

698 
let 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

699 
val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

700 
val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

701 
val strong_rs = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

702 
map4 (fn u => fn v => fn uvr => fn uv_eq => 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

703 
fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

704 

54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

705 
fun build_the_rel rs' T Xs_T = 
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

706 
build_rel lthy (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) 
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

707 
> Term.subst_atomic_types (Xs ~~ fpTs); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

708 

54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

709 
fun build_rel_app rs' usel vsel Xs_T = 
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

710 
fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

711 

54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

712 
fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

713 
(if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

714 
(if null usels then 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

715 
[] 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

716 
else 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

717 
[Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

718 
Library.foldr1 HOLogic.mk_conj (map3 (build_rel_app rs') usels vsels ctrXs_Ts))]); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

719 

54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

720 
fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = 
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

721 
Library.foldr1 HOLogic.mk_conj (flat (map6 (mk_prem_ctr_concls rs' n) 
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

722 
(1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss)) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

723 
handle List.Empty => @{term True}; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

724 

54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

725 
fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

726 
fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

727 
HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

728 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

729 
val concl = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

730 
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

731 
(map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

732 
uvrs us vs)); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

733 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

734 
fun mk_goal rs' = 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

735 
Logic.list_implies (map9 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss 
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

736 
ctrXs_Tsss, concl); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

737 

52345  738 
val goals = map mk_goal [rs, strong_rs]; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

739 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

740 
fun prove dtor_coinduct' goal = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

741 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

742 
mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

743 
abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

744 
> singleton (Proof_Context.export names_lthy lthy) 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

745 
> Thm.close_derivation; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

746 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

747 
fun postproc nn thm = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

748 
Thm.permute_prems 0 nn 
51828  749 
(if nn = 1 then thm RS mp else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

750 
> Drule.zero_var_indexes 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

751 
> `(conj_dests nn); 
53106  752 

753 
val rel_eqs = map rel_eq_of_bnf pre_bnfs; 

754 
val rel_monos = map rel_mono_of_bnf pre_bnfs; 

755 
val dtor_coinducts = 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

756 
[dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy] 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

757 
in 
52345  758 
map2 (postproc nn oo prove) dtor_coinducts goals 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

759 
end; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

760 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

761 
fun mk_coinduct_concls ms discs ctrs = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

762 
let 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

763 
fun mk_disc_concl disc = [name_of_disc disc]; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

764 
fun mk_ctr_concl 0 _ = [] 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

765 
 mk_ctr_concl _ ctor = [name_of_ctr ctor]; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

766 
val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]]; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

767 
val ctr_concls = map2 mk_ctr_concl ms ctrs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

768 
in 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

769 
flat (map2 append disc_concls ctr_concls) 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

770 
end; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

771 

51816  772 
val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

773 
val coinduct_conclss = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

774 
map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

775 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

776 
fun mk_maybe_not pos = not pos ? HOLogic.mk_not; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

777 

55869  778 
val gcorecs = map (lists_bmoc pgss) corecs; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

779 

55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

780 
val corec_thmss = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

781 
let 
55869  782 
fun mk_goal c cps gcorec n k ctr m cfs' = 
783 
fold_rev (fold_rev Logic.all) ([c] :: pgss) 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

784 
(Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, 
55869  785 
mk_Trueprop_eq (gcorec $ c, Term.list_comb (ctr, take m cfs')))); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

786 

55869  787 
val mk_U = typ_subst_nonatomic (map2 (fn C => fn fpT => (mk_sumT (fpT, C), fpT)) Cs fpTs); 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

788 

55869  789 
fun tack (c, u) f = 
790 
let val x' = Free (x, mk_sumT (fastype_of u, fastype_of c)) in 

791 
Term.lambda x' (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ x') 

52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

792 
end; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

793 

55869  794 
fun build_corec cqg = 
795 
let val T = fastype_of cqg in 

52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

796 
if exists_subtype_in Cs T then 
55869  797 
let val U = mk_U T in 
798 
build_map lthy (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ => 

799 
tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg 

52368  800 
end 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

801 
else 
55869  802 
cqg 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

803 
end; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

804 

55869  805 
val cqgsss' = map (map (map build_corec)) cqgsss; 
806 
val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss'; 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

807 

55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

808 
val tacss = 
55867  809 
map4 (map ooo mk_corec_tac corec_defs nesting_map_idents) 
810 
ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss; 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

811 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

812 
fun prove goal tac = 
51815  813 
Goal.prove_sorry lthy [] [] goal (tac o #context) 
814 
> Thm.close_derivation; 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

815 
in 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

816 
map2 (map2 prove) goalss tacss 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

817 
> map (map (unfold_thms lthy @{thms case_sum_if})) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

818 
end; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

819 

55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

820 
val disc_corec_iff_thmss = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

821 
let 
55869  822 
fun mk_goal c cps gcorec n k disc = 
823 
mk_Trueprop_eq (disc $ (gcorec $ c), 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

824 
if n = 1 then @{const True} 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

825 
else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps)); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

826 

55869  827 
val goalss = map6 (map2 oooo mk_goal) cs cpss gcorecs ns kss discss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

828 

51828  829 
fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split}; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

830 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

831 
val case_splitss' = map (map mk_case_split') cpss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

832 

55867  833 
val tacss = map3 (map oo mk_disc_corec_iff_tac) case_splitss' corec_thmss disc_thmsss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

834 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

835 
fun prove goal tac = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

836 
Goal.prove_sorry lthy [] [] goal (tac o #context) 
52357
a5d3730043c2
use right context when exporting variables (cf. AFP Coinductive_List failures)
blanchet
parents:
52356
diff
changeset

837 
> singleton export_args 
51829  838 
> singleton (Proof_Context.export names_lthy lthy) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

839 
> Thm.close_derivation; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

840 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

841 
fun proves [_] [_] = [] 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

842 
 proves goals tacs = map2 prove goals tacs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

843 
in 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

844 
map2 proves goalss tacss 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

845 
end; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

846 

55867  847 
fun mk_disc_corec_thms corecs discIs = map (op RS) (corecs ~~ discIs); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

848 

55867  849 
val disc_corec_thmss = map2 mk_disc_corec_thms corec_thmss discIss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

850 

55867  851 
fun mk_sel_corec_thm corec_thm sel sel_thm = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

852 
let 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

853 
val (domT, ranT) = dest_funT (fastype_of sel); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

854 
val arg_cong' = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

855 
Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT]) 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

856 
[NONE, NONE, SOME (certify lthy sel)] arg_cong 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

857 
> Thm.varifyT_global; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

858 
val sel_thm' = sel_thm RSN (2, trans); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

859 
in 
55867  860 
corec_thm RS arg_cong' RS sel_thm' 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

861 
end; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

862 

55867  863 
fun mk_sel_corec_thms corec_thmss = 
864 
map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss; 

51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

865 

55867  866 
val sel_corec_thmsss = mk_sel_corec_thms corec_thmss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

867 

7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

868 
val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn)); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

869 
val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases)); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

870 
val coinduct_case_concl_attrs = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

871 
map2 (fn casex => fn concls => 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

872 
Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls)))) 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

873 
coinduct_cases coinduct_conclss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

874 
val coinduct_case_attrs = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

875 
coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

876 
in 
52345  877 
((coinduct_thms_pairs, coinduct_case_attrs), 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

878 
(corec_thmss, code_nitpicksimp_attrs), 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

879 
(disc_corec_thmss, []), 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

880 
(disc_corec_iff_thmss, simp_attrs), 
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

881 
(sel_corec_thmsss, simp_attrs)) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

882 
end; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

883 

52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

884 
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp 
55410  885 
(wrap_opts as (no_discs_sels, _), specs) no_defs_lthy0 = 
49112  886 
let 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

887 
(* TODO: sanity checks on arguments *) 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

888 

52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52968
diff
changeset

889 
val _ = if fp = Greatest_FP andalso no_discs_sels then 
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52968
diff
changeset

890 
error "Cannot define codatatypes without discriminators and selectors" 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

891 
else 
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

892 
(); 
49278  893 

49367  894 
val nn = length specs; 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

895 
val fp_bs = map type_binding_of_spec specs; 
49498  896 
val fp_b_names = map Binding.name_of fp_bs; 
897 
val fp_common_name = mk_common_name fp_b_names; 

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

898 
val map_bs = map map_binding_of_spec specs; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

899 
val rel_bs = map rel_binding_of_spec specs; 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

900 

51758  901 
fun prepare_type_arg (_, (ty, c)) = 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

902 
let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

903 
TFree (s, prepare_constraint no_defs_lthy0 c) 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

904 
end; 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

905 

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

906 
val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs; 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

907 
val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0; 
55700  908 
val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0; 
53266
89f7f1cc9ae3
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
blanchet
parents:
53264
diff
changeset

909 
val num_As = length unsorted_As; 
55699
1f9cc432ecd4
reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'
blanchet
parents:
55575
diff
changeset

910 

1f9cc432ecd4
reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'
blanchet
parents:
55575
diff
changeset

911 
val set_boss = map (map fst o type_args_named_constrained_of_spec) specs; 
1f9cc432ecd4
reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'
blanchet
parents:
55575
diff
changeset

912 
val set_bss = map (map (the_default Binding.empty)) set_boss; 
49119  913 

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

914 
val (((Bs0, Cs), Xs), no_defs_lthy) = 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

915 
no_defs_lthy0 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

916 
> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As 
53266
89f7f1cc9ae3
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
blanchet
parents:
53264
diff
changeset

917 
> mk_TFrees num_As 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

918 
>> mk_TFrees nn 
51858
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51857
diff
changeset

919 
>> variant_tfrees fp_b_names; 
49119  920 

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

921 
fun add_fake_type spec = 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

922 
Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec); 
51768  923 

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

924 
val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0; 
49119  925 

53262
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

926 
val qsoty = quote o Syntax.string_of_typ fake_lthy; 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

927 

54253  928 
val _ = (case Library.duplicates (op =) unsorted_As of [] => () 
53262
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

929 
 A :: _ => error ("Duplicate type parameter " ^ qsoty A ^ " in " ^ co_prefix fp ^ 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

930 
"datatype specification")); 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

931 

23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

932 
val bad_args = 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

933 
map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

934 
> filter_out Term.is_TVar; 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

935 
val _ = null bad_args orelse 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

936 
error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^ 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

937 
"datatype specification"); 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

938 

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

939 
val mixfixes = map mixfix_of_spec specs; 
49119  940 

54253  941 
val _ = (case Library.duplicates Binding.eq_name fp_bs of [] => () 
49119  942 
 b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b))); 
943 

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

944 
val mx_ctr_specss = map mixfixed_ctr_specs_of_spec specs; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

945 
val ctr_specss = map (map fst) mx_ctr_specss; 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

946 
val ctr_mixfixess = map (map snd) mx_ctr_specss; 
49119  947 

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

948 
val disc_bindingss = map (map disc_of_ctr_spec) ctr_specss; 
49336  949 
val ctr_bindingss = 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

950 
map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of_ctr_spec)) fp_b_names 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

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

952 
val ctr_argsss = map (map args_of_ctr_spec) ctr_specss; 
49119  953 

49336  954 
val sel_bindingsss = map (map (map fst)) ctr_argsss; 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

955 
val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

956 
val raw_sel_defaultsss = map (map sel_defaults_of_ctr_spec) ctr_specss; 
49286  957 

49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
49302
diff
changeset

958 
val (As :: _) :: fake_ctr_Tsss = 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

959 
burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0); 
53262
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

960 
val As' = map dest_TFree As; 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

961 

49183
0cc46e2dee7e
careful about constructor types w.r.t. fake context (third step of localization)
blanchet
parents:
49182
diff
changeset

962 
val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss []; 
53262
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

963 
val _ = (case subtract (op =) As' rhs_As' of [] => () 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

964 
 extras => error ("Extra type variables on righthand side: " ^ 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

965 
commas (map (qsoty o TFree) extras))); 
49165  966 

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

967 
val fake_Ts = map (fn s => Type (s, As)) fake_T_names; 
de1dc709f9d4
handle type class annotations on (co)datatype parameters gracefully
blanchet
parents:
53266
diff
changeset

968 

53262
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

969 
fun eq_fpT_check (T as Type (s, Ts)) (T' as Type (s', Ts')) = 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

970 
s = s' andalso (Ts = Ts' orelse 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

971 
error ("Wrong type arguments in " ^ co_prefix fp ^ "recursive type " ^ qsoty T ^ 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

972 
" (expected " ^ qsoty T' ^ ")")) 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

973 
 eq_fpT_check _ _ = false; 
49146  974 

53222  975 
fun freeze_fp (T as Type (s, Ts)) = 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

976 
(case find_index (eq_fpT_check T) fake_Ts of 
53222  977 
~1 => Type (s, map freeze_fp Ts) 
49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

978 
 kk => nth Xs kk) 
49204  979 
 freeze_fp T = T; 
49121  980 

53222  981 
val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts); 
982 

52310
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

983 
val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss; 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

984 
val ctrXs_repTs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; 
49119  985 

49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

986 
val fp_eqs = 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

987 
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs; 
49121  988 

53262
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

989 
val rhsXs_As' = fold (fold (fold Term.add_tfreesT)) ctrXs_Tsss []; 
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

990 
val _ = (case subtract (op =) rhsXs_As' As' of [] => () 
53266
89f7f1cc9ae3
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
blanchet
parents:
53264
diff
changeset

991 
 extras => List.app (fn extra => warning ("Unused type variable on righthand side of " ^ 
89f7f1cc9ae3
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
blanchet
parents:
53264
diff
changeset

992 
co_prefix fp ^ "datatype definition: " ^ qsoty (TFree extra))) extras); 
53262
23927b18dce2
rationalize message generation + added a warning
blanchet
parents:
53260
diff
changeset

993 

55701  994 
val killed_As = 
995 
map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE) 

996 
(unsorted_As ~~ transpose set_boss); 

997 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

998 
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, 
55868  999 
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors, 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1000 
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, 
55868  1001 
xtor_co_rec_thms, ...}, 
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

1002 
lthy)) = 
55701  1003 
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) 
1004 
(map dest_TFree killed_As) fp_eqs no_defs_lthy0 

53222  1005 
handle BAD_DEAD (X, X_backdrop) => 
1006 
(case X_backdrop of 

1007 
Type (bad_tc, _) => 

1008 
let 

1009 
val fake_T = qsoty (unfreeze_fp X); 

1010 
val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop); 

1011 
fun register_hint () = 

1012 
"\nUse the " ^ quote (fst (fst @{command_spec "bnf"})) ^ " command to register " ^ 

1013 
quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \ 

1014 
\it"; 

1015 
in 

1016 
if is_some (bnf_of no_defs_lthy bad_tc) orelse 

1017 
is_some (fp_sugar_of no_defs_lthy bad_tc) then 

53256  1018 
error ("Inadmissible " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ 
1019 
" in type expression " ^ fake_T_backdrop) 

53222  1020 
else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy) 
1021 
bad_tc) then 

1022 
error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ 

1023 
" via the oldstyle datatype " ^ quote bad_tc ^ " in type expression " ^ 

1024 
fake_T_backdrop ^ register_hint ()) 

1025 
else 

1026 
error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ 

1027 
" via type constructor " ^ quote bad_tc ^ " in type expression " ^ fake_T_backdrop ^ 

1028 
register_hint ()) 

1029 
end); 

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

1030 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1031 
val abss = map #abs absT_infos; 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1032 
val reps = map #rep absT_infos; 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1033 
val absTs = map #absT absT_infos; 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1034 
val repTs = map #repT absT_infos; 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1035 
val abs_injects = map #abs_inject absT_infos; 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1036 
val abs_inverses = map #abs_inverse absT_infos; 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1037 
val type_definitions = map #type_definition absT_infos; 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1038 

53143
ba80154a1118
configuration option to control timing output for (co)datatypes
traytel
parents:
53126
diff
changeset

1039 
val time = time lthy; 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1040 
val timer = time (Timer.startRealTimer ()); 
49121  1041 

52310
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

1042 
val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As; 
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

1043 
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; 
49226  1044 

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

1045 
val pre_map_defs = map map_def_of_bnf pre_bnfs; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1046 
val pre_set_defss = map set_defs_of_bnf pre_bnfs; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1047 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
53290  1048 
val nesting_set_maps = maps set_map_of_bnf nesting_bnfs; 
1049 
val nested_set_maps = maps set_map_of_bnf nested_bnfs; 

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

1050 

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

1051 
val live = live_of_bnf any_fp_bnf; 
52961  1052 
val _ = 
1053 
if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs) then 

53266
89f7f1cc9ae3
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
blanchet
parents:
53264
diff
changeset

1054 
warning "Map function and relator names ignored" 
52961  1055 
else 
1056 
(); 

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

1057 

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

1058 
val Bs = 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1059 
map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A) 
53266
89f7f1cc9ae3
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
blanchet
parents:
53264
diff
changeset

1060 
(liveness_of_fp_bnf num_As any_fp_bnf) As Bs0; 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1061 

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

1062 
val B_ify = Term.typ_subst_atomic (As ~~ Bs); 
49167  1063 

49501  1064 
val ctors = map (mk_ctor As) ctors0; 
1065 
val dtors = map (mk_dtor As) dtors0; 

49124  1066 

49501  1067 
val fpTs = map (domain_type o fastype_of) dtors; 
49362
1271aca16aed
make tactic more robust in the case where "asm_simp_tac" already finishes the job
blanchet
parents:
49361
diff
changeset

1068 

51780  1069 
fun massage_simple_notes base = 
1070 
filter_out (null o #2) 

1071 
#> map (fn (thmN, thms, attrs) => 

55410  1072 
((Binding.qualify true base (Binding.name thmN), attrs), [(thms, [])])); 
51780  1073 

1074 
val massage_multi_notes = 

1075 
maps (fn (thmN, thmss, attrs) => 

53792  1076 
map3 (fn fp_b_name => fn Type (T_name, _) => fn thms => 
55410  1077 
((Binding.qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])])) 
53792  1078 
fp_b_names fpTs thmss) 
1079 
#> filter_out (null o fst o hd o snd); 

51780  1080 

52310
28063e412793
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
blanchet
parents:
52309
diff
changeset

1081 
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; 
49203  1082 
val ns = map length ctr_Tsss; 
49212  1083 
val kss = map (fn n => 1 upto n) ns; 
49203  1084 
val mss = map (map length) ctr_Tsss; 
1085 

55867  1086 
val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') = 
55868  1087 
mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; 
49210  1088 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1089 
fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor), 
55867  1090 
xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1091 
pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs), 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1092 
abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss), 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1093 
disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = 
49176  1094 
let 
49498  1095 
val fp_b_name = Binding.name_of fp_b; 
1096 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1097 
val ctr_absT = domain_type (fastype_of ctor); 
49119  1098 

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

1099 
val ((((w, xss), yss), u'), names_lthy) = 
49204  1100 
no_defs_lthy 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1101 
> yield_singleton (mk_Frees "w") ctr_absT 
49370  1102 
>> mk_Freess "x" ctr_Tss 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1103 
>> mk_Freess "y" (map (map B_ify) ctr_Tss) 
49498  1104 
>> yield_singleton Variable.variant_fixes fp_b_name; 
49370  1105 

49498  1106 
val u = Free (u', fpT); 
49121  1107 

49129  1108 
val ctr_rhss = 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1109 
map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs)) 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1110 
ks xss; 
49121  1111 

53569
b4db0ade27bd
conceal definitions of highlevel constructors and (co)iterators
traytel
parents:
53553
diff
changeset

1112 
val maybe_conceal_def_binding = Thm.def_binding 
b4db0ade27bd
conceal definitions of highlevel constructors and (co)iterators
traytel
parents:
53553
diff
changeset

1113 
#> Config.get no_defs_lthy bnf_note_all = false ? Binding.conceal; 
b4db0ade27bd
conceal definitions of highlevel constructors and (co)iterators
traytel
parents:
53553
diff
changeset

1114 

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

1115 
val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy 
49169  1116 
> apfst split_list o fold_map3 (fn b => fn mx => fn rhs => 
53569
b4db0ade27bd
conceal definitions of highlevel constructors and (co)iterators
traytel
parents:
53553
diff
changeset

1117 
Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd) 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52964
diff
changeset

1118 
ctr_bindings ctr_mixfixes ctr_rhss 
49121  1119 
> `Local_Theory.restore; 
1120 

1121 
val phi = Proof_Context.export_morphism lthy lthy'; 

1122 

1123 
val ctr_defs = map (Morphism.thm phi) raw_ctr_defs; 

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

1124 
val ctr_defs' = 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1125 
map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs; 
49130
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

1126 

49203  1127 
val ctrs0 = map (Morphism.term phi) raw_ctrs; 
1128 
val ctrs = map (mk_ctr As) ctrs0; 

49121  1129 

51897  1130 
fun wrap_ctrs lthy = 
49123
263b0e330d8b
more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
49121
diff
changeset

1131 
let 
50170  1132 
fun exhaust_tac {context = ctxt, prems = _} = 
49135  1133 
let 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1134 
val ctor_iff_dtor_thm = 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1135 
let 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1136 
val goal = 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1137 
fold_rev Logic.all [w, u] 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1138 
(mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w))); 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1139 
in 
51551  1140 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1141 
mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [ctr_absT, fpT]) 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1142 
(certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor) 
55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55397
diff
changeset

1143 
> Morphism.thm phi 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1144 
> Thm.close_derivation 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1145 
end; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1146 

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

1147 
val sumEN_thm' = 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1148 
unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms) 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1149 
> Morphism.thm phi; 
49135  1150 
in 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1151 
mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm' 
49135  1152 
end; 
1153 

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

1154 
val inject_tacss = 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1155 
map2 (fn ctr_def => fn 0 => []  _ => [fn {context = ctxt, ...} => 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1156 
mk_inject_tac ctxt ctr_def ctor_inject abs_inject]) ctr_defs ms; 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1157 

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

1158 
val half_distinct_tacss = 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1159 
map (map (fn (def, def') => fn {context = ctxt, ...} => 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1160 
mk_half_distinct_tac ctxt ctor_inject abs_inject [def, def'])) 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1161 
(mk_half_pairss (`I ctr_defs)); 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1162 

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

1163 
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss; 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1164 

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

1165 
val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
