author  blanchet 
Fri, 16 Aug 2013 15:35:47 +0200  
changeset 53031  83cbe188855a 
parent 53029  8444e1b8e7a3 
child 53032  953534445ab6 
permissions  rwrr 
49636  1 
(* Title: HOL/BNF/Tools/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, 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

12 
fp: BNF_FP_Util.fp_kind, 
51838  13 
index: int, 
14 
pre_bnfs: BNF_Def.bnf list, 

52356  15 
nested_bnfs: BNF_Def.bnf list, 
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

16 
fp_res: BNF_FP_Util.fp_result, 
51906  17 
ctr_defss: thm list list, 
51842  18 
ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, 
52336  19 
co_iterss: term list list, 
52343  20 
co_inducts: thm list, 
52337  21 
co_iter_thmsss: thm list list list}; 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

22 

52295  23 
val of_fp_sugar: (fp_sugar > 'a list) > fp_sugar > 'a 
51896  24 
val morph_fp_sugar: morphism > fp_sugar > fp_sugar 
25 
val fp_sugar_of: Proof.context > string > fp_sugar option 

51852  26 

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

27 
val tvar_subst: theory > typ list > typ list > ((string * int) * typ) list 
51860  28 
val exists_subtype_in: typ list > typ > bool 
52868  29 
val flat_rec_arg_args: 'a list list > 'a list 
30 
val flat_corec_preds_predsss_gettersss: 'a list > 'a list list list > 'a list list list > 

31 
'a list 

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

32 
val mk_co_iter: theory > BNF_FP_Util.fp_kind > typ > typ list > term > term 
51907  33 
val nesty_bnfs: Proof.context > typ list list list > typ list > BNF_Def.bnf list 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

34 
val mk_map: int > typ list > typ list > term > term 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

35 
val build_map: local_theory > (typ * typ > term) > typ * typ > term 
53031  36 
val dest_map: Proof.context > string > term > term * term list 
52334  37 
val mk_co_iters_prelims: BNF_FP_Util.fp_kind > typ list > typ list > int list > 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

38 
int list list > term list list > Proof.context > 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

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

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

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

42 
* (string * term list * term list list 
52349  43 
* ((term list list * term list list list) * (typ list * typ list list)) list) option) 
51903  44 
* Proof.context 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

45 

52872  46 
val mk_iter_fun_arg_types: typ list > int list > int list list > term > 
52215
7facaee8586f
tuning (use lists rather than pairs of lists throughout)
blanchet
parents:
52214
diff
changeset

47 
typ list list list list 
52872  48 
val mk_coiter_fun_arg_types: typ list > int list > int list list > term > 
52898  49 
typ list list 
50 
* (typ list list list list * typ list list list * typ list list list list * typ list) 

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

52 
(typ list list * typ list list list list * term list list * term list list list list) list > 
52319  53 
(string > binding) > typ list > typ list > term list > Proof.context > 
52320  54 
(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

55 
val define_coiters: string list > string * term list * term list list 
52349  56 
* ((term list list * term list list list) * (typ list * typ list list)) list > 
52319  57 
(string > binding) > typ list > typ list > term list > Proof.context > 
52320  58 
(term list * thm list) * Proof.context 
52346  59 
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

60 
(typ list list * typ list list list list * term list list * term list list list list) list > 
52344  61 
thm list > 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

62 
typ list > typ list list list > term list list > thm list list > term list list > 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

63 
thm list list > local_theory > 
52345  64 
(thm list * thm * Args.src list) * (thm list list * Args.src list) 
51827  65 
* (thm list list * Args.src list) 
52346  66 
val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list > 
52348  67 
string * term list * term list list * ((term list list * term list list list) 
52351  68 
* (typ list * typ list list)) list > 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52964
diff
changeset

69 
thm list > thm list > thm list list > BNF_Def.bnf list > typ list > typ list > typ list > 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52964
diff
changeset

70 
int list list > int list list > int list > thm list list > BNF_Ctr_Sugar.ctr_sugar list > 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52964
diff
changeset

71 
term list list > thm list list > (thm list > thm list) > local_theory > 
52345  72 
((thm list * thm) list * Args.src list) 
51839  73 
* (thm list list * thm list list * Args.src list) 
51811  74 
* (thm list list * thm list list) * (thm list list * thm list list * Args.src list) 
51824  75 
* (thm list list * thm list list * Args.src list) 
76 
* (thm list list * thm list list * Args.src list) 

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

77 

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

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

79 
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

80 
BNF_Def.bnf list > local_theory > BNF_FP_Util.fp_result * local_theory) > 
51767
bbcdd8519253
honor userspecified name for relator + generalize syntax
blanchet
parents:
51766
diff
changeset

81 
(bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) * 
51758  82 
((((binding * binding) * (binding * typ) list) * (binding * term) list) * 
83 
mixfix) list) list > 

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

85 
val parse_co_datatype_cmd: BNF_FP_Util.fp_kind > (mixfix list > binding list > binding list > 
51867  86 
binding list list > binding list > (string * sort) list > typ list * typ list list > 
87 
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

88 
(local_theory > local_theory) parser 
49112  89 
end; 
90 

49636  91 
structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = 
49112  92 
struct 
93 

49119  94 
open BNF_Util 
51797  95 
open BNF_Ctr_Sugar 
49214
2a3cb4c71b87
construct the right iterator theorem in the recursive case
blanchet
parents:
49213
diff
changeset

96 
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

97 
open BNF_FP_Util 
49636  98 
open BNF_FP_Def_Sugar_Tactics 
49119  99 

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

101 

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

104 
fp: fp_kind, 
51838  105 
index: int, 
106 
pre_bnfs: bnf list, 

52356  107 
nested_bnfs: bnf list, 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

108 
fp_res: fp_result, 
51906  109 
ctr_defss: thm list list, 
51842  110 
ctr_sugars: ctr_sugar list, 
52336  111 
co_iterss: term list list, 
52343  112 
co_inducts: thm list, 
52337  113 
co_iter_thmsss: thm list list list}; 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

114 

52295  115 
fun of_fp_sugar f (fp_sugar as {index, ...}) = nth (f fp_sugar) index; 
116 

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

117 
fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, 
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

118 
{T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = 
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

119 
T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

120 

52356  121 
fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, fp_res, ctr_defss, ctr_sugars, 
122 
co_iterss, co_inducts, co_iter_thmsss} = 

123 
{T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, 

124 
nested_bnfs = map (morph_bnf phi) nested_bnfs, fp_res = morph_fp_result phi fp_res, 

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

125 
ctr_defss = map (map (Morphism.thm phi)) ctr_defss, 
52336  126 
ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, 
52343  127 
co_iterss = map (map (Morphism.term phi)) co_iterss, 
128 
co_inducts = map (Morphism.thm phi) co_inducts, 

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

130 

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

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

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

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

135 
val extend = I; 
51840  136 
val merge = Symtab.merge eq_fp_sugar; 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

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

138 

51840  139 
val fp_sugar_of = Symtab.lookup o Data.get o Context.Proof; 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

140 

51840  141 
fun register_fp_sugar key fp_sugar = 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

142 
Local_Theory.declaration {syntax = false, pervasive = true} 
52793  143 
(fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar))); 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

144 

52356  145 
fun register_fp_sugars fp pre_bnfs nested_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss 
146 
co_inducts co_iter_thmsss lthy = 

51844  147 
(0, lthy) 
51859  148 
> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, 
52356  149 
register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, 
150 
nested_bnfs = nested_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, 

151 
co_iterss = co_iterss, co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss} 

52337  152 
lthy)) Ts 
51824  153 
> snd; 
154 

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

155 
(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) 
49622  156 
fun quasi_unambiguous_case_names names = 
157 
let 

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

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

160 
fun underscore s = 

161 
let val ss = space_explode Long_Name.separator s in 

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

163 
end; 

164 
in 

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

166 
end; 

167 

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

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

170 

49300  171 
val simp_attrs = @{attributes [simp]}; 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

172 
val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs; 
49300  173 

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

174 
fun tvar_subst thy Ts Us = 
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

175 
Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; 
6c425d450a8c
more robust iterator construction (needed for mutualized FPs)
blanchet
parents:
51910
diff
changeset

176 

51860  177 
val exists_subtype_in = Term.exists_subtype o member (op =); 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

178 

49342  179 
fun resort_tfree S (TFree (s, _)) = TFree (s, S); 
180 

53029  181 
(* FIXME: merge with function of the same name in "bnf_fp_n2m.ML" (in the 
182 
prim(co)rec repository) *) 

51845  183 
fun typ_subst_nonatomic inst (T as Type (s, Ts)) = 
49214
2a3cb4c71b87
construct the right iterator theorem in the recursive case
blanchet
parents:
49213
diff
changeset

184 
(case AList.lookup (op =) inst T of 
51845  185 
NONE => Type (s, map (typ_subst_nonatomic inst) Ts) 
49214
2a3cb4c71b87
construct the right iterator theorem in the recursive case
blanchet
parents:
49213
diff
changeset

186 
 SOME T' => T') 
51845  187 
 typ_subst_nonatomic inst T = the_default T (AList.lookup (op =) inst T); 
49205  188 

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

190 

52868  191 
fun flat_rec_arg_args xss = 
192 
(* FIXME (once the old datatype package is phased out): The first line below gives the preferred 

193 
order. The second line is for compatibility with the old datatype package. *) 

52215
7facaee8586f
tuning (use lists rather than pairs of lists throughout)
blanchet
parents:
52214
diff
changeset

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

195 
flat xss 
51795
096b96281e34
for compatibility, generate recursor arguments in the same order as old package
blanchet
parents:
51794
diff
changeset

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

197 
map hd xss @ maps tl xss; 
51793
22f22172a361
started working on compatibility with old package's recursor
blanchet
parents:
51790
diff
changeset

198 

52868  199 
fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss); 
51829  200 

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

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

51829  204 

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

205 
fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); 
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

206 
fun mk_uncurried2_fun f xss = 
52868  207 
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

208 

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

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

210 
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

211 

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

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

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

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

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

216 
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

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

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

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

220 

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

223 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

224 
end; 

225 

226 
val mk_ctor = mk_ctor_or_dtor range_type; 

227 
val mk_dtor = mk_ctor_or_dtor domain_type; 

228 

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

229 
fun mk_co_iter thy fp fpT Cs t = 
49536  230 
let 
52309  231 
val (binders, body) = strip_type (fastype_of t); 
232 
val (f_Cs, prebody) = split_last binders; 

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

233 
val fpT0 = if fp = Least_FP then prebody else body; 
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

234 
val Cs0 = distinct (op =) (map (if fp = Least_FP then body_type else domain_type) f_Cs); 
52197  235 
val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs); 
49536  236 
in 
52170
564be617ae84
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet
parents:
52169
diff
changeset

237 
Term.subst_TVars rho t 
49536  238 
end; 
239 

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

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

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

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

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

244 
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

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

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

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

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

249 
end; 
51827  250 

52169  251 
val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of; 
252 

52296  253 
fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) = 
254 
if member (op =) Cs U then Ts else [T] 

52216  255 
 unzip_recT _ T = [T]; 
51827  256 

52871  257 
fun unzip_corecT Cs (T as Type (@{type_name sum}, Ts as [_, U])) = 
258 
if member (op =) Cs U then Ts else [T] 

259 
 unzip_corecT _ T = [T]; 

260 

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

261 
fun mk_map live Ts Us t = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

262 
let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) >> List.last in 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

263 
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

265 

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

266 
fun mk_rel live Ts Us t = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

267 
let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

268 
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

270 

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

271 
fun build_map lthy build_simple = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

273 
fun build (TU as (T, U)) = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

274 
if T = U then 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

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

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

278 
(Type (s, Ts), Type (s', Us)) => 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

279 
if s = s' then 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

281 
val bnf = the (bnf_of lthy s); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

282 
val live = live_of_bnf bnf; 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

283 
val mapx = mk_map live Ts Us (map_of_bnf bnf); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

284 
val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx))); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

285 
in Term.list_comb (mapx, map build TUs') end 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

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

288 
 _ => build_simple TU); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

290 

53031  291 
val dummy_var_name = "?f" 
292 

293 
fun mk_map_pattern ctxt s = 

294 
let 

295 
val bnf = the (bnf_of ctxt s); 

296 
val mapx = map_of_bnf bnf; 

297 
val live = live_of_bnf bnf; 

298 
val (f_Ts, _) = strip_typeN live (fastype_of mapx); 

299 
val fs = map_index (fn (i, T) => Var ((dummy_var_name, i), T)) f_Ts; 

300 
in 

301 
(mapx, betapplys (mapx, fs)) 

302 
end; 

303 

304 
fun dest_map ctxt s call = 

305 
let 

306 
val thy = Proof_Context.theory_of ctxt; 

307 
val (map0, pat) = mk_map_pattern ctxt s; 

308 
val (_, tenv) = Pattern.first_order_match thy (pat, call) (Vartab.empty, Vartab.empty); 

309 
in 

310 
(map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv []) 

311 
end; 

312 

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

313 
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

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

315 
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

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

317 

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

318 
fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

319 

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

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

321 

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

322 
fun merge_type_args (As, As') = 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

323 
if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types (); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

324 

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

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

326 
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

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

328 

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

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

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

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

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

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

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

335 

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

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

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

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

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

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

341 

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

342 
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

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

344 
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

345 
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

346 
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

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

348 
 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

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

350 

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

351 
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

352 
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

353 

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

355 

52872  356 
fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type; 
51846  357 

52872  358 
fun mk_iter_fun_arg_types Cs ns mss = 
51885  359 
mk_fp_iter_fun_types 
52872  360 
#> map3 mk_iter_fun_arg_types0 ns mss 
52296  361 
#> map (map (map (unzip_recT Cs))); 
51885  362 

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

365 
val Css = map2 replicate ns Cs; 
52872  366 
val y_Tsss = map3 mk_iter_fun_arg_types0 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

367 
val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts > C)) Cs y_Tsss; 
51832  368 

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

370 
lthy 

371 
> mk_Freess "f" g_Tss 

372 
>> mk_Freesss "x" y_Tsss; 

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

373 

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

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

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

376 

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

377 
val z_Tssss = 
52296  378 
map3 (fn n => fn ms => map2 (map (unzip_recT Cs) oo dest_tupleT) ms o 
52335  379 
dest_sumTN_balanced n o domain_type o co_rec_of) ns mss ctor_iter_fun_Tss; 
51832  380 

52868  381 
val z_Tsss' = map (map flat_rec_arg_args) z_Tssss; 
52923  382 
val h_Tss = map2 (map2 (curry op >)) z_Tsss' Css; 
51832  383 

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

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

385 
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

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

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

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

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

391 
([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy) 
51832  392 
end; 
393 

52872  394 
fun mk_coiter_fun_arg_types0 Cs ns mss fun_Ts = 
51829  395 
let 
396 
(*avoid "'a itself" arguments in coiterators and corecursors*) 

397 
fun repair_arity [0] = [1] 

398 
 repair_arity ms = ms; 

399 

52870  400 
val f_sum_prod_Ts = map range_type fun_Ts; 
401 
val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; 

402 
val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss; 

52923  403 
val f_Tssss = map2 (fn C => map (map (map (curry op > C) o unzip_corecT Cs))) Cs f_Tsss; 
52871  404 
val q_Tssss = map (map (map (fn [_] => []  [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss; 
52870  405 
in 
406 
(q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) 

407 
end; 

51829  408 

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

411 
fun mk_coiter_fun_arg_types Cs ns mss dtor_coiter = 

412 
(mk_coiter_p_pred_types Cs ns, 

413 
mk_fp_iter_fun_types dtor_coiter > mk_coiter_fun_arg_types0 Cs ns mss); 

52872  414 

52870  415 
fun mk_coiters_args_types Cs ns mss dtor_coiter_fun_Tss lthy = 
416 
let 

52898  417 
val p_Tss = mk_coiter_p_pred_types Cs ns; 
51829  418 

52871  419 
fun mk_types get_Ts = 
51829  420 
let 
52335  421 
val fun_Ts = map get_Ts dtor_coiter_fun_Tss; 
52872  422 
val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 Cs ns mss fun_Ts; 
52868  423 
val pf_Tss = map3 flat_corec_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; 
52870  424 
in 
425 
(q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss)) 

426 
end; 

51829  427 

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

51831  430 

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

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

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

434 
>> mk_Frees "a" Cs 
51829  435 
>> mk_Freess "p" p_Tss 
436 
>> mk_Freessss "g" g_Tssss; 

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

438 

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

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

441 
lthy 

442 
> mk_Freessss "q" s_Tssss 

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

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

51831  445 

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

51829  447 

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

448 
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

449 

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

450 
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

451 
 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

452 
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

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

454 

52349  455 
fun mk_args qssss fssss f_Tsss = 
51831  456 
let 
52868  457 
val pfss = map3 flat_corec_preds_predsss_gettersss pss qssss fssss; 
51831  458 
val cqssss = map2 (map o map o map o rapp) cs qssss; 
459 
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

460 
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

461 
in (pfss, cqfsss) end; 
51831  462 

52349  463 
val unfold_args = mk_args rssss gssss g_Tsss; 
464 
val corec_args = mk_args sssss hssss h_Tsss; 

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

466 
((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy) 
51831  467 
end; 
51829  468 

52334  469 
fun mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy = 
51903  470 
let 
52169  471 
val thy = Proof_Context.theory_of lthy; 
472 

52335  473 
val (xtor_co_iter_fun_Tss, xtor_co_iterss) = 
52329  474 
map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) (transpose xtor_co_iterss0) 
52335  475 
> apsnd transpose o apfst transpose o split_list; 
51903  476 

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

478 
if fp = Least_FP then 
52335  479 
mk_iters_args_types Cs ns mss xtor_co_iter_fun_Tss lthy >> (rpair NONE o SOME) 
51903  480 
else 
52335  481 
mk_coiters_args_types Cs ns mss xtor_co_iter_fun_Tss lthy >> (pair NONE o SOME) 
51903  482 
in 
52335  483 
((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') 
51903  484 
end; 
485 

52298  486 
fun mk_iter_body ctor_iter fss xssss = 
487 
Term.list_comb (ctor_iter, map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss); 

51884  488 

51900  489 
fun mk_preds_getterss_join c cps sum_prod_T cqfss = 
490 
let val n = length cqfss in 

491 
Term.lambda c (mk_IfN sum_prod_T cps 

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

493 
end; 

51886  494 

52348  495 
fun mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter = 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

496 
Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss); 
51886  497 

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

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

501 

52327  502 
val ((csts, defs), (lthy', lthy)) = lthy0 
503 
> apfst split_list o fold_map (fn (b, spec) => 

504 
Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) 

505 
#>> apsnd snd) binding_specs 

506 
> `Local_Theory.restore; 

507 

508 
val phi = Proof_Context.export_morphism lthy lthy'; 

509 

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

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

512 
in 

513 
((csts', defs'), lthy') 

514 
end; 

515 

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

517 
let 

51899  518 
val nn = length fpTs; 
519 

52320  520 
val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters))); 
51897  521 

52320  522 
fun generate_iter suf (f_Tss, _, fss, xssss) ctor_iter = 
51897  523 
let 
52923  524 
val res_T = fold_rev (curry op >) f_Tss fpT_to_C; 
52309  525 
val b = mk_binding suf; 
51897  526 
val spec = 
52309  527 
mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)), 
52298  528 
mk_iter_body ctor_iter fss xssss); 
52309  529 
in (b, spec) end; 
51897  530 
in 
52327  531 
define_co_iters Least_FP fpT Cs (map3 generate_iter iterNs iter_args_typess' ctor_iters) lthy 
51897  532 
end; 
533 

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

534 
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

535 
lthy = 
51897  536 
let 
51899  537 
val nn = length fpTs; 
538 

52326  539 
val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters))); 
51897  540 

52349  541 
fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter = 
51897  542 
let 
52923  543 
val res_T = fold_rev (curry op >) pf_Tss C_to_fpT; 
52309  544 
val b = mk_binding suf; 
51897  545 
val spec = 
52309  546 
mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)), 
52348  547 
mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter); 
52309  548 
in (b, spec) end; 
51897  549 
in 
52327  550 
define_co_iters Greatest_FP fpT Cs 
551 
(map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy 

52320  552 
end; 
51897  553 

52346  554 
fun derive_induct_iters_thms_for_types pre_bnfs [fold_args_types, rec_args_types] [ctor_induct] 
555 
ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss iter_defss 

556 
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

557 
let 
52340  558 
val iterss' = transpose iterss; 
559 
val iter_defss' = transpose iter_defss; 

560 

561 
val [folds, recs] = iterss'; 

562 
val [fold_defs, rec_defs] = iter_defss'; 

563 

51827  564 
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; 
565 

51815  566 
val nn = length pre_bnfs; 
51827  567 
val ns = map length ctr_Tsss; 
568 
val mss = map (map length) ctr_Tsss; 

51815  569 

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

571 
val pre_set_defss = map set_defs_of_bnf pre_bnfs; 
52355  572 
val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs; 
573 
val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nested_bnfs; 

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

574 
val nested_set_map's = 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

575 

51816  576 
val fp_b_names = map base_name_of_typ fpTs; 
51811  577 

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

579 
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

580 
> mk_Frees' "P" (map mk_pred1T fpTs) 
51827  581 
>> mk_Freesss "x" ctr_Tsss 
51816  582 
>> 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

583 

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

584 
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

585 

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

586 
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

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

588 
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

589 
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

590 
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

591 
fun mk_set U = 
52923  592 
(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

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

594 
 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

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

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

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

598 

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

599 
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

600 

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

601 
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

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

603 
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

604 
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

605 
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

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

607 

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

608 
fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) = 
52923  609 
[([], (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

610 
 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

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

612 
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

613 
 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

614 
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

615 
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

616 
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

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

618 
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

619 
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

620 
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

621 
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

622 
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

623 
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

624 
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

625 
 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

626 

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

627 
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

628 
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

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

630 

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

631 
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

632 
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

633 
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

634 
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

635 

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

636 
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

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

638 
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

639 
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

640 
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

641 

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

642 
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

643 
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

644 

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

645 
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

646 

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

647 
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

648 
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, 
52923  649 
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

650 

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

651 
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

652 

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

654 

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

655 
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

656 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

657 
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_map's 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

658 
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

659 
> singleton (Proof_Context.export names_lthy lthy) 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

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

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

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

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

664 

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

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

667 

52305  668 
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; 
669 

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

671 
let 
52305  672 
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

673 

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

674 
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

675 
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

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

677 

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

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

681 
else 

682 
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

683 

52368  684 
fun build_iter (x as Free (_, T)) U = 
685 
if T = U then 

686 
x 

687 
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

688 
build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs 
52368  689 
(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

690 

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

692 

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

694 

52305  695 
val tacss = 
696 
map2 (map o mk_iter_tac pre_map_defs (nested_map_ids'' @ nesting_map_ids'') iter_defs) 

697 
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

698 

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

699 
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

700 
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

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

702 
in 
52305  703 
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

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

705 

52340  706 
val fold_thmss = mk_iter_thmss fold_args_types folds fold_defs (map un_fold_of ctor_iter_thmss); 
707 
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

708 
in 
52345  709 
((induct_thms, induct_thm, [induct_case_names_attr]), 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

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

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

712 

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

713 
fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss, 
52869  714 
coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)]) 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52964
diff
changeset

715 
dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss 
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52964
diff
changeset

716 
ctr_sugars coiterss coiter_defss export_args lthy = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

717 
let 
52339  718 
val coiterss' = transpose coiterss; 
719 
val coiter_defss' = transpose coiter_defss; 

720 

721 
val [unfold_defs, corec_defs] = coiter_defss'; 

52338  722 

51815  723 
val nn = length pre_bnfs; 
724 

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

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

726 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
52355  727 
val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs; 
51830  728 
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

729 

51816  730 
val fp_b_names = map base_name_of_typ fpTs; 
51811  731 

51840  732 
val ctrss = map (map (mk_ctr As) o #ctrs) ctr_sugars; 
733 
val discss = map (map (mk_disc_or_sel As) o #discs) ctr_sugars; 

734 
val selsss = map (map (map (mk_disc_or_sel As)) o #selss) ctr_sugars; 

735 
val exhausts = map #exhaust ctr_sugars; 

736 
val disc_thmsss = map #disc_thmss ctr_sugars; 

737 
val discIss = map #discIs ctr_sugars; 

738 
val sel_thmsss = map #sel_thmss ctr_sugars; 

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

739 

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

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

742 
> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) 
51816  743 
>> Variable.variant_fixes fp_b_names 
744 
>> Variable.variant_fixes (map (suffix "'") fp_b_names); 

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

745 

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

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

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

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

749 

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

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

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

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

753 

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

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

756 
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

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

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

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

760 
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

761 

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

762 
(* TODO: generalize (cf. "build_map") *) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

763 
fun build_rel rs' T = 
52923  764 
(case find_index (curry op = T) fpTs of 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

765 
~1 => 
51856  766 
if exists_subtype_in fpTs T then 
767 
let 

768 
val Type (s, Ts) = T 

769 
val bnf = the (bnf_of lthy s); 

770 
val live = live_of_bnf bnf; 

771 
val rel = mk_rel live Ts Ts (rel_of_bnf bnf); 

772 
val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel))); 

773 
in Term.list_comb (rel, map (build_rel rs') Ts') end 

774 
else 

775 
HOLogic.eq_const T 

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

776 
 kk => nth rs' kk); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

777 

51856  778 
fun build_rel_app rs' usel vsel = fold rapp [usel, vsel] (build_rel rs' (fastype_of usel)); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

779 

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

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

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

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

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

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

785 
[Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

787 

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

788 
fun mk_prem_concl rs' n udiscs uselss vdiscs vselss = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

790 
(flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss)) 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

792 

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

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

794 
fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

796 

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

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

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

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

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

801 

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

802 
fun mk_goal rs' = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

803 
Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss, 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

805 

52345  806 
val goals = map mk_goal [rs, strong_rs]; 
51810
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 prove dtor_coinduct' goal = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

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

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

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

814 

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

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

816 
Thm.permute_prems 0 nn 
51828  817 
(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

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

819 
> `(conj_dests nn); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

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

823 

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

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

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

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

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

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

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

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

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

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

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

834 

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

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

837 
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

838 

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

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

840 

52339  841 
val fcoiterss' as [gunfolds, hcorecs] = 
52869  842 
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

843 

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

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

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

846 
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

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

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

849 
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

850 

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

851 
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

852 
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

853 

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

854 
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

855 
let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

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

858 

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

860 
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

861 
if exists_subtype_in Cs T then 
52368  862 
let val U = mk_U maybe_mk_sumT T in 
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52964
diff
changeset

863 
build_map lthy (indexify snd fpTs (fn kk => fn _ => 
52368  864 
maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf 
865 
end 

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

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

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

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

869 

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

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

873 

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

874 
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

875 
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

876 

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

877 
val unfold_tacss = 
52349  878 
map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'') 
52340  879 
(map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

880 
val corec_tacss = 
52349  881 
map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'') 
52340  882 
(map co_rec_of dtor_coiter_thmss) pre_map_defs ctr_defss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

883 

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

884 
fun prove goal tac = 
51815  885 
Goal.prove_sorry lthy [] [] goal (tac o #context) 
886 
> Thm.close_derivation; 

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

887 

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

888 
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

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

890 
map2 (map2 prove) corec_goalss corec_tacss 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

891 
> map (map (unfold_thms lthy @{thms sum_case_if})); 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

892 

52923  893 
val unfold_safesss = map2 (map2 (map2 (curry op =))) crgsss' crgsss; 
894 
val corec_safesss = map2 (map2 (map2 (curry op =))) cshsss' cshsss; 

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

895 

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

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

897 
map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

898 
curry (op ~~)); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

899 

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

900 
val safe_unfold_thmss = filter_safesss unfold_safesss unfold_thmss; 
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

901 
val safe_corec_thmss = filter_safesss corec_safesss corec_thmss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

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

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

905 

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

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

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

908 
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

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

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

911 
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

912 

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

913 
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

914 
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

915 

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

917 

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

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

919 

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

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

921 
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

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

923 
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

924 

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

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

926 
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

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

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

930 

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

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

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

933 
in 
51828  934 
(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

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

936 

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

937 
val is_triv_discI = is_triv_implies orf is_concl_refl; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

938 

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

939 
fun mk_disc_coiter_thms coiters discIs = 
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

940 
map (op RS) (filter_out (is_triv_discI o snd) (coiters ~~ discIs)); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

941 

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

942 
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

943 
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

944 

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

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

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

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

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

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

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

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

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

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

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

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

956 

52321  957 
fun mk_sel_coiter_thms coiter_thmss = 
958 
map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss > map flat; 

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

959 

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

960 
val sel_unfold_thmss = mk_sel_coiter_thms unfold_thmss; 
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

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

962 

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

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

964 
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

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

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

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

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

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

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

971 
in 
52345  972 
((coinduct_thms_pairs, coinduct_case_attrs), 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

974 
(safe_unfold_thmss, safe_corec_thmss), 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

975 
(disc_unfold_thmss, disc_corec_thmss, simp_attrs), 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

977 
(sel_unfold_thmss, sel_corec_thmss, simp_attrs)) 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

979 

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

980 
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp 
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52968
diff
changeset

981 
(wrap_opts as (no_discs_sels, rep_compat), specs) no_defs_lthy0 = 
49112  982 
let 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

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

984 

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

985 
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

986 
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

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

988 
(); 
49278  989 

49633  990 
fun qualify mandatory fp_b_name = 
991 
Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix); 

992 

49367  993 
val nn = length specs; 
49361
cc1d39529dd1
derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive
blanchet
parents:
49342
diff
changeset

994 
val fp_bs = map type_binding_of specs; 
49498  995 
val fp_b_names = map Binding.name_of fp_bs; 
996 
val fp_common_name = mk_common_name fp_b_names; 

52964  997 
val map_bs = map2 (fn fp_b_name => qualify false fp_b_name o map_binding_of) fp_b_names specs; 
998 
val rel_bs = map2 (fn fp_b_name => qualify false fp_b_name o rel_binding_of) fp_b_names specs; 

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

999 

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

1001 
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

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

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

1004 

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

1006 
val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0; 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1007 
val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0; 
51758  1008 
val set_bss = map (map fst o type_args_named_constrained_of) specs; 
49119  1009 

52960  1010 
val _ = has_duplicates (op =) unsorted_As andalso 
1011 
error ("Duplicate parameters in " ^ co_prefix fp ^ "datatype specification"); 

1012 

52959
8d581fd1b46f
gracefully fail to define polymorphic (co)datatypes in local context
blanchet
parents:
52923
diff
changeset

1013 
val bad_args = 
8d581fd1b46f
gracefully fail to define polymorphic (co)datatypes in local context
blanchet
parents:
52923
diff
changeset

1014 
map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As 
8d581fd1b46f
gracefully fail to define polymorphic (co)datatypes in local context
blanchet
parents:
52923
diff
changeset

1015 
> filter_out Term.is_TVar; 
8d581fd1b46f
gracefully fail to define polymorphic (co)datatypes in local context
blanchet
parents:
52923
diff
changeset

1016 
val _ = null bad_args orelse 
8d581fd1b46f
gracefully fail to define polymorphic (co)datatypes in local context
blanchet
parents:
52923
diff
changeset

1017 
error ("Locally fixed type argument " ^ 
8d581fd1b46f
gracefully fail to define polymorphic (co)datatypes in local context
blanchet
parents:
52923
diff
changeset

1018 
quote (Syntax.string_of_typ no_defs_lthy0 (hd bad_args)) ^ " in " ^ co_prefix fp ^ 
8d581fd1b46f
gracefully fail to define polymorphic (co)datatypes in local context
blanchet
parents:
52923
diff
changeset

1019 
"datatype specification"); 
8d581fd1b46f
gracefully fail to define polymorphic (co)datatypes in local context
blanchet
parents:
52923
diff
changeset

1020 

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

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

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

1023 
> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1024 
> mk_TFrees (length unsorted_As) 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

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

1026 
>> variant_tfrees fp_b_names; 
49119  1027 

52962  1028 
(* TODO: Cleaner handling of fake contexts, without "background_theory". *) 
51768  1029 

51769
5c657ca97d99
simplified code  no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
blanchet
parents:
51768
diff
changeset

1030 
fun add_fake_type spec = 
52962  1031 
(*The "qualify" hack below is for the case where the new type shadows an existing global type 
1032 
defined in the same theory.*) 

1033 
Sign.add_type no_defs_lthy (qualify false "" (type_binding_of spec), 

51769
5c657ca97d99
simplified code  no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
blanchet
parents:
51768
diff
changeset

1034 
length (type_args_named_constrained_of spec), mixfix_of spec); 
51768  1035 

52788  1036 
val fake_thy = fold add_fake_type specs; 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1037 
val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy; 
49119  1038 

49182
b8517107ffc5
read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)
blanchet
parents:
49181
diff
changeset

1039 
fun mk_fake_T b = 
49121  1040 
Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))), 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1041 
unsorted_As); 
49121  1042 

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

1043 
val fake_Ts = map mk_fake_T fp_bs; 
49121  1044 

49181  1045 
val mixfixes = map mixfix_of specs; 
49119  1046 

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

1047 
val _ = (case duplicates Binding.eq_name fp_bs of [] => () 
49119  1048 
 b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b))); 
1049 

49121  1050 
val ctr_specss = map ctr_specs_of specs; 
49119  1051 

49336  1052 
val disc_bindingss = map (map disc_of) ctr_specss; 
1053 
val ctr_bindingss = 

49633  1054 
map2 (fn fp_b_name => map (qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss; 
49121  1055 
val ctr_argsss = map (map args_of) ctr_specss; 
49181  1056 
val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss; 
49119  1057 

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

1059 
val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; 
49286  1060 
val raw_sel_defaultsss = map (map defaults_of) ctr_specss; 
1061 

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

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

1063 
burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0); 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1064 

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

1065 
val _ = (case duplicates (op =) unsorted_As of [] => () 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1066 
 A :: _ => error ("Duplicate type parameter " ^ 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1067 
quote (Syntax.string_of_typ no_defs_lthy A))); 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1068 

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

1069 
val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss []; 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1070 
val _ = (case subtract (op =) (map dest_TFree As) rhs_As' of 
49165  1071 
[] => () 
49342  1072 
 A' :: _ => error ("Extra type variable on righthand side: " ^ 
49204  1073 
quote (Syntax.string_of_typ no_defs_lthy (TFree A')))); 
49165  1074 

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

1075 
fun eq_fpT_check (T as Type (s, Us)) (Type (s', Us')) = 
49146  1076 
s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^ 
1077 
quote (Syntax.string_of_typ fake_lthy T))) 

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

1078 
 eq_fpT_check _ _ = false; 
49146  1079 

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

1081 
(case find_index (eq_fpT_check T) fake_Ts of 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

1082 
~1 => Type (s, map freeze_fp Us) 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

1083 
 kk => nth Xs kk) 
49204  1084 
 freeze_fp T = T; 
49121  1085 

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

1086 
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

1087 
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; 
49119  1088 

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

1089 
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

1090 
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts; 
49121  1091 

51839  1092 
val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, 
52344  1093 
xtor_co_iterss = xtor_co_iterss0, xtor_co_inducts, dtor_ctors, ctor_dtors, ctor_injects, 
1094 
xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, lthy)) = 

51868  1095 
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs 
1096 
no_defs_lthy0; 

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

1097 

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

1098 
val timer = time (Timer.startRealTimer ()); 
49121  1099 

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

1100 
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

1101 
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; 
49226  1102 

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

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

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

1105 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
51830  1106 
val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs; 
51766
f19a4d0ab1bf
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet
parents:
51758
diff
changeset

1107 
val nested_set_map's = maps set_map'_of_bnf nested_bnfs; 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1108 

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

1109 
val live = live_of_bnf any_fp_bnf; 
52961  1110 
val _ = 
1111 
if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs) then 

1112 
warning ("Map function and relator names ignored") 

1113 
else 

1114 
(); 

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

1115 

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

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

1117 
map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A) 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

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

1119 

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

1120 
val B_ify = Term.typ_subst_atomic (As ~~ Bs); 
49167  1121 

49501  1122 
val ctors = map (mk_ctor As) ctors0; 
1123 
val dtors = map (mk_dtor As) dtors0; 

49124  1124 

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

1126 

51780  1127 
fun massage_simple_notes base = 
1128 
filter_out (null o #2) 

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

1130 
((qualify true base (Binding.name thmN), attrs), [(thms, [])])); 

1131 

1132 
val massage_multi_notes = 

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

1134 
if forall null thmss then 

1135 
[] 

1136 
else 

1137 
map3 (fn fp_b_name => fn Type (T_name, _) => fn thms => 

52311  1138 
((qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])])) 
1139 
fp_b_names fpTs thmss); 

51780  1140 

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

1141 
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; 
49203  1142 
val ns = map length ctr_Tsss; 
49212  1143 
val kss = map (fn n => 1 upto n) ns; 
49203  1144 
val mss = map (map length) ctr_Tsss; 
1145 

52367  1146 
val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') = 
52334  1147 
mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy; 
49210  1148 

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

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

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

49176  1153 
let 
49498  1154 
val fp_b_name = Binding.name_of fp_b; 
1155 

49501  1156 
val dtorT = domain_type (fastype_of ctor); 
49210  1157 
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

1158 
val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts; 
49119  1159 

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

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

1164 
>> mk_Freess "y" (map (map B_ify) ctr_Tss) 
49498  1165 
>> yield_singleton Variable.variant_fixes fp_b_name; 
49370  1166 

49498  1167 
val u = Free (u', fpT); 
49121  1168 

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

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

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

1171 

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

1173 
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

1174 
mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs; 
49121  1175 

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

1176 
val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy 
49169  1177 
> apfst split_list o fold_map3 (fn b => fn mx => fn rhs => 
49302
f5bd87aac224
added optional qualifiers for constructors and destructors, similarly to the old package
blanchet
parents:
49300
diff
changeset

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

1179 
c 