author  blanchet 
Fri, 16 May 2014 12:56:39 +0200  
changeset 56978  0c1b4987e6b2 
parent 56956  7425fa3763ff 
child 56991  8e9ca31e9b8e 
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 

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

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 = 
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

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

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

31 
* (thm list list * Args.src list) 
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 

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

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

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

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

73 

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

74 
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

75 
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

76 
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

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

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

80 
val parse_co_datatype_cmd: BNF_Util.fp_kind > (mixfix list > binding list > binding list > 
51867  81 
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

82 
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

83 
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

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

49636  87 
structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = 
49112  88 
struct 
89 

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

94 
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

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

97 
open BNF_LFP_Size 
49119  98 

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

101 

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

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

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

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

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

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

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

109 

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

110 
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

111 
Symtab.lookup (Data.get (Context.Proof ctxt)) 
53907  112 
#> Option.map (transfer_fp_sugar ctxt); 
113 

114 
fun fp_sugars_of ctxt = 

115 
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

116 

53106  117 
fun co_induct_of (i :: _) = i; 
118 
fun strong_co_induct_of [_, s] = s; 

119 

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

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

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

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

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

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

125 

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

126 
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

127 
thy 
56767  128 
> Sign.root_path 
129 
> Sign.add_path (Long_Name.qualifier s) 

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

130 
> f fp_sugars 
56767  131 
> 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

132 

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

134 

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

135 
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

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

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

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

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

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

142 

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

143 
fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res 
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

144 
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

145 
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

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

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

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

149 
{T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, 
56637
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

150 
pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs, 
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

151 
nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, 
56648
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

152 
ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, 
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

153 
maps = nth mapss kk, common_co_inducts = common_co_inducts, 
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

154 
co_inducts = nth co_inductss kk, co_rec_thms = nth co_rec_thmss kk, 
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

155 
disc_co_recs = nth disc_co_recss kk, sel_co_recss = nth sel_co_recsss kk, 
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

156 
rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}) Ts 
56637
d1d55f1bbc8a
invoke 'fp_sugar' interpretation hook on mutually recursive clique
blanchet
parents:
56523
diff
changeset

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

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

159 
end; 
51824  160 

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

49622  163 
fun quasi_unambiguous_case_names names = 
164 
let 

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

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

167 
fun underscore s = 

168 
let val ss = space_explode Long_Name.separator s in 

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

170 
end; 

171 
in 

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

173 
end; 

174 

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

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

177 

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

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

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

180 
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; 
49300  181 
val simp_attrs = @{attributes [simp]}; 
182 

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

184 

55871  185 
fun flat_corec_predss_getterss qss gss = maps (op @) (qss ~~ gss); 
51829  186 

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

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

51829  190 

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

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

192 
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

193 

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

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

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

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

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

198 
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

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

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

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

202 

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

205 
Term.subst_atomic_types (Ts0 ~~ Ts) t 

206 
end; 

207 

208 
val mk_ctor = mk_ctor_or_dtor range_type; 

209 
val mk_dtor = mk_ctor_or_dtor domain_type; 

210 

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

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

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

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

215 
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

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

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

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

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

220 
end; 
51827  221 

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

222 
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

223 
 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

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

225 

53591  226 
fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] 
53901  227 
 unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts 
52871  228 
 unzip_corecT _ T = [T]; 
229 

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

230 
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

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

232 
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

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

234 

55700  235 
fun cannot_merge_types fp = 
236 
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

237 

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

239 

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

242 

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

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

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

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

246 

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

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

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

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

250 

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

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

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

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

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

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

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

257 

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

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

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 

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

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

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

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 = 
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset

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

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

286 
* (thm list list * Args.src list) 
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 

54256  290 
fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs), 
55871  291 
(corecss, corec_attrs), (disc_corecss, disc_corec_attrs), 
292 
(disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) = 

54256  293 
((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, 
294 
coinduct_attrs), 

55867  295 
(map (map (Morphism.thm phi)) corecss, corec_attrs), 
55871  296 
(map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs), 
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 

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

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

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 

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

448 
nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses 
55864  449 
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

450 
let 
51827  451 
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; 
452 

51815  453 
val nn = length pre_bnfs; 
51827  454 
val ns = map length ctr_Tsss; 
455 
val mss = map (map length) ctr_Tsss; 

51815  456 

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

457 
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

458 
val pre_set_defss = map set_defs_of_bnf pre_bnfs; 
53329  459 
val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; 
460 
val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs; 

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

462 

51816  463 
val fp_b_names = map base_name_of_typ fpTs; 
51811  464 

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

466 
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

467 
> mk_Frees' "P" (map mk_pred1T fpTs) 
51827  468 
>> mk_Freesss "x" ctr_Tsss 
51816  469 
>> 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

470 

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

471 
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

472 

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

473 
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

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

475 
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

476 
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

477 
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

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

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

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

481 
 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

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

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

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

485 

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

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

487 

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

488 
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

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

490 
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

491 
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

492 
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

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

494 

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

495 
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

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

497 
 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

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

499 
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

500 
 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

501 
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

502 
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

503 
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

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

505 
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

506 
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

507 
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

508 
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

509 
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

510 
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

511 
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

512 
 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

513 

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

514 
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

515 
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

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

517 

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

518 
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

519 
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

520 
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

521 
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

522 

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

523 
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

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

525 
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

526 
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

527 
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

528 

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

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

530 
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

531 

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

532 
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

533 

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

535 
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

536 
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

537 

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

538 
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

539 

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

540 
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

541 

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

542 
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

543 
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

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

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

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

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

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

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

550 
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

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

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

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

554 

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

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

557 

52305  558 
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; 
559 

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

561 
let 
55867  562 
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

563 

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

565 
fold_rev (fold_rev Logic.all) (xs :: fss) 
55867  566 
(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

567 

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

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

571 
else 

572 
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

573 

55867  574 
fun build_rec (x as Free (_, T)) U = 
52368  575 
if T = U then 
576 
x 

577 
else 

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

578 
build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs 
55867  579 
(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

580 

55867  581 
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; 
55871  582 
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

583 

52305  584 
val tacss = 
55867  585 
map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs) 
586 
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

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

589 
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

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

591 
in 
52305  592 
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

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

594 

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

595 
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

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

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

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

600 

55871  601 
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _)) 
55867  602 
dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

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

605 
let 
55867  606 
fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = 
607 
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

608 

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

610 

51815  611 
val nn = length pre_bnfs; 
612 

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

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

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

617 

51816  618 
val fp_b_names = map base_name_of_typ fpTs; 
51811  619 

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

620 
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

621 
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

622 
val selsss = map #selss ctr_sugars; 
51840  623 
val exhausts = map #exhaust ctr_sugars; 
624 
val disc_thmsss = map #disc_thmss ctr_sugars; 

625 
val discIss = map #discIs ctr_sugars; 

626 
val sel_thmsss = map #sel_thmss ctr_sugars; 

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

627 

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

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

630 
> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) 
51816  631 
>> Variable.variant_fixes fp_b_names 
632 
>> Variable.variant_fixes (map (suffix "'") fp_b_names); 

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

633 

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

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

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

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

637 

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

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

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

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

641 

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

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

644 
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

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

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

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

648 
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

649 

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

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

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

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

653 

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

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

655 
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

656 

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

657 
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

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

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

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

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

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

663 
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

664 

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

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

666 
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

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

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

669 

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

670 
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

671 
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

672 
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

673 

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

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

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

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

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

678 

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

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

680 
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

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

682 

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

684 

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

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

686 
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

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

688 
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

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

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

691 

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

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

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

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

696 
> `(conj_dests nn); 
53106  697 

698 
val rel_eqs = map rel_eq_of_bnf pre_bnfs; 

699 
val rel_monos = map rel_mono_of_bnf pre_bnfs; 

700 
val dtor_coinducts = 

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

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

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

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

705 

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

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

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

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

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

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

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

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

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

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

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

716 

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

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

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

720 

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

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

722 

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

724 

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

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

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

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

729 
(Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, 
55869  730 
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

731 

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

733 

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

736 
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

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

738 

55869  739 
fun build_corec cqg = 
740 
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

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

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

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

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

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

749 

55869  750 
val cqgsss' = map (map (map build_corec)) cqgsss; 
751 
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

752 

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

753 
val tacss = 
55867  754 
map4 (map ooo mk_corec_tac corec_defs nesting_map_idents) 
755 
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

756 

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

757 
fun prove goal tac = 
51815  758 
Goal.prove_sorry lthy [] [] goal (tac o #context) 
759 
> Thm.close_derivation; 

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

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

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

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

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

764 

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

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

766 
let 
55869  767 
fun mk_goal c cps gcorec n k disc = 
768 
mk_Trueprop_eq (disc $ (gcorec $ c), 

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

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

770 
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

771 

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

773 

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

775 

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

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

777 

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

779 

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

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

781 
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

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

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

785 

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

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

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

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

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

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

791 

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

793 

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

795 

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

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

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

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

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

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

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

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

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

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

807 

55867  808 
fun mk_sel_corec_thms corec_thmss = 
809 
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

810 

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

812 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

828 

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

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

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

833 

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

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

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

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

837 
(); 
49278  838 

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

840 
val fp_bs = map type_binding_of_spec specs; 
49498  841 
val fp_b_names = map Binding.name_of fp_bs; 
842 
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

843 
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

844 
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

845 

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

847 
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

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

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

850 

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

851 
val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs; 
56254  852 
val unsorted_Ass0 = map (map (resort_tfree @{sort type})) Ass0; 
55700  853 
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

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

855 

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

856 
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

857 
val set_bss = map (map (the_default Binding.empty)) set_boss; 
49119  858 

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

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

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

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

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

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

864 
>> variant_tfrees fp_b_names; 
49119  865 

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

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

867 
Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec); 
51768  868 

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

869 
val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0; 
49119  870 

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

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

872 

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

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

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

876 

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

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

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

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

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

881 
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

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

883 

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

884 
val mixfixes = map mixfix_of_spec specs; 
49119  885 

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

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

889 
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

890 
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

891 
val ctr_mixfixess = map (map snd) mx_ctr_specss; 
49119  892 

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

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

895 
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

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

897 
val ctr_argsss = map (map args_of_ctr_spec) ctr_specss; 
49119  898 

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

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

901 
val raw_sel_defaultsss = map (map sel_defaults_of_ctr_spec) ctr_specss; 
49286  902 

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

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

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

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

906 

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

907 
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

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

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

910 
commas (map (qsoty o TFree) extras))); 
49165  911 

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

912 
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

913 

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

914 
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

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

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

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

918 
 eq_fpT_check _ _ = false; 
49146  919 

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

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

923 
 kk => nth Xs kk) 
49204  924 
 freeze_fp T = T; 
49121  925 

53222  926 
val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts); 
927 

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

928 
val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss; 
55966  929 
val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss; 
49119  930 

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

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

932 
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs; 
49121  933 

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

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

935 
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

936 
 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

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

938 

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

941 
(unsorted_As ~~ transpose set_boss); 

942 

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

943 
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, 
55868  944 
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

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

947 
lthy)) = 
55701  948 
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) 
949 
(map dest_TFree killed_As) fp_eqs no_defs_lthy0 

53222  950 
handle BAD_DEAD (X, X_backdrop) => 
951 
(case X_backdrop of 

952 
Type (bad_tc, _) => 

953 
let 

954 
val fake_T = qsoty (unfreeze_fp X); 

955 
val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop); 

956 
fun register_hint () = 

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

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

959 
\it"; 

960 
in 

961 
if is_some (bnf_of no_defs_lthy bad_tc) orelse 

962 
is_some (fp_sugar_of no_defs_lthy bad_tc) then 

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

53222  965 
else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy) 
966 
bad_tc) then 

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

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

969 
fake_T_backdrop ^ register_hint ()) 

970 
else 

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

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

973 
register_hint ()) 

974 
end); 

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

975 

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

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

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

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

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

980 
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

981 
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

982 
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

983 

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

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

985 
val timer = time (Timer.startRealTimer ()); 
49121  986 

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

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

988 
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; 
49226  989 

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

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

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

992 
val pre_rel_defs = map rel_def_of_bnf pre_bnfs; 
53290  993 
val nesting_set_maps = maps set_map_of_bnf nesting_bnfs; 
994 
val nested_set_maps = maps set_map_of_bnf nested_bnfs; 

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

995 

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

996 
val live = live_of_bnf any_fp_bnf; 
52961  997 
val _ = 
998 
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

999 
warning "Map function and relator names ignored" 
52961  1000 
else 
1001 
(); 

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

1002 

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

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

1004 
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

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

1006 

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

1007 
val B_ify = Term.typ_subst_atomic (As ~~ Bs); 
49167  1008 

49501  1009 
val ctors = map (mk_ctor As) ctors0; 
1010 
val dtors = map (mk_dtor As) dtors0; 

49124  1011 

49501  1012 
val fpTs = map (domain_type o fastype_of) dtors; 
56638  1013 
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

1014 

51780  1015 
fun massage_simple_notes base = 
1016 
filter_out (null o #2) 

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

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

1020 
val massage_multi_notes = 

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

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

51780  1026 

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

1027 
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; 
49203  1028 
val ns = map length ctr_Tsss; 
49212  1029 
val kss = map (fn n => 1 upto n) ns; 
49203  1030 
val mss = map (map length) ctr_Tsss; 
1031 

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

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

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

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

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

1039 
disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = 
49176  1040 
let 
49498  1041 
val fp_b_name = Binding.name_of fp_b; 
1042 

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

1043 
val ctr_absT = domain_type (fastype_of ctor); 
49119  1044 

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

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

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

1049 
>> mk_Freess "y" (map (map B_ify) ctr_Tss) 
49498  1050 
>> yield_singleton Variable.variant_fixes fp_b_name; 
49370  1051 

49498  1052 
val u = Free (u', fpT); 
49121  1053 

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

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

1056 
ks xss; 
49121  1057 

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

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

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

1060 

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

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

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

1064 
ctr_bindings ctr_mixfixes ctr_rhss 
49121  1065 
> `Local_Theory.restore; 
1066 

1067 
val phi = Proof_Context.export_morphism lthy lthy'; 

1068 

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

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

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

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

1072 

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

49121  1075 

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

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

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

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

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

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

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

1085 
in 
51551  1086 
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

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

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

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

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

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

1092 

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

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

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

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

1097 
mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm' 
49135  1098 
end; 
1099 

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

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

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

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

1103 

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

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

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

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

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

1108 

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

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

1110 

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

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

1112 

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

1113 
fun ctr_spec_of disc_b ctr0 sel_bs sel_defs = (((disc_b, ctr0), sel_bs), sel_defs); 
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

1114 
val ctr_specs = map4 ctr_spec_of disc_bindings ctrs0 sel_bindingss sel_defaultss; 
49123
263b0e330d8b
more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
49121
diff
changeset

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

1116 
free_constructors tacss ((wrap_opts, standard_binding), ctr_specs) lthy 
49123
263b0e330d8b
more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
49121
diff
changeset

1117 
end; 
49121  1118 

56956  1119 
fun derive_maps_sets_rels 
1120 
(ctr_sugar as {case_cong, discs, ctrs, exhaust, disc_thmss, ...} : ctr_sugar, lthy) = 

51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1121 
if live = 0 then 
51840  1122 
((([], [], [], []), ctr_sugar), lthy) 
51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1123 
else 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1124 
let 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1125 
val rel_flip = rel_flip_of_bnf fp_bnf; 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1126 
val nones = replicate live NONE; 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1127 

51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

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

1129 
if fp = Least_FP then 
51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1130 
Drule.dummy_thm 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1131 
else 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1132 
let val ctor' = mk_ctor Bs ctor in 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1133 
cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

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

1135 

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

1136 
fun mk_cIn ctor k xs = 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1137 
let val absT = domain_type (fastype_of ctor) in 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1138 
mk_absumprod absT abs n k xs 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1139 
> fp = Greatest_FP ? curry (op $) ctor 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1140 
> certify lthy 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

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

1142 

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

1143 
val cxIns = map2 (mk_cIn ctor) ks xss; 
56638  1144 
val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss; 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1145 

51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1146 
fun mk_map_thm ctr_def' cxIn = 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1147 
fold_thms lthy [ctr_def'] 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1148 
(unfold_thms lthy (o_apply :: pre_map_def :: 
56978
0c1b4987e6b2
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all lowlevel constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
blanchet
parents:
56956
diff
changeset

1149 
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1150 
abs_inverses) 
51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1151 
(cterm_instantiate_pos (nones @ [SOME cxIn]) 
56978
0c1b4987e6b2
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all lowlevel constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
blanchet
parents:
56956
diff
changeset

1152 
(if fp = Least_FP then fp_map_thm 
0c1b4987e6b2
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all lowlevel constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
blanchet
parents:
56956
diff
changeset

1153 
else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans)))) 
51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1154 
> singleton (Proof_Context.export names_lthy no_defs_lthy); 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1155 

51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1156 
fun mk_set_thm fp_set_thm ctr_def' cxIn = 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1157 
fold_thms lthy [ctr_def'] 
53290  1158 
(unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @ 
55966  1159 
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @ 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

1160 
abs_inverses) 
51835
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1161 
(cterm_instantiate_pos [SOME cxIn] fp_set_thm)) 
56523caf372f
Added maps, sets, rels to "simps" thm collection
blanchet
parents:
51833
diff
changeset

1162 
> singleton (Proof_Context.export names_lthy no_defs_lthy); 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49583
diff
changeset

1163 

5183 