author  blanchet 
Thu, 24 May 2012 17:46:35 +0200  
changeset 47990  7a642e5c272c 
parent 47909  5f1afeebafbc 
child 48811  d1688612668d 
permissions  rwrr 
33978
2380c1dac86e
fix soundness bug in Nitpick's "destroy_constrs" optimization
blanchet
parents:
33968
diff
changeset

1 
(* Title: HOL/Tools/Nitpick/nitpick_hol.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Auxiliary HOLrelated functions used by Nitpick. 

6 
*) 

7 

8 
signature NITPICK_HOL = 

9 
sig 

33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33583
diff
changeset

10 
type styp = Nitpick_Util.styp 
33192  11 
type const_table = term list Symtab.table 
12 
type special_fun = (styp * int list * term list) * styp 

13 
type unrolled = styp * styp 

14 
type wf_cache = (styp * (bool * bool)) list 

15 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

16 
type hol_context = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

17 
{thy: theory, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

18 
ctxt: Proof.context, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

19 
max_bisim_depth: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

20 
boxes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

21 
stds: (typ option * bool) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

22 
wfs: (styp option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

23 
user_axioms: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

24 
debug: bool, 
38209  25 
whacks: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

26 
binary_ints: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

27 
destroy_constrs: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

28 
specialize: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

29 
star_linear_preds: bool, 
41871
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41860
diff
changeset

30 
total_consts: bool option, 
41876  31 
needs: term list option, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

32 
tac_timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

33 
evals: term list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

34 
case_names: (string * int) list, 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

35 
def_tables: const_table * const_table, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

36 
nondef_table: const_table, 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42414
diff
changeset

37 
nondefs: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

38 
simp_table: const_table Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

39 
psimp_table: const_table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

40 
choice_spec_table: const_table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

41 
intro_table: const_table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

42 
ground_thm_table: term list Inttab.table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

43 
ersatz_table: (string * string) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

44 
skolems: (string * string list) list Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

45 
special_funs: special_fun list Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

46 
unrolled_preds: unrolled list Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

47 
wf_cache: wf_cache Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

48 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  49 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

50 
datatype fixpoint_kind = Lfp  Gfp  NoFp 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

51 
datatype boxability = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

52 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

53 

33192  54 
val name_sep : string 
55 
val numeral_prefix : string 

35718  56 
val base_prefix : string 
57 
val step_prefix : string 

58 
val unrolled_prefix : string 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

59 
val ubfp_prefix : string 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

60 
val lbfp_prefix : string 
35311  61 
val quot_normal_prefix : string 
33192  62 
val skolem_prefix : string 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

63 
val special_prefix : string 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

64 
val uncurry_prefix : string 
33192  65 
val eval_prefix : string 
35718  66 
val iter_var_prefix : string 
67 
val strip_first_name_sep : string > string * string 

33192  68 
val original_name : string > string 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37269
diff
changeset

69 
val abs_var : indexname * typ > term > term 
34998  70 
val s_conj : term * term > term 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

71 
val s_disj : term * term > term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

72 
val strip_any_connective : term > term list * term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

73 
val conjuncts_of : term > term list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

74 
val disjuncts_of : term > term list 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

75 
val unarize_unbox_etc_type : typ > typ 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

76 
val uniterize_unarize_unbox_etc_type : typ > typ 
33192  77 
val string_for_type : Proof.context > typ > string 
38188  78 
val pretty_for_type : Proof.context > typ > Pretty.T 
33192  79 
val prefix_name : string > string > string 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

80 
val shortest_name : string > string 
33192  81 
val short_name : string > string 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

82 
val shorten_names_in_term : term > term 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

83 
val strict_type_match : theory > typ * typ > bool 
33192  84 
val type_match : theory > typ * typ > bool 
85 
val const_match : theory > styp * styp > bool 

86 
val term_match : theory > term * term > bool 

35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

87 
val frac_from_term_pair : typ > term > term > term 
33192  88 
val is_TFree : typ > bool 
89 
val is_fun_type : typ > bool 

46115  90 
val is_set_type : typ > bool 
91 
val is_fun_or_set_type : typ > bool 

46081
8f6465f7021b
ported mono calculus to handle "set" type constructors
blanchet
parents:
45980
diff
changeset

92 
val is_set_like_type : typ > bool 
33192  93 
val is_pair_type : typ > bool 
94 
val is_lfp_iterator_type : typ > bool 

95 
val is_gfp_iterator_type : typ > bool 

96 
val is_fp_iterator_type : typ > bool 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

97 
val is_iterator_type : typ > bool 
33192  98 
val is_boolean_type : typ > bool 
99 
val is_integer_type : typ > bool 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

100 
val is_bit_type : typ > bool 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

101 
val is_word_type : typ > bool 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

102 
val is_integer_like_type : typ > bool 
33192  103 
val is_record_type : typ > bool 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

104 
val is_number_type : Proof.context > typ > bool 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

105 
val is_higher_order_type : typ > bool 
46081
8f6465f7021b
ported mono calculus to handle "set" type constructors
blanchet
parents:
45980
diff
changeset

106 
val elem_type : typ > typ 
46083  107 
val pseudo_domain_type : typ > typ 
108 
val pseudo_range_type : typ > typ 

33192  109 
val const_for_iterator_type : typ > styp 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

110 
val strip_n_binders : int > typ > typ list * typ 
33192  111 
val nth_range_type : int > typ > typ 
112 
val num_factors_in_type : typ > int 

113 
val num_binder_types : typ > int 

114 
val curried_binder_types : typ > typ list 

115 
val mk_flat_tuple : typ > term list > term 

116 
val dest_n_tuple : int > term > term list 

33978
2380c1dac86e
fix soundness bug in Nitpick's "destroy_constrs" optimization
blanchet
parents:
33968
diff
changeset

117 
val is_real_datatype : theory > string > bool 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

118 
val is_standard_datatype : theory > (typ option * bool) list > typ > bool 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

119 
val is_codatatype : Proof.context > typ > bool 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

120 
val is_quot_type : Proof.context > typ > bool 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

121 
val is_pure_typedef : Proof.context > typ > bool 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

122 
val is_univ_typedef : Proof.context > typ > bool 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

123 
val is_datatype : Proof.context > (typ option * bool) list > typ > bool 
33192  124 
val is_record_constr : styp > bool 
125 
val is_record_get : theory > styp > bool 

126 
val is_record_update : theory > styp > bool 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

127 
val is_abs_fun : Proof.context > styp > bool 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

128 
val is_rep_fun : Proof.context > styp > bool 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

129 
val is_quot_abs_fun : Proof.context > styp > bool 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

130 
val is_quot_rep_fun : Proof.context > styp > bool 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

131 
val mate_of_rep_fun : Proof.context > styp > styp 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

132 
val is_constr_like : Proof.context > styp > bool 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

133 
val is_constr : Proof.context > (typ option * bool) list > styp > bool 
33192  134 
val is_sel : string > bool 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

135 
val is_sel_like_and_no_discr : string > bool 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

136 
val box_type : hol_context > boxability > typ > typ 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

137 
val binarize_nat_and_int_in_type : typ > typ 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

138 
val binarize_nat_and_int_in_term : term > term 
33192  139 
val discr_for_constr : styp > styp 
140 
val num_sels_for_constr_type : typ > int 

141 
val nth_sel_name_for_constr_name : string > int > string 

142 
val nth_sel_for_constr : styp > int > styp 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

143 
val binarized_and_boxed_nth_sel_for_constr : 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

144 
hol_context > bool > styp > int > styp 
33192  145 
val sel_no_from_name : string > int 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

146 
val close_form : term > term 
33192  147 
val distinctness_formula : typ > term list > term 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

148 
val register_frac_type : 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

149 
string > (string * string) list > morphism > Context.generic 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

150 
> Context.generic 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

151 
val register_frac_type_global : 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

152 
string > (string * string) list > theory > theory 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

153 
val unregister_frac_type : 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

154 
string > morphism > Context.generic > Context.generic 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

155 
val unregister_frac_type_global : string > theory > theory 
44012  156 
val register_ersatz : 
157 
(string * string) list > morphism > Context.generic > Context.generic 

158 
val register_ersatz_global : (string * string) list > theory > theory 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

159 
val register_codatatype : 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

160 
typ > string > styp list > morphism > Context.generic > Context.generic 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

161 
val register_codatatype_global : 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

162 
typ > string > styp list > theory > theory 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

163 
val unregister_codatatype : 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

164 
typ > morphism > Context.generic > Context.generic 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

165 
val unregister_codatatype_global : typ > theory > theory 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

166 
val datatype_constrs : hol_context > typ > styp list 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

167 
val binarized_and_boxed_datatype_constrs : 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

168 
hol_context > bool > typ > styp list 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

169 
val num_datatype_constrs : hol_context > typ > int 
33192  170 
val constr_name_for_sel_like : string > string 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

171 
val binarized_and_boxed_constr_for_sel : hol_context > bool > styp > styp 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

172 
val card_of_type : (typ * int) list > typ > int 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

173 
val bounded_card_of_type : int > int > (typ * int) list > typ > int 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

174 
val bounded_exact_card_of_type : 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

175 
hol_context > typ list > int > int > (typ * int) list > typ > int 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

176 
val typical_card_of_type : typ > int 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

177 
val is_finite_type : hol_context > typ > bool 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

178 
val is_special_eligible_arg : bool > typ list > term > bool 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

179 
val s_let : 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

180 
typ list > string > int > typ > typ > (term > term) > term > term 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

181 
val s_betapply : typ list > term * term > term 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

182 
val s_betapplys : typ list > term * term list > term 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

183 
val discriminate_value : hol_context > styp > term > term 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

184 
val select_nth_constr_arg : 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

185 
Proof.context > (typ option * bool) list > styp > term > int > typ 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

186 
> term 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

187 
val construct_value : 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

188 
Proof.context > (typ option * bool) list > styp > term list > term 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

189 
val coerce_term : hol_context > typ list > typ > typ > term > term 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

190 
val special_bounds : term list > (indexname * typ) list 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

191 
val is_funky_typedef : Proof.context > typ > bool 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42414
diff
changeset

192 
val all_defs_of : theory > (term * term) list > term list 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42414
diff
changeset

193 
val all_nondefs_of : Proof.context > (term * term) list > term list 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

194 
val arity_of_built_in_const : 
39359  195 
theory > (typ option * bool) list > styp > int option 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

196 
val is_built_in_const : 
39359  197 
theory > (typ option * bool) list > styp > bool 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

198 
val term_under_def : term > term 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

199 
val case_const_names : 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

200 
Proof.context > (typ option * bool) list > (string * int) list 
35718  201 
val unfold_defs_in_term : hol_context > term > term 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

202 
val const_def_tables : 
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

203 
Proof.context > (term * term) list > term list 
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

204 
> const_table * const_table 
33192  205 
val const_nondef_table : term list > const_table 
35335  206 
val const_simp_table : Proof.context > (term * term) list > const_table 
207 
val const_psimp_table : Proof.context > (term * term) list > const_table 

35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35743
diff
changeset

208 
val const_choice_spec_table : 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35743
diff
changeset

209 
Proof.context > (term * term) list > const_table 
35335  210 
val inductive_intro_table : 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

211 
Proof.context > (term * term) list > const_table * const_table 
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

212 
> const_table 
33192  213 
val ground_theorem_table : theory > term list Inttab.table 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

214 
val ersatz_table : Proof.context > (string * string) list 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

215 
val add_simps : const_table Unsynchronized.ref > string > term list > unit 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

216 
val inverse_axioms_for_rep_fun : Proof.context > styp > term list 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

217 
val optimized_typedef_axioms : Proof.context > string * typ list > term list 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

218 
val optimized_quot_type_axioms : 
35311  219 
Proof.context > (typ option * bool) list > string * typ list > term list 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

220 
val def_of_const : theory > const_table * const_table > styp > term option 
35718  221 
val fixpoint_kind_of_rhs : term > fixpoint_kind 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

222 
val fixpoint_kind_of_const : 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

223 
theory > const_table * const_table > string * typ > fixpoint_kind 
38205
37a7272cb453
handle inductive predicates correctly after change in "def" semantics
blanchet
parents:
38204
diff
changeset

224 
val is_real_inductive_pred : hol_context > styp > bool 
41994
c567c860caf6
always destroy constructor patterns, since this seems to be always useful
blanchet
parents:
41898
diff
changeset

225 
val is_constr_pattern : Proof.context > term > bool 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

226 
val is_constr_pattern_lhs : Proof.context > term > bool 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

227 
val is_constr_pattern_formula : Proof.context > term > bool 
35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35743
diff
changeset

228 
val nondef_props_for_const : 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35743
diff
changeset

229 
theory > bool > const_table > styp > term list 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35743
diff
changeset

230 
val is_choice_spec_fun : hol_context > styp > bool 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35743
diff
changeset

231 
val is_choice_spec_axiom : theory > const_table > term > bool 
38205
37a7272cb453
handle inductive predicates correctly after change in "def" semantics
blanchet
parents:
38204
diff
changeset

232 
val is_real_equational_fun : hol_context > styp > bool 
38202
379fb08da97b
prevent the expansion of too large definitions  use equations for these instead
blanchet
parents:
38201
diff
changeset

233 
val is_equational_fun_but_no_plain_def : hol_context > styp > bool 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

234 
val codatatype_bisim_axioms : hol_context > typ > term list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

235 
val is_well_founded_inductive_pred : hol_context > styp > bool 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

236 
val unrolled_inductive_pred_const : hol_context > bool > styp > term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

237 
val equational_fun_axioms : hol_context > styp > term list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

238 
val is_equational_fun_surely_complete : hol_context > styp > bool 
38212
a7e92239922f
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
blanchet
parents:
38209
diff
changeset

239 
val merged_type_var_table_for_terms : 
a7e92239922f
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
blanchet
parents:
38209
diff
changeset

240 
theory > term list > (sort * string) list 
a7e92239922f
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
blanchet
parents:
38209
diff
changeset

241 
val merge_type_vars_in_term : 
a7e92239922f
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
blanchet
parents:
38209
diff
changeset

242 
theory > bool > (sort * string) list > term > term 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

243 
val ground_types_in_type : hol_context > bool > typ > typ list 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

244 
val ground_types_in_terms : hol_context > bool > term list > typ list 
33192  245 
end; 
246 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

247 
structure Nitpick_HOL : NITPICK_HOL = 
33192  248 
struct 
249 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

250 
open Nitpick_Util 
33192  251 

252 
type const_table = term list Symtab.table 

253 
type special_fun = (styp * int list * term list) * styp 

254 
type unrolled = styp * styp 

255 
type wf_cache = (styp * (bool * bool)) list 

256 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

257 
type hol_context = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

258 
{thy: theory, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

259 
ctxt: Proof.context, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

260 
max_bisim_depth: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

261 
boxes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

262 
stds: (typ option * bool) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

263 
wfs: (styp option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

264 
user_axioms: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

265 
debug: bool, 
38209  266 
whacks: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

267 
binary_ints: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

268 
destroy_constrs: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

269 
specialize: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

270 
star_linear_preds: bool, 
41871
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41860
diff
changeset

271 
total_consts: bool option, 
41876  272 
needs: term list option, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

273 
tac_timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

274 
evals: term list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

275 
case_names: (string * int) list, 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

276 
def_tables: const_table * const_table, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

277 
nondef_table: const_table, 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42414
diff
changeset

278 
nondefs: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

279 
simp_table: const_table Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

280 
psimp_table: const_table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

281 
choice_spec_table: const_table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

282 
intro_table: const_table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

283 
ground_thm_table: term list Inttab.table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

284 
ersatz_table: (string * string) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

285 
skolems: (string * string list) list Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

286 
special_funs: special_fun list Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

287 
unrolled_preds: unrolled list Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

288 
wf_cache: wf_cache Unsynchronized.ref, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

289 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  290 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

291 
datatype fixpoint_kind = Lfp  Gfp  NoFp 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

292 
datatype boxability = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

293 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

294 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41052
diff
changeset

295 
structure Data = Generic_Data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41052
diff
changeset

296 
( 
33192  297 
type T = {frac_types: (string * (string * string) list) list, 
44012  298 
ersatz_table: (string * string) list, 
33192  299 
codatatypes: (string * (string * styp list)) list} 
44012  300 
val empty = {frac_types = [], ersatz_table = [], codatatypes = []} 
33192  301 
val extend = I 
44012  302 
fun merge ({frac_types = fs1, ersatz_table = et1, codatatypes = cs1}, 
303 
{frac_types = fs2, ersatz_table = et2, codatatypes = cs2}) : T = 

33699
f33b036ef318
permissive AList.merge  most likely setup for theory data (beware of spurious AList.DUP);
wenzelm
parents:
33583
diff
changeset

304 
{frac_types = AList.merge (op =) (K true) (fs1, fs2), 
44012  305 
ersatz_table = AList.merge (op =) (K true) (et1, et2), 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41052
diff
changeset

306 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)} 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41052
diff
changeset

307 
) 
33192  308 

309 
val name_sep = "$" 

310 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

311 
val sel_prefix = nitpick_prefix ^ "sel" 

312 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

313 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

314 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

315 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

316 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

317 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

318 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

319 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

320 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

35311  321 
val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep 
33192  322 
val skolem_prefix = nitpick_prefix ^ "sk" 
323 
val special_prefix = nitpick_prefix ^ "sp" 

324 
val uncurry_prefix = nitpick_prefix ^ "unc" 

325 
val eval_prefix = nitpick_prefix ^ "eval" 

326 
val iter_var_prefix = "i" 

35718  327 

328 
(** Constant/type information and term/type manipulation **) 

33192  329 

330 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

35311  331 
fun quot_normal_name_for_type ctxt T = 
332 
quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T) 

33192  333 

334 
val strip_first_name_sep = 

335 
Substring.full #> Substring.position name_sep ##> Substring.triml 1 

336 
#> pairself Substring.string 

337 
fun original_name s = 

338 
if String.isPrefix nitpick_prefix s then 

339 
case strip_first_name_sep s of (s1, "") => s1  (_, s2) => original_name s2 

340 
else 

341 
s 

35718  342 

34998  343 
fun s_conj (t1, @{const True}) = t1 
344 
 s_conj (@{const True}, t2) = t2 

345 
 s_conj (t1, t2) = 

346 
if t1 = @{const False} orelse t2 = @{const False} then @{const False} 

347 
else HOLogic.mk_conj (t1, t2) 

348 
fun s_disj (t1, @{const False}) = t1 

349 
 s_disj (@{const False}, t2) = t2 

350 
 s_disj (t1, t2) = 

351 
if t1 = @{const True} orelse t2 = @{const True} then @{const True} 

352 
else HOLogic.mk_disj (t1, t2) 

353 

354 
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) = 

355 
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t] 

356 
 strip_connective _ t = [t] 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

357 
fun strip_any_connective (t as (t0 $ _ $ _)) = 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

358 
if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then 
34998  359 
(strip_connective t0 t, t0) 
360 
else 

361 
([t], @{const Not}) 

362 
 strip_any_connective t = ([t], @{const Not}) 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

363 
val conjuncts_of = strip_connective @{const HOL.conj} 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

364 
val disjuncts_of = strip_connective @{const HOL.disj} 
34998  365 

33192  366 
(* When you add constants to these lists, make sure to handle them in 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

367 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  368 
well. *) 
369 
val built_in_consts = 

370 
[(@{const_name all}, 1), 

371 
(@{const_name "=="}, 2), 

372 
(@{const_name "==>"}, 2), 

373 
(@{const_name Pure.conjunction}, 2), 

374 
(@{const_name Trueprop}, 1), 

375 
(@{const_name Not}, 1), 

376 
(@{const_name False}, 0), 

377 
(@{const_name True}, 0), 

378 
(@{const_name All}, 1), 

379 
(@{const_name Ex}, 1), 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

380 
(@{const_name HOL.eq}, 1), 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

381 
(@{const_name HOL.conj}, 2), 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

382 
(@{const_name HOL.disj}, 2), 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38652
diff
changeset

383 
(@{const_name HOL.implies}, 2), 
33192  384 
(@{const_name If}, 3), 
385 
(@{const_name Let}, 2), 

386 
(@{const_name Pair}, 2), 

387 
(@{const_name fst}, 1), 

388 
(@{const_name snd}, 1), 

46083  389 
(@{const_name Set.member}, 2), 
390 
(@{const_name Collect}, 1), 

33192  391 
(@{const_name Id}, 0), 
392 
(@{const_name converse}, 1), 

393 
(@{const_name trancl}, 1), 

47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47109
diff
changeset

394 
(@{const_name relcomp}, 2), 
33192  395 
(@{const_name finite}, 1), 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

396 
(@{const_name unknown}, 0), 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

397 
(@{const_name is_unknown}, 1), 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

398 
(@{const_name safe_The}, 1), 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

399 
(@{const_name Nitpick.Frac}, 0), 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

400 
(@{const_name Nitpick.norm_frac}, 0)] 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

401 
val built_in_nat_consts = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

402 
[(@{const_name Suc}, 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

403 
(@{const_name nat}, 0), 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

404 
(@{const_name Nitpick.nat_gcd}, 0), 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

405 
(@{const_name Nitpick.nat_lcm}, 0)] 
33192  406 
val built_in_typed_consts = 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

407 
[((@{const_name zero_class.zero}, int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

408 
((@{const_name one_class.one}, int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

409 
((@{const_name plus_class.plus}, int_T > int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

410 
((@{const_name minus_class.minus}, int_T > int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

411 
((@{const_name times_class.times}, int_T > int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

412 
((@{const_name div_class.div}, int_T > int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

413 
((@{const_name uminus_class.uminus}, int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

414 
((@{const_name ord_class.less}, int_T > int_T > bool_T), 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

415 
((@{const_name ord_class.less_eq}, int_T > int_T > bool_T), 2)] 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

416 
val built_in_typed_nat_consts = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

417 
[((@{const_name zero_class.zero}, nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

418 
((@{const_name one_class.one}, nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

419 
((@{const_name plus_class.plus}, nat_T > nat_T > nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

420 
((@{const_name minus_class.minus}, nat_T > nat_T > nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

421 
((@{const_name times_class.times}, nat_T > nat_T > nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

422 
((@{const_name div_class.div}, nat_T > nat_T > nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

423 
((@{const_name ord_class.less}, nat_T > nat_T > bool_T), 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

424 
((@{const_name ord_class.less_eq}, nat_T > nat_T > bool_T), 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

425 
((@{const_name of_nat}, nat_T > int_T), 0)] 
46081
8f6465f7021b
ported mono calculus to handle "set" type constructors
blanchet
parents:
45980
diff
changeset

426 
val built_in_set_like_consts = 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37269
diff
changeset

427 
[(@{const_name ord_class.less_eq}, 2)] 
33192  428 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

429 
fun unarize_type @{typ "unsigned_bit word"} = nat_T 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

430 
 unarize_type @{typ "signed_bit word"} = int_T 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

431 
 unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

432 
 unarize_type T = T 
41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41049
diff
changeset

433 
fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

434 
unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

435 
 unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) = 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38188
diff
changeset

436 
Type (@{type_name prod}, map unarize_unbox_etc_type Ts) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

437 
 unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

438 
 unarize_unbox_etc_type @{typ "signed_bit word"} = int_T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

439 
 unarize_unbox_etc_type (Type (s, Ts as _ :: _)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

440 
Type (s, map unarize_unbox_etc_type Ts) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

441 
 unarize_unbox_etc_type T = T 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

442 
fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

443 
 uniterize_type @{typ bisim_iterator} = nat_T 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

444 
 uniterize_type T = T 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

445 
val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

446 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

447 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type 
38188  448 
fun pretty_for_type ctxt = Syntax.pretty_typ ctxt o unarize_unbox_etc_type 
33192  449 

450 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

451 
fun shortest_name s = List.last (space_explode "." s) handle List.Empty => "" 
33192  452 
val prefix_abs_vars = Term.map_abs_vars o prefix_name 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

453 
fun short_name s = 
33192  454 
case space_explode name_sep s of 
455 
[_] => s > String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

456 
 ss => map shortest_name ss > space_implode "_" 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

457 
fun shorten_names_in_type (Type (s, Ts)) = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

458 
Type (short_name s, map shorten_names_in_type Ts) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

459 
 shorten_names_in_type T = T 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

460 
val shorten_names_in_term = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

461 
map_aterms (fn Const (s, T) => Const (short_name s, T)  t => t) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

462 
#> map_types shorten_names_in_type 
33192  463 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

464 
fun strict_type_match thy (T1, T2) = 
33192  465 
(Sign.typ_match thy (T2, T1) Vartab.empty; true) 
466 
handle Type.TYPE_MATCH => false 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

467 
fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type 
33192  468 
fun const_match thy ((s1, T1), (s2, T2)) = 
469 
s1 = s2 andalso type_match thy (T1, T2) 

470 
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2) 

471 
 term_match thy (Free (s1, T1), Free (s2, T2)) = 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

472 
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

473 
 term_match _ (t1, t2) = t1 aconv t2 
33192  474 

35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

475 
fun frac_from_term_pair T t1 t2 = 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

476 
case snd (HOLogic.dest_number t1) of 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

477 
0 => HOLogic.mk_number T 0 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

478 
 n1 => case snd (HOLogic.dest_number t2) of 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

479 
1 => HOLogic.mk_number T n1 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

480 
 n2 => Const (@{const_name divide}, T > T > T) 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

481 
$ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35671
diff
changeset

482 

33192  483 
fun is_TFree (TFree _) = true 
484 
 is_TFree _ = false 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

485 
fun is_fun_type (Type (@{type_name fun}, _)) = true 
33192  486 
 is_fun_type _ = false 
46115  487 
fun is_set_type (Type (@{type_name set}, _)) = true 
488 
 is_set_type _ = false 

489 
val is_fun_or_set_type = is_fun_type orf is_set_type 

490 
fun is_set_like_type (Type (@{type_name fun}, [_, T'])) = 

491 
(body_type T' = bool_T) 

46081
8f6465f7021b
ported mono calculus to handle "set" type constructors
blanchet
parents:
45980
diff
changeset

492 
 is_set_like_type (Type (@{type_name set}, _)) = true 
8f6465f7021b
ported mono calculus to handle "set" type constructors
blanchet
parents:
45980
diff
changeset

493 
 is_set_like_type _ = false 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38188
diff
changeset

494 
fun is_pair_type (Type (@{type_name prod}, _)) = true 
33192  495 
 is_pair_type _ = false 
496 
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s 

497 
 is_lfp_iterator_type _ = false 

498 
fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s 

499 
 is_gfp_iterator_type _ = false 

500 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

501 
fun is_iterator_type T = 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

502 
(T = @{typ bisim_iterator} orelse is_fp_iterator_type T) 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

503 
fun is_boolean_type T = (T = prop_T orelse T = bool_T) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

504 
fun is_integer_type T = (T = nat_T orelse T = int_T) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

505 
fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit}) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

506 
fun is_word_type (Type (@{type_name word}, _)) = true 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

507 
 is_word_type _ = false 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

508 
val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type 
33192  509 
val is_record_type = not o null o Record.dest_recTs 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

510 
fun is_frac_type ctxt (Type (s, [])) = 
44012  511 
s > AList.defined (op =) (#frac_types (Data.get (Context.Proof ctxt))) 
33192  512 
 is_frac_type _ _ = false 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

513 
fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

514 
fun is_higher_order_type (Type (@{type_name fun}, _)) = true 
46115  515 
 is_higher_order_type (Type (@{type_name set}, _)) = true 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

516 
 is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

517 
 is_higher_order_type _ = false 
33192  518 

46083  519 
fun elem_type (Type (@{type_name set}, [T'])) = T' 
46081
8f6465f7021b
ported mono calculus to handle "set" type constructors
blanchet
parents:
45980
diff
changeset

520 
 elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], []) 
46083  521 
fun pseudo_domain_type (Type (@{type_name fun}, [T1, _])) = T1 
522 
 pseudo_domain_type T = elem_type T 

523 
fun pseudo_range_type (Type (@{type_name fun}, [_, T2])) = T2 

524 
 pseudo_range_type (Type (@{type_name set}, _)) = bool_T 

525 
 pseudo_range_type T = raise TYPE ("Nitpick_HOL.pseudo_range_type", [T], []) 

46081
8f6465f7021b
ported mono calculus to handle "set" type constructors
blanchet
parents:
45980
diff
changeset

526 

33192  527 
fun iterator_type_for_const gfp (s, T) = 
528 
Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s, 

529 
binder_types T) 

35718  530 
fun const_for_iterator_type (Type (s, Ts)) = 
531 
(strip_first_name_sep s > snd, Ts > bool_T) 

33192  532 
 const_for_iterator_type T = 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

533 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  534 

535 
fun strip_n_binders 0 T = ([], T) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

536 
 strip_n_binders n (Type (@{type_name fun}, [T1, T2])) = 
33192  537 
strip_n_binders (n  1) T2 >> cons T1 
538 
 strip_n_binders n (Type (@{type_name fun_box}, Ts)) = 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

539 
strip_n_binders n (Type (@{type_name fun}, Ts)) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

540 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  541 
val nth_range_type = snd oo strip_n_binders 
542 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38188
diff
changeset

543 
fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) = 
33192  544 
fold (Integer.add o num_factors_in_type) [T1, T2] 0 
545 
 num_factors_in_type _ = 1 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

546 
fun num_binder_types (Type (@{type_name fun}, [_, T2])) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

547 
1 + num_binder_types T2 
33192  548 
 num_binder_types _ = 0 
549 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

550 
fun maybe_curried_binder_types T = 

551 
(if is_pair_type (body_type T) then binder_types else curried_binder_types) T 

552 

553 
fun mk_flat_tuple _ [t] = t 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38188
diff
changeset

554 
 mk_flat_tuple (Type (@{type_name prod}, [T1, T2])) (t :: ts) = 
33192  555 
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

556 
 mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts) 
33192  557 
fun dest_n_tuple 1 t = [t] 
558 
 dest_n_tuple n t = HOLogic.dest_prod t > dest_n_tuple (n  1) > op :: 

559 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

560 
type typedef_info = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

561 
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

562 
set_def: thm option, prop_of_Rep: thm, set_name: string, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

563 
Abs_inverse: thm option, Rep_inverse: thm option} 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

564 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

565 
fun typedef_info ctxt s = 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

566 
if is_frac_type ctxt (Type (s, [])) then 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

567 
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

568 
Abs_name = @{const_name Nitpick.Abs_Frac}, 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

569 
Rep_name = @{const_name Nitpick.Rep_Frac}, 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

570 
set_def = NONE, 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

571 
prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"} 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

572 
> Logic.varify_global, 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

573 
set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE, 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

574 
Rep_inverse = NONE} 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

575 
else case Typedef.get_info ctxt s of 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

576 
(* When several entries are returned, it shouldn't matter much which one 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

577 
we take (according to Florian Haftmann). *) 
39315
27f7b7748425
always handle type variables in typedefs as global
blanchet
parents:
38864
diff
changeset

578 
(* The "Logic.varifyT_global" calls are a temporary hack because these 
27f7b7748425
always handle type variables in typedefs as global
blanchet
parents:
38864
diff
changeset

579 
types's type variables sometimes clash with locally fixed type variables. 
27f7b7748425
always handle type variables in typedefs as global
blanchet
parents:
38864
diff
changeset

580 
Remove these calls once "Typedef" is fully localized. *) 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

581 
({abs_type, rep_type, Abs_name, Rep_name, ...}, 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

582 
{set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ => 
39315
27f7b7748425
always handle type variables in typedefs as global
blanchet
parents:
38864
diff
changeset

583 
SOME {abs_type = Logic.varifyT_global abs_type, 
27f7b7748425
always handle type variables in typedefs as global
blanchet
parents:
38864
diff
changeset

584 
rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name, 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

585 
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

586 
set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

587 
Rep_inverse = SOME Rep_inverse} 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

588 
 _ => NONE 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

589 

2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

590 
val is_typedef = is_some oo typedef_info 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

591 
val is_real_datatype = is_some oo Datatype.get_info 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

592 
fun is_standard_datatype thy = the oo triple_lookup (type_match thy) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

593 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

594 
(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype", 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

595 
e.g., by adding a field to "Datatype_Aux.info". *) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

596 
fun is_basic_datatype thy stds s = 
46083  597 
member (op =) [@{type_name prod}, @{type_name set}, @{type_name bool}, 
598 
@{type_name int}, "Code_Numeral.code_numeral"] s orelse 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

599 
(s = @{type_name nat} andalso is_standard_datatype thy stds nat_T) 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

600 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

601 
fun repair_constr_type ctxt body_T' T = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

602 
varify_and_instantiate_type ctxt (body_type T) body_T' T 
33192  603 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

604 
fun register_frac_type_generic frac_s ersaetze generic = 
33192  605 
let 
44012  606 
val {frac_types, ersatz_table, codatatypes} = Data.get generic 
33192  607 
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types 
44012  608 
in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, 
609 
codatatypes = codatatypes} generic end 

38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

610 
(* TODO: Consider morphism. *) 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

611 
fun register_frac_type frac_s ersaetze (_ : morphism) = 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

612 
register_frac_type_generic frac_s ersaetze 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

613 
val register_frac_type_global = Context.theory_map oo register_frac_type_generic 
33192  614 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

615 
fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s [] 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

616 
(* TODO: Consider morphism. *) 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

617 
fun unregister_frac_type frac_s (_ : morphism) = 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

618 
unregister_frac_type_generic frac_s 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

619 
val unregister_frac_type_global = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

620 
Context.theory_map o unregister_frac_type_generic 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

621 

44012  622 
fun register_ersatz_generic ersatz generic = 
623 
let 

624 
val {frac_types, ersatz_table, codatatypes} = Data.get generic 

625 
val ersatz_table = AList.merge (op =) (K true) (ersatz_table, ersatz) 

626 
in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, 

627 
codatatypes = codatatypes} generic end 

628 
(* TODO: Consider morphism. *) 

629 
fun register_ersatz ersatz (_ : morphism) = 

630 
register_ersatz_generic ersatz 

631 
val register_ersatz_global = Context.theory_map o register_ersatz_generic 

632 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

633 
fun register_codatatype_generic co_T case_name constr_xs generic = 
33192  634 
let 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

635 
val ctxt = Context.proof_of generic 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

636 
val thy = Context.theory_of generic 
44012  637 
val {frac_types, ersatz_table, codatatypes} = Data.get generic 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

638 
val constr_xs = map (apsnd (repair_constr_type ctxt co_T)) constr_xs 
33192  639 
val (co_s, co_Ts) = dest_Type co_T 
640 
val _ = 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

641 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

642 
co_s <> @{type_name fun} andalso 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

643 
not (is_basic_datatype thy [(NONE, true)] co_s) then 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

644 
() 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

645 
else 
38242  646 
raise TYPE ("Nitpick_HOL.register_codatatype_generic", [co_T], []) 
33192  647 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
648 
codatatypes 

44012  649 
in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, 
650 
codatatypes = codatatypes} generic end 

38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

651 
(* TODO: Consider morphism. *) 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

652 
fun register_codatatype co_T case_name constr_xs (_ : morphism) = 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

653 
register_codatatype_generic co_T case_name constr_xs 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

654 
val register_codatatype_global = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

655 
Context.theory_map ooo register_codatatype_generic 
33192  656 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

657 
fun unregister_codatatype_generic co_T = register_codatatype_generic co_T "" [] 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

658 
(* TODO: Consider morphism. *) 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

659 
fun unregister_codatatype co_T (_ : morphism) = 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38282
diff
changeset

660 
unregister_codatatype_generic co_T 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

661 
val unregister_codatatype_global = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

662 
Context.theory_map o unregister_codatatype_generic 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

663 

a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

664 
fun is_codatatype ctxt (Type (s, _)) = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

665 
s > AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

666 
> Option.map snd > these > null > not 
33192  667 
 is_codatatype _ _ = false 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

668 
fun is_registered_type ctxt T = is_frac_type ctxt T orelse is_codatatype ctxt T 
45280  669 
fun is_real_quot_type ctxt (Type (s, _)) = 
670 
is_some (Quotient_Info.lookup_quotients ctxt s) 

38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38212
diff
changeset

671 
 is_real_quot_type _ _ = false 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

672 
fun is_quot_type ctxt T = 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

673 
is_real_quot_type ctxt T andalso not (is_registered_type ctxt T) 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

674 
fun is_pure_typedef ctxt (T as Type (s, _)) = 
42361  675 
let val thy = Proof_Context.theory_of ctxt in 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

676 
is_frac_type ctxt T orelse 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

677 
(is_typedef ctxt s andalso 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

678 
not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

679 
is_codatatype ctxt T orelse is_record_type T orelse 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

680 
is_integer_like_type T)) 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

681 
end 
33192  682 
 is_pure_typedef _ _ = false 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

683 
fun is_univ_typedef ctxt (Type (s, _)) = 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

684 
(case typedef_info ctxt s of 
33192  685 
SOME {set_def, prop_of_Rep, ...} => 
35332
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

686 
let 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

687 
val t_opt = 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

688 
case set_def of 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

689 
SOME thm => try (snd o Logic.dest_equals o prop_of) thm 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

690 
 NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

691 
prop_of_Rep 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

692 
in 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

693 
case t_opt of 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

694 
SOME (Const (@{const_name top}, _)) => true 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

695 
(* "Multiset.multiset" *) 
35332
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

696 
 SOME (Const (@{const_name Collect}, _) 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

697 
$ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

698 
(* "FinFun.finfun" *) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

699 
 SOME (Const (@{const_name Collect}, _) $ Abs (_, _, 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

700 
Const (@{const_name Ex}, _) $ Abs (_, _, 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

701 
Const (@{const_name finite}, _) $ _))) => true 
35332
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

702 
 _ => false 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

703 
end 
33192  704 
 NONE => false) 
705 
 is_univ_typedef _ _ = false 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

706 
fun is_datatype ctxt stds (T as Type (s, _)) = 
42361  707 
let val thy = Proof_Context.theory_of ctxt in 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

708 
(is_typedef ctxt s orelse is_registered_type ctxt T orelse 
45280  709 
T = @{typ ind} orelse is_real_quot_type ctxt T) andalso 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

710 
not (is_basic_datatype thy stds s) 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

711 
end 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

712 
 is_datatype _ _ _ = false 
33192  713 

714 
fun all_record_fields thy T = 

715 
let val (recs, more) = Record.get_extT_fields thy T in 

716 
recs @ more :: all_record_fields thy (snd more) 

717 
end 

718 
handle TYPE _ => [] 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

719 
fun is_record_constr (s, T) = 
33192  720 
String.isSuffix Record.extN s andalso 
721 
let val dataT = body_type T in 

722 
is_record_type dataT andalso 

723 
s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN 

724 
end 

725 
val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields 

726 
fun no_of_record_field thy s T1 = 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

727 
find_index (curry (op =) s o fst) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

728 
(Record.get_extT_fields thy T1 > single > op @) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

729 
fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) = 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

730 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  731 
 is_record_get _ _ = false 
732 
fun is_record_update thy (s, T) = 

733 
String.isSuffix Record.updateN s andalso 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

734 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  735 
(all_record_fields thy (body_type T)) 
736 
handle TYPE _ => false 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

737 
fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) = 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

738 
(case typedef_info ctxt s' of 
33192  739 
SOME {Abs_name, ...} => s = Abs_name 
740 
 NONE => false) 

741 
 is_abs_fun _ _ = false 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

742 
fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) = 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

743 
(case typedef_info ctxt s' of 
33192  744 
SOME {Rep_name, ...} => s = Rep_name 
745 
 NONE => false) 

746 
 is_rep_fun _ _ = false 

38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38212
diff
changeset

747 
fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun}, 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38212
diff
changeset

748 
[_, abs_T as Type (s', _)]))) = 
45797  749 
try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s' 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

750 
= SOME (Const x) andalso not (is_registered_type ctxt abs_T) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

751 
 is_quot_abs_fun _ _ = false 
46819
9b38f8527510
addressed a quotienttyperelated issue that arose with the port to "set"
blanchet
parents:
46746
diff
changeset

752 
fun is_quot_rep_fun ctxt (s, Type (@{type_name fun}, 
9b38f8527510
addressed a quotienttyperelated issue that arose with the port to "set"
blanchet
parents:
46746
diff
changeset

753 
[abs_T as Type (abs_s, _), _])) = 
46746
a10dcc985e8d
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
blanchet
parents:
46745
diff
changeset

754 
(case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

755 
SOME (Const (s', _)) => 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

756 
s = s' andalso not (is_registered_type ctxt abs_T) 
46746
a10dcc985e8d
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
blanchet
parents:
46745
diff
changeset

757 
 NONE => false) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

758 
 is_quot_rep_fun _ _ = false 
33192  759 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

760 
fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun}, 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

761 
[T1 as Type (s', _), T2]))) = 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

762 
(case typedef_info ctxt s' of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

763 
SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1])) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

764 
 NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])) 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

765 
 mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) 
45280  766 
fun rep_type_for_quot_type ctxt (T as Type (s, _)) = 
767 
let 

768 
val thy = Proof_Context.theory_of ctxt 

769 
val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients ctxt s) 

770 
in 

39345  771 
instantiate_type thy qtyp T rtyp 
772 
end 

773 
 rep_type_for_quot_type _ T = 

774 
raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], []) 

35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

775 
fun equiv_relation_for_quot_type thy (Type (s, Ts)) = 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

776 
let 
46745
a6f83f21dc2c
fixed handling of "Rep_" function of quotient types  sideeffect of "set" constructor reintroduction
blanchet
parents:
46320
diff
changeset

777 
val {qtyp, equiv_rel, equiv_thm, ...} = 
a6f83f21dc2c
fixed handling of "Rep_" function of quotient types  sideeffect of "set" constructor reintroduction
blanchet
parents:
46320
diff
changeset

778 
the (Quotient_Info.lookup_quotients thy s) 
38243  779 
val partial = 
780 
case prop_of equiv_thm of 

781 
@{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false 

782 
 @{const Trueprop} $ (Const (@{const_name part_equivp}, _) $ _) => true 

783 
 _ => raise NOT_SUPPORTED "Illformed quotient type equivalence \ 

784 
\relation theorem" 

35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

785 
val Ts' = qtyp > dest_Type > snd 
38243  786 
in (subst_atomic_types (Ts' ~~ Ts) equiv_rel, partial) end 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

787 
 equiv_relation_for_quot_type _ T = 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

788 
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) 
33192  789 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

790 
fun is_coconstr ctxt (s, T) = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

791 
case body_type T of 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

792 
co_T as Type (co_s, _) => 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

793 
let val {codatatypes, ...} = Data.get (Context.Proof ctxt) in 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

794 
exists (fn (s', T') => s = s' andalso repair_constr_type ctxt co_T T' = T) 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

795 
(AList.lookup (op =) codatatypes co_s > Option.map snd > these) 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

796 
end 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

797 
 _ => false 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

798 
fun is_constr_like ctxt (s, T) = 
41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41049
diff
changeset

799 
member (op =) [@{const_name FunBox}, @{const_name PairBox}, 
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41049
diff
changeset

800 
@{const_name Quot}, @{const_name Zero_Rep}, 
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41049
diff
changeset

801 
@{const_name Suc_Rep}] s orelse 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

802 
let 
42361  803 
val thy = Proof_Context.theory_of ctxt 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

804 
val (x as (_, T)) = (s, unarize_unbox_etc_type T) 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

805 
in 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37258
diff
changeset

806 
is_real_constr thy x orelse is_record_constr x orelse 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

807 
(is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

808 
is_coconstr ctxt x 
33192  809 
end 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

810 
fun is_stale_constr ctxt (x as (s, T)) = 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

811 
is_registered_type ctxt (body_type T) andalso is_constr_like ctxt x andalso 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

812 
not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x) 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

813 
fun is_constr ctxt stds (x as (_, T)) = 
42361  814 
let val thy = Proof_Context.theory_of ctxt in 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

815 
is_constr_like ctxt x andalso 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

816 
not (is_basic_datatype thy stds 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

817 
(fst (dest_Type (unarize_type (body_type T))))) andalso 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

818 
not (is_stale_constr ctxt x) 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

819 
end 
33192  820 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 
821 
val is_sel_like_and_no_discr = 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

822 
String.isPrefix sel_prefix orf 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

823 
(member (op =) [@{const_name fst}, @{const_name snd}]) 
33192  824 

825 
fun in_fun_lhs_for InConstr = InSel 

826 
 in_fun_lhs_for _ = InFunLHS 

827 
fun in_fun_rhs_for InConstr = InConstr 

828 
 in_fun_rhs_for InSel = InSel 

829 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

830 
 in_fun_rhs_for _ = InFunRHS1 

831 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

832 
fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = 
33192  833 
case T of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

834 
Type (@{type_name fun}, _) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

835 
(boxy = InPair orelse boxy = InFunLHS) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

836 
not (is_boolean_type (body_type T)) 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38188
diff
changeset

837 
 Type (@{type_name prod}, Ts) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

838 
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

839 
((boxy = InExpr orelse boxy = InFunLHS) andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

840 
exists (is_boxing_worth_it hol_ctxt InPair) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

841 
(map (box_type hol_ctxt InPair) Ts)) 
33192  842 
 _ => false 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

843 
and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z = 
33192  844 
case triple_lookup (type_match thy) boxes (Type z) of 
845 
SOME (SOME box_me) => box_me 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

846 
 _ => is_boxing_worth_it hol_ctxt boxy (Type z) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

847 
and box_type hol_ctxt boxy T = 
33192  848 
case T of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

849 
Type (z as (@{type_name fun}, [T1, T2])) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

850 
if boxy <> InConstr andalso boxy <> InSel andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

851 
should_box_type hol_ctxt boxy z then 
33192  852 
Type (@{type_name fun_box}, 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

853 
[box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2]) 
33192  854 
else 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

855 
box_type hol_ctxt (in_fun_lhs_for boxy) T1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

856 
> box_type hol_ctxt (in_fun_rhs_for boxy) T2 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38188
diff
changeset

857 
 Type (z as (@{type_name prod}, Ts)) => 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

858 
if boxy <> InConstr andalso boxy <> InSel 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

859 
andalso should_box_type hol_ctxt boxy z then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

860 
Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts) 
33192  861 
else 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38188
diff
changeset

862 
Type (@{type_name prod}, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

863 
map (box_type hol_ctxt 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

864 
(if boxy = InConstr orelse boxy = InSel then boxy 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

865 
else InPair)) Ts) 
33192  866 
 _ => T 
867 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

868 
fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"} 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

869 
 binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"} 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

870 
 binarize_nat_and_int_in_type (Type (s, Ts)) = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

871 
Type (s, map binarize_nat_and_int_in_type Ts) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

872 
 binarize_nat_and_int_in_type T = T 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

873 
val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

874 

33192  875 
fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T > bool_T) 
876 

877 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

878 
fun nth_sel_name_for_constr_name s n = 

879 
if s = @{const_name Pair} then 

880 
if n = 0 then @{const_name fst} else @{const_name snd} 

881 
else 

882 
sel_prefix_for n ^ s 

883 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

884 
 nth_sel_for_constr (s, T) n = 

885 
(nth_sel_name_for_constr_name s n, 

886 
body_type T > nth (maybe_curried_binder_types T) n) 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

887 
fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

888 
apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

889 
oo nth_sel_for_constr 
33192  890 

891 
fun sel_no_from_name s = 

892 
if String.isPrefix discr_prefix s then 

893 
~1 

894 
else if String.isPrefix sel_prefix s then 

895 
s > unprefix sel_prefix > Int.fromString > the 

896 
else if s = @{const_name snd} then 

897 
1 

898 
else 

899 
0 

900 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

901 
val close_form = 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

902 
let 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

903 
fun close_up zs zs' = 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

904 
fold (fn (z as ((s, _), T)) => fn t' => 
46217
7b19666f0e3d
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
wenzelm
parents:
46115
diff
changeset

905 
Logic.all_const T $ Abs (s, T, abstract_over (Var z, t'))) 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

906 
(take (length zs'  length zs) zs') 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

907 
fun aux zs (@{const "==>"} $ t1 $ t2) = 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

908 
let val zs' = Term.add_vars t1 zs in 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

909 
close_up zs zs' (Logic.mk_implies (t1, aux zs' t2)) 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

910 
end 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

911 
 aux zs t = close_up zs (Term.add_vars t zs) t 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

912 
in aux [] end 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

913 

33192  914 
fun distinctness_formula T = 
915 
all_distinct_unordered_pairs_of 

916 
#> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2)) 

917 
#> List.foldr (s_conj o swap) @{const True} 

918 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

919 
fun zero_const T = Const (@{const_name zero_class.zero}, T) 
33192  920 
fun suc_const T = Const (@{const_name Suc}, T > T) 
921 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

922 
fun uncached_datatype_constrs ({thy, ctxt, stds, ...} : hol_context) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

923 
(T as Type (s, Ts)) = 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

924 
(case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

925 
s of 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

926 
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type ctxt T)) xs' 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

927 
 _ => 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

928 
if is_frac_type ctxt T then 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

929 
case typedef_info ctxt s of 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

930 
SOME {abs_type, rep_type, Abs_name, ...} => 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

931 
[(Abs_name, 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

932 
varify_and_instantiate_type ctxt abs_type T rep_type > T)] 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

933 
 NONE => [] (* impossible *) 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
47782
diff
changeset

934 
else if is_datatype ctxt stds T then 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

935 
case Datatype.get_info thy s of 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

936 
SOME {index, descr, ...} => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

937 
let 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

938 
val (_, dtyps, constrs) = AList.lookup (op =) descr index > the 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

939 
in 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37258
diff
changeset

940 
map (apsnd (fn Us => 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37258
diff
changeset

941 
map (typ_of_dtyp descr (dtyps ~~ Ts)) Us > T)) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37258
diff
changeset

942 
constrs 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

943 
end 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

944 
 NONE => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

945 
if is_record_type T then 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

946 
let 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

947 
val s' = unsuffix Record.ext_typeN s ^ Record.extN 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

948 
val T' = (Record.get_extT_fields thy T 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

949 
> apsnd single > uncurry append > map snd) > T 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

950 
in [(s', T')] end 
45280  951 
else if is_real_quot_type ctxt T then 
952 
[(@{const_name Quot}, rep_type_for_quot_type ctxt T > T)] 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

953 
else case typedef_info ctxt s of 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

954 
SOME {abs_type, rep_type, Abs_name, ...} => 
35311  955 
[(Abs_name, 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

956 
varify_and_instantiate_type ctxt abs_type T rep_type > T)] 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

957 
 NONE => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

958 
if T = @{typ ind} then 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

959 
[dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}] 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

960 
else 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

961 
[] 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

962 
else 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

963 
[]) 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

964 
 uncached_datatype_constrs _ _ = [] 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

965 
fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T = 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

966 
case AList.lookup (op =) (!constr_cache) T of 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

967 
SOME xs => xs 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

968 
 NONE => 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

969 
let val xs = uncached_datatype_constrs hol_ctxt T in 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

970 
(Unsynchronized.change constr_cache (cons (T, xs)); xs) 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

971 
end 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

972 
fun binarized_and_boxed_datatype_constrs hol_ctxt binarize = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

973 
map (apsnd ((binarize ? binarize_nat_and_int_in_type) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

974 
o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt 
33192  975 
val num_datatype_constrs = length oo datatype_constrs 
976 

977 
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair} 

978 
 constr_name_for_sel_like @{const_name snd} = @{const_name Pair} 

979 
 constr_name_for_sel_like s' = original_name s' 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

980 
fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') = 
33192  981 
let val s = constr_name_for_sel_like s' in 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

982 
AList.lookup (op =) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

983 
(binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T')) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

984 
s 
33192  985 
> the > pair s 
986 
end 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

987 

41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

988 
fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

989 
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

990 
 card_of_type assigns (Type (@{type_name prod}, [T1, T2])) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

991 
card_of_type assigns T1 * card_of_type assigns T2 
46083  992 
 card_of_type assigns (Type (@{type_name set}, [T'])) = 
993 
reasonable_power 2 (card_of_type assigns T') 

41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

994 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

995 
 card_of_type _ @{typ prop} = 2 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

996 
 card_of_type _ @{typ bool} = 2 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

997 
 card_of_type assigns T = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

998 
case AList.lookup (op =) assigns T of 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

999 
SOME k => k 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1000 
 NONE => if T = @{typ bisim_iterator} then 0 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1001 
else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1002 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1003 
fun bounded_card_of_type max default_card assigns 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1004 
(Type (@{type_name fun}, [T1, T2])) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1005 
let 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1006 
val k1 = bounded_card_of_type max default_card assigns T1 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1007 
val k2 = bounded_card_of_type max default_card assigns T2 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1008 
in 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1009 
if k1 = max orelse k2 = max then max 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1010 
else Int.min (max, reasonable_power k2 k1) 
47668  1011 
handle TOO_LARGE _ => max 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1012 
end 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1013 
 bounded_card_of_type max default_card assigns 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1014 
(Type (@{type_name prod}, [T1, T2])) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1015 
let 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1016 
val k1 = bounded_card_of_type max default_card assigns T1 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1017 
val k2 = bounded_card_of_type max default_card assigns T2 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1018 
in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end 
46083  1019 
 bounded_card_of_type max default_card assigns 
1020 
(Type (@{type_name set}, [T'])) = 

1021 
bounded_card_of_type max default_card assigns (T' > bool_T) 

41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1022 
 bounded_card_of_type max default_card assigns T = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1023 
Int.min (max, if default_card = ~1 then 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1024 
card_of_type assigns T 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1025 
else 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1026 
card_of_type assigns T 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1027 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1028 
default_card) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1029 

46320  1030 
(* Similar to "ATP_Util.tiny_card_of_type". *) 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1031 
fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1032 
assigns T = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1033 
let 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1034 
fun aux avoid T = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1035 
(if member (op =) avoid T then 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1036 
0 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1037 
else if member (op =) finitizable_dataTs T then 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1038 
raise SAME () 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1039 
else case T of 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1040 
Type (@{type_name fun}, [T1, T2]) => 
42679  1041 
(case (aux avoid T1, aux avoid T2) of 
1042 
(_, 1) => 1 

1043 
 (0, _) => 0 

1044 
 (_, 0) => 0 

1045 
 (k1, k2) => 

1046 
if k1 >= max orelse k2 >= max then max 

1047 
else Int.min (max, reasonable_power k2 k1)) 

41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1048 
 Type (@{type_name prod}, [T1, T2]) => 
42679  1049 
(case (aux avoid T1, aux avoid T2) of 
1050 
(0, _) => 0 

1051 
 (_, 0) => 0 

1052 
 (k1, k2) => 

1053 
if k1 >= max orelse k2 >= max then max 

1054 
else Int.min (max, k1 * k2)) 

46083  1055 
 Type (@{type_name set}, [T']) => aux avoid (T' > bool_T) 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1056 
 Type (@{type_name itself}, _) => 1 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1057 
 @{typ prop} => 2 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1058 
 @{typ bool} => 2 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1059 
 Type _ => 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1060 
(case datatype_constrs hol_ctxt T of 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1061 
[] => if is_integer_type T orelse is_bit_type T then 0 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1062 
else raise SAME () 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1063 
 constrs => 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1064 
let 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1065 
val constr_cards = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1066 
map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1067 
constrs 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1068 
in 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1069 
if exists (curry (op =) 0) constr_cards then 0 
42679  1070 
else Int.min (max, Integer.sum constr_cards) 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1071 
end) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1072 
 _ => raise SAME ()) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1073 
handle SAME () => 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1074 
AList.lookup (op =) assigns T > the_default default_card 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1075 
in Int.min (max, aux [] T) end 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1076 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1077 
val typical_atomic_card = 4 
41898
55d981e1232a
improved formula for specialization, to prevent needless specializations  and removed dead code
blanchet
parents:
41876
diff
changeset

1078 
val typical_card_of_type = bounded_card_of_type 16777217 typical_atomic_card [] 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1079 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1080 
fun is_finite_type hol_ctxt T = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1081 
bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1082 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1083 
fun is_special_eligible_arg strict Ts t = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1084 
case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1085 
[] => true 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1086 
 bad_Ts => 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1087 
let 
41898
55d981e1232a
improved formula for specialization, to prevent needless specializations  and removed dead code
blanchet
parents:
41876
diff
changeset

1088 
val bad_Ts_cost = 
55d981e1232a
improved formula for specialization, to prevent needless specializations  and removed dead code
blanchet
parents:
41876
diff
changeset

1089 
if strict then fold (curry (op *) o typical_card_of_type) bad_Ts 1 
55d981e1232a
improved formula for specialization, to prevent needless specializations  and removed dead code
blanchet
parents:
41876
diff
changeset

1090 
else fold (Integer.max o typical_card_of_type) bad_Ts 0 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1091 
val T_cost = typical_card_of_type (fastype_of1 (Ts, t)) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1092 
in (bad_Ts_cost, T_cost) > (if strict then op < else op <=) end 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1093 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1094 
fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1095 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1096 
fun let_var s = (nitpick_prefix ^ s, 999) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1097 
val let_inline_threshold = 20 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1098 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1099 
fun s_let Ts s n abs_T body_T f t = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1100 
if (n  1) * (size_of_term t  1) <= let_inline_threshold orelse 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1101 
is_special_eligible_arg false Ts t then 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1102 
f t 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1103 
else 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1104 
let val z = (let_var s, abs_T) in 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1105 
Const (@{const_name Let}, abs_T > (abs_T > body_T) > body_T) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1106 
$ t $ abs_var z (incr_boundvars 1 (f (Var z))) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1107 
end 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1108 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1109 
fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1110 
 loose_bvar1_count (t1 $ t2, k) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1111 
loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1112 
 loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1113 
 loose_bvar1_count _ = 0 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1114 

42414
9465651c0db7
optimize trivial equalities early in Nitpick  it shouldn't be the job of the peephole optimizer
blanchet
parents:
42361
diff
changeset

1115 
fun s_betapply _ (t1 as Const (@{const_name "=="}, _) $ t1', t2) = 
9465651c0db7
optimize trivial equalities early in Nitpick  it shouldn't be the job of the peephole optimizer
blanchet
parents:
42361
diff
changeset

1116 
if t1' aconv t2 then @{prop True} else t1 $ t2 
9465651c0db7
optimize trivial equalities early in Nitpick  it shouldn't be the job of the peephole optimizer
blanchet
parents:
42361
diff
changeset

1117 
 s_betapply _ (t1 as Const (@{const_name HOL.eq}, _) $ t1', t2) = 
9465651c0db7
optimize trivial equalities early in Nitpick  it shouldn't be the job of the peephole optimizer
blanchet
parents:
42361
diff
changeset

1118 
if t1' aconv t2 then @{term True} else t1 $ t2 
9465651c0db7
optimize trivial equalities early in Nitpick  it shouldn't be the job of the peephole optimizer
blanchet
parents:
42361
diff
changeset

1119 
 s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1' 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1120 
 s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1121 
 s_betapply Ts (Const (@{const_name Let}, 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1122 
Type (_, [bound_T, Type (_, [_, body_T])])) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1123 
$ t12 $ Abs (s, T, t13'), t2) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1124 
let val body_T' = range_type body_T in 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1125 
Const (@{const_name Let}, bound_T > (bound_T > body_T') > body_T') 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1126 
$ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2)) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1127 
end 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1128 
 s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1129 
(s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1')) 
42958  1130 
(curry betapply t1) t2 
1131 
(* FIXME: fix all "s_betapply []" calls *) 

1132 
handle TERM _ => betapply (t1, t2) 

1133 
 General.Subscript => betapply (t1, t2)) 

41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1134 
 s_betapply _ (t1, t2) = t1 $ t2 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1135 
fun s_betapplys Ts = Library.foldl (s_betapply Ts) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1136 

49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1137 
fun s_beta_norm Ts t = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1138 
let 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1139 
fun aux _ (Var _) = raise Same.SAME 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1140 
 aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t') 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1141 
 aux Ts ((t1 as Abs _) $ t2) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1142 
Same.commit (aux Ts) (s_betapply Ts (t1, t2)) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1143 
 aux Ts (t1 $ t2) = 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1144 
((case aux Ts t1 of 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1145 
t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2)) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1146 
 t1 => t1 $ Same.commit (aux Ts) t2) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1147 
handle Same.SAME => t1 $ aux Ts t2) 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1148 
 aux _ _ = raise Same.SAME 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1149 
in aux Ts t handle Same.SAME => t end 
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41859
diff
changeset

1150 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

1151 
fun discr_term_for_constr hol_ctxt (x as (s, T)) = 
33192  1152 
let val dataT = body_type T in 
1153 
if s = @{const_name Suc} then 

1154 
Abs (Name.uu, dataT, 

1155 
@{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0)) 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

1156 
else if num_datatype_constrs hol_ctxt dataT >= 2 then 
33192  1157 
Const (discr_for_constr x) 
1158 
else 

1159 
Abs (Name.uu, dataT, @{const True}) 

1160 
end 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1161 
fun discriminate_value (hol_ctxt as {ctxt, ...}) x t = 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1162 
case head_of t of 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1163 
Const x' => 
33192  1164 
if x = x' then @{const True} 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1165 
else if is_constr_like ctxt x' then @{const False} 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37269
diff
changeset

1166 
else s_betapply [] (discr_term_for_constr hol_ctxt x, t) 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37269
diff
changeset

1167 
 _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t) 
33192  1168 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1169 
fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n = 
33192  1170 
let val (arg_Ts, dataT) = strip_type T in 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1171 
if dataT = nat_T andalso is_standard_datatype thy stds nat_T then 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1172 
@{term "%n::nat. n  1"} 
33192  1173 
else if is_pair_type dataT then 
1174 
Const (nth_sel_for_constr x n) 

1175 
else 

1176 
let 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38188
diff
changeset

1177 
fun aux m (Type (@{type_name prod}, [T1, T2])) = 
33192  1178 
let 
1179 
val (m, t1) = aux m T1 

1180 
val (m, t2) = aux m T2 

1181 
in (m, HOLogic.mk_prod (t1, t2)) end 

1182 
 aux m T = 

1183 
(m + 1, Const (nth_sel_name_for_constr_name s m, dataT > T) 

1184 
$ Bound 0) 

1185 
val m = fold (Integer.add o num_factors_in_type) 

1186 
(List.take (arg_Ts, n)) 0 

1187 
in Abs ("x", dataT, aux m (nth arg_Ts n) > snd) end 

1188 
end 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1189 
fun select_nth_constr_arg ctxt stds x t n res_T = 
42361  1190 
let val thy = Proof_Context.theory_of ctxt in 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1191 
(case strip_comb t of 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1192 
(Const x', args) => 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanche 