author  blanchet 
Sun, 23 Feb 2014 22:51:11 +0100  
changeset 55700  cf6a029b28d8 
parent 55699  1f9cc432ecd4 
child 55701  38f75365fc2a 
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, 
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

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

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

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

15 
pre_bnf: BNF_Def.bnf, 
52356  16 
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

17 
nesting_bnfs: BNF_Def.bnf list, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

19 
ctr_sugar: Ctr_Sugar.ctr_sugar, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

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

22 
common_co_inducts: thm list, 
52343  23 
co_inducts: thm list, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

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

26 
sel_co_itersss: thm list list list}; 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

27 

51896  28 
val morph_fp_sugar: morphism > fp_sugar > fp_sugar 
54256  29 
val transfer_fp_sugar: Proof.context > fp_sugar > fp_sugar 
51896  30 
val fp_sugar_of: Proof.context > string > fp_sugar option 
53907  31 
val fp_sugars_of: Proof.context > fp_sugar list 
51852  32 

53106  33 
val co_induct_of: 'a list > 'a 
34 
val strong_co_induct_of: 'a list > 'a 

35 

52868  36 
val flat_corec_preds_predsss_gettersss: 'a list > 'a list list list > 'a list list list > 
37 
'a list 

51907  38 
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

39 

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

40 
type lfp_sugar_thms = 
55571  41 
(thm list * thm * Args.src list) * (thm list 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

42 

54256  43 
val morph_lfp_sugar_thms: morphism > lfp_sugar_thms > lfp_sugar_thms 
44 
val transfer_lfp_sugar_thms: Proof.context > lfp_sugar_thms > lfp_sugar_thms 

45 

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

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

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

48 
* (thm list list * thm list list * Args.src list) 
54030
732b53d9b720
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
blanchet
parents:
54006
diff
changeset

49 
* (thm list 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

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

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

52 

54256  53 
val morph_gfp_sugar_thms: morphism > gfp_sugar_thms > gfp_sugar_thms 
54 
val transfer_gfp_sugar_thms: Proof.context > gfp_sugar_thms > gfp_sugar_thms 

55 

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

56 
val mk_co_iters_prelims: BNF_Util.fp_kind > typ list list list > typ list > typ list > 
53591  57 
int list > int list list > term list list > Proof.context > 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

58 
(term list list 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

59 
* (typ list list * typ list list list list * term list list 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

60 
* term list list list list) list option 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

61 
* (string * term list * term list list 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55471
diff
changeset

62 
* ((term list list * term list list list) * typ list) list) option) 
51903  63 
* Proof.context 
53591  64 
val mk_coiter_fun_arg_types: typ list list list > typ list > int list > term > 
52898  65 
typ list list 
66 
* (typ list list list list * typ list list list * typ list list list list * typ list) 

52320  67 
val define_iters: string list > 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

68 
(typ list list * typ list list list list * term list list * term list list list list) list > 
52319  69 
(string > binding) > typ list > typ list > term list > Proof.context > 
52320  70 
(term list * thm list) * Proof.context 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

71 
val define_coiters: string list > string * term list * term list list 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55471
diff
changeset

72 
* ((term list list * term list list list) * typ list) list > 
52319  73 
(string > binding) > typ list > typ list > term list > Proof.context > 
52320  74 
(term list * thm list) * Proof.context 
52346  75 
val derive_induct_iters_thms_for_types: BNF_Def.bnf list > 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

76 
(typ list list * typ list list list list * term list list * term list list list list) list > 
53106  77 
thm > thm list list > BNF_Def.bnf list > BNF_Def.bnf list > typ list > typ list > 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

78 
typ list > typ list list list > term list list > thm list list > term list list > 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

79 
thm list list > local_theory > lfp_sugar_thms 
52346  80 
val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list > 
52348  81 
string * term list * term list list * ((term list list * term list list list) 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55471
diff
changeset

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

83 
thm > thm list > thm list > thm list list > BNF_Def.bnf list > typ list > typ list > 
54235  84 
typ list > typ list list list > int list list > int list list > int list > thm list list > 
85 
Ctr_Sugar.ctr_sugar list > term list list > thm list list > (thm list > thm list) > 

86 
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

87 

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

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

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

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

91 

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

92 
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

93 
binding list list > binding list > (string * sort) list > typ list * typ list list > 
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

94 
BNF_Def.bnf list > local_theory > 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

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

97 
val parse_co_datatype_cmd: BNF_Util.fp_kind > (mixfix list > binding list > binding list > 
51867  98 
binding list list > binding list > (string * sort) list > typ list * typ list list > 
99 
BNF_Def.bnf list > local_theory > 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

100 
(local_theory > local_theory) parser 
49112  101 
end; 
102 

49636  103 
structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = 
49112  104 
struct 
105 

54006  106 
open Ctr_Sugar 
55571  107 
open BNF_FP_Rec_Sugar_Util 
49119  108 
open BNF_Util 
53222  109 
open BNF_Comp 
49214
2a3cb4c71b87
construct the right iterator theorem in the recursive case
blanchet
parents:
49213
diff
changeset

110 
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

111 
open BNF_FP_Util 
49636  112 
open BNF_FP_Def_Sugar_Tactics 
49119  113 

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

115 

51840  116 
type fp_sugar = 
51859  117 
{T: typ, 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

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

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

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

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

123 
nesting_bnfs: bnf list, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

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

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

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

128 
common_co_inducts: thm list, 
52343  129 
co_inducts: thm list, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

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

132 
sel_co_itersss: thm list list list}; 
52295  133 

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

134 
fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

135 
ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

136 
sel_co_itersss} : fp_sugar) = 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

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

139 
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

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

141 
pre_bnf = morph_bnf phi pre_bnf, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

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

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

145 
ctr_sugar = morph_ctr_sugar phi ctr_sugar, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

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

148 
common_co_inducts = map (Morphism.thm phi) common_co_inducts, 
52343  149 
co_inducts = map (Morphism.thm phi) co_inducts, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

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

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

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

153 

53907  154 
val transfer_fp_sugar = 
54740  155 
morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; 
53907  156 

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

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

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

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

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

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

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

164 

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

165 
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

166 
Symtab.lookup (Data.get (Context.Proof ctxt)) 
53907  167 
#> Option.map (transfer_fp_sugar ctxt); 
168 

169 
fun fp_sugars_of ctxt = 

170 
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

171 

53106  172 
fun co_induct_of (i :: _) = i; 
173 
fun strong_co_induct_of [_, s] = s; 

174 

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

51840  177 
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

178 
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

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

180 

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

181 
fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

182 
ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss 
55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55397
diff
changeset

183 
sel_co_iterssss lthy = 
51844  184 
(0, lthy) 
51859  185 
> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

186 
register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

187 
pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

188 
ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

189 
maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

190 
co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk, 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55535
diff
changeset

191 
sel_co_itersss = nth sel_co_iterssss kk} 
52337  192 
lthy)) Ts 
51824  193 
> snd; 
194 

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

49622  197 
fun quasi_unambiguous_case_names names = 
198 
let 

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

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

201 
fun underscore s = 

202 
let val ss = space_explode Long_Name.separator s in 

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

204 
end; 

205 
in 

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

207 
end; 

208 

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

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

211 

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

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

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

214 
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; 
49300  215 
val simp_attrs = @{attributes [simp]}; 
216 

49297  217 
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

218 

52868  219 
fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss); 
51829  220 

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

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

51829  224 

54171  225 
fun mk_tupled_fun x f xs = 
226 
if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs)); 

227 

52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

228 
fun mk_uncurried2_fun f xss = 
52868  229 
mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat_rec_arg_args xss); 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

230 

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

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

232 
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

233 

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

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

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

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

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

238 
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

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

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

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

242 

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

245 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

246 
end; 

247 

248 
val mk_ctor = mk_ctor_or_dtor range_type; 

249 
val mk_dtor = mk_ctor_or_dtor domain_type; 

250 

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

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

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

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

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

255 
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

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

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

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

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

260 
end; 
51827  261 

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

262 

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

263 
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

264 
 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

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

266 

53591  267 
fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] 
53901  268 
 unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts 
52871  269 
 unzip_corecT _ T = [T]; 
270 

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

271 
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

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

273 
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

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

275 

55700  276 
fun cannot_merge_types fp = 
277 
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

278 

55700  279 
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

280 

55700  281 
fun merge_type_args fp (As, As') = 
282 
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

283 

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

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

285 
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

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

287 

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

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

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

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

291 

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

292 
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

293 
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

294 
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

295 
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

296 
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

297 
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

298 

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

299 
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

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

301 
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

302 
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

303 
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

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

305 
 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

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

307 

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

308 
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

309 
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

310 

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

311 
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

312 

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

313 
type lfp_sugar_thms = 
55571  314 
(thm list * thm * Args.src list) * (thm list 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

315 

54256  316 
fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) = 
317 
((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs), 

55095  318 
(map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs)) 
319 
: lfp_sugar_thms; 

54256  320 

321 
val transfer_lfp_sugar_thms = 

54740  322 
morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; 
54256  323 

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

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

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

326 
* (thm list list * thm list list * Args.src list) 
54030
732b53d9b720
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
blanchet
parents:
54006
diff
changeset

327 
* (thm list 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

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

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

330 

54256  331 
fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs), 
332 
(unfoldss, corecss, coiter_attrs), (disc_unfoldss, disc_corecss, disc_iter_attrs), 

333 
(disc_unfold_iffss, disc_corec_iffss, disc_iter_iff_attrs), 

334 
(sel_unfoldsss, sel_corecsss, sel_iter_attrs)) = 

335 
((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, 

336 
coinduct_attrs), 

337 
(map (map (Morphism.thm phi)) unfoldss, map (map (Morphism.thm phi)) corecss, coiter_attrs), 

338 
(map (map (Morphism.thm phi)) disc_unfoldss, map (map (Morphism.thm phi)) disc_corecss, 

339 
disc_iter_attrs), 

340 
(map (map (Morphism.thm phi)) disc_unfold_iffss, map (map (Morphism.thm phi)) disc_corec_iffss, 

341 
disc_iter_iff_attrs), 

342 
(map (map (map (Morphism.thm phi))) sel_unfoldsss, 

55093  343 
map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms; 
54256  344 

345 
val transfer_gfp_sugar_thms = 

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

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

348 
fun mk_iter_fun_arg_types n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type; 
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

349 

53592
5a7bf8c859f6
made nonco case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset

350 
fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy = 
51832  351 
let 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

352 
val Css = map2 replicate ns Cs; 
55573  353 
val y_Tsss = map3 mk_iter_fun_arg_types ns mss (map un_fold_of ctor_iter_fun_Tss); 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

354 
val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts > C)) Cs y_Tsss; 
51832  355 

356 
val ((gss, ysss), lthy) = 

357 
lthy 

358 
> mk_Freess "f" g_Tss 

359 
>> mk_Freesss "x" y_Tsss; 

52301
7935e82a4ae4
simpler, more robust iterator goal construction code
blanchet
parents:
52300
diff
changeset

360 

7935e82a4ae4
simpler, more robust iterator goal construction code
blanchet
parents:
52300
diff
changeset

361 
val y_Tssss = map (map (map single)) y_Tsss; 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

362 
val yssss = map (map (map single)) ysss; 
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

363 

4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

364 
val z_Tssss = 
53592
5a7bf8c859f6
made nonco case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset

365 
map4 (fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts => 
5a7bf8c859f6
made nonco case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset

366 
map3 (fn m => fn ctr_Ts => fn ctor_iter_fun_T => 
5a7bf8c859f6
made nonco case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset

367 
map2 unzip_recT ctr_Ts (dest_tupleT m ctor_iter_fun_T)) 
5a7bf8c859f6
made nonco case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset

368 
ms ctr_Tss (dest_sumTN_balanced n (domain_type (co_rec_of ctor_iter_fun_Ts)))) 
5a7bf8c859f6
made nonco case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset

369 
ns mss ctr_Tsss ctor_iter_fun_Tss; 
51832  370 

52868  371 
val z_Tsss' = map (map flat_rec_arg_args) z_Tssss; 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

372 
val h_Tss = map2 (map2 (curry (op >))) z_Tsss' Css; 
51832  373 

374 
val hss = map2 (map2 retype_free) h_Tss gss; 

52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

375 
val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss; 
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

376 
val (zssss_tl, lthy) = 
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

377 
lthy 
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

378 
> mk_Freessss "y" (map (map (map tl)) z_Tssss); 
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

379 
val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl; 
51832  380 
in 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

381 
([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy) 
51832  382 
end; 
383 

53591  384 
fun mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts = 
51829  385 
let 
53591  386 
(*avoid "'a itself" arguments in coiterators*) 
387 
fun repair_arity [[]] = [[@{typ unit}]] 

388 
 repair_arity Tss = Tss; 

51829  389 

53591  390 
val ctr_Tsss' = map repair_arity ctr_Tsss; 
52870  391 
val f_sum_prod_Ts = map range_type fun_Ts; 
392 
val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; 

53591  393 
val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss; 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

394 
val f_Tssss = map3 (fn C => map2 (map2 (map (curry (op >) C) oo unzip_corecT))) 
53591  395 
Cs ctr_Tsss' f_Tsss; 
52871  396 
val q_Tssss = map (map (map (fn [_] => []  [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss; 
52870  397 
in 
398 
(q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) 

399 
end; 

51829  400 

52898  401 
fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n  1)) o mk_pred1T) ns Cs; 
402 

53591  403 
fun mk_coiter_fun_arg_types ctr_Tsss Cs ns dtor_coiter = 
52898  404 
(mk_coiter_p_pred_types Cs ns, 
55570  405 
mk_coiter_fun_arg_types0 ctr_Tsss Cs ns (binder_fun_types (fastype_of dtor_coiter))); 
52872  406 

53901  407 
fun mk_coiters_args_types ctr_Tsss Cs ns dtor_coiter_fun_Tss lthy = 
52870  408 
let 
52898  409 
val p_Tss = mk_coiter_p_pred_types Cs ns; 
51829  410 

52871  411 
fun mk_types get_Ts = 
51829  412 
let 
52335  413 
val fun_Ts = map get_Ts dtor_coiter_fun_Tss; 
53591  414 
val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts; 
52870  415 
in 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55471
diff
changeset

416 
(q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) 
52870  417 
end; 
51829  418 

52871  419 
val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types un_fold_of; 
420 
val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types co_rec_of; 

51831  421 

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

422 
val ((((Free (z, _), cs), pss), gssss), lthy) = 
51829  423 
lthy 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

424 
> yield_singleton (mk_Frees "z") dummyT 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

425 
>> mk_Frees "a" Cs 
51829  426 
>> mk_Freess "p" p_Tss 
427 
>> mk_Freessss "g" g_Tssss; 

428 
val rssss = map (map (map (fn [] => []))) r_Tssss; 

429 

430 
val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss; 

431 
val ((sssss, hssss_tl), lthy) = 

432 
lthy 

433 
> mk_Freessss "q" s_Tssss 

434 
>> mk_Freessss "h" (map (map (map tl)) h_Tssss); 

435 
val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl; 

51831  436 

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

51829  438 

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

439 
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

440 

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

441 
fun build_dtor_coiter_arg _ [] [cf] = cf 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

442 
 build_dtor_coiter_arg T [cq] [cf, cf'] = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

443 
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

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

445 

52349  446 
fun mk_args qssss fssss f_Tsss = 
51831  447 
let 
52868  448 
val pfss = map3 flat_corec_preds_predsss_gettersss pss qssss fssss; 
51831  449 
val cqssss = map2 (map o map o map o rapp) cs qssss; 
450 
val cfssss = map2 (map o map o map o rapp) cs fssss; 

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

451 
val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

452 
in (pfss, cqfsss) end; 
51831  453 

52349  454 
val unfold_args = mk_args rssss gssss g_Tsss; 
455 
val corec_args = mk_args sssss hssss h_Tsss; 

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

457 
((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy) 
51831  458 
end; 
51829  459 

53591  460 
fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy = 
51903  461 
let 
52169  462 
val thy = Proof_Context.theory_of lthy; 
463 

52335  464 
val (xtor_co_iter_fun_Tss, xtor_co_iterss) = 
55570  465 
map (mk_co_iters thy fp fpTs Cs #> `(binder_fun_types o fastype_of o hd)) 
466 
(transpose xtor_co_iterss0) 

52335  467 
> apsnd transpose o apfst transpose o split_list; 
51903  468 

52329  469 
val ((iters_args_types, coiters_args_types), lthy') = 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

470 
if fp = Least_FP then 
53592
5a7bf8c859f6
made nonco case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset

471 
mk_iters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy >> (rpair NONE o SOME) 
51903  472 
else 
55342  473 
mk_coiters_args_types ctr_Tsss Cs ns xtor_co_iter_fun_Tss lthy >> (pair NONE o SOME); 
51903  474 
in 
52335  475 
((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') 
51903  476 
end; 
477 

51900  478 
fun mk_preds_getterss_join c cps sum_prod_T cqfss = 
479 
let val n = length cqfss in 

480 
Term.lambda c (mk_IfN sum_prod_T cps 

481 
(map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n))) 

482 
end; 

51886  483 

52327  484 
fun define_co_iters fp fpT Cs binding_specs lthy0 = 
51897  485 
let 
52170
564be617ae84
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet
parents:
52169
diff
changeset

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

487 

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

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

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

490 

52327  491 
val ((csts, defs), (lthy', lthy)) = lthy0 
54623
59388c359dec
avoid userlevel 'Specification.definition' for lowlevel definitions
blanchet
parents:
54601
diff
changeset

492 
> apfst split_list o fold_map (fn (b, rhs) => 
59388c359dec
avoid userlevel 'Specification.definition' for lowlevel definitions
blanchet
parents:
54601
diff
changeset

493 
Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) 
52327  494 
#>> apsnd snd) binding_specs 
495 
> `Local_Theory.restore; 

496 

497 
val phi = Proof_Context.export_morphism lthy lthy'; 

498 

499 
val csts' = map (mk_co_iter thy fp fpT Cs o Morphism.term phi) csts; 

500 
val defs' = map (Morphism.thm phi) defs; 

501 
in 

502 
((csts', defs'), lthy') 

503 
end; 

504 

505 
fun define_iters iterNs iter_args_typess' mk_binding fpTs Cs ctor_iters lthy = 

506 
let 

51899  507 
val nn = length fpTs; 
508 

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

509 
val Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters))); 
51897  510 

54623
59388c359dec
avoid userlevel 'Specification.definition' for lowlevel definitions
blanchet
parents:
54601
diff
changeset

511 
fun generate_iter pre (_, _, fss, xssss) ctor_iter = 
59388c359dec
avoid userlevel 'Specification.definition' for lowlevel definitions
blanchet
parents:
54601
diff
changeset

512 
(mk_binding pre, 
59388c359dec
avoid userlevel 'Specification.definition' for lowlevel definitions
blanchet
parents:
54601
diff
changeset

513 
fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter, 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55410
diff
changeset

514 
map2 (mk_case_sumN_balanced oo map2 mk_uncurried2_fun) fss xssss))); 
51897  515 
in 
52327  516 
define_co_iters Least_FP fpT Cs (map3 generate_iter iterNs iter_args_typess' ctor_iters) lthy 
51897  517 
end; 
518 

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

519 
fun define_coiters coiterNs (_, cs, cpss, coiter_args_typess') mk_binding fpTs Cs dtor_coiters 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

520 
lthy = 
51897  521 
let 
51899  522 
val nn = length fpTs; 
523 

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

524 
val Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters))); 
51897  525 

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

526 
fun generate_coiter pre ((pfss, cqfsss), f_sum_prod_Ts) dtor_coiter = 
54623
59388c359dec
avoid userlevel 'Specification.definition' for lowlevel definitions
blanchet
parents:
54601
diff
changeset

527 
(mk_binding pre, 
59388c359dec
avoid userlevel 'Specification.definition' for lowlevel definitions
blanchet
parents:
54601
diff
changeset

528 
fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter, 
59388c359dec
avoid userlevel 'Specification.definition' for lowlevel definitions
blanchet
parents:
54601
diff
changeset

529 
map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss))); 
51897  530 
in 
52327  531 
define_co_iters Greatest_FP fpT Cs 
532 
(map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy 

52320  533 
end; 
51897  534 

53106  535 
fun derive_induct_iters_thms_for_types pre_bnfs [fold_args_types, rec_args_types] ctor_induct 
52346  536 
ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss iter_defss 
537 
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

538 
let 
52340  539 
val iterss' = transpose iterss; 
540 
val iter_defss' = transpose iter_defss; 

541 

542 
val [folds, recs] = iterss'; 

543 
val [fold_defs, rec_defs] = iter_defss'; 

544 

51827  545 
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; 
546 

51815  547 
val nn = length pre_bnfs; 
51827  548 
val ns = map length ctr_Tsss; 
549 
val mss = map (map length) ctr_Tsss; 

51815  550 

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

551 
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

552 
val pre_set_defss = map set_defs_of_bnf pre_bnfs; 
53329  553 
val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; 
554 
val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs; 

53290  555 
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

556 

51816  557 
val fp_b_names = map base_name_of_typ fpTs; 
51811  558 

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

560 
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

561 
> mk_Frees' "P" (map mk_pred1T fpTs) 
51827  562 
>> mk_Freesss "x" ctr_Tsss 
51816  563 
>> 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

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

566 

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

567 
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

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

569 
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

570 
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

571 
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

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

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

574 
~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

575 
 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

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

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

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

581 

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

582 
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

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

584 
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

585 
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

586 
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

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

588 

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

589 
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

590 
[([], (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

591 
 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

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

593 
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

594 
 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

595 
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

596 
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

597 
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

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

599 
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

600 
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

601 
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

602 
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

603 
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

604 
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

605 
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

606 
 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

607 

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

608 
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

609 
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

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

611 

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

612 
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

613 
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

614 
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

615 
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

616 

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

617 
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

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

619 
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

620 
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

621 
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

622 

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

623 
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

624 
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

625 

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

626 
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

627 

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

628 
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

629 
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

630 
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

631 

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

632 
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

633 

51814  634 
val ctor_induct' = ctor_induct OF (map mk_sumEN_tupled_balanced 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

635 

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

636 
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

637 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
53290  638 
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_maps 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

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

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

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

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

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

644 
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

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

646 
`(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

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

648 

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

649 
val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); 
52305  650 
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

651 

52305  652 
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; 
653 

52306  654 
fun mk_iter_thmss (_, x_Tssss, fss, _) iters iter_defs ctor_iter_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

655 
let 
52305  656 
val fiters = map (lists_bmoc fss) iters; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

657 

51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

658 
fun mk_goal fss fiter 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

659 
fold_rev (fold_rev Logic.all) (xs :: fss) 
51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

660 
(mk_Trueprop_eq (fiter $ 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

661 

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

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

665 
else 

666 
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

667 

52368  668 
fun build_iter (x as Free (_, T)) U = 
669 
if T = U then 

670 
x 

671 
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

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

674 

52868  675 
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_iter))) xsss x_Tssss; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

676 

52306  677 
val goalss = map5 (map4 o mk_goal fss) fiters 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

678 

52305  679 
val tacss = 
53329  680 
map2 (map o mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) iter_defs) 
52305  681 
ctor_iter_thms 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

682 

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

683 
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

684 
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

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

686 
in 
52305  687 
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

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

689 

52340  690 
val fold_thmss = mk_iter_thmss fold_args_types folds fold_defs (map un_fold_of ctor_iter_thmss); 
691 
val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs (map co_rec_of ctor_iter_thmss); 

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

692 
in 
52345  693 
((induct_thms, induct_thm, [induct_case_names_attr]), 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54107
diff
changeset

694 
(fold_thmss, 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

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

696 

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

697 
fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss, 
52869  698 
coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)]) 
54235  699 
dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss 
700 
mss ns ctr_defss (ctr_sugars : ctr_sugar list) coiterss coiter_defss export_args lthy = 

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

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

702 
fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter = 
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

703 
iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]]; 
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

704 

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

705 
val ctor_dtor_coiter_thmss = 
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

706 
map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss; 
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

707 

52339  708 
val coiterss' = transpose coiterss; 
709 
val coiter_defss' = transpose coiter_defss; 

710 

711 
val [unfold_defs, corec_defs] = coiter_defss'; 

52338  712 

51815  713 
val nn = length pre_bnfs; 
714 

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

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

716 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
53329  717 
val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; 
51830  718 
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

719 

51816  720 
val fp_b_names = map base_name_of_typ fpTs; 
51811  721 

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

722 
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

723 
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

724 
val selsss = map #selss ctr_sugars; 
51840  725 
val exhausts = map #exhaust ctr_sugars; 
726 
val disc_thmsss = map #disc_thmss ctr_sugars; 

727 
val discIss = map #discIs ctr_sugars; 

728 
val sel_thmsss = map #sel_thmss ctr_sugars; 

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

729 

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

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

732 
> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) 
51816  733 
>> Variable.variant_fixes fp_b_names 
734 
>> Variable.variant_fixes (map (suffix "'") fp_b_names); 

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

735 

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

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

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

738 
val uselsss = map2 (map o map o rapp) us selsss; 
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 
val vs = map2 (curry Free) vs' fpTs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

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

743 

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

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

746 
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

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

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

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

750 
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

751 

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

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

753 
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

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

755 

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

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

757 
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

758 

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

759 
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

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

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

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

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

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

765 
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

766 

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

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

768 
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

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

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

771 

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

772 
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

773 
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

774 
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

775 

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

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

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

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

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

780 

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

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

782 
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

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

784 

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

786 

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

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

788 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

789 
mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors 
51819  790 
exhausts ctr_defss disc_thmsss sel_thmsss) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

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

793 

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

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

795 
Thm.permute_prems 0 nn 
51828  796 
(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

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

798 
> `(conj_dests nn); 
53106  799 

800 
val rel_eqs = map rel_eq_of_bnf pre_bnfs; 

801 
val rel_monos = map rel_mono_of_bnf pre_bnfs; 

802 
val dtor_coinducts = 

803 
[dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos lthy]; 

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

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

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

807 

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

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

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

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

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

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

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

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

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

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

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

818 

51816  819 
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

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

821 
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

822 

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

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

824 

52339  825 
val fcoiterss' as [gunfolds, hcorecs] = 
52869  826 
map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss'; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

827 

54030
732b53d9b720
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
blanchet
parents:
54006
diff
changeset

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

829 
let 
51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

830 
fun mk_goal pfss c cps fcoiter n k ctr m cfs' = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

831 
fold_rev (fold_rev Logic.all) ([c] :: pfss) 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

832 
(Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, 
51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

833 
mk_Trueprop_eq (fcoiter $ c, Term.list_comb (ctr, take m cfs')))); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

834 

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

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

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

837 

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

838 
fun tack z_name (c, u) f = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

839 
let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55410
diff
changeset

840 
Term.lambda z (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ z) 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

842 

52368  843 
fun build_coiter fcoiters maybe_mk_sumT maybe_tack cqf = 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

844 
let val T = fastype_of cqf in 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

845 
if exists_subtype_in Cs T then 
52368  846 
let val U = mk_U maybe_mk_sumT T in 
55483
f223445a4d0c
tuned code to allow mutualized corecursion through different functions with the same target type
blanchet
parents:
55480
diff
changeset

847 
build_map lthy (indexify fst (map2 maybe_mk_sumT fpTs Cs) (fn kk => fn _ => 
52368  848 
maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf 
849 
end 

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

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

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

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

853 

52368  854 
val crgsss' = map (map (map (build_coiter (un_fold_of fcoiterss') (K I) (K I)))) crgsss; 
855 
val cshsss' = map (map (map (build_coiter (co_rec_of fcoiterss') (curry mk_sumT) (tack z)))) 

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

857 

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

858 
val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss'; 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

859 
val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

860 

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

861 
val unfold_tacss = 
53329  862 
map3 (map oo mk_coiter_tac unfold_defs nesting_map_idents) 
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

863 
(map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

864 
val corec_tacss = 
53329  865 
map3 (map oo mk_coiter_tac corec_defs nesting_map_idents) 
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

866 
(map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss; 
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 
fun prove goal tac = 
51815  869 
Goal.prove_sorry lthy [] [] goal (tac o #context) 
870 
> Thm.close_derivation; 

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

871 

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

872 
val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss; 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

874 
map2 (map2 prove) corec_goalss corec_tacss 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55410
diff
changeset

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

876 
in 
54030
732b53d9b720
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
blanchet
parents:
54006
diff
changeset

877 
(unfold_thmss, corec_thmss) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

879 

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

880 
val (disc_unfold_iff_thmss, disc_corec_iff_thmss) = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

881 
let 
51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

882 
fun mk_goal c cps fcoiter n k disc = 
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

883 
mk_Trueprop_eq (disc $ (fcoiter $ c), 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

885 
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

886 

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

887 
val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

888 
val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

889 

51828  890 
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

891 

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

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

893 

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

894 
val unfold_tacss = 
51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

895 
map3 (map oo mk_disc_coiter_iff_tac) case_splitss' unfold_thmss disc_thmsss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

896 
val corec_tacss = 
51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

897 
map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

898 

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

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

900 
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

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

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

904 

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

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

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

907 
in 
51828  908 
(map2 proves unfold_goalss unfold_tacss, map2 proves corec_goalss corec_tacss) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

910 

53741
c9068aade859
killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away  this solves issues in 'primcorec'
blanchet
parents:
53701
diff
changeset

911 
fun mk_disc_coiter_thms coiters discIs = map (op RS) (coiters ~~ discIs); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

912 

51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

913 
val disc_unfold_thmss = map2 mk_disc_coiter_thms unfold_thmss discIss; 
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

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

915 

51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

916 
fun mk_sel_coiter_thm coiter_thm sel sel_thm = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

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

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

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

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

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

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

924 
in 
51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

925 
coiter_thm RS arg_cong' RS sel_thm' 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

927 

52321  928 
fun mk_sel_coiter_thms coiter_thmss = 
53475  929 
map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

930 

53475  931 
val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss; 
932 
val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss; 

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

933 

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

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

935 
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

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

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

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

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

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

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

942 
in 
52345  943 
((coinduct_thms_pairs, coinduct_case_attrs), 
54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54107
diff
changeset

944 
(unfold_thmss, corec_thmss, code_nitpicksimp_attrs), 
53701  945 
(disc_unfold_thmss, disc_corec_thmss, []), 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

946 
(disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs), 
53475  947 
(sel_unfold_thmsss, sel_corec_thmsss, simp_attrs)) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

949 

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

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

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

954 

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

955 
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

956 
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

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

958 
(); 
49278  959 

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

961 
val fp_bs = map type_binding_of_spec specs; 
49498  962 
val fp_b_names = map Binding.name_of fp_bs; 
963 
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

964 
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

965 
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

966 

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

968 
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

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

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

971 

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

972 
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

973 
val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0; 
55700  974 
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

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

976 

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

977 
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

978 
val set_bss = map (map (the_default Binding.empty)) set_boss; 
49119  979 

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

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

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

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

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

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

985 
>> variant_tfrees fp_b_names; 
49119  986 

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

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

988 
Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec); 
51768  989 

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

990 
val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0; 
49119  991 

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

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

993 

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

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

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

997 

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

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

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

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

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

1002 
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

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

1004 

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

1005 
val mixfixes = map mixfix_of_spec specs; 
49119  1006 

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

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

1010 
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

1011 
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

1012 
val ctr_mixfixess = map (map snd) mx_ctr_specss; 
49119  1013 

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

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

1016 
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

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

1018 
val ctr_argsss = map (map args_of_ctr_spec) ctr_specss; 
49119  1019 

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

1021 
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

1022 
val raw_sel_defaultsss = map (map sel_defaults_of_ctr_spec) ctr_specss; 
49286  1023 

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

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

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

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

1027 

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

1028 
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

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

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

1031 
commas (map (qsoty o TFree) extras))); 
49165  1032 

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

1033 
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

1034 

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

1035 
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

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

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

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

1039 
 eq_fpT_check _ _ = false; 
49146  1040 

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

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

1044 
 kk => nth Xs kk) 
49204  1045 
 freeze_fp T = T; 
49121  1046 

53222  1047 
val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts); 
1048 

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

1049 
val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss; 
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

1050 
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; 
49119  1051 

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

1052 
val fp_eqs = 
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

1053 
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts; 
49121  1054 

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

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

1056 
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

1057 
 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

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

1059 

51839  1060 
val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, 
53106  1061 
xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, 
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

1062 
dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, 
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

1063 
lthy)) = 
53222  1064 
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs 
1065 
no_defs_lthy0 

1066 
handle BAD_DEAD (X, X_backdrop) => 

1067 
(case X_backdrop of 

1068 
Type (bad_tc, _) => 

1069 
let 

1070 
val fake_T = qsoty (unfreeze_fp X); 

1071 
val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop); 

1072 
fun register_hint () = 

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

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

1075 
\it"; 

1076 
in 

1077 
if is_some (bnf_of no_defs_lthy bad_tc) orelse 

1078 
is_some (fp_sugar_of no_defs_lthy bad_tc) then 

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

53222  1081 
else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy) 
1082 
bad_tc) then 

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

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

1085 
fake_T_backdrop ^ register_hint ()) 

1086 
else 

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

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

1089 
register_hint ()) 

1090 
end); 

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

1091 

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

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

1093 
val timer = time (Timer.startRealTimer ()); 
49121  1094 

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

1095 
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

1096 
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; 
49226  1097 

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

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

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

1100 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
53290  1101 
val nesting_set_maps = maps set_map_of_bnf nesting_bnfs; 
1102 
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

1103 

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

1104 
val live = live_of_bnf any_fp_bnf; 
52961  1105 
val _ = 
1106 
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

1107 
warning "Map function and relator names ignored" 
52961  1108 
else 
1109 
(); 

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

1110 

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

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

1112 
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

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

1114 

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

1115 
val B_ify = Term.typ_subst_atomic (As ~~ Bs); 
49167  1116 

49501  1117 
val ctors = map (mk_ctor As) ctors0; 
1118 
val dtors = map (mk_dtor As) dtors0; 

49124  1119 

49501  1120 
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

1121 

51780  1122 
fun massage_simple_notes base = 
1123 
filter_out (null o #2) 

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

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

1127 
val massage_multi_notes = 

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

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

51780  1133 

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

1134 
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; 
49203  1135 
val ns = map length ctr_Tsss; 
49212  1136 
val kss = map (fn n => 1 upto n) ns; 
49203  1137 
val mss = map (map length) ctr_Tsss; 
1138 

52367  1139 
val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') = 
53591  1140 
mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy; 
49210  1141 

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

1142 
fun define_ctrs_dtrs_for_type (((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor), 
52345  1143 
xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), 
1144 
pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings), 

1145 
ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = 

49176  1146 
let 
49498  1147 
val fp_b_name = Binding.name_of fp_b; 
1148 

49501  1149 
val dtorT = domain_type (fastype_of ctor); 
49210  1150 
val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; 
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49254
diff
changeset

1151 
val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts; 
49119  1152 

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

1153 
val ((((w, xss), yss), u'), names_lthy) = 
49204  1154 
no_defs_lthy 
49501  1155 
> yield_singleton (mk_Frees "w") dtorT 
49370  1156 
>> mk_Freess "x" ctr_Tss 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1157 
>> mk_Freess "y" (map (map B_ify) ctr_Tss) 
49498  1158 
>> yield_singleton Variable.variant_fixes fp_b_name; 
49370  1159 

49498  1160 
val u = Free (u', fpT); 
49121  1161 

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

1162 
val tuple_xs = map HOLogic.mk_tuple xss; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1163 
val tuple_ys = map HOLogic.mk_tuple yss; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1164 

49129  1165 
val ctr_rhss = 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1166 
map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $ 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1167 
mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs; 
49121  1168 

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

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

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