author  blanchet 
Thu, 06 Jun 2013 15:49:08 +0200  
changeset 52319  37a3b00759dc 
parent 52317  7132de305921 
child 52320  597fcdb7ea64 
permissions  rwrr 
49636  1 
(* Title: HOL/BNF/Tools/bnf_fp_def_sugar.ML 
49112  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2012 

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, 

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

15 
fp_res: BNF_FP_Util.fp_result, 
51906  16 
ctr_defss: thm list list, 
51842  17 
ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, 
51857
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

18 
un_folds: term list, 
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

19 
co_recs: term list, 
51864  20 
co_induct: thm, 
21 
strong_co_induct: thm, 

51857
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

22 
un_fold_thmss: thm list list, 
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

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

24 

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

51852  28 

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

29 
val tvar_subst: theory > typ list > typ list > ((string * int) * typ) list 
51860  30 
val exists_subtype_in: typ list > typ > bool 
52301
7935e82a4ae4
simpler, more robust iterator goal construction code
blanchet
parents:
52300
diff
changeset

31 
val flat_rec: 'a list list > '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 
52207
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

34 
val mk_un_fold_co_rec_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

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

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

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

38 
* term list list list list) list option 
51903  39 
* (term list * term list list 
40 
* ((term list list * term list list list list * term list list list list) 

41 
* (typ list * typ list list list * typ list list)) 

42 
* ((term list list * term list list list list * term list list list list) 

43 
* (typ list * typ list list list * typ list list))) option) 

44 
* Proof.context 

52293  45 
val mk_map: int > typ list > typ list > term > term 
51855  46 
val build_map: local_theory > (typ * typ > term) > typ * typ > term 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

47 

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

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

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

50 
val define_fold_rec: 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

51 
(typ list list * typ list list list list * term list list * term list list list list) list > 
52319  52 
(string > binding) > typ list > typ list > term list > Proof.context > 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

53 
(term * term * thm * thm) * Proof.context 
51902  54 
val define_unfold_corec: term list * term list list 
55 
* ((term list list * term list list list list * term list list list list) 

56 
* (typ list * typ list list list * typ list list)) 

57 
* ((term list list * term list list list list * term list list list list) 

58 
* (typ list * typ list list list * typ list list)) > 

52319  59 
(string > binding) > typ list > typ list > term list > Proof.context > 
51902  60 
(term * term * thm * thm) * Proof.context 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

61 
val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list > term list list > 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

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

63 
thm > thm list list > BNF_Def.bnf list > BNF_Def.bnf list > typ list > typ list > 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

64 
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

65 
thm list list > local_theory > 
51811  66 
(thm * thm list * Args.src list) * (thm list list * Args.src list) 
51827  67 
* (thm list list * Args.src list) 
51837
087498724486
lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
blanchet
parents:
51835
diff
changeset

68 
val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list > term list > term list > 
087498724486
lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
blanchet
parents:
51835
diff
changeset

69 
thm > thm > thm list > thm list > thm list > BNF_Def.bnf list > BNF_Def.bnf list > 
51829  70 
typ list > typ list > typ list > int list list > int list list > int list > 
51840  71 
thm list list > BNF_Ctr_Sugar.ctr_sugar list > term list > term list > thm list > 
51852  72 
thm list > local_theory > 
51839  73 
(thm * thm list * thm * thm list * Args.src list) 
74 
* (thm list list * thm list list * Args.src list) 

51811  75 
* (thm list list * thm list list) * (thm list list * thm list list * Args.src list) 
51824  76 
* (thm list list * thm list list * Args.src list) 
77 
* (thm list list * thm list list * Args.src list) 

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

78 

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

79 
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

80 
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

81 
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

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

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

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

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

49636  92 
structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = 
49112  93 
struct 
94 

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

97 
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

98 
open BNF_FP_Util 
49636  99 
open BNF_FP_Def_Sugar_Tactics 
49119  100 

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

102 

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

105 
fp: fp_kind, 
51838  106 
index: int, 
107 
pre_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, 
51857
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

111 
un_folds: term list, 
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

112 
co_recs: term list, 
51864  113 
co_induct: thm, 
114 
strong_co_induct: thm, 

51857
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

115 
un_fold_thmss: thm list list, 
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

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

117 

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

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

120 
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

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

122 
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

123 

52299  124 
fun morph_fp_sugar phi {T, fp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, un_folds, 
125 
co_recs, co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} = 

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

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

128 
ctr_defss = map (map (Morphism.thm phi)) ctr_defss, 
51906  129 
ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, un_folds = map (Morphism.term phi) un_folds, 
130 
co_recs = map (Morphism.term phi) co_recs, co_induct = Morphism.thm phi co_induct, 

131 
strong_co_induct = Morphism.thm phi strong_co_induct, 

51857
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

132 
un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss, 
17e7f00563fb
tuned names  co_ and un_ with underscore are to be understood as (co) and (un)
blanchet
parents:
51856
diff
changeset

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

134 

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

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

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

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

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

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

142 

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

144 

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

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

148 

52299  149 
fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds co_recs 
150 
co_induct strong_co_induct un_fold_thmss co_rec_thmss lthy = 

51844  151 
(0, lthy) 
51859  152 
> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, 
52299  153 
register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res, 
154 
ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs, 

155 
co_induct = co_induct, strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss, 

51864  156 
co_rec_thmss = co_rec_thmss} lthy)) Ts 
51824  157 
> snd; 
158 

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

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

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

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

164 
fun underscore s = 

165 
let val ss = space_explode Long_Name.separator s in 

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

167 
end; 

168 
in 

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

170 
end; 

171 

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

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

173 

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

175 
val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs; 
49300  176 

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

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

178 
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

179 

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

181 

49342  182 
fun resort_tfree S (TFree (s, _)) = TFree (s, S); 
183 

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

185 
(case AList.lookup (op =) inst T of 
51845  186 
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

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

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

191 

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

192 
fun flat_rec xss = 
7935e82a4ae4
simpler, more robust iterator goal construction code
blanchet
parents:
52300
diff
changeset

193 
(* The first line below gives the preferred order. The second line is for compatibility with the 
7935e82a4ae4
simpler, more robust iterator goal construction code
blanchet
parents:
52300
diff
changeset

194 
old datatype package: *) 
52215
7facaee8586f
tuning (use lists rather than pairs of lists throughout)
blanchet
parents:
52214
diff
changeset

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

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

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

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

199 

51829  200 
fun flat_predss_getterss qss fss = maps (op @) (qss ~~ fss); 
201 

202 
fun flat_preds_predsss_gettersss [] [qss] [fss] = flat_predss_getterss qss fss 

203 
 flat_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) = 

204 
p :: flat_predss_getterss qss fss @ flat_preds_predsss_gettersss ps qsss fsss; 

205 

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

206 
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

207 
fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; 
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

208 
fun mk_uncurried2_fun f xss = 
52301
7935e82a4ae4
simpler, more robust iterator goal construction code
blanchet
parents:
52300
diff
changeset

209 
mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat_rec xss); 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

210 

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

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

212 
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

213 

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

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

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

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

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

218 
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

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

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

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

222 

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

225 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

226 
end; 

227 

228 
val mk_ctor = mk_ctor_or_dtor range_type; 

229 
val mk_dtor = mk_ctor_or_dtor domain_type; 

230 

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

231 
fun mk_co_iter thy fp fpT Cs t = 
49536  232 
let 
52309  233 
val (binders, body) = strip_type (fastype_of t); 
234 
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

235 
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

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

239 
Term.subst_TVars rho t 
49536  240 
end; 
241 

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

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

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

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

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

246 
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

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

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

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

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

251 
end; 
51827  252 

52169  253 
val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of; 
254 

52297  255 
fun project_co_recT special_Tname Cs proj = 
51827  256 
let 
52297  257 
fun project (Type (s, Ts as [T, U])) = 
258 
if s = special_Tname andalso member (op =) Cs U then proj (T, U) 

52209  259 
else Type (s, map project Ts) 
52297  260 
 project (Type (s, Ts)) = Type (s, map project Ts) 
52209  261 
 project T = T; 
262 
in project end; 

263 

264 
val project_corecT = project_co_recT @{type_name sum}; 

265 

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

52216  268 
 unzip_recT _ T = [T]; 
51827  269 

51846  270 
fun mk_fun_arg_typess n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type; 
271 

52296  272 
fun mk_iter_fun_arg_typessss Cs ns mss = 
51885  273 
mk_fp_iter_fun_types 
274 
#> map3 mk_fun_arg_typess ns mss 

52296  275 
#> map (map (map (unzip_recT Cs))); 
51885  276 

52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

277 
fun mk_fold_rec_args_types Cs ns mss [ctor_fold_fun_Ts, ctor_rec_fun_Ts] lthy = 
51832  278 
let 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

279 
val Css = map2 replicate ns Cs; 
51843
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

280 
val y_Tsss = map3 mk_fun_arg_typess ns mss ctor_fold_fun_Ts; 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

281 
val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts > C)) Cs y_Tsss; 
51832  282 

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

284 
lthy 

285 
> mk_Freess "f" g_Tss 

286 
>> mk_Freesss "x" y_Tsss; 

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

287 

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

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

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

290 

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

291 
val z_Tssss = 
52296  292 
map3 (fn n => fn ms => map2 (map (unzip_recT Cs) oo dest_tupleT) ms o 
52214
4cc5a80bba80
generalized recursors, effectively reverting inductive half of c7a034d01936
blanchet
parents:
52213
diff
changeset

293 
dest_sumTN_balanced n o domain_type) ns mss ctor_rec_fun_Ts; 
51832  294 

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

295 
val z_Tsss' = map (map flat_rec) z_Tssss; 
52215
7facaee8586f
tuning (use lists rather than pairs of lists throughout)
blanchet
parents:
52214
diff
changeset

296 
val h_Tss = map2 (map2 (curry (op >))) z_Tsss' Css; 
51832  297 

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

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

299 
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

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

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

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

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

305 
([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy) 
51832  306 
end; 
307 

52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

308 
fun mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy = 
51829  309 
let 
310 
(*avoid "'a itself" arguments in coiterators and corecursors*) 

311 
fun repair_arity [0] = [1] 

312 
 repair_arity ms = ms; 

313 

314 
fun unzip_corecT T = 

52297  315 
if exists_subtype_in Cs T then [project_corecT Cs fst T, project_corecT Cs snd T] 
52209  316 
else [T]; 
51829  317 

51831  318 
val p_Tss = map2 (fn n => replicate (Int.max (0, n  1)) o mk_pred1T) ns Cs; 
51829  319 

320 
fun mk_types maybe_unzipT fun_Ts = 

321 
let 

322 
val f_sum_prod_Ts = map range_type fun_Ts; 

323 
val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; 

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

51889  325 
val f_Tssss = map2 (fn C => map (map (map (curry (op >) C) o maybe_unzipT))) Cs f_Tsss; 
51829  326 
val q_Tssss = 
52213  327 
map (map (map (fn [_] => []  [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss; 
51829  328 
val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; 
51889  329 
in (q_Tssss, f_Tssss, (f_sum_prod_Ts, f_Tsss, pf_Tss)) end; 
51829  330 

51889  331 
val (r_Tssss, g_Tssss, unfold_types) = mk_types single dtor_unfold_fun_Ts; 
332 
val (s_Tssss, h_Tssss, corec_types) = mk_types unzip_corecT dtor_corec_fun_Ts; 

51831  333 

51829  334 
val (((cs, pss), gssss), lthy) = 
335 
lthy 

336 
> mk_Frees "a" Cs 

337 
>> mk_Freess "p" p_Tss 

338 
>> mk_Freessss "g" g_Tssss; 

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

340 

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

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

343 
lthy 

344 
> mk_Freessss "q" s_Tssss 

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

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

51831  347 

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

51829  349 

51889  350 
fun mk_args qssss fssss = 
51831  351 
let 
352 
val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss; 

353 
val cqssss = map2 (map o map o map o rapp) cs qssss; 

354 
val cfssss = map2 (map o map o map o rapp) cs fssss; 

355 
in (pfss, cqssss, cfssss) end; 

356 

51889  357 
val unfold_args = mk_args rssss gssss; 
358 
val corec_args = mk_args sssss hssss; 

51831  359 
in 
51889  360 
((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy) 
51831  361 
end; 
51829  362 

52317  363 
fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy = 
51903  364 
let 
52169  365 
val thy = Proof_Context.theory_of lthy; 
366 

52317  367 
val (xtor_co_iter_fun_Tss, xtor_co_iterss) = 
368 
map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) xtor_co_iterss0 

369 
> split_list; 

51903  370 

371 
val ((fold_rec_args_types, unfold_corec_args_types), lthy') = 

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

372 
if fp = Least_FP then 
52317  373 
mk_fold_rec_args_types Cs ns mss xtor_co_iter_fun_Tss lthy >> (rpair NONE o SOME) 
51903  374 
else 
52317  375 
mk_unfold_corec_args_types Cs ns mss xtor_co_iter_fun_Tss lthy >> (pair NONE o SOME) 
51903  376 
in 
52317  377 
((xtor_co_iterss, fold_rec_args_types, unfold_corec_args_types), lthy') 
51903  378 
end; 
379 

49536  380 
fun mk_map live Ts Us t = 
381 
let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) >> List.last in 

382 
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t 

383 
end; 

384 

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

385 
fun mk_rel live Ts Us t = 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

386 
let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

387 
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

388 
end; 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

389 

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

390 
fun liveness_of_fp_bnf n bnf = 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

391 
(case T_of_bnf bnf of 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

392 
Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

393 
 _ => replicate n false); 
49536  394 

49124  395 
fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; 
49119  396 

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

397 
fun merge_type_arg T T' = if T = T' then T else cannot_merge_types (); 
49119  398 

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

399 
fun merge_type_args (As, As') = 
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

400 
if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types (); 
49119  401 

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

402 
fun reassoc_conjs thm = 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

403 
reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]}) 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

404 
handle THM _ => thm; 
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

405 

51767
bbcdd8519253
honor userspecified name for relator + generalize syntax
blanchet
parents:
51766
diff
changeset

406 
fun type_args_named_constrained_of ((((ncAs, _), _), _), _) = ncAs; 
bbcdd8519253
honor userspecified name for relator + generalize syntax
blanchet
parents:
51766
diff
changeset

407 
fun type_binding_of ((((_, b), _), _), _) = b; 
bbcdd8519253
honor userspecified name for relator + generalize syntax
blanchet
parents:
51766
diff
changeset

408 
fun map_binding_of (((_, (b, _)), _), _) = b; 
bbcdd8519253
honor userspecified name for relator + generalize syntax
blanchet
parents:
51766
diff
changeset

409 
fun rel_binding_of (((_, (_, b)), _), _) = b; 
49181  410 
fun mixfix_of ((_, mx), _) = mx; 
49121  411 
fun ctr_specs_of (_, ctr_specs) = ctr_specs; 
49119  412 

49286  413 
fun disc_of ((((disc, _), _), _), _) = disc; 
414 
fun ctr_of ((((_, ctr), _), _), _) = ctr; 

415 
fun args_of (((_, args), _), _) = args; 

416 
fun defaults_of ((_, ds), _) = ds; 

49181  417 
fun ctr_mixfix_of (_, mx) = mx; 
49119  418 

51907  419 
fun add_nesty_bnf_names Us = 
420 
let 

421 
fun add (Type (s, Ts)) ss = 

422 
let val (needs, ss') = fold_map add Ts ss in 

423 
if exists I needs then (true, insert (op =) s ss') else (false, ss') 

424 
end 

425 
 add T ss = (member (op =) Us T, ss); 

426 
in snd oo add end; 

427 

428 
fun nesty_bnfs ctxt ctr_Tsss Us = 

429 
map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []); 

430 

52302  431 
fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p; 
51855  432 

51854  433 
fun build_map lthy build_simple = 
51853  434 
let 
435 
fun build (TU as (T, U)) = 

436 
if T = U then 

437 
id_const T 

438 
else 

439 
(case TU of 

51854  440 
(Type (s, Ts), Type (s', Us)) => 
441 
if s = s' then 

442 
let 

443 
val bnf = the (bnf_of lthy s); 

444 
val live = live_of_bnf bnf; 

445 
val mapx = mk_map live Ts Us (map_of_bnf bnf); 

446 
val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx))); 

447 
in Term.list_comb (mapx, map build TUs') end 

448 
else 

449 
build_simple TU 

51853  450 
 _ => build_simple TU); 
451 
in build end; 

452 

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

51884  455 

51900  456 
fun mk_preds_getterss_join c cps sum_prod_T cqfss = 
457 
let val n = length cqfss in 

458 
Term.lambda c (mk_IfN sum_prod_T cps 

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

460 
end; 

51886  461 

51900  462 
fun mk_coiter_body lthy cs cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter = 
51888  463 
let 
464 
fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd); 

465 

466 
fun build_dtor_coiter_arg _ [] [cf] = cf 

467 
 build_dtor_coiter_arg T [cq] [cf, cf'] = 

468 
mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf) 

469 
(build_sum_inj Inr_const (fastype_of cf', T) $ cf') 

470 

471 
val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; 

472 
in 

51900  473 
Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss) 
51888  474 
end; 
51886  475 

52319  476 
fun define_fold_rec [fold_args_types, rec_args_types] mk_binding fpTs Cs [ctor_fold, ctor_rec] 
477 
lthy0 = 

51897  478 
let 
52170
564be617ae84
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet
parents:
52169
diff
changeset

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

480 

51899  481 
val nn = length fpTs; 
482 

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

483 
val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of ctor_fold)); 
51897  484 

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

485 
fun generate_iter (suf, ctor_iter, (f_Tss, _, fss, xssss)) = 
51897  486 
let 
51899  487 
val res_T = fold_rev (curry (op >)) f_Tss fpT_to_C; 
52309  488 
val b = mk_binding suf; 
51897  489 
val spec = 
52309  490 
mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)), 
52298  491 
mk_iter_body ctor_iter fss xssss); 
52309  492 
in (b, spec) end; 
51897  493 

494 
val binding_specs = 

52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

495 
map generate_iter [(foldN, ctor_fold, fold_args_types), (recN, ctor_rec, rec_args_types)]; 
51897  496 

51907  497 
val ((csts, defs), (lthy', lthy)) = lthy0 
51897  498 
> apfst split_list o fold_map (fn (b, spec) => 
499 
Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) 

500 
#>> apsnd snd) binding_specs 

501 
> `Local_Theory.restore; 

502 

503 
val phi = Proof_Context.export_morphism lthy lthy'; 

504 

505 
val [fold_def, rec_def] = map (Morphism.thm phi) defs; 

506 

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

507 
val [foldx, recx] = map (mk_co_iter thy Least_FP fpT Cs o Morphism.term phi) csts; 
51897  508 
in 
509 
((foldx, recx, fold_def, rec_def), lthy') 

510 
end; 

511 

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

512 
(* TODO: merge with above function? *) 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

513 
fun define_unfold_corec (cs, cpss, unfold_args_types, corec_args_types) mk_binding fpTs Cs 
52319  514 
[dtor_unfold, dtor_corec] lthy0 = 
51897  515 
let 
52170
564be617ae84
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet
parents:
52169
diff
changeset

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

517 

51899  518 
val nn = length fpTs; 
519 

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

520 
val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of dtor_unfold)); 
51897  521 

522 
fun generate_coiter (suf, dtor_coiter, ((pfss, cqssss, cfssss), 

523 
(f_sum_prod_Ts, f_Tsss, pf_Tss))) = 

524 
let 

51899  525 
val res_T = fold_rev (curry (op >)) pf_Tss C_to_fpT; 
52309  526 
val b = mk_binding suf; 
51897  527 
val spec = 
52309  528 
mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)), 
51907  529 
mk_coiter_body lthy0 cs cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter); 
52309  530 
in (b, spec) end; 
51897  531 

532 
val binding_specs = 

52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

533 
map generate_coiter [(unfoldN, dtor_unfold, unfold_args_types), 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

534 
(corecN, dtor_corec, corec_args_types)]; 
51897  535 

51907  536 
val ((csts, defs), (lthy', lthy)) = lthy0 
51897  537 
> apfst split_list o fold_map (fn (b, spec) => 
538 
Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) 

539 
#>> apsnd snd) binding_specs 

540 
> `Local_Theory.restore; 

541 

542 
val phi = Proof_Context.export_morphism lthy lthy'; 

543 

544 
val [unfold_def, corec_def] = map (Morphism.thm phi) defs; 

545 

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

546 
val [unfold, corec] = map (mk_co_iter thy Greatest_FP fpT Cs o Morphism.term phi) csts; 
51897  547 
in 
548 
((unfold, corec, unfold_def, corec_def), lthy') 

52172  549 
end ; 
51897  550 

52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

551 
fun derive_induct_fold_rec_thms_for_types pre_bnfs [ctor_folds, ctor_recs] 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

552 
[fold_args_types, rec_args_types] ctor_induct [ctor_fold_thms, ctor_rec_thms] nesting_bnfs 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

553 
nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss [folds, recs] [fold_defs, rec_defs] lthy = 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

554 
let 
51827  555 
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; 
556 

51815  557 
val nn = length pre_bnfs; 
51827  558 
val ns = map length ctr_Tsss; 
559 
val mss = map (map length) ctr_Tsss; 

51815  560 

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

561 
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

562 
val pre_set_defss = map set_defs_of_bnf pre_bnfs; 
51830  563 
val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_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

564 
val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

565 
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

566 

51816  567 
val fp_b_names = map base_name_of_typ fpTs; 
51811  568 

52171  569 
val ctor_fold_fun_Ts = mk_fp_iter_fun_types (hd ctor_folds); 
570 
val ctor_rec_fun_Ts = mk_fp_iter_fun_types (hd ctor_recs); 

51827  571 

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

573 
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

574 
> mk_Frees' "P" (map mk_pred1T fpTs) 
51827  575 
>> mk_Freesss "x" ctr_Tsss 
51816  576 
>> 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

577 

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

578 
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

579 

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

580 
fun mk_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

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

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

583 
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

584 
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

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

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

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

588 
 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

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

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

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

592 

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

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

594 

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

595 
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

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

597 
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

598 
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

599 
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

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

601 

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

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

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

604 
 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

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

606 
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

607 
 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

608 
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

609 
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

610 
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

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

612 
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

613 
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

614 
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

615 
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

616 
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

617 
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

618 
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

619 
 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

620 

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

621 
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

622 
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

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

624 

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

625 
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

626 
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

627 
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

628 
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

629 

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

630 
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

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

632 
val (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

633 
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

634 
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

635 

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

636 
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

637 
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

638 

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

640 

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

641 
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

642 
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (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

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

644 

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

645 
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

646 

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

648 

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

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

650 
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

651 
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

652 
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

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

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

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

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

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

658 

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

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

661 

52305  662 
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; 
663 

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

665 
let 
52305  666 
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

667 

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

668 
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

669 
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

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

671 

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

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

675 
else 

676 
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

677 

52305  678 
fun unzip_iters (x as Free (_, T)) = 
52301
7935e82a4ae4
simpler, more robust iterator goal construction code
blanchet
parents:
52300
diff
changeset

679 
map (fn U => if U = T then x 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

680 
build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs 
52305  681 
(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

682 

52305  683 
val fxsss = map2 (map2 (flat_rec oo map2 unzip_iters)) 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

684 

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

686 

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

689 
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

690 

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

691 
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

692 
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

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

694 
in 
52305  695 
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

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

697 

52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

698 
val fold_thmss = mk_iter_thmss fold_args_types folds fold_defs ctor_fold_thms; 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

699 
val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs ctor_rec_thms; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

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

701 
((induct_thm, induct_thms, [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

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

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

704 

52171  705 
fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs dtor_unfolds dtor_corecs dtor_coinduct 
51814  706 
dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs 
51840  707 
As kss mss ns ctr_defss ctr_sugars unfolds corecs unfold_defs corec_defs lthy = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

708 
let 
51815  709 
val nn = length pre_bnfs; 
710 

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

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

712 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
51830  713 
val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs; 
714 
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

715 
val nested_map_comp's = map map_comp'_of_bnf nested_bnfs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

716 
val nested_map_comps'' = map ((fn thm => thm RS sym) o map_comp_of_bnf) nested_bnfs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

717 
val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

718 

51816  719 
val fp_b_names = map base_name_of_typ fpTs; 
51811  720 

52171  721 
val dtor_unfold_fun_Ts = mk_fp_iter_fun_types (hd dtor_unfolds); 
722 
val dtor_corec_fun_Ts = mk_fp_iter_fun_types (hd dtor_corecs); 

51829  723 

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

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

727 
val exhausts = map #exhaust ctr_sugars; 

728 
val disc_thmsss = map #disc_thmss ctr_sugars; 

729 
val discIss = map #discIs ctr_sugars; 

730 
val sel_thmsss = map #sel_thmss ctr_sugars; 

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

731 

51831  732 
val ((cs, cpss, ((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)), names_lthy0) = 
52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

733 
mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy; 
51831  734 

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

735 
val (((rs, us'), vs'), names_lthy) = 
51831  736 
names_lthy0 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

737 
> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) 
51816  738 
>> Variable.variant_fixes fp_b_names 
739 
>> Variable.variant_fixes (map (suffix "'") fp_b_names); 

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

740 

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

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

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

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

744 

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

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

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

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

748 

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

749 
val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

751 
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

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

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

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

755 
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

756 

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

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

758 
(case find_index (curry (op =) T) fpTs of 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

759 
~1 => 
51856  760 
if exists_subtype_in fpTs T then 
761 
let 

762 
val Type (s, Ts) = T 

763 
val bnf = the (bnf_of lthy s); 

764 
val live = live_of_bnf bnf; 

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

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

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

768 
else 

769 
HOLogic.eq_const T 

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

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

771 

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

773 

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

774 
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

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

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

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

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

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

780 
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

781 

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

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

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

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

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

786 

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

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

788 
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

789 
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

790 

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

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

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

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

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

795 

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

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

797 
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

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

799 

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

800 
val goal = mk_goal rs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

801 
val strong_goal = mk_goal strong_rs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

802 

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

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

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

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

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

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

809 

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

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

811 
Thm.permute_prems 0 nn 
51828  812 
(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

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

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

815 
in 
51814  816 
(postproc nn (prove dtor_coinduct goal), postproc nn (prove dtor_strong_induct strong_goal)) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

818 

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

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

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

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

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

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

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

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

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

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

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

829 

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

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

832 
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

833 

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

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

835 

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

836 
val gunfolds = map (lists_bmoc pgss) unfolds; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

837 
val hcorecs = map (lists_bmoc phss) corecs; 
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 
val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

841 
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

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

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

844 
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

845 

51845  846 
val mk_U = typ_subst_nonatomic (map2 pair Cs fpTs); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

847 

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

848 
fun intr_coiters fcoiters [] [cf] = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

849 
let val T = fastype_of cf in 
51855  850 
if exists_subtype_in Cs T then 
52302  851 
build_map lthy (indexify fst Cs (K o nth fcoiters)) (T, mk_U T) $ cf 
51855  852 
else 
853 
cf 

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

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

855 
 intr_coiters fcoiters [cq] [cf, cf'] = 
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

856 
mk_If cq (intr_coiters fcoiters [] [cf]) (intr_coiters fcoiters [] [cf']); 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

857 

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

858 
val crgsss = map2 (map2 (map2 (intr_coiters gunfolds))) crssss cgssss; 
899663644482
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
blanchet
parents:
51842
diff
changeset

859 
val cshsss = map2 (map2 (map2 (intr_coiters hcorecs))) csssss chssss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

860 

51828  861 
val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss; 
862 
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

863 

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

864 
fun mk_map_if_distrib bnf = 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

866 
val mapx = map_of_bnf bnf; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

867 
val live = live_of_bnf bnf; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

868 
val ((Ts, T), U) = strip_typeN (live + 1) (fastype_of mapx) >> split_last; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

869 
val fs = Variable.variant_frees lthy [mapx] (map (pair "f") Ts); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

870 
val t = Term.list_comb (mapx, map (Var o apfst (rpair 0)) fs); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

872 
Drule.instantiate' (map (SOME o certifyT lthy) [U, T]) [SOME (certify lthy t)] 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

873 
@{thm if_distrib} 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

875 

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

876 
val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

877 

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

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

879 
map3 (map oo mk_coiter_tac unfold_defs [] [] nesting_map_ids'' []) 
51814  880 
dtor_unfold_thms pre_map_defs ctr_defss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

882 
map3 (map oo mk_coiter_tac corec_defs nested_map_comps'' nested_map_comp's 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

883 
(nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs) 
51814  884 
dtor_corec_thms pre_map_defs ctr_defss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

885 

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

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

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

889 

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

890 
val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

891 
val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

892 

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

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

894 
map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

895 
curry (op ~~)) (map2 (map2 (map2 (member (op =)))) cgssss crgsss); 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

896 

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

897 
val safe_unfold_thmss = filter_safesss unfold_thmss; 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

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

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

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

902 

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

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

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

905 
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

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

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

908 
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

909 

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

910 
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

911 
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

912 

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

914 

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

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

916 

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

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

918 
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

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

920 
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

921 

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

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

923 
Goal.prove_sorry lthy [] [] goal (tac o #context) 
51829  924 
> singleton (Proof_Context.export names_lthy lthy) 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

926 

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

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

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

929 
in 
51828  930 
(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

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

932 

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

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

934 

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

935 
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

936 
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

937 

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

938 
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

939 
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

940 

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

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

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

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

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

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

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

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

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

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

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

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

952 

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

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

954 
map3 (map3 (map2 o mk_sel_coiter_thm)) coiterss selsss sel_thmsss > map flat; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

955 

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

956 
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

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

958 

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

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

960 
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

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

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

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

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

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

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

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

968 
((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms, coinduct_case_attrs), 
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

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

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

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

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

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

975 

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

976 
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp 
49633  977 
(wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 = 
49112  978 
let 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

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

980 

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

981 
val _ = if fp = Greatest_FP andalso no_dests then 
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

982 
error "Cannot define destructorless codatatypes" 
21026c312cc3
tuning  avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52197
diff
changeset

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

984 
(); 
49278  985 

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

988 

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

990 
val fp_bs = map type_binding_of specs; 
49498  991 
val fp_b_names = map Binding.name_of fp_bs; 
992 
val fp_common_name = mk_common_name fp_b_names; 

51758  993 
val map_bs = map map_binding_of specs; 
51767
bbcdd8519253
honor userspecified name for relator + generalize syntax
blanchet
parents:
51766
diff
changeset

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

995 

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

997 
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

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

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

1000 

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

1002 
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

1003 
val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0; 
51758  1004 
val set_bss = map (map fst o type_args_named_constrained_of) specs; 
49119  1005 

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

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

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

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

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

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

1011 
>> variant_tfrees fp_b_names; 
49119  1012 

52195  1013 
(* TODO: Cleaner handling of fake contexts, without "background_theory". The case where the new 
1014 
type is defined in a locale and shadows an existing global type is currently not handled. *) 

51768  1015 

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

1016 
fun add_fake_type spec = 
51768  1017 
Sign.add_type no_defs_lthy (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

1018 
length (type_args_named_constrained_of spec), mixfix_of spec); 
51768  1019 

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

1020 
val fake_thy = Theory.copy #> fold add_fake_type specs; 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

1021 
val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy; 
49119  1022 

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

1023 
fun mk_fake_T b = 
49121  1024 
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

1025 
unsorted_As); 
49121  1026 

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

1027 
val fake_Ts = map mk_fake_T fp_bs; 
49121  1028 

49181  1029 
val mixfixes = map mixfix_of specs; 
49119  1030 

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

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

49121  1034 
val ctr_specss = map ctr_specs_of specs; 
49119  1035 

49336  1036 
val disc_bindingss = map (map disc_of) ctr_specss; 
1037 
val ctr_bindingss = 

49633  1038 
map2 (fn fp_b_name => map (qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss; 
49121  1039 
val ctr_argsss = map (map args_of) ctr_specss; 
49181  1040 
val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss; 
49119  1041 

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

1043 
val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; 
49286  1044 
val raw_sel_defaultsss = map (map defaults_of) ctr_specss; 
1045 

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

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

1047 
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

1048 

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

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

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

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

1052 

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

1053 
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

1054 
val _ = (case subtract (op =) (map dest_TFree As) rhs_As' of 
49165  1055 
[] => () 
49342  1056 
 A' :: _ => error ("Extra type variable on righthand side: " ^ 
49204  1057 
quote (Syntax.string_of_typ no_defs_lthy (TFree A')))); 
49165  1058 

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

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

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

1062 
 eq_fpT_check _ _ = false; 
49146  1063 

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

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

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

1067 
 kk => nth Xs kk) 
49204  1068 
 freeze_fp T = T; 
49121  1069 

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

1070 
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

1071 
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; 
49119  1072 

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

1073 
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

1074 
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts; 
49121  1075 

51839  1076 
val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, 
52313  1077 
xtor_un_folds = xtor_un_folds0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, 
52314  1078 
xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, 
1079 
xtor_set_thmss, xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms, ...}, lthy)) = 

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

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

1082 

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

1083 
val timer = time (Timer.startRealTimer ()); 
49121  1084 

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

1085 
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

1086 
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; 
49226  1087 

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

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

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

1090 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
51830  1091 
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

1092 
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

1093 

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

1094 
val live = live_of_bnf any_fp_bnf; 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1095 

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

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

1097 
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

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

1099 

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

1100 
val B_ify = Term.typ_subst_atomic (As ~~ Bs); 
49167  1101 

49501  1102 
val ctors = map (mk_ctor As) ctors0; 
1103 
val dtors = map (mk_dtor As) dtors0; 

49124  1104 

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

1106 

51780  1107 
fun massage_simple_notes base = 
1108 
filter_out (null o #2) 

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

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

1111 

1112 
val massage_multi_notes = 

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

1114 
if forall null thmss then 

1115 
[] 

1116 
else 

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

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

51780  1120 

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

1121 
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; 
49203  1122 
val ns = map length ctr_Tsss; 
49212  1123 
val kss = map (fn n => 1 upto n) ns; 
49203  1124 
val mss = map (map length) ctr_Tsss; 
1125 

52315
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

1126 
val (([xtor_un_folds, xtor_co_recs], fold_rec_args_types, unfold_corec_args_types), lthy) = 
fafab8eac3ee
avoid duplicate call to "mk_fold_rec_args_types" function
blanchet
parents:
52314
diff
changeset

1127 
mk_un_fold_co_rec_prelims fp fpTs Cs ns mss [xtor_un_folds0, xtor_co_recs0] lthy; 
49210  1128 

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

1129 
fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor), 
52313  1130 
xtor_un_fold), xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), 
1131 
pre_set_defs), pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), 

1132 
ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) 

1133 
no_defs_lthy = 

49176  1134 
let 
49498  1135 
val fp_b_name = Binding.name_of fp_b; 
1136 

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

1139 
val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts; 
49134
846264f80f16
optionally provide extra dead variables to the FP constructions
blanchet
parents:
49130
diff
changeset

1140 
val case_Ts = map (fn Ts => Ts > C) ctr_Tss; 
49119  1141 

49593  1142 
val (((((w, fs), xss), yss), u'), names_lthy) = 
49204  1143 
no_defs_lthy 
49501  1144 
> yield_singleton (mk_Frees "w") dtorT 
49176  1145 
>> mk_Frees "f" case_Ts 
49370  1146 
>> mk_Freess "x" ctr_Tss 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1147 
>> mk_Freess "y" (map (map B_ify) ctr_Tss) 
49498  1148 
>> yield_singleton Variable.variant_fixes fp_b_name; 
49370  1149 

49498  1150 
val u = Free (u', fpT); 
49121  1151 

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

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

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

1154 

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

1156 
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

1157 
mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs; 
49121  1158 

49633  1159 
val case_binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ caseN) fp_b); 
49129  1160 

49134
846264f80f16
optionally provide extra dead variables to the FP constructions
blanchet
parents:
49130
diff
changeset

1161 
val case_rhs = 
49498  1162 
fold_rev Term.lambda (fs @ [u]) 
49501  1163 
(mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (dtor $ u)); 
49129  1164 

49201  1165 
val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy 
49169  1166 
> 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

1167 
Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd) 
49336  1168 
(case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss) 
49121  1169 
> `Local_Theory.restore; 
1170 

1171 
val phi = Proof_Context.export_morphism lthy lthy'; 

1172 

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

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

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

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

1176 
val case_def = Morphism.thm phi raw_case_def; 
3c26e17b2849
implemented "mk_case_tac"  and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset

1177 

49203  1178 
val ctrs0 = map (Morphism.term phi) raw_ctrs; 
1179 
val casex0 = Morphism.term phi raw_case; 

1180 

1181 
val ctrs = map (mk_ctr As) ctrs0; 

49121  1182 

51897  1183 
fun wrap_ctrs lthy = 
49123 