author  blanchet 
Wed, 09 Jul 2014 11:54:01 +0200  
changeset 57535  9b99b773acd4 
parent 57525  f9dd8a33f820 
child 57558  6bb3dd7f8097 
permissions  rwrr 
55061  1 
(* Title: HOL/Tools/BNF/bnf_fp_def_sugar.ML 
49112  2 
Author: Jasmin Blanchette, TU Muenchen 
52349  3 
Copyright 2012, 2013 
49112  4 

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

49636  8 
signature BNF_FP_DEF_SUGAR = 
49112  9 
sig 
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56648
diff
changeset

10 
val fp_sugar_of: Proof.context > string > BNF_FP_Util.fp_sugar option 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56648
diff
changeset

11 
val fp_sugars_of: Proof.context > BNF_FP_Util.fp_sugar list 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56648
diff
changeset

12 
val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list > theory > theory) > theory > theory 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56648
diff
changeset

13 
val register_fp_sugars: BNF_FP_Util.fp_sugar list > local_theory > local_theory 
51852  14 

53106  15 
val co_induct_of: 'a list > 'a 
16 
val strong_co_induct_of: 'a list > 'a 

17 

52868  18 
val flat_corec_preds_predsss_gettersss: 'a list > 'a list list list > 'a list list list > 
19 
'a list 

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

21 

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

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

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

24 

54256  25 
val morph_lfp_sugar_thms: morphism > lfp_sugar_thms > lfp_sugar_thms 
26 
val transfer_lfp_sugar_thms: Proof.context > lfp_sugar_thms > lfp_sugar_thms 

27 

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

28 
type gfp_sugar_thms = 
57260
8747af0d1012
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
blanchet
parents:
57206
diff
changeset

29 
((thm list * thm) list * (Args.src list * Args.src list)) 
57489  30 
* thm list list 
31 
* thm list list 

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

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

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

34 

54256  35 
val morph_gfp_sugar_thms: morphism > gfp_sugar_thms > gfp_sugar_thms 
36 
val transfer_gfp_sugar_thms: Proof.context > gfp_sugar_thms > gfp_sugar_thms 

37 

55867  38 
val mk_co_recs_prelims: BNF_Util.fp_kind > typ list list list > typ list > typ list > 
39 
typ list > typ list > int list > int list list > term list > Proof.context > 

40 
(term list 

41 
* (typ list list * typ list list list list * term list list * term list list list list) option 

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

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

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

45 
val repair_nullary_single_ctr: typ list list > typ list list 
55867  46 
val mk_corec_p_pred_types: typ list > int list > typ list list 
47 
val mk_corec_fun_arg_types: typ list list list > typ list > typ list > typ list > int list > 

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

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

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

50 
* (typ list list list list * typ list list list * typ list list list list * typ list) 
55867  51 
val define_rec: 
56641
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

52 
typ list list * typ list list list list * term list list * term list list list list > 
55862
b458558cbcc2
optimized simple nonrecursive datatypes by reusing 'case' for 'rec' constant
blanchet
parents:
55861
diff
changeset

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

56 
* ((term list list * term list list list) * typ list) > (string > binding) > 'b list > 
56347
6edbd4d20717
added newstyle (co)datatype interpretation hook
blanchet
parents:
56254
diff
changeset

57 
typ list > term list > term > local_theory > (term * thm) * local_theory 
55867  58 
val derive_induct_recs_thms_for_types: BNF_Def.bnf list > 
59 
('a * typ list list list list * term list list * 'b) option > thm > thm list > 

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

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

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

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

66 
typ list > typ list list list > int list list > int list list > int list > thm list > 
55864  67 
thm list > (thm > thm) > thm list list > Ctr_Sugar.ctr_sugar list > term list > 
56347
6edbd4d20717
added newstyle (co)datatype interpretation hook
blanchet
parents:
56254
diff
changeset

68 
thm list > (thm list > thm list) > Proof.context > gfp_sugar_thms 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

69 

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

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

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

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

73 
BNF_FP_Util.fp_result * local_theory) > 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57199
diff
changeset

74 
(bool * bool) 
57206
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57205
diff
changeset

75 
* ((((((binding option * (typ * sort)) list * binding) * mixfix) 
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57205
diff
changeset

76 
* ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * (binding * binding)) 
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57205
diff
changeset

77 
* term list) list > 
49297  78 
local_theory > local_theory 
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset

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

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

82 
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

83 
(local_theory > local_theory) parser 
49112  84 
end; 
85 

49636  86 
structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = 
49112  87 
struct 
88 

54006  89 
open Ctr_Sugar 
55571  90 
open BNF_FP_Rec_Sugar_Util 
49119  91 
open BNF_Util 
53222  92 
open BNF_Comp 
49214
2a3cb4c71b87
construct the right iterator theorem in the recursive case
blanchet
parents:
49213
diff
changeset

93 
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

94 
open BNF_FP_Util 
49636  95 
open BNF_FP_Def_Sugar_Tactics 
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56648
diff
changeset

96 
open BNF_LFP_Size 
49119  97 

51788  98 
val EqN = "Eq_"; 
57489  99 

100 
val corec_codeN = "corec_code"; 

57046
b3613d7e108b
generate 'sel_map[simp]' theorem for (co)datatypes and tuning 'disc_map_iff'
desharna
parents:
56991
diff
changeset

101 
val disc_map_iffN = "disc_map_iff"; 
b3613d7e108b
generate 'sel_map[simp]' theorem for (co)datatypes and tuning 'disc_map_iff'
desharna
parents:
56991
diff
changeset

102 
val sel_mapN = "sel_map"; 
57152  103 
val sel_setN = "sel_set"; 
56956  104 
val set_emptyN = "set_empty"; 
51777
48a0ae342ea0
generate proper attributes for coinduction rules
blanchet
parents:
51769
diff
changeset

105 

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

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

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

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

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

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

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

113 

57525  114 
fun choose_relator Rs AB = find_first 
115 
(fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) Rs; 

116 

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

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

118 
Symtab.lookup (Data.get (Context.Proof ctxt)) 
53907  119 
#> Option.map (transfer_fp_sugar ctxt); 
120 

121 
fun fp_sugars_of ctxt = 

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

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

123 

53106  124 
fun co_induct_of (i :: _) = i; 
125 
fun strong_co_induct_of [_, s] = s; 

126 

56347
6edbd4d20717
added newstyle (co)datatype interpretation hook
blanchet
parents:
56254
diff
changeset

127 
structure FP_Sugar_Interpretation = Interpretation 
6edbd4d20717
added newstyle (co)datatype interpretation hook
blanchet
parents:
56254
diff
changeset

128 
( 
56637
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

129 
type T = fp_sugar list; 
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

130 
val eq: T * T > bool = op = o pairself (map #T); 
56347
6edbd4d20717
added newstyle (co)datatype interpretation hook
blanchet
parents:
56254
diff
changeset

131 
); 
6edbd4d20717
added newstyle (co)datatype interpretation hook
blanchet
parents:
56254
diff
changeset

132 

56648
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

133 
fun with_repaired_path f (fp_sugars as ({T = Type (s, _), ...} : fp_sugar) :: _) thy = 
56376
5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56347
diff
changeset

134 
thy 
56767  135 
> Sign.root_path 
136 
> Sign.add_path (Long_Name.qualifier s) 

56637
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

137 
> f fp_sugars 
56767  138 
> Sign.restore_naming thy; 
56376
5a93b8f928a2
added same idiomatic handling of namings for Ctr_Sugar/BNFrelated interpretation hooks as for typedef and (oldstyle) datatypes
blanchet
parents:
56347
diff
changeset

139 

56657  140 
fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f); 
56347
6edbd4d20717
added newstyle (co)datatype interpretation hook
blanchet
parents:
56254
diff
changeset

141 

56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56648
diff
changeset

142 
fun register_fp_sugars (fp_sugars as {fp, ...} :: _) = 
56648
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

143 
fold (fn fp_sugar as {T = Type (s, _), ...} => 
56637
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

144 
Local_Theory.declaration {syntax = false, pervasive = true} 
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

145 
(fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar)))) 
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

146 
fp_sugars 
56651  147 
#> fp = Least_FP ? generate_lfp_size fp_sugars 
56637
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

148 
#> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars); 
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset

149 

57397  150 
fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res 
56648
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

151 
ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss 
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

152 
co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss = 
56637
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

153 
let 
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

154 
val fp_sugars = 
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

155 
map_index (fn (kk, T) => 
56648
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

156 
{T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, 
57397  157 
pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, 
158 
fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, 

159 
ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, 

160 
co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk, 

161 
common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, 

162 
co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk, 

163 
sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk, 

164 
rel_distincts = nth rel_distinctss kk}) Ts 

56637
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

165 
in 
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

166 
register_fp_sugars fp_sugars 
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

167 
end; 
51824  168 

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

49622  171 
fun quasi_unambiguous_case_names names = 
172 
let 

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

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

175 
fun underscore s = 

176 
let val ss = space_explode Long_Name.separator s in 

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

178 
end; 

179 
in 

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

181 
end; 

182 

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

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

184 

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

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

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

187 
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; 
49300  188 
val simp_attrs = @{attributes [simp]}; 
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 

55871  192 
fun flat_corec_predss_getterss qss gss = maps (op @) (qss ~~ gss); 
51829  193 

55871  194 
fun flat_corec_preds_predsss_gettersss [] [qss] [gss] = flat_corec_predss_getterss qss gss 
195 
 flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (gss :: gsss) = 

196 
p :: flat_corec_predss_getterss qss gss @ flat_corec_preds_predsss_gettersss ps qsss gsss; 

51829  197 

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

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

199 
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

200 

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

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

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

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

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

205 
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

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

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

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

209 

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

212 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

213 
end; 

214 

215 
val mk_ctor = mk_ctor_or_dtor range_type; 

216 
val mk_dtor = mk_ctor_or_dtor domain_type; 

217 

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

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

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

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

222 
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

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

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

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

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

227 
end; 
51827  228 

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

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

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

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

232 

53591  233 
fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] 
53901  234 
 unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts 
52871  235 
 unzip_corecT _ T = [T]; 
236 

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

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

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

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

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

241 

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

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

244 

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

246 

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

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

249 

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

250 
fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs; 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57199
diff
changeset

251 
fun type_binding_of_spec (((((_, b), _), _), _), _) = b; 
57206
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57205
diff
changeset

252 
fun mixfix_of_spec ((((_, mx), _), _), _) = mx; 
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57205
diff
changeset

253 
fun mixfixed_ctr_specs_of_spec (((_, mx_ctr_specs), _), _) = mx_ctr_specs; 
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57205
diff
changeset

254 
fun map_binding_of_spec ((_, (b, _)), _) = b; 
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57205
diff
changeset

255 
fun rel_binding_of_spec ((_, (_, b)), _) = b; 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57199
diff
changeset

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

257 

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

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

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

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

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

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

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

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

266 

57397  267 
fun nesting_bnfs ctxt ctr_Tsss Us = 
268 
map_filter (bnf_of ctxt) (fold (fold (fold (add_nesting_bnf_names Us))) ctr_Tsss []); 

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

269 

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

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

271 

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

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

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

274 

55867  275 
fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) = 
54256  276 
((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs), 
55867  277 
(map (map (Morphism.thm phi)) recss, rec_attrs)) 
55095  278 
: lfp_sugar_thms; 
54256  279 

280 
val transfer_lfp_sugar_thms = 

54740  281 
morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; 
54256  282 

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

283 
type gfp_sugar_thms = 
57260
8747af0d1012
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
blanchet
parents:
57206
diff
changeset

284 
((thm list * thm) list * (Args.src list * Args.src list)) 
57489  285 
* thm list list 
286 
* thm list list 

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

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

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

289 

57260
8747af0d1012
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
blanchet
parents:
57206
diff
changeset

290 
fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair), 
57489  291 
corecss, disc_corecss, (disc_corec_iffss, disc_corec_iff_attrs), 
292 
(sel_corecsss, sel_corec_attrs)) = 

54256  293 
((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, 
57260
8747af0d1012
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
blanchet
parents:
57206
diff
changeset

294 
coinduct_attrs_pair), 
57489  295 
map (map (Morphism.thm phi)) corecss, 
296 
map (map (Morphism.thm phi)) disc_corecss, 

55871  297 
(map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs), 
298 
(map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms; 

54256  299 

300 
val transfer_gfp_sugar_thms = 

54740  301 
morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; 
54256  302 

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

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

308 
map2 (map2 unzip_recT) 
55867  309 
ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T))) 
310 
absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts; 

51832  311 

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

51832  314 

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

316 
lthy 
55869  317 
> mk_Freess "f" f_Tss 
318 
>> mk_Freessss "x" x_Tssss; 

51832  319 
in 
55869  320 
((f_Tss, x_Tssss, fss, xssss), lthy) 
51832  321 
end; 
322 

55867  323 
(*avoid "'a itself" arguments in corecursors*) 
55966  324 
fun repair_nullary_single_ctr [[]] = [[HOLogic.unitT]] 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55701
diff
changeset

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

326 

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

329 
val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss; 
55869  330 
val g_absTs = map range_type fun_Ts; 
331 
val g_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss g_absTs); 

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

333 
Cs ctr_Tsss' g_Tsss; 

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

52870  335 
in 
55869  336 
(q_Tssss, g_Tsss, g_Tssss, g_absTs) 
52870  337 
end; 
51829  338 

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

55867  341 
fun mk_corec_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_corec = 
342 
(mk_corec_p_pred_types Cs ns, 

343 
mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss 

344 
(binder_fun_types (fastype_of dtor_corec))); 

51829  345 

55867  346 
fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy = 
347 
let 

348 
val p_Tss = mk_corec_p_pred_types Cs ns; 

51829  349 

55869  350 
val (q_Tssss, g_Tsss, g_Tssss, corec_types) = 
55867  351 
mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts; 
51831  352 

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

356 
>> mk_Frees "a" Cs 
51829  357 
>> mk_Freess "p" p_Tss 
55869  358 
>> mk_Freessss "q" q_Tssss 
359 
>> mk_Freessss "g" g_Tssss; 

51831  360 

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

51829  362 

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

364 

55871  365 
fun build_dtor_corec_arg _ [] [cg] = cg 
366 
 build_dtor_corec_arg T [cq] [cg, cg'] = 

367 
mk_If cq (build_sum_inj Inl_const (fastype_of cg, T) $ cg) 

368 
(build_sum_inj Inr_const (fastype_of cg', T) $ cg'); 

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

369 

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

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

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

51831  374 
in 
55869  375 
((x, cs, cpss, ((pgss, cqgsss), corec_types)), lthy) 
51831  376 
end; 
51829  377 

55867  378 
fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy = 
51903  379 
let 
52169  380 
val thy = Proof_Context.theory_of lthy; 
381 

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

51903  384 

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

386 
if fp = Least_FP then 
56641
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

387 
mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

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

391 
>> (pair NONE o SOME); 
51903  392 
in 
55867  393 
((xtor_co_recs, recs_args_types, corecs_args_types), lthy') 
51903  394 
end; 
395 

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

397 
let 
55869  398 
val n = length cqgss; 
399 
val ts = map2 (mk_absumprod absT abs n) (1 upto n) cqgss; 

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

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

401 
Term.lambda c (mk_IfN absT cps ts) 
51900  402 
end; 
51886  403 

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

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

407 

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

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

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

410 

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

52327  413 
> `Local_Theory.restore; 
414 

415 
val phi = Proof_Context.export_morphism lthy lthy'; 

416 

55869  417 
val cst' = mk_co_rec thy fp fpT Cs (Morphism.term phi cst); 
55864  418 
val def' = Morphism.thm phi def; 
52327  419 
in 
55864  420 
((cst', def'), lthy') 
52327  421 
end; 
422 

56641
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

423 
fun define_rec (_, _, fss, xssss) mk_binding fpTs Cs reps ctor_rec = 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

424 
let 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

425 
val nn = length fpTs; 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

426 
val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec) 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

427 
>> map domain_type > domain_type; 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

428 
in 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

429 
define_co_rec Least_FP fpT Cs (mk_binding recN) 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

430 
(fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec, 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

431 
map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss => 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

432 
mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss) 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

433 
(map flat_rec_arg_args xsss)) 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

434 
ctor_rec_absTs reps fss xssss))) 
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

435 
end; 
51897  436 

55869  437 
fun define_corec (_, cs, cpss, ((pgss, cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec = 
51897  438 
let 
51899  439 
val nn = length fpTs; 
55867  440 
val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec))); 
51897  441 
in 
55867  442 
define_co_rec Greatest_FP fpT Cs (mk_binding corecN) 
55869  443 
(fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec, 
444 
map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss))) 

52320  445 
end; 
51897  446 

57471  447 
fun postproc_co_induct lthy nn prop prop_conj = 
448 
Drule.zero_var_indexes 

449 
#> `(conj_dests nn) 

450 
#>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop)) 

451 
##> (fn thm => Thm.permute_prems 0 (~nn) 

452 
(if nn = 1 then thm RS prop 

453 
else funpow nn (fn thm => Local_Defs.unfold lthy @{thms conj_assoc} (thm RS prop_conj)) thm)); 

454 

455 
fun mk_induct_attrs ctrss = 

456 
let 

457 
val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); 

458 
val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases)); 

459 
in 

460 
[induct_case_names_attr] 

461 
end; 

462 

57535  463 
fun derive_rel_induct_thms_for_types lthy fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct 
464 
ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs = 

57471  465 
let 
466 
val B_ify = typ_subst_nonatomic (As ~~ Bs) 

467 
val fpB_Ts = map B_ify fpA_Ts; 

468 
val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss; 

469 
val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss; 

470 

471 
val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy 

472 
> mk_Frees "R" (map2 mk_pred2T As Bs) 

473 
>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts) 

474 
>> mk_Freesss "a" ctrAs_Tsss 

475 
>> mk_Freesss "b" ctrBs_Tsss; 

476 

477 
val premises = 

478 
let 

57525  479 
fun build_the_rel A B = build_rel lthy fpA_Ts (the o choose_relator (Rs @ IRs)) (A, B); 
57471  480 
fun build_rel_app a b = build_the_rel (fastype_of a) (fastype_of b) $ a $ b; 
481 

482 
fun mk_prem ctrA ctrB argAs argBs = 

483 
fold_rev Logic.all (argAs @ argBs) (fold_rev (curry Logic.mk_implies) 

484 
(map2 (HOLogic.mk_Trueprop oo build_rel_app) argAs argBs) 

485 
(HOLogic.mk_Trueprop 

486 
(build_rel_app (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs))))); 

487 
in 

488 
flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss) 

489 
end; 

490 

57525  491 
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq 
492 
(map (build_rel lthy [] (the o choose_relator (Rs @ IRs))) (fpA_Ts ~~ fpB_Ts)) IRs)); 

57471  493 

494 
val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal 

495 
(fn {context = ctxt, prems = prems} => 

57535  496 
mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss 
497 
ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs) 

57471  498 
> singleton (Proof_Context.export names_lthy lthy) 
499 
> Thm.close_derivation; 

500 
in 

501 
(postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} 

502 
rel_induct0_thm, 

503 
mk_induct_attrs ctrAss) 

504 
end; 

505 

55867  506 
fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms 
57397  507 
live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions 
508 
abs_inverses ctrss ctr_defss recs rec_defs lthy = 

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

509 
let 
51827  510 
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; 
511 

51815  512 
val nn = length pre_bnfs; 
51827  513 
val ns = map length ctr_Tsss; 
514 
val mss = map (map length) ctr_Tsss; 

51815  515 

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

516 
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

517 
val pre_set_defss = map set_defs_of_bnf pre_bnfs; 
57399  518 
val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; 
519 
val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; 

57397  520 
val fp_nesting_set_maps = maps set_map_of_bnf fp_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

521 

51816  522 
val fp_b_names = map base_name_of_typ fpTs; 
51811  523 

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

525 
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

526 
> mk_Frees' "P" (map mk_pred1T fpTs) 
51827  527 
>> mk_Freesss "x" ctr_Tsss 
51816  528 
>> 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

529 

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

530 
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

531 

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

532 
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

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

534 
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

535 
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

536 
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

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

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

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

540 
 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

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

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

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

544 

57397  545 
val setss_nested = map mk_sets_nested fp_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

546 

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

547 
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

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

549 
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

550 
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

551 
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

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

553 

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

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

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

556 
 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

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

558 
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

559 
 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

560 
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

561 
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

562 
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

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

564 
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

565 
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

566 
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

567 
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

568 
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

569 
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

570 
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

571 
 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

572 

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

573 
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

574 
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

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

576 

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

577 
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

578 
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

579 
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

580 
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

581 

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

582 
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

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

584 
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

585 
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

586 
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

587 

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

588 
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

589 
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

590 

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

591 
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

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 goal = 
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

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

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

596 

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

597 
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

598 

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

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

600 

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

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

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

603 
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses 
57397  604 
abs_inverses fp_nesting_set_maps pre_set_defss) 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

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

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

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

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

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

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

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

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

613 

52305  614 
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; 
615 

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

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

619 

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

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

623 

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

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

627 
else 

628 
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

629 

55867  630 
fun build_rec (x as Free (_, T)) U = 
52368  631 
if T = U then 
632 
x 

633 
else 

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

636 

55867  637 
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; 
55871  638 
val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

639 

57397  640 
val tacss = map4 (map ooo 
57399  641 
mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs) 
55867  642 
ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss; 
51808
355dcd6a9b3c
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
blanchet
parents:
51805
diff
changeset

643 

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

644 
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

645 
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

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

647 
in 
52305  648 
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

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

650 

56641
029997d3b5d8
reverted rb458558cbcc2  better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the lowlevel recursor) and 'rec'
blanchet
parents:
56640
diff
changeset

651 
val rec_thmss = mk_rec_thmss (the rec_args_typess) 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

652 
in 
57471  653 
((induct_thms, induct_thm, mk_induct_attrs ctrss), 
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55803
diff
changeset

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

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

656 

57535  657 
fun mk_coinduct_attributes fpTs ctrss discss mss = 
57302  658 
let 
659 
val nn = length fpTs; 

660 
val fp_b_names = map base_name_of_typ fpTs; 

57535  661 

57302  662 
fun mk_coinduct_concls ms discs ctrs = 
663 
let 

664 
fun mk_disc_concl disc = [name_of_disc disc]; 

665 
fun mk_ctr_concl 0 _ = [] 

666 
 mk_ctr_concl _ ctor = [name_of_ctr ctor]; 

667 
val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]]; 

668 
val ctr_concls = map2 mk_ctr_concl ms ctrs; 

669 
in 

670 
flat (map2 append disc_concls ctr_concls) 

671 
end; 

57535  672 

57302  673 
val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names); 
674 
val coinduct_conclss = 

675 
map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; 

676 

677 
val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn)); 

678 
val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); 

679 

680 
val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases)); 

681 
val coinduct_case_concl_attrs = 

682 
map2 (fn casex => fn concls => 

683 
Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls)))) 

684 
coinduct_cases coinduct_conclss; 

685 

686 
val common_coinduct_attrs = 

687 
common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; 

688 
val coinduct_attrs = 

689 
coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; 

690 
in 

691 
(coinduct_attrs, common_coinduct_attrs) 

692 
end; 

693 

57535  694 
fun derive_rel_coinduct_thm_for_types lthy fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list) 
695 
abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct 

696 
live_nesting_rel_eqs = 

57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

697 
let 
57302  698 
val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts; 
57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

699 

7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

700 
val (Rs, IRs, fpAs, fpBs, names_lthy) = 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

701 
let 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

702 
val fp_names = map base_name_of_typ fpA_Ts; 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

703 
val ((((Rs, IRs), fpAs_names), fpBs_names), names_lthy) = lthy 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

704 
> mk_Frees "R" (map2 mk_pred2T As Bs) 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

705 
>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts) 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

706 
>> Variable.variant_fixes fp_names 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

707 
>> Variable.variant_fixes (map (suffix "'") fp_names); 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

708 
in 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

709 
(Rs, IRs, 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

710 
map2 (curry Free) fpAs_names fpA_Ts, 
57302  711 
map2 (curry Free) fpBs_names fpB_Ts, 
712 
names_lthy) 

57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

713 
end; 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

714 

7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

715 
val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) = 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

716 
let 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

717 
val discss = map #discs ctr_sugars; 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

718 
val selsss = map #selss ctr_sugars; 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

719 
fun mk_discss ts Ts = map2 (map o rapp) ts (map (map (mk_disc_or_sel Ts)) discss); 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

720 
fun mk_selsss ts Ts = map2 (map o map o rapp) ts (map (map (map (mk_disc_or_sel Ts))) 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

721 
selsss); 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

722 
in 
57302  723 
((mk_discss fpAs As, mk_selsss fpAs As), 
724 
(mk_discss fpBs Bs, mk_selsss fpBs Bs)) 

57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

725 
end; 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

726 

7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

727 
val premises = 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

728 
let 
57525  729 
fun build_the_rel A B = build_rel lthy fpA_Ts (the o choose_relator (Rs @ IRs)) (A, B); 
57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

730 

7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

731 
fun build_rel_app selA_t selB_t = 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

732 
(build_the_rel (fastype_of selA_t) (fastype_of selB_t )) $ selA_t $ selB_t 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

733 

7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

734 
fun mk_prem_ctr_concls n k discA_t selA_ts discB_t selB_ts = 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

735 
(if k = n then [] else [HOLogic.mk_eq (discA_t, discB_t)]) @ 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

736 
(case (selA_ts, selB_ts) of 
57303  737 
([], []) => [] 
57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

738 
 (_ :: _, _ :: _) => 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

739 
[Library.foldr HOLogic.mk_imp (if n = 1 then [] else [discA_t, discB_t], 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

740 
Library.foldr1 HOLogic.mk_conj (map2 build_rel_app selA_ts selB_ts))]); 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

741 

7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

742 
fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss = 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

743 
Library.foldr1 HOLogic.mk_conj (flat (map5 (mk_prem_ctr_concls n) 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

744 
(1 upto n) discA_ts selA_tss discB_ts selB_tss)) 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

745 
handle List.Empty => @{term True}; 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

746 

7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

747 
fun mk_prem IR tA tB n discA_ts selA_tss discB_ts selB_tss = 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

748 
fold_rev Logic.all [tA, tB] (Logic.mk_implies (HOLogic.mk_Trueprop (IR $ tA $ tB), 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

749 
HOLogic.mk_Trueprop (mk_prem_concl n discA_ts selA_tss discB_ts selB_tss))); 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

750 
in 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

751 
map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

752 
end; 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

753 

57525  754 
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq 
755 
IRs (map (build_rel lthy [] (the o choose_relator (Rs @ IRs))) (fpA_Ts ~~ fpB_Ts)))); 

57302  756 

757 
val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal 

57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

758 
(fn {context = ctxt, prems = prems} => 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

759 
mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems 
57303  760 
(map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) 
761 
(map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects 

57471  762 
rel_pre_defs abs_inverses live_nesting_rel_eqs) 
57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

763 
> singleton (Proof_Context.export names_lthy lthy) 
57302  764 
> Thm.close_derivation; 
765 
in 

57471  766 
(postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} 
767 
rel_coinduct0_thm, 

57535  768 
mk_coinduct_attributes fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss) 
57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

769 
end; 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

770 

55871  771 
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _)) 
57397  772 
dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss 
773 
kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) 

55864  774 
corecs corec_defs export_args lthy = 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

775 
let 
55867  776 
fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = 
777 
iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; 

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

778 

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

780 

51815  781 
val nn = length pre_bnfs; 
782 

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

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

784 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
57399  785 
val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; 
57397  786 
val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

787 

51816  788 
val fp_b_names = map base_name_of_typ fpTs; 
51811  789 

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

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

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

792 
val selsss = map #selss ctr_sugars; 
51840  793 
val exhausts = map #exhaust ctr_sugars; 
794 
val disc_thmsss = map #disc_thmss ctr_sugars; 

795 
val discIss = map #discIs ctr_sugars; 

796 
val sel_thmsss = map #sel_thmss ctr_sugars; 

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

797 

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

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

800 
> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) 
51816  801 
>> Variable.variant_fixes fp_b_names 
802 
>> Variable.variant_fixes (map (suffix "'") fp_b_names); 

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

803 

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

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

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

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

807 

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

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

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

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

811 

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

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

814 
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

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

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

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

818 
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

819 

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

820 
fun build_the_rel rs' T Xs_T = 
57303  821 
build_rel lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) 
54237
7cc6e286fe28
made sugared 'coinduct' theorem construction n2mproof
blanchet
parents:
54236
diff
changeset

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

823 

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

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

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

826 

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

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

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

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

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

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

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

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

834 

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

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

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

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

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

839 

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

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

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

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

843 

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

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

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

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

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

848 

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

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

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

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

852 

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

854 

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

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

856 
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => 
57397  857 
mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs 
858 
fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss) 

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

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

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

861 

53106  862 
val rel_eqs = map rel_eq_of_bnf pre_bnfs; 
863 
val rel_monos = map rel_mono_of_bnf pre_bnfs; 

864 
val dtor_coinducts = 

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

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

866 
in 
57471  867 
map2 (postproc_co_induct lthy nn mp mp_conj oo prove) dtor_coinducts goals 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

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

869 

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

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

871 

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

873 

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

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

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

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

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

880 

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

882 

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

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

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

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

887 

55869  888 
fun build_corec cqg = 
889 
let val T = fastype_of cqg in 

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

890 
if exists_subtype_in Cs T then 
55869  891 
let val U = mk_U T in 
57303  892 
build_map lthy [] (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ => 
55869  893 
tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg 
52368  894 
end 
52347
ead18e3b2c1b
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
blanchet
parents:
52346
diff
changeset

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

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

898 

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

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

901 

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

902 
val tacss = 
57399  903 
map4 (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s) 
55867  904 
ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss; 
51810
7b75fab5ebf5
factored out derivation of coinduction, unfold, corec
blanchet
parents:
51808
diff
changeset

905 

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

906 
fun prove goal tac = 
51815  907 
Goal.prove_sorry lthy [] [] goal (tac o #context) 
908 
> Thm.close_derivation; 

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

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

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

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

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

913 

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

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

915 
let 
55869  916 
fun mk_goal c cps gcorec n k disc = 
917 
mk_Trueprop_eq (disc $ (gcorec $ c), 

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

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

919 
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

920 

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

922 

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

924 

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

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

926 

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

928 

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

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

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

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

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

934 

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

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

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

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

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

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

940 

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

942 

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

944 

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

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

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

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

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

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

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

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

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

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

956 

55867  957 
fun mk_sel_corec_thms corec_thmss = 
958 
map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss; 

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

959 

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

961 
in 
57535  962 
((coinduct_thms_pairs, 
963 
mk_coinduct_attributes fpTs (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss), 

57489  964 
corec_thmss, 
965 
disc_corec_thmss, 

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

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

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

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

969 

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

970 
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp 
57094
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset

971 
((discs_sels0, no_code), specs) no_defs_lthy0 = 
49112  972 
let 
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49297
diff
changeset

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

974 

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

975 
val discs_sels = discs_sels0 orelse fp = Greatest_FP; 
49278  976 

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

978 
val fp_bs = map type_binding_of_spec specs; 
49498  979 
val fp_b_names = map Binding.name_of fp_bs; 
980 
val fp_common_name = mk_common_name fp_b_names; 

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

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

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

983 

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

985 
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

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

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

988 

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

989 
val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs; 
56254  990 
val unsorted_Ass0 = map (map (resort_tfree @{sort type})) Ass0; 
55700  991 
val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0; 
53266
89f7f1cc9ae3
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
blanchet
parents:
53264
diff
changeset

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

993 

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

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

995 
val set_bss = map (map (the_default Binding.empty)) set_boss; 
49119  996 

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

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

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

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

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

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

1002 
>> variant_tfrees fp_b_names; 
49119  1003 

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

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

1005 
Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec); 
51768  1006 

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

1007 
val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0; 
49119  1008 

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

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

1010 

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

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

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

1014 

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

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

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

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

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

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

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

1021 

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

1022 
val mixfixes = map mixfix_of_spec specs; 
49119  1023 

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

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

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

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

1029 
val ctr_mixfixess = map (map snd) mx_ctr_specss; 
49119  1030 

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

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

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

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

1035 
val ctr_argsss = map (map args_of_ctr_spec) ctr_specss; 
49119  1036 

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

1038 
val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57199
diff
changeset

1039 
val raw_sel_default_eqss = map sel_default_eqs_of_spec specs; 
49286  1040 

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

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

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

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

1044 

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

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

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

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

1048 
commas (map (qsoty o TFree) extras))); 
49165  1049 

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

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

1051 

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

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

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

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

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

1056 
 eq_fpT_check _ _ = false; 
49146  1057 

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

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

1061 
 kk => nth Xs kk) 
49204  1062 
 freeze_fp T = T; 
49121  1063 

53222  1064 
val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts); 
1065 

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

1066 
val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss; 
55966  1067 
val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss; 
49119  1068 

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

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

1070 
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs; 
49121  1071 

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

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

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

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

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

1076 

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

1079 
(unsorted_As ~~ transpose set_boss); 

1080 

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

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

1083 
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, 
57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

1084 
xtor_co_rec_thms, rel_xtor_co_induct_thm, ...}, 
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53143
diff
changeset

1085 
lthy)) = 
55701  1086 
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) 
1087 
(map dest_TFree killed_As) fp_eqs no_defs_lthy0 

53222  1088 
handle BAD_DEAD (X, X_backdrop) => 
1089 
(case X_backdrop of 

1090 
Type (bad_tc, _) => 

1091 
let 

1092 
val fake_T = qsoty (unfreeze_fp X); 

1093 
val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop); 

1094 
fun register_hint () = 

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

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

1097 
\it"; 

1098 
in 

1099 
if is_some (bnf_of no_defs_lthy bad_tc) orelse 

1100 
is_some (fp_sugar_of no_defs_lthy bad_tc) then 

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

53222  1103 
else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy) 
1104 
bad_tc) then 

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

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

1107 
fake_T_backdrop ^ register_hint ()) 

1108 
else 

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

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

1111 
register_hint ()) 

1112 
end); 

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

1113 

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

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

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

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

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

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

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

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

1121 

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

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

1123 
val timer = time (Timer.startRealTimer ()); 
49121  1124 

57397  1125 
val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs; 
1126 
val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As; 

49226  1127 

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

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

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

1130 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
57397  1131 
val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs; 
1132 
val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs; 

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

1133 

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

1134 
val live = live_of_bnf any_fp_bnf; 
52961  1135 
val _ = 
1136 
if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs) then 

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

1137 
warning "Map function and relator names ignored" 
52961  1138 
else 
1139 
(); 

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

1140 

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

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

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

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

1144 

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

1145 
val B_ify = Term.typ_subst_atomic (As ~~ Bs); 
49167  1146 

49501  1147 
val ctors = map (mk_ctor As) ctors0; 
1148 
val dtors = map (mk_dtor As) dtors0; 

49124  1149 

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

1152 

51780  1153 
fun massage_simple_notes base = 
1154 
filter_out (null o #2) 

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

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

1158 
val massage_multi_notes = 

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

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

51780  1164 

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

1165 
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; 
49203  1166 
val ns = map length ctr_Tsss; 
49212  1167 
val kss = map (fn n => 1 upto n) ns; 
49203  1168 
val mss = map (map length) ctr_Tsss; 
1169 

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

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

1173 
fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor), 
55867
