author  blanchet 
Thu, 10 Mar 2016 19:15:06 +0100  
changeset 62583  8c7301325f9f 
parent 62582  969480bdef55 
child 62686  6e8924f957f6 
permissions  rwrr 
55061  1 
(* Title: HOL/Tools/BNF/bnf_gfp_rec_sugar.ML 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

2 
Author: Lorenz Panny, TU Muenchen 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

4 
Copyright 2013 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

5 

55538  6 
Corecursor sugar ("primcorec" and "primcorecursive"). 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

7 
*) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

8 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

9 
signature BNF_GFP_REC_SUGAR = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

10 
sig 
59281  11 
datatype corec_option = 
12 
Plugins_Option of Proof.context > Plugin_Name.filter  

13 
Sequential_Option  

14 
Exhaustive_Option  

15 
Transfer_Option 

54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54883
diff
changeset

16 

58223
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

17 
datatype corec_call = 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

18 
Dummy_No_Corec of int  
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

19 
No_Corec of int  
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

20 
Mutual_Corec of int * int * int  
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

21 
Nested_Corec of int 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

22 

ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

23 
type corec_ctr_spec = 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

24 
{ctr: term, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

25 
disc: term, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

26 
sels: term list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

27 
pred: int option, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

28 
calls: corec_call list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

29 
discI: thm, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

30 
sel_thms: thm list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

31 
distinct_discss: thm list list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

32 
collapse: thm, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

33 
corec_thm: thm, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

34 
corec_disc: thm, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

35 
corec_sels: thm list} 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

36 

ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

37 
type corec_spec = 
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

38 
{T: typ, 
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

39 
corec: term, 
58223
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

40 
exhaust_discs: thm list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

41 
sel_defs: thm list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

42 
fp_nesting_maps: thm list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

43 
fp_nesting_map_ident0s: thm list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

44 
fp_nesting_map_comps: thm list, 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

45 
ctr_specs: corec_ctr_spec list} 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

46 

60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

47 
val abstract_over_list: term list > term > term 
59945  48 
val abs_tuple_balanced: term list > term > term 
49 

60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

50 
val mk_conjs: term list > term 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

51 
val mk_disjs: term list > term 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

52 
val mk_dnf: term list list > term 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

53 
val conjuncts_s: term > term list 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

54 
val s_not: term > term 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

55 
val s_not_conj: term list > term list 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

56 
val s_conjs: term list > term 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

57 
val s_disjs: term list > term 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

58 
val s_dnf: term list list > term list 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

59 

59674  60 
val fold_rev_let_if_case: Proof.context > (term list > term > 'a > 'a) > typ list > 
61 
term > 'a > 'a 

62 
val massage_let_if_case: Proof.context > (term > bool) > (typ list > term > term) > 

62318  63 
(typ list > term > unit) > (typ list > term > term) > typ list > term > term 
59674  64 
val massage_nested_corec_call: Proof.context > (term > bool) > 
59989  65 
(typ list > typ > typ > term > term) > (typ list > typ > typ > term > term) > 
66 
typ list > typ > typ > term > term 

60683  67 
val expand_to_ctr_term: Proof.context > typ > term > term 
59674  68 
val massage_corec_code_rhs: Proof.context > (typ list > term > term list > term) > 
69 
typ list > term > term 

70 
val fold_rev_corec_code_rhs: Proof.context > (term list > term > term list > 'a > 'a) > 

71 
typ list > term > 'a > 'a 

72 
val case_thms_of_term: Proof.context > term > 

73 
thm list * thm list * thm list * thm list * thm list 

74 
val map_thms_of_type: Proof.context > typ > thm list 

75 

58223
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

76 
val corec_specs_of: binding list > typ list > typ list > term list > 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

77 
(term * term list list) list list > local_theory > 
58283
71d74e641538
preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents:
58223
diff
changeset

78 
corec_spec list * typ list * thm * thm * thm list * thm list * (Token.src list * Token.src list) 
71d74e641538
preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents:
58223
diff
changeset

79 
* bool * local_theory 
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

80 

59281  81 
val gfp_rec_sugar_interpretation: string > 
82 
(BNF_FP_Rec_Sugar_Util.fp_rec_sugar > local_theory > local_theory) > theory > theory 

59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

83 

61301  84 
val primcorec_ursive_cmd: bool > corec_option list > 
85 
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list > 

86 
Proof.context > 

87 
(term * 'a list) list list * (thm list list > local_theory > local_theory) * local_theory 

60003  88 
val primcorecursive_cmd: corec_option list > 
53831
80423b9080cf
support "of" syntax to disambiguate selector equations
panny
parents:
53830
diff
changeset

89 
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list > 
80423b9080cf
support "of" syntax to disambiguate selector equations
panny
parents:
53830
diff
changeset

90 
Proof.context > Proof.state 
60003  91 
val primcorec_cmd: corec_option list > 
53831
80423b9080cf
support "of" syntax to disambiguate selector equations
panny
parents:
53830
diff
changeset

92 
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list > 
80423b9080cf
support "of" syntax to disambiguate selector equations
panny
parents:
53830
diff
changeset

93 
local_theory > local_theory 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

94 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

95 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

96 
structure BNF_GFP_Rec_Sugar : BNF_GFP_REC_SUGAR = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

97 
struct 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

98 

54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

99 
open Ctr_Sugar_General_Tactics 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

100 
open Ctr_Sugar 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

101 
open BNF_Util 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

102 
open BNF_Def 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

103 
open BNF_FP_Util 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

104 
open BNF_FP_Def_Sugar 
54243  105 
open BNF_FP_N2M_Sugar 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

106 
open BNF_FP_Rec_Sugar_Util 
59276  107 
open BNF_FP_Rec_Sugar_Transfer 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

108 
open BNF_GFP_Rec_Sugar_Tactics 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

109 

58387  110 
val codeN = "code"; 
111 
val ctrN = "ctr"; 

112 
val discN = "disc"; 

113 
val disc_iffN = "disc_iff"; 

114 
val excludeN = "exclude"; 

115 
val selN = "sel"; 

53791  116 

54145
297d1c603999
make sure that registered code equations are actually equations
blanchet
parents:
54133
diff
changeset

117 
val nitpicksimp_attrs = @{attributes [nitpick_simp]}; 
53794  118 
val simp_attrs = @{attributes [simp]}; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

119 

59599  120 
fun extra_variable ctxt ts var = 
121 
error_at ctxt ts ("Extra variable " ^ quote (Syntax.string_of_term ctxt var)); 

59594  122 
fun not_codatatype ctxt T = 
123 
error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T); 

124 
fun ill_formed_corec_call ctxt t = 

125 
error ("Illformed corecursive call " ^ quote (Syntax.string_of_term ctxt t)); 

126 
fun invalid_map ctxt t = 

127 
error_at ctxt [t] "Invalid map function"; 

59598  128 
fun nonprimitive_corec ctxt eqns = 
129 
error_at ctxt eqns "Nonprimitive corecursive specification"; 

59594  130 
fun unexpected_corec_call ctxt eqns t = 
59596
c067eba942e7
no quick_and_dirty for goals that may fail + tuned messages
blanchet
parents:
59595
diff
changeset

131 
error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); 
62318  132 
fun unsupported_case_around_corec_call ctxt eqns t = 
133 
error_at ctxt eqns ("Unsupported corecursive call under case expression " ^ 

62583
8c7301325f9f
don't throw an exception when trying to print an error message
blanchet
parents:
62582
diff
changeset

134 
quote (Syntax.string_of_term ctxt t) ^ " for datatype with no discriminators and selectors"); 
59597  135 
fun use_primcorecursive () = 
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59873
diff
changeset

136 
error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^ 
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59873
diff
changeset

137 
quote (#1 @{command_keyword primcorec}) ^ ")"); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

138 

59281  139 
datatype corec_option = 
140 
Plugins_Option of Proof.context > Plugin_Name.filter  

141 
Sequential_Option  

142 
Exhaustive_Option  

143 
Transfer_Option; 

54591
c822230fd22b
prevent exception when equations for a function are missing;
panny
parents:
54279
diff
changeset

144 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

145 
datatype corec_call = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

146 
Dummy_No_Corec of int  
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

147 
No_Corec of int  
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

148 
Mutual_Corec of int * int * int  
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

149 
Nested_Corec of int; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

150 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

151 
type basic_corec_ctr_spec = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

152 
{ctr: term, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

153 
disc: term, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

154 
sels: term list}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

155 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

156 
type corec_ctr_spec = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

157 
{ctr: term, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

158 
disc: term, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

159 
sels: term list, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

160 
pred: int option, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

161 
calls: corec_call list, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

162 
discI: thm, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

163 
sel_thms: thm list, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

164 
distinct_discss: thm list list, 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

165 
collapse: thm, 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

166 
corec_thm: thm, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

167 
corec_disc: thm, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

168 
corec_sels: thm list}; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

169 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

170 
type corec_spec = 
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

171 
{T: typ, 
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

172 
corec: term, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

173 
exhaust_discs: thm list, 
56858  174 
sel_defs: thm list, 
57397  175 
fp_nesting_maps: thm list, 
57399  176 
fp_nesting_map_ident0s: thm list, 
57397  177 
fp_nesting_map_comps: thm list, 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

178 
ctr_specs: corec_ctr_spec list}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

179 

58223
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

180 
exception NO_MAP of term; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

181 

60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

182 
fun abstract_over_list rev_vs = 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

183 
let 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

184 
val vs = rev rev_vs; 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

185 

fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

186 
fun abs n (t $ u) = abs n t $ abs n u 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

187 
 abs n (Abs (s, T, t)) = Abs (s, T, abs (n + 1) t) 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

188 
 abs n t = 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

189 
let val j = find_index (curry (op =) t) vs in 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

190 
if j < 0 then t else Bound (n + j) 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

191 
end; 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

192 
in 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

193 
abs 0 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

194 
end; 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

195 

59945  196 
val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced; 
197 

60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

198 
fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

199 
Ts > T; 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

200 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59044
diff
changeset

201 
fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs); 
54948  202 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

203 
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

204 
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False}; 
54900  205 
val mk_dnf = mk_disjs o map mk_conjs; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

206 

55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

207 
val conjuncts_s = filter_out (curry (op aconv) @{const True}) o HOLogic.conjuncts; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

208 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

209 
fun s_not @{const True} = @{const False} 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

210 
 s_not @{const False} = @{const True} 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

211 
 s_not (@{const Not} $ t) = t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

212 
 s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

213 
 s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

214 
 s_not t = @{const Not} $ t; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

215 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

216 
val s_not_conj = conjuncts_s o s_not o mk_conjs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

217 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

218 
fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

219 
fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

220 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

221 
fun propagate_units css = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

222 
(case List.partition (can the_single) css of 
58393  223 
([], _) => css 
224 
 ([u] :: uss, css') => 

225 
[u] :: propagate_units (map (propagate_unit_neg (s_not u)) 

226 
(map (propagate_unit_pos u) (uss @ css')))); 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

227 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

228 
fun s_conjs cs = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

229 
if member (op aconv) cs @{const False} then @{const False} 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

230 
else mk_conjs (remove (op aconv) @{const True} cs); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

231 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

232 
fun s_disjs ds = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

233 
if member (op aconv) ds @{const True} then @{const True} 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

234 
else mk_disjs (remove (op aconv) @{const False} ds); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

235 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

236 
fun s_dnf css0 = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

237 
let val css = propagate_units css0 in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

238 
if null css then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

239 
[@{const False}] 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

240 
else if exists null css then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

241 
[] 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

242 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

243 
map (fn c :: cs => (c, cs)) css 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

244 
> AList.coalesce (op =) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

245 
> map (fn (c, css) => c :: s_dnf css) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

246 
> (fn [cs] => cs  css => [s_disjs (map s_conjs css)]) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

247 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

248 

55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

249 
fun fold_rev_let_if_case ctxt f bound_Ts = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

250 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

251 
val thy = Proof_Context.theory_of ctxt; 
53794  252 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

253 
fun fld conds t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

254 
(case Term.strip_comb t of 
55343  255 
(Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_lets_splits t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

256 
 (Const (@{const_name If}, _), [cond, then_branch, else_branch]) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

257 
fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

258 
 (Const (c, _), args as _ :: _ :: _) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

259 
let val n = num_binder_types (Sign.the_const_type thy c)  1 in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

260 
if n >= 0 andalso n < length args then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

261 
(case fastype_of1 (bound_Ts, nth args n) of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

262 
Type (s, Ts) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

263 
(case dest_case ctxt s Ts t of 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

264 
SOME ({split_sels = _ :: _, ...}, conds', branches) => 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

265 
fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches) 
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

266 
 _ => f conds t) 
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

267 
 _ => f conds t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

268 
else 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

269 
f conds t 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

270 
end 
55342  271 
 _ => f conds t); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

272 
in 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

273 
fld [] 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

274 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

275 

54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

276 
fun case_of ctxt s = 
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

277 
(case ctr_sugar_of ctxt s of 
62318  278 
SOME {casex = Const (s', _), split_sels, ...} => SOME (s', not (null split_sels)) 
54970
891141de5672
only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents:
54969
diff
changeset

279 
 _ => NONE); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

280 

62318  281 
fun massage_let_if_case ctxt has_call massage_leaf unexpected_call unsupported_case bound_Ts t0 = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

282 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

283 
val thy = Proof_Context.theory_of ctxt; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

284 

60001  285 
fun check_no_call bound_Ts t = if has_call t then unexpected_call bound_Ts t else (); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

286 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

287 
fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

288 
 massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m  1) t) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

289 
 massage_abs bound_Ts m t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

290 
let val T = domain_type (fastype_of1 (bound_Ts, t)) in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

291 
Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m  1) (incr_boundvars 1 t $ Bound 0)) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

292 
end 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

293 
and massage_rec bound_Ts t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

294 
let val typof = curry fastype_of1 bound_Ts in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

295 
(case Term.strip_comb t of 
55343  296 
(Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

297 
 (Const (@{const_name If}, _), obj :: (branches as [_, _])) => 
59612
7ea413656b64
avoid needless 'if ... undefined' in generated theorems
blanchet
parents:
59609
diff
changeset

298 
(case List.partition Term.is_dummy_pattern (map (massage_rec bound_Ts) branches) of 
7ea413656b64
avoid needless 'if ... undefined' in generated theorems
blanchet
parents:
59609
diff
changeset

299 
(dummy_branch' :: _, []) => dummy_branch' 
7ea413656b64
avoid needless 'if ... undefined' in generated theorems
blanchet
parents:
59609
diff
changeset

300 
 (_, [branch']) => branch' 
7ea413656b64
avoid needless 'if ... undefined' in generated theorems
blanchet
parents:
59609
diff
changeset

301 
 (_, branches') => 
60001  302 
Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj, 
303 
branches')) 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61348
diff
changeset

304 
 (c as Const (@{const_name case_prod}, _), arg :: args) => 
55343  305 
massage_rec bound_Ts 
57895  306 
(unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args))) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

307 
 (Const (c, _), args as _ :: _ :: _) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

308 
(case try strip_fun_type (Sign.the_const_type thy c) of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

309 
SOME (gen_branch_Ts, gen_body_fun_T) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

310 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

311 
val gen_branch_ms = map num_binder_types gen_branch_Ts; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

312 
val n = length gen_branch_ms; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

313 
in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

314 
if n < length args then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

315 
(case gen_body_fun_T of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

316 
Type (_, [Type (T_name, _), _]) => 
62318  317 
(case case_of ctxt T_name of 
318 
SOME (c', has_split_sels) => 

319 
if c' = c then 

320 
if has_split_sels then 

321 
let 

322 
val (branches, obj_leftovers) = chop n args; 

323 
val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches; 

324 
val branch_Ts' = map typof branches'; 

325 
val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts')); 

326 
val casex' = 

327 
Const (c, branch_Ts' > map typof obj_leftovers > body_T'); 

328 
in 

329 
Term.list_comb (casex', 

330 
branches' @ tap (List.app (check_no_call bound_Ts)) obj_leftovers) 

331 
end 

332 
else 

333 
unsupported_case bound_Ts t 

334 
else 

335 
massage_leaf bound_Ts t 

336 
 NONE => massage_leaf bound_Ts t) 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

337 
 _ => massage_leaf bound_Ts t) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

338 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

339 
massage_leaf bound_Ts t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

340 
end 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

341 
 NONE => massage_leaf bound_Ts t) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

342 
 _ => massage_leaf bound_Ts t) 
55342  343 
end; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

344 
in 
59596
c067eba942e7
no quick_and_dirty for goals that may fail + tuned messages
blanchet
parents:
59595
diff
changeset

345 
massage_rec bound_Ts t0 
59612
7ea413656b64
avoid needless 'if ... undefined' in generated theorems
blanchet
parents:
59609
diff
changeset

346 
> Term.map_aterms (fn t => 
7ea413656b64
avoid needless 'if ... undefined' in generated theorems
blanchet
parents:
59609
diff
changeset

347 
if Term.is_dummy_pattern t then Const (@{const_name undefined}, fastype_of t) else t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

348 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

349 

60001  350 
fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 = 
62318  351 
massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call ctxt [t0])) 
352 
(K (unsupported_case_around_corec_call ctxt [t0])) bound_Ts t0; 

60001  353 

59989  354 
fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

355 
let 
59596
c067eba942e7
no quick_and_dirty for goals that may fail + tuned messages
blanchet
parents:
59595
diff
changeset

356 
fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else (); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

357 

59609  358 
fun massage_mutual_call bound_Ts (Type (@{type_name fun}, [_, U2])) 
359 
(Type (@{type_name fun}, [T1, T2])) t = 

62582  360 
Abs (Name.uu, T1, massage_mutual_call (T1 :: bound_Ts) U2 T2 (incr_boundvars 1 t $ Bound 0)) 
59609  361 
 massage_mutual_call bound_Ts U T t = 
59989  362 
(if has_call t then massage_call else massage_noncall) bound_Ts U T t; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

363 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

364 
fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

365 
(case try (dest_map ctxt s) t of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

366 
SOME (map0, fs) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

367 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

368 
val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t)); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

369 
val map' = mk_map (length fs) dom_Ts Us map0; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

370 
val fs' = 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58462
diff
changeset

371 
map_flattened_map_args ctxt s (@{map 3} (massage_map_or_map_arg bound_Ts) Us Ts) fs; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

372 
in 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

373 
Term.list_comb (map', fs') 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

374 
end 
58223
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

375 
 NONE => raise NO_MAP t) 
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

376 
 massage_map _ _ _ t = raise NO_MAP t 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

377 
and massage_map_or_map_arg bound_Ts U T t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

378 
if T = U then 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

379 
tap check_no_call t 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

380 
else 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

381 
massage_map bound_Ts U T t 
58223
ba7a2d19880c
export useful functions for users of (co)recursors
blanchet
parents:
58211
diff
changeset

382 
handle NO_MAP _ => massage_mutual_fun bound_Ts U T t 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

383 
and massage_mutual_fun bound_Ts U T t = 
60741  384 
let 
385 
val j = Term.maxidx_of_term t + 1; 

386 
val var = Var ((Name.uu, j), domain_type (fastype_of1 (bound_Ts, t))); 

387 

388 
fun massage_body () = 

59947  389 
Term.lambda var (Term.incr_boundvars 1 (massage_any_call bound_Ts U T 
60741  390 
(betapply (t, var)))); 
391 
in 

392 
(case t of 

393 
Const (@{const_name comp}, _) $ t1 $ t2 => 

394 
if has_call t2 then massage_body () 

395 
else mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, t2) 

396 
 _ => massage_body ()) 

397 
end 

59947  398 
and massage_any_call bound_Ts U T = 
60001  399 
massage_let_if_case_corec ctxt has_call (fn bound_Ts => fn t => 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

400 
if has_call t then 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

401 
(case U of 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

402 
Type (s, Us) => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

403 
(case try (dest_ctr ctxt s) t of 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

404 
SOME (f, args) => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

405 
let 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

406 
val typof = curry fastype_of1 bound_Ts; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

407 
val f' = mk_ctr Us f 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

408 
val f'_T = typof f'; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

409 
val arg_Ts = map typof args; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

410 
in 
59598  411 
Term.list_comb (f', 
59947  412 
@{map 3} (massage_any_call bound_Ts) (binder_types f'_T) arg_Ts args) 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

413 
end 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

414 
 NONE => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

415 
(case t of 
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61348
diff
changeset

416 
Const (@{const_name case_prod}, _) $ t' => 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

417 
let 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

418 
val U' = curried_type U; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

419 
val T' = curried_type T; 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

420 
in 
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61348
diff
changeset

421 
Const (@{const_name case_prod}, U' > U) $ massage_any_call bound_Ts U' T' t' 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

422 
end 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

423 
 t1 $ t2 => 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

424 
(if has_call t2 then 
59989  425 
massage_mutual_call bound_Ts U T t 
426 
else 

427 
massage_map bound_Ts U T t1 $ t2 

428 
handle NO_MAP _ => massage_mutual_call bound_Ts U T t) 

54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

429 
 Abs (s, T', t') => 
59947  430 
Abs (s, T', massage_any_call (T' :: bound_Ts) (range_type U) (range_type T) t') 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

431 
 _ => massage_mutual_call bound_Ts U T t)) 
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

432 
 _ => ill_formed_corec_call ctxt t) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

433 
else 
59989  434 
massage_noncall bound_Ts U T t) bound_Ts; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

435 
in 
59989  436 
(if has_call t0 then massage_any_call else massage_noncall) bound_Ts U T t0 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

437 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

438 

60683  439 
fun expand_to_ctr_term ctxt (T as Type (s, Ts)) t = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

440 
(case ctr_sugar_of ctxt s of 
60683  441 
SOME {ctrs, casex, ...} => Term.list_comb (mk_case Ts T casex, map (mk_ctr Ts) ctrs) $ t 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

442 
 NONE => raise Fail "expand_to_ctr_term"); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

443 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

444 
fun expand_corec_code_rhs ctxt has_call bound_Ts t = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

445 
(case fastype_of1 (bound_Ts, t) of 
60683  446 
T as Type (s, _) => 
60001  447 
massage_let_if_case_corec ctxt has_call (fn _ => fn t => 
60683  448 
if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt T t) bound_Ts t 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

449 
 _ => raise Fail "expand_corec_code_rhs"); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

450 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

451 
fun massage_corec_code_rhs ctxt massage_ctr = 
60001  452 
massage_let_if_case_corec ctxt (K false) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

453 
(fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

454 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

455 
fun fold_rev_corec_code_rhs ctxt f = 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

456 
fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

457 

55400  458 
fun case_thms_of_term ctxt t = 
459 
let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

460 
(maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #exhaust_discs ctr_sugars, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

461 
maps #split_sels ctr_sugars, maps #split_sel_asms ctr_sugars) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

462 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

463 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

464 
fun basic_corec_specs_of ctxt res_T = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

465 
(case res_T of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

466 
Type (T_name, _) => 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

467 
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

468 
NONE => not_codatatype ctxt res_T 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58131
diff
changeset

469 
 SOME {T = fpT, ctrs, discs, selss, ...} => 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

470 
let 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

471 
val thy = Proof_Context.theory_of ctxt; 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

472 

58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58131
diff
changeset

473 
val As_rho = tvar_subst thy [fpT] [res_T]; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

474 
val substA = Term.subst_TVars As_rho; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

475 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

476 
fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels}; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

477 
in 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58462
diff
changeset

478 
@{map 3} mk_spec ctrs discs selss 
54911  479 
handle ListPair.UnequalLengths => not_codatatype ctxt res_T 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

480 
end) 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

481 
 _ => not_codatatype ctxt res_T); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

482 

59674  483 
fun map_thms_of_type ctxt (Type (s, _)) = 
58462  484 
(case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms  NONE => []) 
59674  485 
 map_thms_of_type _ _ = []; 
54955
cf8d429dc24e
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents:
54954
diff
changeset

486 

59281  487 
structure GFP_Rec_Sugar_Plugin = Plugin(type T = fp_rec_sugar); 
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

488 

59281  489 
fun gfp_rec_sugar_interpretation name f = 
490 
GFP_Rec_Sugar_Plugin.interpretation name (fn fp_rec_sugar => fn lthy => 

491 
f (transfer_fp_rec_sugar (Proof_Context.theory_of lthy) fp_rec_sugar) lthy); 

59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

492 

59281  493 
val interpret_gfp_rec_sugar = GFP_Rec_Sugar_Plugin.data; 
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59058
diff
changeset

494 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

495 
fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

496 
let 
55005  497 
val thy = Proof_Context.theory_of lthy0; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

498 

57397  499 
val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs, 
58461  500 
fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _, 
501 
(_, gfp_sugar_thms)), lthy) = 

58335
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58286
diff
changeset

502 
nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

503 

58286  504 
val coinduct_attrs_pair = 
505 
(case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair  NONE => ([], [])); 

58283
71d74e641538
preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents:
58223
diff
changeset

506 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59044
diff
changeset

507 
val perm_fp_sugars = sort (int_ord o apply2 #fp_res_index) fp_sugars; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

508 

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

509 
val indices = map #fp_res_index fp_sugars; 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55538
diff
changeset

510 
val perm_indices = map #fp_res_index perm_fp_sugars; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

511 

58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58131
diff
changeset

512 
val perm_fpTs = map #T perm_fp_sugars; 
58460  513 
val perm_ctrXs_Tsss' = 
514 
map (repair_nullary_single_ctr o #ctrXs_Tss o #fp_ctr_sugar) perm_fp_sugars; 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

515 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

516 
val nn0 = length res_Ts; 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58131
diff
changeset

517 
val nn = length perm_fpTs; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

518 
val kks = 0 upto nn  1; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

519 
val perm_ns' = map length perm_ctrXs_Tsss'; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

520 

367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

521 
val perm_Ts = map #T perm_fp_sugars; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

522 
val perm_Xs = map #X perm_fp_sugars; 
58461  523 
val perm_Cs = 
524 
map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars; 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

525 
val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

526 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

527 
fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)] 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

528 
 zip_corecT U = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

529 
(case AList.lookup (op =) Xs_TCs U of 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

530 
SOME (T, C) => [T, C] 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

531 
 NONE => [U]); 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

532 

55869  533 
val perm_p_Tss = mk_corec_p_pred_types perm_Cs perm_ns'; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

534 
val perm_f_Tssss = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

535 
map2 (fn C => map (map (map (curry (op >) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss'; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

536 
val perm_q_Tssss = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

537 
map (map (map (fn [_] => []  [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

538 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

539 
val (perm_p_hss, h) = indexedd perm_p_Tss 0; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

540 
val (perm_q_hssss, h') = indexedddd perm_q_Tssss h; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

541 
val (perm_f_hssss, _) = indexedddd perm_f_Tssss h'; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

542 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

543 
val fun_arg_hs = 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58462
diff
changeset

544 
flat (@{map 3} flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss); 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

545 

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

546 
fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs; 
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55462
diff
changeset

547 
fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

548 

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

549 
val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

550 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

551 
val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

552 
val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

553 
val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss); 
53358  554 

54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

555 
val f_Tssss = unpermute perm_f_Tssss; 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58131
diff
changeset

556 
val fpTs = unpermute perm_fpTs; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

557 
val Cs = unpermute perm_Cs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

558 

58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58131
diff
changeset

559 
val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

560 
val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

561 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

562 
val substA = Term.subst_TVars As_rho; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

563 
val substAT = Term.typ_subst_TVars As_rho; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

564 
val substCT = Term.typ_subst_TVars Cs_rho; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

565 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

566 
val perm_Cs' = map substCT perm_Cs; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

567 

8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

568 
fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] = 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

569 
(if exists_subtype_in Cs T then Nested_Corec 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

570 
else if nullary then Dummy_No_Corec 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

571 
else No_Corec) g_i 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

572 
 call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i'); 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

573 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

574 
fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms distinct_discss collapse 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

575 
corec_thm corec_disc corec_sels = 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

576 
let val nullary = not (can dest_funT (fastype_of ctr)) in 
54900  577 
{ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io, 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58462
diff
changeset

578 
calls = @{map 3} (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

579 
distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm, 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

580 
corec_disc = corec_disc, corec_sels = corec_sels} 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

581 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

582 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

583 
fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...} 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

584 
: ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss = 
55863  585 
let val p_ios = map SOME p_is @ [NONE] in 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58462
diff
changeset

586 
@{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

587 
distinct_discsss collapses corec_thms corec_discs corec_selss 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

588 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

589 

58461  590 
fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, 
591 
fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs, 

58459  592 
co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = 
59598  593 
{T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, 
594 
exhaust_discs = exhaust_discs, sel_defs = sel_defs, 

59674  595 
fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs, 
57399  596 
fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs, 
57397  597 
fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs, 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

598 
ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57895
diff
changeset

599 
corec_selss}; 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

600 
in 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58462
diff
changeset

601 
(@{map 5} mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, 
58283
71d74e641538
preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents:
58223
diff
changeset

602 
co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms, 
71d74e641538
preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents:
58223
diff
changeset

603 
co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair, 
71d74e641538
preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents:
58223
diff
changeset

604 
is_some gfp_sugar_thms, lthy) 
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

605 
end; 
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset

606 

53358  607 
val undef_const = Const (@{const_name undefined}, dummyT); 
53357  608 

58393  609 
type coeqn_data_disc = 
610 
{fun_name: string, 

611 
fun_T: typ, 

612 
fun_args: term list, 

613 
ctr: term, 

614 
ctr_no: int, 

615 
disc: term, 

616 
prems: term list, 

617 
auto_gen: bool, 

618 
ctr_rhs_opt: term option, 

619 
code_rhs_opt: term option, 

620 
eqn_pos: int, 

621 
user_eqn: term}; 

54001  622 

58393  623 
type coeqn_data_sel = 
624 
{fun_name: string, 

625 
fun_T: typ, 

626 
fun_args: term list, 

627 
ctr: term, 

628 
sel: term, 

629 
rhs_term: term, 

630 
ctr_rhs_opt: term option, 

631 
code_rhs_opt: term option, 

632 
eqn_pos: int, 

633 
user_eqn: term}; 

54001  634 

59602  635 
fun ctr_sel_of ({ctr, sel, ...} : coeqn_data_sel) = (ctr, sel); 
636 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

637 
datatype coeqn_data = 
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

638 
Disc of coeqn_data_disc  
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

639 
Sel of coeqn_data_sel; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

640 

59948  641 
fun is_free_in frees (Free (s, _)) = member (op =) frees s 
59594  642 
 is_free_in _ _ = false; 
643 

59948  644 
fun is_catch_all_prem (Free (s, _)) = s = Name.uu_ 
59799
0b21e85fd9ba
clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
wenzelm
parents:
59674
diff
changeset

645 
 is_catch_all_prem _ = false; 
0b21e85fd9ba
clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
wenzelm
parents:
59674
diff
changeset

646 

59599  647 
fun add_extra_frees ctxt frees names = 
59948  648 
fold_aterms (fn x as Free (s, _) => 
649 
(not (member (op =) frees x) andalso not (member (op =) names s) andalso 

650 
not (Variable.is_fixed ctxt s) andalso not (is_catch_all_prem x)) 

59599  651 
? cons x  _ => I); 
652 

653 
fun check_extra_frees ctxt frees names t = 

654 
let val bads = add_extra_frees ctxt frees names t [] in 

655 
null bads orelse extra_variable ctxt [t] (hd bads) 

56152  656 
end; 
657 

59604  658 
fun check_fun_args ctxt eqn fun_args = 
659 
let 

660 
val dups = duplicates (op =) fun_args; 

661 
val _ = null dups orelse error_at ctxt [eqn] 

662 
("Duplicate variable " ^ quote (Syntax.string_of_term ctxt (hd dups))); 

663 

59607  664 
val _ = forall is_Free fun_args orelse 
665 
error_at ctxt [eqn] ("Nonvariable function argument on lefthand side " ^ 

666 
quote (Syntax.string_of_term ctxt (the (find_first (not o is_Free) fun_args)))); 

667 

59604  668 
val fixeds = filter (Variable.is_fixed ctxt o fst o dest_Free) fun_args; 
669 
val _ = null fixeds orelse error_at ctxt [eqn] ("Function argument " ^ 

670 
quote (Syntax.string_of_term ctxt (hd fixeds)) ^ " is fixed in context"); 

671 
in () end; 

672 

59594  673 
fun dissect_coeqn_disc ctxt fun_names sequentials 
674 
(basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos ctr_rhs_opt code_rhs_opt prems0 

675 
concl matchedsss = 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

676 
let 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

677 
fun find_subterm p = 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

678 
let (* FIXME \<exists>? *) 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

679 
fun find (t as u $ v) = if p t then SOME t else merge_options (find u, find v) 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

680 
 find t = if p t then SOME t else NONE; 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

681 
in find end; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

682 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

683 
val applied_fun = concl 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

684 
> find_subterm (member (op = o apsnd SOME) fun_names o try (fst o dest_Free o head_of)) 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

685 
> the 
59594  686 
handle Option.Option => error_at ctxt [concl] "Illformed discriminator formula"; 
53720  687 
val ((fun_name, fun_T), fun_args) = strip_comb applied_fun >> dest_Free; 
56152  688 

59604  689 
val _ = check_fun_args ctxt concl fun_args; 
56152  690 

59594  691 
val bads = filter (Term.exists_subterm (is_free_in fun_names)) prems0; 
692 
val _ = null bads orelse error_at ctxt bads "Corecursive call(s) in condition(s)"; 

56152  693 

58393  694 
val (sequential, basic_ctr_specs) = 
695 
the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name); 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

696 

54160  697 
val discs = map #disc basic_ctr_specs; 
698 
val ctrs = map #ctr basic_ctr_specs; 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

699 
val not_disc = head_of concl = @{term Not}; 
53401  700 
val _ = not_disc andalso length ctrs <> 2 andalso 
59594  701 
error_at ctxt [concl] "Negated discriminator for a type with \<noteq> 2 constructors"; 
54160  702 
val disc' = find_subterm (member (op =) discs o head_of) concl; 
54209  703 
val eq_ctr0 = concl > perhaps (try HOLogic.dest_not) > try (HOLogic.dest_eq #> snd) 
59598  704 
> (fn SOME t => let val n = find_index (curry (op =) t) ctrs in 
705 
if n >= 0 then SOME n else NONE end  _ => NONE); 

56152  706 

59594  707 
val _ = is_none disc' orelse perhaps (try HOLogic.dest_not) concl = the disc' orelse 
708 
error_at ctxt [concl] "Illformed discriminator formula"; 

709 
val _ = is_some disc' orelse is_some eq_ctr0 orelse 

710 
error_at ctxt [concl] "No discriminator in equation"; 

56152  711 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

712 
val ctr_no' = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

713 
if is_none disc' then the eq_ctr0 else find_index (curry (op =) (head_of (the disc'))) discs; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

714 
val ctr_no = if not_disc then 1  ctr_no' else ctr_no'; 
54160  715 
val {ctr, disc, ...} = nth basic_ctr_specs ctr_no; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

716 

59605  717 
val catch_all = 
718 
(case prems0 of 

719 
[prem] => is_catch_all_prem prem 

720 
 _ => 

721 
if exists is_catch_all_prem prems0 then error_at ctxt [concl] "Superfluous premises" 

722 
else false); 

53720  723 
val matchedss = AList.lookup (op =) matchedsss fun_name > the_default []; 
60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

724 
val prems = map (abstract_over_list fun_args) prems0; 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

725 
val actual_prems = 
54901
0b8871677e0b
use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents:
54900
diff
changeset

726 
(if catch_all orelse sequential then maps s_not_conj matchedss else []) @ 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

727 
(if catch_all then [] else prems); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

728 

53720  729 
val matchedsss' = AList.delete (op =) fun_name matchedsss 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

730 
> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [actual_prems]); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

731 

53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

732 
val user_eqn = 
54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

733 
(actual_prems, concl) 
60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

734 
>> map HOLogic.mk_Trueprop > HOLogic.mk_Trueprop o abstract_over_list fun_args 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

735 
> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies; 
56152  736 

59599  737 
val _ = check_extra_frees ctxt fun_args fun_names user_eqn; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

738 
in 
58393  739 
(Disc {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no, 
740 
disc = disc, prems = actual_prems, auto_gen = catch_all, ctr_rhs_opt = ctr_rhs_opt, 

741 
code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = user_eqn}, 

742 
matchedsss') 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

743 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

744 

59594  745 
fun dissect_coeqn_sel ctxt fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

746 
ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

747 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

748 
val (lhs, rhs) = HOLogic.dest_eq eqn 
59594  749 
handle TERM _ => error_at ctxt [eqn] "Illformed equation (expected \"lhs = rhs\")"; 
59604  750 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

751 
val sel = head_of lhs; 
53720  752 
val ((fun_name, fun_T), fun_args) = dest_comb lhs > snd > strip_comb > apfst dest_Free 
59594  753 
handle TERM _ => error_at ctxt [eqn] "Illformed selector argument in lefthand side"; 
59604  754 
val _ = check_fun_args ctxt eqn fun_args; 
56152  755 

54160  756 
val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name) 
59594  757 
handle Option.Option => error_at ctxt [eqn] "Illformed selector argument in lefthand side"; 
54160  758 
val {ctr, ...} = 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

759 
(case of_spec_opt of 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

760 
SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs) 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

761 
 NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs > the_single 
59594  762 
handle List.Empty => error_at ctxt [eqn] "Ambiguous selector (without \"of\")"); 
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

763 
val user_eqn = drop_all eqn0; 
56152  764 

59599  765 
val _ = check_extra_frees ctxt fun_args fun_names user_eqn; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

766 
in 
58393  767 
Sel {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, sel = sel, 
768 
rhs_term = rhs, ctr_rhs_opt = ctr_rhs_opt, code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, 

769 
user_eqn = user_eqn} 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

770 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

771 

59594  772 
fun dissect_coeqn_ctr ctxt fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

773 
eqn_pos eqn0 code_rhs_opt prems concl matchedsss = 
53910  774 
let 
54065  775 
val (lhs, rhs) = HOLogic.dest_eq concl; 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

776 
val (fun_name, fun_args) = strip_comb lhs >> fst o dest_Free; 
56152  777 

59604  778 
val _ = check_fun_args ctxt concl fun_args; 
59599  779 
val _ = check_extra_frees ctxt fun_args fun_names (drop_all eqn0); 
56152  780 

58393  781 
val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); 
55343  782 
val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs); 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

783 
val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs) 
59594  784 
handle Option.Option => error_at ctxt [ctr] "Not a constructor"; 
53341  785 

54065  786 
val disc_concl = betapply (disc, lhs); 
54976
b502f04c0442
repair 'exhaustive' feature for oneconstructor types
blanchet
parents:
54975
diff
changeset

787 
val (eqn_data_disc_opt, matchedsss') = 
59042  788 
if null (tl basic_ctr_specs) andalso not (null sels) then 
54976
b502f04c0442
repair 'exhaustive' feature for oneconstructor types
blanchet
parents:
54975
diff
changeset

789 
(NONE, matchedsss) 
b502f04c0442
repair 'exhaustive' feature for oneconstructor types
blanchet
parents:
54975
diff
changeset

790 
else 
59594  791 
apfst SOME (dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos 
60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

792 
(SOME (abstract_over_list fun_args rhs)) code_rhs_opt prems disc_concl matchedsss); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

793 

54159
eb5d58c99049
set stage for more flexible 'primrec' syntax for recursion through functions
blanchet
parents:
54157
diff
changeset

794 
val sel_concls = sels ~~ ctr_args 
56152  795 
> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)) 
59595  796 
handle ListPair.UnequalLengths => 
797 
error_at ctxt [rhs] "Partially applied constructor in righthand side"; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

798 

54160  799 
val eqns_data_sel = 
59594  800 
map (dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos 
60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

801 
(SOME (abstract_over_list fun_args rhs)) code_rhs_opt eqn0 (SOME ctr)) 
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

802 
sel_concls; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

803 
in 
54926
28b621fce2f9
more SMLish (less Haskellish) naming convention
blanchet
parents:
54925
diff
changeset

804 
(the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss') 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

805 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

806 

59594  807 
fun dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss = 
54065  808 
let 
59594  809 
val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl > `(expand_corec_code_rhs ctxt has_call []); 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

810 
val (fun_name, fun_args) = strip_comb lhs >> fst o dest_Free; 
56152  811 

59604  812 
val _ = check_fun_args ctxt concl fun_args; 
59599  813 
val _ = check_extra_frees ctxt fun_args fun_names concl; 
56152  814 

58393  815 
val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); 
54065  816 

59594  817 
val cond_ctrs = fold_rev_corec_code_rhs ctxt (fn cs => fn ctr => fn _ => 
55008
b5b2e193ca33
use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents:
55005
diff
changeset

818 
if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs) 
59594  819 
else error ("Not a constructor: " ^ quote (Syntax.string_of_term ctxt ctr))) [] rhs' [] 
54065  820 
> AList.group (op =); 
821 

54068  822 
val ctr_premss = (case cond_ctrs of [_] => [[]]  _ => map (s_dnf o snd) cond_ctrs); 
54065  823 
val ctr_concls = cond_ctrs > map (fn (ctr, _) => 
58393  824 
binder_types (fastype_of ctr) 
59594  825 
> map_index (fn (n, T) => massage_corec_code_rhs ctxt (fn _ => fn ctr' => fn args => 
59612
7ea413656b64
avoid needless 'if ... undefined' in generated theorems
blanchet
parents:
59609
diff
changeset

826 
if ctr' = ctr then nth args n else Term.dummy_pattern T) [] rhs') 
58393  827 
> curry Term.list_comb ctr 
828 
> curry HOLogic.mk_eq lhs); 

54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

829 

59594  830 
val bads = maps (filter (Term.exists_subterm (is_free_in fun_names))) ctr_premss; 
831 
val _ = null bads orelse unexpected_corec_call ctxt [eqn0] rhs; 

832 

54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

833 
val sequentials = replicate (length fun_names) false; 
54065  834 
in 
59594  835 
@{fold_map 2} (dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0 
60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

836 
(SOME (abstract_over_list fun_args rhs))) 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

837 
ctr_premss ctr_concls matchedsss 
54065  838 
end; 
839 

59594  840 
fun dissect_coeqn ctxt has_call fun_names sequentials 
54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

841 
(basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

842 
let 
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54978
diff
changeset

843 
val eqn = drop_all eqn0 
59600  844 
handle TERM _ => error_at ctxt [eqn0] "Illformed formula"; 
54065  845 
val (prems, concl) = Logic.strip_horn eqn 
57527  846 
> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop 
59607  847 
handle TERM _ => error_at ctxt [eqn] "Illformed equation"; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

848 

54065  849 
val head = concl 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

850 
> perhaps (try HOLogic.dest_not) > perhaps (try (fst o HOLogic.dest_eq)) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

851 
> head_of; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

852 

59601  853 
val rhs_opt = concl > perhaps (try HOLogic.dest_not) > try (HOLogic.dest_eq #> snd); 
59605  854 

855 
fun check_num_args () = 

856 
is_none rhs_opt orelse not (can dest_funT (fastype_of (the rhs_opt))) orelse 

857 
error_at ctxt [eqn] "Expected more arguments to function on lefthand side"; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

858 

54160  859 
val discs = maps (map #disc) basic_ctr_specss; 
860 
val sels = maps (maps #sels) basic_ctr_specss; 

861 
val ctrs = maps (map #ctr) basic_ctr_specss; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

862 
in 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

863 
if member (op =) discs head orelse 
58393  864 
(is_some rhs_opt andalso 
865 
member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso 

866 
member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt)) then 

59608  867 
(dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl 
59605  868 
matchedsss 
869 
>> single) 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

870 
else if member (op =) sels head then 
59594  871 
(null prems orelse error_at ctxt [eqn] "Unexpected condition in selector formula"; 
872 
([dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt 

57550  873 
concl], matchedsss)) 
59594  874 
else if is_some rhs_opt andalso is_Free head andalso is_free_in fun_names head then 
55343  875 
if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then 
59605  876 
(check_num_args (); 
877 
dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0 

878 
(if null prems then 

879 
SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0)))) 

880 
else 

881 
NONE) 

882 
prems concl matchedsss) 

54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

883 
else if null prems then 
59605  884 
(check_num_args (); 
885 
dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss 

886 
>> flat) 

54951
e25b4d22082b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents:
54948
diff
changeset

887 
else 
59594  888 
error_at ctxt [eqn] "Cannot mix constructor and code views" 
59600  889 
else if is_some rhs_opt then 
59607  890 
error_at ctxt [eqn] ("Illformed equation head: " ^ quote (Syntax.string_of_term ctxt head)) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

891 
else 
59607  892 
error_at ctxt [eqn] "Expected equation or discriminator formula" 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

893 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

894 

54002  895 
fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list) 
54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

896 
({fun_args, ctr_no, prems, ...} : coeqn_data_disc) = 
56858  897 
if is_none (#pred (nth ctr_specs ctr_no)) then 
898 
I 

899 
else 

54068  900 
s_conjs prems 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

901 
> curry subst_bounds (List.rev fun_args) 
55969  902 
> abs_tuple_balanced fun_args 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

903 
> K > nth_map (the (#pred (nth ctr_specs ctr_no))); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

904 

54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

905 
fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

906 
find_first (curry (op =) sel o #sel) sel_eqns 
55969  907 
> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term) 
53720  908 
> the_default undef_const 
53411  909 
> K; 
53360  910 

59594  911 
fun build_corec_args_mutual_call ctxt has_call (sel_eqns : coeqn_data_sel list) sel = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

912 
(case find_first (curry (op =) sel o #sel) sel_eqns of 
54208  913 
NONE => (I, I, I) 
914 
 SOME {fun_args, rhs_term, ... } => 

53876  915 
let 
54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

916 
val bound_Ts = List.rev (map fastype_of fun_args); 
59946  917 

54207
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

918 
fun rewrite_stop _ t = if has_call t then @{term False} else @{term True}; 
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

919 
fun rewrite_end _ t = if has_call t then undef_const else t; 
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

920 
fun rewrite_cont bound_Ts t = 
55969  921 
if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const; 
60001  922 
fun massage f _ = massage_let_if_case_corec ctxt has_call f bound_Ts rhs_term 
55969  923 
> abs_tuple_balanced fun_args; 
53876  924 
in 
54207
9296ebf40db0
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents:
54206
diff
changeset

925 
(massage rewrite_stop, massage rewrite_end, massage rewrite_cont) 
54208  926 
end); 
53360  927 

59594  928 
fun build_corec_arg_nested_call ctxt has_call (sel_eqns : coeqn_data_sel list) sel = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

929 
(case find_first (curry (op =) sel o #sel) sel_eqns of 
54208  930 
NONE => I 
931 
 SOME {fun_args, rhs_term, ...} => 

53899  932 
let 
59989  933 
fun massage_call bound_Ts U T t0 = 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

934 
let 
59946  935 
val U2 = 
936 
(case try dest_sumT U of 

937 
SOME (U1, U2) => if U1 = T then U2 else invalid_map ctxt t0 

938 
 NONE => invalid_map ctxt t0); 

939 

59948  940 
fun rewrite bound_Ts (Abs (s, T', t')) = Abs (s, T', rewrite (T' :: bound_Ts) t') 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

941 
 rewrite bound_Ts (t as _ $ _) = 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

942 
let val (u, vs) = strip_comb t in 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

943 
if is_Free u andalso has_call u then 
59946  944 
Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs 
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61348
diff
changeset

945 
else if try (fst o dest_Const) u = SOME @{const_name case_prod} then 
55343  946 
map (rewrite bound_Ts) vs > chop 1 
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61348
diff
changeset

947 
>> HOLogic.mk_case_prod o the_single 
55343  948 
> Term.list_comb 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

949 
else 
55343  950 
Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs) 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

951 
end 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

952 
 rewrite _ t = 
59946  953 
if is_Free t andalso has_call t then Inr_const T U2 $ HOLogic.unit else t; 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

954 
in 
59946  955 
rewrite bound_Ts t0 
55339
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

956 
end; 
f09037306f25
properly massage 'if's / 'case's etc. under lambdas
blanchet
parents:
55100
diff
changeset

957 

60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

958 
fun massage_noncall U T t = 
59989  959 
build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t; 
59947  960 

54097
92c5bd3b342d
prove usersupplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents:
54074
diff
changeset

961 
val bound_Ts = List.rev (map fastype_of fun_args); 
53899  962 
in 
59989  963 
fn t => 
964 
rhs_term 

60704
fdd965b35bcd
tuned ML signature (and rationalized code a bit)
blanchet
parents:
60683
diff
changeset

965 
> massage_nested_corec_call ctxt has_call massage_call (K massage_noncall) bound_Ts 
59989  966 
(range_type (fastype_of t)) (fastype_of1 (bound_Ts, rhs_term)) 
967 
> abs_tuple_balanced fun_args 

54208  968 
end); 
53360  969 

59594  970 
fun build_corec_args_sel ctxt has_call (all_sel_eqns : coeqn_data_sel list) 
54002  971 
(ctr_spec : corec_ctr_spec) = 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

972 
(case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of 
54208  973 
[] => I 
974 
 sel_eqns => 

975 
let 

976 
val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec; 

977 
val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list; 

978 
val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list; 

979 
val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list; 

980 
in 

981 
I 

982 
#> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls' 

983 
#> fold (fn (sel, (q, g, h)) => 

59594  984 
let val (fq, fg, fh) = build_corec_args_mutual_call ctxt has_call sel_eqns sel in 
54208  985 
nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls' 
986 
#> fold (fn (sel, n) => nth_map n 

59594  987 
(build_corec_arg_nested_call ctxt has_call sel_eqns sel)) nested_calls' 
54208  988 
end); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

989 

59673  990 
fun build_defs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list) 
54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

991 
(disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) = 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

992 
let 
54160  993 
val corecs = map #corec corec_specs; 
994 
val ctr_specss = map #ctr_specs corec_specs; 

53360  995 
val corec_args = hd corecs 
996 
> fst o split_last o binder_types o fastype_of 

59044  997 
> map (fn T => 
998 
if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False}) 

54806
a0f024caa04c
pass autoproved exhaustiveness properties to tactic;
panny
parents:
54628
diff
changeset

999 
else Const (@{const_name undefined}, T)) 
53720  1000 
> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss 
59594  1001 
> fold2 (fold o build_corec_args_sel ctxt has_call) sel_eqnss ctr_specss; 
59041  1002 

59599  1003 
val bad = fold (add_extra_frees ctxt [] []) corec_args []; 
1004 
val _ = null bad orelse 

1005 
(if exists has_call corec_args then nonprimitive_corec ctxt [] 

1006 
else extra_variable ctxt [] (hd bad)); 

1007 

54835  1008 
val excludess' = 
53720  1009 
disc_eqnss 
53822  1010 
> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x)) 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1011 
#> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs []) 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1012 
#> maps (uncurry (map o pair) 
53822  1013 
#> map (fn ((fun_args, c, x, a), (_, c', y, a')) => 
54068  1014 
((c, c', a orelse a'), (x, s_not (s_conjs y))) 
57527  1015 
> map_prod (map HOLogic.mk_Trueprop) HOLogic.mk_Trueprop 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1016 
> Logic.list_implies 
55342  1017 
> curry Logic.list_all (map dest_Free fun_args)))); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1018 
in 
55343  1019 
map (Term.list_comb o rpair corec_args) corecs 
59873  1020 
> map2 abs_curried_balanced arg_Tss 
59598  1021 
> (fn ts => Syntax.check_terms ctxt ts 
1022 
handle ERROR _ => nonprimitive_corec ctxt []) 

61760  1023 
> @{map 3} (fn b => fn mx => fn t => 
1024 
((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) bs mxs 

54835  1025 
> rpair excludess' 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1026 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1027 

54905
2fdec6c29eb7
don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents:
54904
diff
changeset

1028 
fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec) 
54153
67487a607ce2
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents:
54145
diff
changeset

1029 
(sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) = 
59603  1030 
let 
1031 
val fun_name = Binding.name_of fun_binding; 

1032 
val num_disc_eqns = length disc_eqns; 

1033 
val num_ctrs = length ctr_specs; 

1034 
in 

1035 
if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> num_ctrs  1 then 

1036 
(num_disc_eqns > 0 orelse error ("Missing discriminator formula for " ^ quote fun_name); 

1037 
disc_eqns) 

54910  1038 
else 
1039 
let 

59603  1040 
val ctr_no = 0 upto length ctr_specs 
55342  1041 
> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns)); 
59603  1042 
val {ctr, disc, ...} = nth ctr_specs ctr_no; 
58393  1043 
val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns; 
1044 

1045 
val fun_T = arg_Ts > body_type (fastype_of (#ctr (hd ctr_specs))); 

54910  1046 
val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) 
1047 
> the_default (map (curry Free Name.uu) arg_Ts) o merge_options; 

58393  1048 
val prems = maps (s_not_conj o #prems) disc_eqns; 
1049 
val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt > the_default NONE; 

1050 
val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt > the_default NONE; 

61760  1051 
val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt 
1052 
> the_default 100000; (* FIXME *) 

58393  1053 

1054 
val extra_disc_eqn = 

59603  1055 
{fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no, 
58393  1056 
disc = disc, prems = prems, auto_gen = true, ctr_rhs_opt = ctr_rhs_opt, 
1057 
code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = undef_const}; 

54910  1058 
in 
59603  1059 
chop ctr_no disc_eqns > cons extra_disc_eqn > op @ 
54910  1060 
end 
1061 
end; 

53720  1062 

55100  1063 
fun find_corec_calls ctxt has_call (basic_ctr_specs : basic_corec_ctr_spec list) 
1064 
({ctr, sel, rhs_term, ...} : coeqn_data_sel) = 

54160  1065 
let 
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1066 
val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs 
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54921
diff
changeset

1067 
> find_index (curry (op =) sel) o #sels o the; 
54160  1068 
in 
55341
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

1069 
K (if has_call rhs_term then fold_rev_let_if_case ctxt (K cons) [] rhs_term [] else []) 
3d2c97392e25
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents:
55339
diff
changeset

1070 
> nth_map sel_no > AList.map_entry (op =) ctr 
54160  1071 
end; 
1072 

54900  1073 
fun applied_fun_of fun_name fun_T fun_args = 
55343  1074 
Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args  1 downto 0)); 
54900  1075 

54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1076 
fun is_trivial_implies thm = 
54967
78de75e3e52a
exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial
blanchet
parents:
54959
diff
changeset

1077 
uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm)); 
54921
862c36b6e57c
avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents:
54917
diff
changeset

1078 

60003  1079 
fun primcorec_ursive auto opts fixes specs of_specs_opt lthy = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1080 
let 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

1081 
val thy = Proof_Context.theory_of lthy; 
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

1082 

53352  1083 
val (bs, mxs) = map_split (apfst fst) fixes; 
55969  1084 
val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes > split_list; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1085 

56254  1086 
val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

1087 
[] => () 
59594  1088 
 (b, _) :: _ => error ("Type of " ^ Binding.print b ^ " contains top sort")); 
54272
9d623cada37f
avoid subtle failure in the presence of top sort
blanchet
parents:
54271
diff
changeset

1089 

54902
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

1090 
val actual_nn = length bs; 
a9291e4d2366
internally allow different values for 'sequential' for different constructors
blanchet
parents:
54901
diff
changeset

1091 

59281  1092 
val plugins = get_first (fn Plugins_Option f => SOME (f lthy)  _ => NONE) (rev opts) 
1093 
> the_default Plugin_Name.default_filter; 

1094 
val sequentials = replicate actual_nn (exists (can (fn Sequential_Option => ())) opts); 

1095 
val exhaustives = replicate actual_nn (exists (can (fn Exhaustive_Option => ())) opts); 

1096 
val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts); 

54591
c822230fd22b
prevent exception when equations for a function are missing;
panny
parents:
54279
diff
changeset

1097 

54160  1098 
val fun_names = map Binding.name_of bs; 
62497
5b5b704f4811
respect qualification when noting theorems in prim(co)rec
traytel
parents:
62318
diff
changeset

1099 
val qualifys = map (fold_rev (uncurry Binding.qualify o swap) o Binding.path_of) bs; 
54160  1100 
val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

1101 
val frees = map (fst #>> Binding.name_of #> Free) fixes; 
59594  1102 
val has_call = Term.exists_subterm (member (op =) frees); 
54160  1103 
val eqns_data = 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58462
diff
changeset

1104 
@{fold_map 2} (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) 
55871  1105 
(tag_list 0 (map snd specs)) of_specs_opt [] 
54160  1106 
> flat o fst; 
1107 

59662  1108 
val missing = fun_names 
1109 
> filter (map (fn Disc x => #fun_name x  Sel x => #fun_name x) eqns_data 

1110 
> not oo member (op =)); 

1111 
val _ = null missing orelse error ("Missing equations for " ^ commas missing); 

56152  1112 

54160  1113 
val callssss = 
1114 
map_filter (try (fn Sel x => x)) eqns_data 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59044
diff
changeset

1115 
> partition_eq (op = o apply2 #fun_name) 
54160  1116 
> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 
54161  1117 
> map (flat o snd) 
54243  1118 
> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss 
54160  1119 
> map2 (curry (op >)) (map (map (fn {ctr, sels, ...} => 
1120 
(ctr, map (K []) sels))) basic_ctr_specss); 

1121 

59603  1122 
val (corec_specs0, _, coinduct_thm, coinduct_strong_thm, coinduct_thms, coinduct_strong_thms, 
61334
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
61301
diff
changeset

1123 
(coinduct_attrs, common_coinduct_attrs), n2m, lthy) = 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset

1124 
corec_specs_of bs arg_Ts res_Ts frees callssss lthy; 
59603  1125 
val corec_specs = take actual_nn corec_specs0; 
54178  1126 
val ctr_specss = map #ctr_specs corec_specs; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

1127 

59603  1128 
val disc_eqnss0 = map_filter (try (fn Disc x => x)) eqns_data 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59044
diff
changeset

1129 
> partition_eq (op = o apply2 #fun_name) 
53720  1130 
> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59044
diff
changeset

1131 
> map (sort (op < o apply2 #ctr_no > make_ord) o flat o snd); 
56152  1132 

59603  1133 
val _ = disc_eqnss0 > map (fn x => 
59602  1134 
let val dups = duplicates (op = o apply2 #ctr_no) x in 
1135 
null dups orelse 

59600  1136 
error_at lthy 
59602  1137 
(maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) dups 
59600  1138 
> map (fn {ctr_rhs_opt = SOME t, ...} => t  {user_eqn, ...} => user_eqn)) 
59606  1139 
"Overspecified case(s)" 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59044
diff
changeset

1140 
end); 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1141 

8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1142 
val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59044
diff
changeset

1143 
> partition_eq (op = o apply2 #fun_name) 
53720  1144 
> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1145 
> map (flat o snd); 
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1146 

59602  1147 
val _ = sel_eqnss > map (fn x => 
1148 
let val dups = duplicates (op = o apply2 ctr_sel_of) x in 

1149 
null dups orelse 

1150 
error_at lthy 

1151 
(maps (fn t => filter (curry (op =) (ctr_sel_of t) o ctr_sel_of) x) dups 

1152 
> map (fn {ctr_rhs_opt = SOME t, ...} => t  {user_eqn, ...} => user_eqn)) 

59606  1153 
"Overspecified case(s)" 
59602  1154 
end); 
1155 

53360  1156 
val arg_Tss = map (binder_types o snd o fst) fixes; 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58462
diff
changeset

1157 
val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss 
59603  1158 
disc_eqnss0; 
54835  1159 
val (defs, excludess') = 
61334
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
61301
diff
changeset

1160 
build_defs lthy bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; 
53654
8b9ea4420f81
prove simp theorems for newly generated definitions
panny
parents:
53411
diff
changeset

1161 

55009
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1162 
val tac_opts = 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1163 
map (fn {code_rhs_opt, ...} :: _ => 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1164 
if auto orelse is_some code_rhs_opt then SOME (auto_tac o #context) else NONE) disc_eqnss; 
d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1165 

d4b69107a86a
automatically solve proof obligations produced for code equations
blanchet
parents:
55008
diff
changeset

1166 
fun exclude_tac tac_opt sequential (c, c', a) = 
54901
0b8871677e0b
use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents:
54900
diff
changeset

1167 