author  blanchet 
Wed, 02 Mar 2011 13:09:57 +0100  
changeset 41870  a14a492f472f 
parent 41860  49d0fc8c418c 
child 41875  e3cd0dce9b1a 
permissions  rwrr 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1 
(* Title: HOL/Tools/Nitpick/nitpick_preproc.ML 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

3 
Copyright 2008, 2009, 2010 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

4 

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

5 
Nitpick's HOL preprocessor. 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

7 

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

8 
signature NITPICK_PREPROC = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

10 
type hol_context = Nitpick_HOL.hol_context 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

11 
val preprocess_formulas : 
41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41001
diff
changeset

12 
hol_context > term list > term 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41793
diff
changeset

13 
> term list * term list * term list * bool * bool * bool 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35807
diff
changeset

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

15 

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

16 
structure Nitpick_Preproc : NITPICK_PREPROC = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

18 

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

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

20 
open Nitpick_HOL 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

22 

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

23 
fun is_positive_existential polar quant_s = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

24 
(polar = Pos andalso quant_s = @{const_name Ex}) orelse 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

25 
(polar = Neg andalso quant_s <> @{const_name Ex}) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

26 

37271  27 
val is_descr = 
39360
cdf2c3341422
eliminate more clutter related to "fast_descrs" optimization
blanchet
parents:
39359
diff
changeset

28 
member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}] 
37271  29 

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

30 
(** Binary coding of integers **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

31 

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

32 
(* If a formula contains a numeral whose absolute value is more than this 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

33 
threshold, the unary coding is likely not to work well and we prefer the 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

34 
binary coding. *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

35 
val binary_int_threshold = 3 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

36 

35718  37 
val may_use_binary_ints = 
38 
let 

39 
fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) = 

40 
aux def t1 andalso aux false t2 

41 
 aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2 

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

42 
 aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = 
35718  43 
aux def t1 andalso aux false t2 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset

44 
 aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2 
35718  45 
 aux def (t1 $ t2) = aux def t1 andalso aux def t2 
46 
 aux def (t as Const (s, _)) = 

47 
(not def orelse t <> @{const Suc}) andalso 

48 
not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, 

49 
@{const_name nat_gcd}, @{const_name nat_lcm}, 

50 
@{const_name Frac}, @{const_name norm_frac}] s) 

51 
 aux def (Abs (_, _, t')) = aux def t' 

52 
 aux _ _ = true 

53 
in aux end 

54 
val should_use_binary_ints = 

55 
let 

56 
fun aux (t1 $ t2) = aux t1 orelse aux t2 

57 
 aux (Const (s, T)) = 

58 
((s = @{const_name times} orelse s = @{const_name div}) andalso 

59 
is_integer_type (body_type T)) orelse 

60 
(String.isPrefix numeral_prefix s andalso 

61 
let val n = the (Int.fromString (unprefix numeral_prefix s)) in 

62 
n < ~ binary_int_threshold orelse n > binary_int_threshold 

63 
end) 

64 
 aux (Abs (_, _, t')) = aux t' 

65 
 aux _ = false 

66 
in aux end 

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

67 

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

68 
(** Uncurrying **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

69 

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

70 
fun add_to_uncurry_table ctxt t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

72 
val thy = ProofContext.theory_of ctxt 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

73 
fun aux (t1 $ t2) args table = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

74 
let val table = aux t2 [] table in aux t1 (t2 :: args) table end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

75 
 aux (Abs (_, _, t')) _ table = aux t' [] table 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

76 
 aux (t as Const (x as (s, _))) args table = 
39359  77 
if is_built_in_const thy [(NONE, true)] x orelse 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

78 
is_constr_like ctxt x orelse 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

79 
is_sel s orelse s = @{const_name Sigma} then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

81 
else 
36384  82 
Termtab.map_default (t, 65536) (Integer.min (length args)) table 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

83 
 aux _ _ table = table 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

84 
in aux t [] end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

85 

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

86 
fun uncurry_prefix_for k j = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

87 
uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

88 

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

89 
fun uncurry_term table t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

91 
fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args) 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

92 
 aux (Abs (s, T, t')) args = s_betapplys [] (Abs (s, T, aux t' []), args) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

93 
 aux (t as Const (s, T)) args = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

94 
(case Termtab.lookup table t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

95 
SOME n => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

96 
if n >= 2 then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

98 
val arg_Ts = strip_n_binders n T > fst 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

100 
if is_iterator_type (hd arg_Ts) then 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

102 
else case find_index (not_equal bool_T) arg_Ts of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

103 
~1 => n 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

104 
 j => j 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

105 
val ((before_args, tuple_args), after_args) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

106 
args > chop n >> chop j 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

107 
val ((before_arg_Ts, tuple_arg_Ts), rest_T) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

108 
T > strip_n_binders n >> chop j 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

109 
val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

111 
if n  j < 2 then 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

112 
s_betapplys [] (t, args) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

113 
else 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

114 
s_betapplys [] 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

115 
(Const (uncurry_prefix_for (n  j) j ^ s, 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

116 
before_arg_Ts > tuple_T > rest_T), 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

117 
before_args @ [mk_flat_tuple tuple_T tuple_args] @ 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

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

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

120 
else 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

121 
s_betapplys [] (t, args) 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

122 
 NONE => s_betapplys [] (t, args)) 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

123 
 aux t args = s_betapplys [] (t, args) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

124 
in aux t [] end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

125 

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

126 
(** Boxing **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

127 

39359  128 
fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, ...}) def orig_t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

130 
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

131 
Type (@{type_name fun}, map box_relational_operator_type Ts) 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38170
diff
changeset

132 
 box_relational_operator_type (Type (@{type_name prod}, Ts)) = 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38170
diff
changeset

133 
Type (@{type_name prod}, map (box_type hol_ctxt InPair) Ts) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

134 
 box_relational_operator_type T = T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

135 
fun add_boxed_types_for_var (z as (_, T)) (T', t') = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

136 
case t' of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

137 
Var z' => z' = z ? insert (op =) T' 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

138 
 Const (@{const_name Pair}, _) $ t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

139 
(case T' of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

140 
Type (_, [T1, T2]) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

141 
fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

142 
 _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\ 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

143 
\add_boxed_types_for_var", [T'], [])) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

144 
 _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

145 
fun box_var_in_def new_Ts old_Ts t (z as (_, T)) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

146 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

147 
@{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

148 
 Const (s0, _) $ t1 $ _ => 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

149 
if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

151 
val (t', args) = strip_comb t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

152 
val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t') 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

154 
case fold (add_boxed_types_for_var z) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

155 
(fst (strip_n_binders (length args) T') ~~ args) [] of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

156 
[T''] => T'' 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

157 
 _ => T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

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

161 
 _ => T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

162 
and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

164 
val abs_T' = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

165 
if polar = Neut orelse is_positive_existential polar quant_s then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

166 
box_type hol_ctxt InFunLHS abs_T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

169 
val body_T = body_type quant_T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

171 
Const (quant_s, (abs_T' > body_T) > body_T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

172 
$ Abs (abs_s, abs_T', 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

173 
t > do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

175 
and do_equals new_Ts old_Ts s0 T0 t1 t2 = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

177 
val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

178 
val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) 
37704
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37678
diff
changeset

179 
val T = if def then T1 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37678
diff
changeset

180 
else [T1, T2] > sort (int_ord o pairself size_of_typ) > hd 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

182 
list_comb (Const (s0, T > T > body_type T0), 
35384  183 
map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2]) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

184 
end 
37271  185 
and do_descr s T = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

186 
let val T1 = box_type hol_ctxt InFunLHS (range_type T) in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

187 
Const (s, (T1 > bool_T) > T1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

189 
and do_term new_Ts old_Ts polar t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

190 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

191 
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

192 
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

193 
 Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

194 
do_equals new_Ts old_Ts s0 T0 t1 t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

195 
 @{const "==>"} $ t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

196 
@{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

197 
$ do_term new_Ts old_Ts polar t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

198 
 @{const Pure.conjunction} $ t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

199 
@{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

200 
$ do_term new_Ts old_Ts polar t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

201 
 @{const Trueprop} $ t1 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

202 
@{const Trueprop} $ do_term new_Ts old_Ts polar t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

203 
 @{const Not} $ t1 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

204 
@{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

205 
 Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

206 
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

207 
 Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

208 
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

209 
 Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

210 
do_equals new_Ts old_Ts s0 T0 t1 t2 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

211 
 @{const HOL.conj} $ t1 $ t2 => 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

212 
@{const HOL.conj} $ do_term new_Ts old_Ts polar t1 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

213 
$ do_term new_Ts old_Ts polar t2 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

214 
 @{const HOL.disj} $ t1 $ t2 => 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

215 
@{const HOL.disj} $ do_term new_Ts old_Ts polar t1 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

216 
$ do_term new_Ts old_Ts polar t2 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset

217 
 @{const HOL.implies} $ t1 $ t2 => 
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset

218 
@{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

219 
$ do_term new_Ts old_Ts polar t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

220 
 Const (x as (s, T)) => 
37271  221 
if is_descr s then 
222 
do_descr s T 

223 
else 

224 
Const (s, if s = @{const_name converse} orelse 

225 
s = @{const_name trancl} then 

226 
box_relational_operator_type T 

227 
else if String.isPrefix quot_normal_prefix s then 

228 
let val T' = box_type hol_ctxt InFunLHS (domain_type T) in 

229 
T' > T' 

230 
end 

39359  231 
else if is_built_in_const thy stds x orelse 
37271  232 
s = @{const_name Sigma} then 
233 
T 

234 
else if is_constr_like ctxt x then 

235 
box_type hol_ctxt InConstr T 

236 
else if is_sel s orelse is_rep_fun ctxt x then 

237 
box_type hol_ctxt InSel T 

238 
else 

239 
box_type hol_ctxt InExpr T) 

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

240 
 t1 $ Abs (s, T, t2') => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

242 
val t1 = do_term new_Ts old_Ts Neut t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

243 
val T1 = fastype_of1 (new_Ts, t1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

244 
val (s1, Ts1) = dest_Type T1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

245 
val T' = hd (snd (dest_Type (hd Ts1))) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

246 
val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2') 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

247 
val T2 = fastype_of1 (new_Ts, t2) 
35384  248 
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

249 
in 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

250 
s_betapply new_Ts (if s1 = @{type_name fun} then 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

251 
t1 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

252 
else 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

253 
select_nth_constr_arg ctxt stds 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

254 
(@{const_name FunBox}, 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

255 
Type (@{type_name fun}, Ts1) > T1) t1 0 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

256 
(Type (@{type_name fun}, Ts1)), t2) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

258 
 t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

260 
val t1 = do_term new_Ts old_Ts Neut t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

261 
val T1 = fastype_of1 (new_Ts, t1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

262 
val (s1, Ts1) = dest_Type T1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

263 
val t2 = do_term new_Ts old_Ts Neut t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

264 
val T2 = fastype_of1 (new_Ts, t2) 
35384  265 
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

266 
in 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

267 
s_betapply new_Ts (if s1 = @{type_name fun} then 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

268 
t1 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

269 
else 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

270 
select_nth_constr_arg ctxt stds 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

271 
(@{const_name FunBox}, 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

272 
Type (@{type_name fun}, Ts1) > T1) t1 0 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

273 
(Type (@{type_name fun}, Ts1)), t2) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

275 
 Free (s, T) => Free (s, box_type hol_ctxt InExpr T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

276 
 Var (z as (x, T)) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

277 
Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

278 
else box_type hol_ctxt InExpr T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

279 
 Bound _ => t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

280 
 Abs (s, T, t') => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

281 
Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t') 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

282 
in do_term [] [] Pos orig_t end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

283 

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

284 
(** Destruction of constructors **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

285 

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

286 
val val_var_prefix = nitpick_prefix ^ "v" 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

287 

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

288 
fun fresh_value_var Ts k n j t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

289 
Var ((val_var_prefix ^ nat_subscript (n  j), k), fastype_of1 (Ts, t)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

290 

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

291 
fun has_heavy_bounds_or_vars Ts t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

293 
fun aux [] = false 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

294 
 aux [T] = is_fun_type T orelse is_pair_type T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

295 
 aux _ = true 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

296 
in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

297 

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

298 
fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level 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

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

300 
let val t_comb = list_comb (t, args) in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

301 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

302 
Const x => 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

303 
if not relax andalso is_constr ctxt stds x andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

304 
not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

305 
has_heavy_bounds_or_vars Ts t_comb andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

306 
not (loose_bvar (t_comb, level)) then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

308 
val (j, seen) = case find_index (curry (op =) t_comb) seen of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

309 
~1 => (0, t_comb :: seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

310 
 j => (j, seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

311 
in (fresh_value_var Ts k (length seen) j t_comb, seen) end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

313 
(t_comb, seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

314 
 _ => (t_comb, seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

316 

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

317 
fun equations_for_pulled_out_constrs mk_eq Ts k seen = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

318 
let val n = length seen in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

319 
map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

320 
(index_seq 0 n) seen 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

322 

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

323 
fun pull_out_universal_constrs hol_ctxt def t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

325 
val k = maxidx_of_term t + 1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

326 
fun do_term Ts def t args seen = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

327 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

328 
(t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

329 
do_eq_or_imp Ts true def t0 t1 t2 seen 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

330 
 (t0 as @{const "==>"}) $ t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

331 
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

332 
 (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

333 
do_eq_or_imp Ts true def t0 t1 t2 seen 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset

334 
 (t0 as @{const HOL.implies}) $ t1 $ t2 => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

335 
do_eq_or_imp Ts false def t0 t1 t2 seen 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

336 
 Abs (s, T, t') => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

337 
let val (t', seen) = do_term (T :: Ts) def t' [] seen in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

338 
(list_comb (Abs (s, T, t'), args), seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

340 
 t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

341 
let val (t2, seen) = do_term Ts def t2 [] seen in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

342 
do_term Ts def t1 (t2 :: args) seen 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

343 
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

344 
 _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

345 
and do_eq_or_imp Ts eq def t0 t1 t2 seen = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

347 
val (t2, seen) = if eq andalso def then (t2, seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

348 
else do_term Ts false t2 [] seen 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

349 
val (t1, seen) = do_term Ts false t1 [] seen 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

350 
in (t0 $ t1 $ t2, seen) end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

351 
val (concl, seen) = do_term [] def t [] [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

353 
Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

354 
seen, concl) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

356 

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

357 
fun mk_exists v t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

358 
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

359 

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

360 
fun pull_out_existential_constrs hol_ctxt t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

362 
val k = maxidx_of_term t + 1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

363 
fun aux Ts num_exists t args seen = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

364 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

365 
(t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

367 
val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

368 
val n = length seen' 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

369 
fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen' 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

371 
(equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen' 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

372 
> List.foldl s_conj t1 > fold mk_exists (vars ()) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

373 
> curry3 Abs s1 T1 > curry (op $) t0, seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

375 
 t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

376 
let val (t2, seen) = aux Ts num_exists t2 [] seen in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

377 
aux Ts num_exists t1 (t2 :: args) seen 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

379 
 Abs (s, T, t') => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

381 
val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

382 
in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

383 
 _ => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

384 
if num_exists > 0 then 
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

385 
pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

387 
(list_comb (t, args), seen) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

388 
in aux [] 0 t [] [] > fst end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

389 

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

390 
fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

392 
val num_occs_of_var = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

393 
fold_aterms (fn Var z => (fn f => fn z' => f z' > z = z' ? Integer.add 1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

394 
 _ => I) t (K 0) 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

395 
fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) = 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

396 
aux_eq Ts careful true t0 t1 t2 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

397 
 aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) = 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

398 
t0 $ aux Ts false t1 $ aux Ts careful t2 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

399 
 aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) = 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

400 
aux_eq Ts careful true t0 t1 t2 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

401 
 aux Ts careful ((t0 as @{const HOL.implies}) $ t1 $ t2) = 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

402 
t0 $ aux Ts false t1 $ aux Ts careful t2 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

403 
 aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t') 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

404 
 aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

405 
 aux _ _ t = t 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

406 
and aux_eq Ts careful pass1 t0 t1 t2 = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

407 
((if careful then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

408 
raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

409 
else if axiom andalso is_Var t2 andalso 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

410 
num_occs_of_var (dest_Var t2) = 1 then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

411 
@{const True} 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

412 
else case strip_comb t2 of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

413 
(* The first case is not as general as it could be. *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

414 
(Const (@{const_name PairBox}, _), 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

415 
[Const (@{const_name fst}, _) $ Var z1, 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

416 
Const (@{const_name snd}, _) $ Var z2]) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

417 
if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True} 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

418 
else raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

419 
 (Const (x as (s, T)), args) => 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

420 
let 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

421 
val (arg_Ts, dataT) = strip_type T 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

422 
val n = length arg_Ts 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

423 
in 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

424 
if length args = n andalso 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

425 
(is_constr ctxt stds x orelse s = @{const_name Pair} orelse 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

426 
x = (@{const_name Suc}, nat_T > nat_T)) andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

427 
(not careful orelse not (is_Var t1) orelse 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

428 
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

429 
s_let Ts "l" (n + 1) dataT bool_T 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

430 
(fn t1 => 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

431 
discriminate_value hol_ctxt x t1 :: 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

432 
map3 (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

433 
> foldr1 s_conj) t1 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

435 
raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

437 
 _ => raise SAME ()) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

438 
> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop) 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

439 
handle SAME () => if pass1 then aux_eq Ts careful false t0 t2 t1 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

440 
else t0 $ aux Ts false t2 $ aux Ts false t1 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

441 
and sel_eq Ts x t n nth_T nth_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

442 
HOLogic.eq_const nth_T $ nth_t 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

443 
$ select_nth_constr_arg ctxt stds x t n nth_T 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

444 
> aux Ts false 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

445 
in aux [] axiom t end 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

446 

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

447 
(** Destruction of universal and existential equalities **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

448 

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

449 
fun curry_assms (@{const "==>"} $ (@{const Trueprop} 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

450 
$ (@{const HOL.conj} $ t1 $ t2)) $ t3) = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

451 
curry_assms (Logic.list_implies ([t1, t2] > map HOLogic.mk_Trueprop, t3)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

452 
 curry_assms (@{const "==>"} $ t1 $ t2) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

453 
@{const "==>"} $ curry_assms t1 $ curry_assms t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

454 
 curry_assms t = t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

455 

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

456 
val destroy_universal_equalities = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

458 
fun aux prems zs t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

459 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

460 
@{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

461 
 _ => Logic.list_implies (rev prems, t) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

462 
and aux_implies prems zs t1 t2 = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

463 
case t1 of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

464 
Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

465 
 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

466 
aux_eq prems zs z t' t1 t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

467 
 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

468 
aux_eq prems zs z t' t1 t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

469 
 _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

470 
and aux_eq prems zs z t' t1 t2 = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

471 
if not (member (op =) zs z) andalso 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

472 
not (exists_subterm (curry (op =) (Var z)) t') then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

473 
aux prems zs (subst_free [(Var z, t')] t2) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

475 
aux (t1 :: prems) (Term.add_vars t1 zs) t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

476 
in aux [] [] end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

477 

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

478 
fun find_bound_assign ctxt stds j = 
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

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

480 
fun do_term _ [] = NONE 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

481 
 do_term seen (t :: ts) = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

483 
fun do_eq pass1 t1 t2 = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

484 
(if loose_bvar1 (t2, j) 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

485 
if pass1 then do_eq false t2 t1 else raise SAME () 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

487 
Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME () 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

488 
 Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' => 
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

489 
if j' = j andalso 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

490 
s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

491 
SOME (construct_value ctxt stds 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

492 
(@{const_name FunBox}, T2 > T1) [t2], 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

493 
ts @ seen) 
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

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

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

496 
 _ => raise SAME ()) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

497 
handle SAME () => do_term (t :: seen) ts 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

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

500 
Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2 
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

501 
 _ => do_term (t :: seen) ts 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

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

504 

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

505 
fun subst_one_bound j arg t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

507 
fun aux (Bound i, lev) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

508 
if i < lev then raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

509 
else if i = lev then incr_boundvars (lev  j) arg 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

510 
else Bound (i  1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

511 
 aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

512 
 aux (f $ t, lev) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

513 
(aux (f, lev) $ (aux (t, lev) handle SAME () => t) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

514 
handle SAME () => f $ aux (t, lev)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

515 
 aux _ = raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

516 
in aux (t, j) handle SAME () => t end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

517 

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

518 
fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

520 
fun kill [] [] ts = foldr1 s_conj ts 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

521 
 kill (s :: ss) (T :: Ts) ts = 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

522 
(case find_bound_assign ctxt stds (length ss) [] ts of 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

523 
SOME (_, []) => @{const True} 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

524 
 SOME (arg_t, ts) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

525 
kill ss Ts (map (subst_one_bound (length ss) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

526 
(incr_bv (~1, length ss + 1, arg_t))) ts) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

527 
 NONE => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

528 
Const (@{const_name Ex}, (T > bool_T) > bool_T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

529 
$ Abs (s, T, kill ss Ts ts)) 
40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
39687
diff
changeset

530 
 kill _ _ _ = raise ListPair.UnequalLengths 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

531 
fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

532 
gather (ss @ [s1]) (Ts @ [T1]) t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

533 
 gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

534 
 gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

535 
 gather [] [] t = t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

536 
 gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

537 
in gather [] [] end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

538 

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

539 
(** Skolemization **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

540 

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

541 
fun skolem_prefix_for k j = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

542 
skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

543 

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

544 
fun skolemize_term_and_more (hol_ctxt as {thy, def_tables, skolems, ...}) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

547 
val incrs = map (Integer.add 1) 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

548 
fun aux ss Ts js skolemizable polar t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

550 
fun do_quantifier quant_s quant_T abs_s abs_T t = 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

551 
(if not (loose_bvar1 (t, 0)) then 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

552 
aux ss Ts js skolemizable polar (incr_boundvars ~1 t) 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

553 
else if is_positive_existential polar quant_s then 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

554 
let 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

555 
val j = length (!skolems) + 1 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

556 
val (js', (ss', Ts')) = 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

557 
js ~~ (ss ~~ Ts) 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

558 
> filter (fn (j, _) => loose_bvar1 (t, j + 1)) 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

559 
> ListPair.unzip > ListPair.unzip 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

560 
in 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

561 
if skolemizable andalso length js' <= skolem_depth then 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

562 
let 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

563 
val sko_s = skolem_prefix_for (length js') j ^ abs_s 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

564 
val _ = Unsynchronized.change skolems (cons (sko_s, ss')) 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

565 
val sko_t = list_comb (Const (sko_s, rev Ts' > abs_T), 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

566 
map Bound (rev js')) 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

567 
val abs_t = Abs (abs_s, abs_T, 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

568 
aux ss Ts (incrs js) skolemizable polar t) 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

569 
in 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

570 
if null js' then 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

571 
s_betapply Ts (abs_t, sko_t) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

572 
else 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

573 
Const (@{const_name Let}, abs_T > quant_T) $ sko_t 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

574 
$ abs_t 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

575 
end 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

576 
else 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

577 
raise SAME () 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

578 
end 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

579 
else 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

580 
raise SAME ()) 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

581 
handle SAME () => 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

582 
Const (quant_s, quant_T) 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

583 
$ Abs (abs_s, abs_T, 
38166
28bb89672cc7
fix Skolemizer  last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset

584 
aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js) 
28bb89672cc7
fix Skolemizer  last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset

585 
(skolemizable andalso 
28bb89672cc7
fix Skolemizer  last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset

586 
not (is_higher_order_type abs_T)) polar t) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

588 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

589 
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

590 
do_quantifier s0 T0 s1 T1 t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

591 
 @{const "==>"} $ t1 $ t2 => 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

592 
@{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

593 
$ aux ss Ts js skolemizable polar t2 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

594 
 @{const Pure.conjunction} $ t1 $ t2 => 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

595 
@{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

596 
$ aux ss Ts js skolemizable polar t2 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

597 
 @{const Trueprop} $ t1 => 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

598 
@{const Trueprop} $ aux ss Ts js skolemizable polar t1 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

599 
 @{const Not} $ t1 => 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

600 
@{const Not} $ aux ss Ts js skolemizable (flip_polarity polar) t1 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

601 
 Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

602 
do_quantifier s0 T0 s1 T1 t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

603 
 Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

604 
do_quantifier s0 T0 s1 T1 t1 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

605 
 @{const HOL.conj} $ t1 $ t2 => 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

606 
s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

607 
 @{const HOL.disj} $ t1 $ t2 => 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

608 
s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset

609 
 @{const HOL.implies} $ t1 $ t2 => 
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset

610 
@{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

611 
$ aux ss Ts js skolemizable polar t2 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

612 
 (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 => 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

613 
t0 $ t1 $ aux ss Ts js skolemizable polar t2 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

614 
 Const (x as (s, T)) => 
38205
37a7272cb453
handle inductive predicates correctly after change in "def" semantics
blanchet
parents:
38204
diff
changeset

615 
if is_real_inductive_pred hol_ctxt x andalso 
37a7272cb453
handle inductive predicates correctly after change in "def" semantics
blanchet
parents:
38204
diff
changeset

616 
not (is_real_equational_fun hol_ctxt x) andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

617 
not (is_well_founded_inductive_pred hol_ctxt x) then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

618 
let 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41052
diff
changeset

619 
val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp) 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

620 
val (pref, connective) = 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

621 
if gfp then (lbfp_prefix, @{const HOL.disj}) 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

622 
else (ubfp_prefix, @{const HOL.conj}) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

623 
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

624 
> aux ss Ts js skolemizable polar 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

625 
fun neg () = Const (pref ^ s, T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

626 
in 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

627 
case polar > gfp ? flip_polarity of 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

628 
Pos => pos () 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

629 
 Neg => neg () 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

630 
 Neut => 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

631 
let 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

632 
val arg_Ts = binder_types T 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

633 
fun app f = 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

634 
list_comb (f (), map Bound (length arg_Ts  1 downto 0)) 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

635 
in 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

636 
List.foldr absdummy (connective $ app pos $ app neg) arg_Ts 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

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

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

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

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

641 
 t1 $ t2 => 
38166
28bb89672cc7
fix Skolemizer  last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset

642 
s_betapply Ts (aux ss Ts js false polar t1, 
28bb89672cc7
fix Skolemizer  last week's optimizations resulted in UnequalLengths errors
blanchet
parents:
38165
diff
changeset

643 
aux ss Ts js false Neut t2) 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

644 
 Abs (s, T, t1) => 
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

645 
Abs (s, T, aux ss Ts (incrs js) skolemizable polar t1) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

646 
 _ => t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

647 
end 
37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

648 
in aux [] [] [] true Pos end 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

649 

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

650 
(** Function specialization **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

651 

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

652 
fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

653 
 params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

654 
 params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

655 
snd (strip_comb t1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

656 
 params_in_equation _ = [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

657 

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

658 
fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

660 
val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

662 
val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T)  t' => t') t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

663 
val fixed_params = filter_indices fixed_js (params_in_equation t) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

664 
fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

665 
 aux args (t1 $ t2) = aux (aux [] t2 :: args) t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

666 
 aux args t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

667 
if t = Const x then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

668 
list_comb (Const x', extra_args @ filter_out_indices fixed_js args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

670 
let val j = find_index (curry (op =) t) fixed_params in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

671 
list_comb (if j >= 0 then nth fixed_args j else t, args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

673 
in aux [] t end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

674 

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

675 
fun static_args_in_term ({ersatz_table, ...} : hol_context) x t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

677 
fun fun_calls (Abs (_, _, t)) _ = fun_calls t [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

678 
 fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

679 
 fun_calls t args = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

680 
(case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

681 
Const (x' as (s', T')) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

682 
x = x' orelse (case AList.lookup (op =) ersatz_table s' of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

683 
SOME s'' => x = (s'', T') 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

684 
 NONE => false) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

685 
 _ => false) ? cons args 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

686 
fun call_sets [] [] vs = [vs] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

687 
 call_sets [] uss vs = vs :: call_sets uss [] [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

688 
 call_sets ([] :: _) _ _ = [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

689 
 call_sets ((t :: ts) :: tss) uss vs = 
39687  690 
Ord_List.insert Term_Ord.term_ord t vs > call_sets tss (ts :: uss) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

691 
val sets = call_sets (fun_calls t [] []) [] [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

692 
val indexed_sets = sets ~~ (index_seq 0 (length sets)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

694 
fold_rev (fn (set, j) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

695 
case set of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

696 
[Var _] => AList.lookup (op =) indexed_sets set = SOME j 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

697 
? cons (j, NONE) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

698 
 [t as Const _] => cons (j, SOME t) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

699 
 [t as Free _] => cons (j, SOME t) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

700 
 _ => I) indexed_sets [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

702 
fun static_args_in_terms hol_ctxt x = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

703 
map (static_args_in_term hol_ctxt x) 
39687  704 
#> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord))) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

705 

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

706 
fun overlapping_indices [] _ = [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

707 
 overlapping_indices _ [] = [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

708 
 overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

709 
if j1 < j2 then overlapping_indices ps1' ps2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

710 
else if j1 > j2 then overlapping_indices ps1 ps2' 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

711 
else overlapping_indices ps1' ps2' > the_default t2 t1 = t2 ? cons j1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

712 

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

713 
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

714 

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

715 
(* If a constant's definition is picked up deeper than this threshold, we 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

716 
prevent excessive specialization by not specializing it. *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

717 
val special_max_depth = 20 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

718 

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

719 
val bound_var_prefix = "b" 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

720 

38165
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset

721 
fun special_fun_aconv ((x1, js1, ts1), (x2, js2, ts2)) = 
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset

722 
x1 = x2 andalso js1 = js2 andalso length ts1 = length ts2 andalso 
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset

723 
forall (op aconv) (ts1 ~~ ts2) 
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset

724 

38204  725 
fun specialize_consts_in_term 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41052
diff
changeset

726 
(hol_ctxt as {ctxt, thy, stds, specialize, def_tables, simp_table, 
39359  727 
special_funs, ...}) def depth t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

728 
if not specialize orelse depth > special_max_depth then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

731 
let 
38206  732 
val blacklist = 
733 
if def then case term_under_def t of Const x => [x]  _ => [] else [] 

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

734 
fun aux args Ts (Const (x as (s, T))) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

735 
((if not (member (op =) blacklist x) andalso not (null args) andalso 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

736 
not (String.isPrefix special_prefix s) andalso 
39359  737 
not (is_built_in_const thy stds x) andalso 
38204  738 
(is_equational_fun_but_no_plain_def hol_ctxt x orelse 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41052
diff
changeset

739 
(is_some (def_of_const thy def_tables x) andalso 
38204  740 
not (is_of_class_const thy x) andalso 
741 
not (is_constr ctxt stds x) andalso 

742 
not (is_choice_spec_fun hol_ctxt x))) then 

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

743 
let 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

744 
val eligible_args = 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

745 
filter (is_special_eligible_arg true Ts o snd) 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

746 
(index_seq 0 (length args) ~~ args) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

747 
val _ = not (null eligible_args) orelse raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

748 
val old_axs = equational_fun_axioms hol_ctxt x 
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

749 
> map (destroy_existential_equalities hol_ctxt) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

750 
val static_params = static_args_in_terms hol_ctxt x old_axs 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

751 
val fixed_js = overlapping_indices static_params eligible_args 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

752 
val _ = not (null fixed_js) orelse raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

753 
val fixed_args = filter_indices fixed_js args 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

754 
val vars = fold Term.add_vars fixed_args [] 
35408  755 
> sort (Term_Ord.fast_indexname_ord o pairself fst) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

756 
val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

757 
fixed_args [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

758 
> sort int_ord 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

759 
val live_args = filter_out_indices fixed_js args 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

760 
val extra_args = map Var vars @ map Bound bound_js @ live_args 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

761 
val extra_Ts = map snd vars @ filter_indices bound_js Ts 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

762 
val k = maxidx_of_term t + 1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

763 
fun var_for_bound_no j = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

764 
Var ((bound_var_prefix ^ 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

765 
nat_subscript (find_index (curry (op =) j) bound_js 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

766 
+ 1), k), 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

767 
nth Ts j) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

768 
val fixed_args_in_axiom = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

769 
map (curry subst_bounds 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

770 
(map var_for_bound_no (index_seq 0 (length Ts)))) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

772 
in 
38165
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset

773 
case AList.lookup special_fun_aconv (!special_funs) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

774 
(x, fixed_js, fixed_args_in_axiom) of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

775 
SOME x' => list_comb (Const x', extra_args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

776 
 NONE => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

778 
val extra_args_in_axiom = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

779 
map Var vars @ map var_for_bound_no bound_js 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

780 
val x' as (s', _) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

781 
(special_prefix_for (length (!special_funs) + 1) ^ s, 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

782 
extra_Ts @ filter_out_indices fixed_js (binder_types T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

783 
> body_type T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

784 
val new_axs = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

785 
map (specialize_fun_axiom x x' fixed_js 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

786 
fixed_args_in_axiom extra_args_in_axiom) old_axs 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

787 
val _ = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

788 
Unsynchronized.change special_funs 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

789 
(cons ((x, fixed_js, fixed_args_in_axiom), x')) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

790 
val _ = add_simps simp_table s' new_axs 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

791 
in list_comb (Const x', extra_args) end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

794 
raise SAME ()) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

795 
handle SAME () => list_comb (Const x, args)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

796 
 aux args Ts (Abs (s, T, t)) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

797 
list_comb (Abs (s, T, aux [] (T :: Ts) t), args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

798 
 aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

799 
 aux args _ t = list_comb (t, args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

800 
in aux [] [] t end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

801 

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

802 
type special_triple = int list * term list * styp 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

803 

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

804 
val cong_var_prefix = "c" 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

805 

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

806 
fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

808 
val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

809 
val Ts = binder_types T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

810 
val max_j = fold (fold Integer.max) [js1, js2] ~1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

811 
val (eqs, (args1, args2)) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

812 
fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

813 
(js1 ~~ ts1, js2 ~~ ts2) of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

814 
(SOME t1, SOME t2) => apfst (cons (t1, t2)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

815 
 (SOME t1, NONE) => apsnd (apsnd (cons t1)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

816 
 (NONE, SOME t2) => apsnd (apfst (cons t2)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

817 
 (NONE, NONE) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

818 
let val v = Var ((cong_var_prefix ^ nat_subscript j, 0), 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

819 
nth Ts j) in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

820 
apsnd (pairself (cons v)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

821 
end) (max_j downto 0) ([], ([], [])) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

822 
in 
38165
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset

823 
Logic.list_implies (eqs > filter_out (op aconv) > distinct (op =) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

824 
> map Logic.mk_equals, 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

825 
Logic.mk_equals (list_comb (Const x1, bounds1 @ args1), 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

826 
list_comb (Const x2, bounds2 @ args2))) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

828 

38170  829 
fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) ts = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

831 
val groups = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

833 
> map (fn ((x, js, ts), x') => (x, (js, ts, x'))) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

834 
> AList.group (op =) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

835 
> filter_out (is_equational_fun_surely_complete hol_ctxt o fst) 
38170  836 
> map (fn (x, zs) => 
837 
(x, zs > member (op =) ts (Const x) ? cons ([], [], x))) 

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

838 
fun generality (js, _, _) = ~(length js) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

839 
fun is_more_specific (j1, t1, x1) (j2, t2, x2) = 
38165
9797be44df23
prevent generation of needless specialized constants etc.
blanchet
parents:
37928
diff
changeset

840 
x1 <> x2 andalso length j2 < length j1 andalso 
39687  841 
Ord_List.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

842 
fun do_pass_1 _ [] [_] [_] = I 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

843 
 do_pass_1 T skipped _ [] = do_pass_2 T skipped 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

844 
 do_pass_1 T skipped all (z :: zs) = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

845 
case filter (is_more_specific z) all 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

846 
> sort (int_ord o pairself generality) of 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

847 
[] => do_pass_1 T (z :: skipped) all zs 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

848 
 (z' :: _) => cons (special_congruence_axiom T z z') 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

849 
#> do_pass_1 T skipped all zs 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

850 
and do_pass_2 _ [] = I 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

851 
 do_pass_2 T (z :: zs) = 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

852 
fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

853 
in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

854 

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

855 
(** Axiom selection **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

856 

38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

857 
fun defined_free_by_assumption t = 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

858 
let 
38170  859 
fun do_equals x def = 
860 
if exists_subterm (curry (op aconv) (Free x)) def then NONE else SOME x 

38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

861 
in 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

862 
case t of 
38170  863 
Const (@{const_name "=="}, _) $ Free x $ def => do_equals x def 
864 
 @{const Trueprop} $ (Const (@{const_name "=="}, _) $ Free x $ def) => 

865 
do_equals x def 

38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

866 
 _ => NONE 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

867 
end 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

868 

b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

869 
fun assumption_exclusively_defines_free assm_ts t = 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

870 
case defined_free_by_assumption t of 
38170  871 
SOME x => 
872 
length (filter ((fn SOME x' => x = x'  NONE => false) 

38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

873 
o defined_free_by_assumption) assm_ts) = 1 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

874 
 NONE => false 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

875 

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

876 
fun all_table_entries table = Symtab.fold (append o snd) table [] 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41052
diff
changeset

877 
fun extra_table tables s = 
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41052
diff
changeset

878 
Symtab.make [(s, pairself all_table_entries tables > op @)] 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

879 

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

880 
fun eval_axiom_for_term j t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

881 
Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

882 

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

883 
val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

884 

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

885 
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

886 
val axioms_max_depth = 255 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

887 

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

888 
fun axioms_for_term 
35311  889 
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms, 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41052
diff
changeset

890 
evals, def_tables, nondef_table, choice_spec_table, 
39359  891 
user_nondefs, ...}) assm_ts neg_t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

892 
let 
38170  893 
val (def_assm_ts, nondef_assm_ts) = 
894 
List.partition (assumption_exclusively_defines_free assm_ts) assm_ts 

895 
val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts 

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

896 
type accumulator = styp list * (term list * term list) 
38206  897 
fun add_axiom get app def depth t (accum as (seen, axs)) = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

899 
val t = t > unfold_defs_in_term hol_ctxt 
38206  900 
> skolemize_term_and_more hol_ctxt ~1 (* FIXME: why ~1? *) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

902 
if is_trivial_equation t then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

904 
else 
38206  905 
let val t' = t > specialize_consts_in_term hol_ctxt def depth in 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

906 
if exists (member (op aconv) (get axs)) [t, t'] then accum 
38170  907 
else add_axioms_for_term (depth + 1) t' (seen, app (cons t') axs) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

909 
end 
38206  910 
and add_def_axiom depth = add_axiom fst apfst true depth 
911 
and add_nondef_axiom depth = add_axiom snd apsnd false depth 

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

912 
and add_maybe_def_axiom depth t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

913 
(if head_of t <> @{const "==>"} then add_def_axiom 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

914 
else add_nondef_axiom) depth t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

915 
and add_eq_axiom depth t = 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

916 
(if is_constr_pattern_formula ctxt t then add_def_axiom 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

917 
else add_nondef_axiom) depth t 
38170  918 
and add_axioms_for_term depth t (accum as (seen, axs)) = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

919 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

920 
t1 $ t2 => accum > fold (add_axioms_for_term depth) [t1, t2] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

921 
 Const (x as (s, T)) => 
39359  922 
(if member (op aconv) seen t orelse is_built_in_const thy stds x then 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

924 
else 
38170  925 
let val accum = (t :: seen, axs) in 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

926 
if depth > axioms_max_depth then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

927 
raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\ 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

928 
\add_axioms_for_term", 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

929 
"too many nested axioms (" ^ 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

930 
string_of_int depth ^ ")") 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

931 
else if is_of_class_const thy x then 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

933 
val class = Logic.class_of_const s 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

934 
val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

935 
class) 
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset

936 
val ax1 = try (specialize_type thy x) of_class 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset

937 
val ax2 = Option.map (specialize_type thy x o snd) 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

938 
(get_class_def thy class) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

940 
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2]) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

943 
else if is_constr ctxt stds x then 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

944 
accum 
37271  945 
else if is_descr (original_name s) then 
946 
fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x) 

947 
accum 

38202
379fb08da97b
prevent the expansion of too large definitions  use equations for these instead
blanchet
parents:
38190
diff
changeset

948 
else if is_equational_fun_but_no_plain_def hol_ctxt x then 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

949 
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

951 
else if is_choice_spec_fun hol_ctxt x then 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset

952 
fold (add_nondef_axiom depth) 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset

953 
(nondef_props_for_const thy true choice_spec_table x) accum 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

954 
else if is_abs_fun ctxt x then 
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

955 
accum > fold (add_nondef_axiom depth) 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

956 
(nondef_props_for_const thy false nondef_table x) 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

957 
> (is_funky_typedef ctxt (range_type T) orelse 
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

958 
range_type T = nat_T) 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

959 
? fold (add_maybe_def_axiom depth) 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

960 
(nondef_props_for_const thy true 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41052
diff
changeset

961 
(extra_table def_tables s) x) 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

962 
else if is_rep_fun ctxt x then 
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

963 
accum > fold (add_nondef_axiom depth) 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

964 
(nondef_props_for_const thy false nondef_table x) 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

965 
> (is_funky_typedef ctxt (range_type T) orelse 
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

966 
range_type T = nat_T) 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

967 
? fold (add_maybe_def_axiom depth) 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

968 
(nondef_props_for_const thy true 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41052
diff
changeset

969 
(extra_table def_tables s) x) 
38215
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

970 
> add_axioms_for_term depth 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

971 
(Const (mate_of_rep_fun ctxt x)) 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

972 
> fold (add_def_axiom depth) 
1c7d7eaebdf2
quotient types registered as codatatypes are no longer quotient types
blanchet
parents:
38207
diff
changeset

973 
(inverse_axioms_for_rep_fun ctxt x) 
37253  974 
else if s = @{const_name TYPE} then 
975 
accum 

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

976 
else case def_of_const thy def_tables x of 
39345  977 
SOME _ => 
38202
379fb08da97b
prevent the expansion of too large definitions  use equations for these instead
blanchet
parents:
38190
diff
changeset

978 
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) 
379fb08da97b
prevent the expansion of too large definitions  use equations for these instead
blanchet
parents:
38190
diff
changeset

979 
accum 
379fb08da97b
prevent the expansion of too large definitions  use equations for these instead
blanchet
parents:
38190
diff
changeset

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

981 
accum > user_axioms <> SOME false 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

982 
? fold (add_nondef_axiom depth) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

983 
(nondef_props_for_const thy false nondef_table x) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

985 
> add_axioms_for_type depth T 
38170  986 
 Free (x as (_, T)) => 
987 
(if member (op aconv) seen t then 

988 
accum 

989 
else case AList.lookup (op =) def_assm_table x of 

990 
SOME t => add_def_axiom depth t accum 

991 
 NONE => accum) 

992 
> add_axioms_for_type depth T 

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

993 
 Var (_, T) => add_axioms_for_type depth T accum 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

994 
 Bound _ => accum 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

995 
 Abs (_, T, t) => accum > add_axioms_for_term depth t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

996 
> add_axioms_for_type depth T 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

997 
and add_axioms_for_type depth T = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

998 
case T of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

999 
Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38170
diff
changeset

1000 
 Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1001 
 @{typ prop} => I 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1002 
 @{typ bool} => I 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1003 
 TFree (_, S) => add_axioms_for_sort depth T S 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1004 
 TVar (_, S) => add_axioms_for_sort depth T S 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1005 
 Type (z as (_, Ts)) => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1006 
fold (add_axioms_for_type depth) Ts 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1007 
#> (if is_pure_typedef ctxt T then 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1008 
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z) 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38215
diff
changeset

1009 
else if is_quot_type ctxt T then 
35311  1010 
fold (add_def_axiom depth) 
1011 
(optimized_quot_type_axioms ctxt stds z) 

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

1012 
else if max_bisim_depth >= 0 andalso is_codatatype ctxt T then 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1013 
fold (add_maybe_def_axiom depth) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1014 
(codatatype_bisim_axioms hol_ctxt T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

1017 
and add_axioms_for_sort depth T S = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1019 
val supers = Sign.complete_sort thy S 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1020 
val class_axioms = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1021 
maps (fn class => map prop_of (AxClass.get_info thy class > #axioms 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1022 
handle ERROR _ => [])) supers 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1023 
val monomorphic_class_axioms = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1024 
map (fn t => case Term.add_tvars t [] of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1025 
[] => t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1026 
 [(x, S)] => 
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset

1027 
monomorphic_term (Vartab.make [(x, (S, T))]) t 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1028 
 _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\ 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1029 
\add_axioms_for_sort", [t])) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1031 
in fold (add_nondef_axiom depth) monomorphic_class_axioms end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1032 
val (mono_user_nondefs, poly_user_nondefs) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1033 
List.partition (null o Term.hidden_polymorphism) user_nondefs 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1034 
val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1035 
evals 
38170  1036 
val (seen, (defs, nondefs)) = 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1037 
([], ([], [])) 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1038 
> add_axioms_for_term 1 neg_t 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1039 
> fold_rev (add_nondef_axiom 1) nondef_assm_ts 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1040 
> fold_rev (add_def_axiom 1) eval_axioms 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1041 
> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs 
38170  1042 
val defs = defs @ special_congruence_axioms hol_ctxt seen 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

1043 
val got_all_mono_user_axioms = 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

1044 
(user_axioms = SOME true orelse null mono_user_nondefs) 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1045 
in 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1046 
(neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

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

1048 

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

1049 
(** Simplification of constructor/selector terms **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1050 

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

1051 
fun simplify_constrs_and_sels ctxt t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1053 
fun is_nth_sel_on t' n (Const (s, _) $ t) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1054 
(t = t' andalso is_sel_like_and_no_discr s andalso 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1055 
sel_no_from_name s = n) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1056 
 is_nth_sel_on _ _ _ = false 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1057 
fun do_term (Const (@{const_name Rep_Frac}, _) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1058 
$ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1059 
 do_term (Const (@{const_name Abs_Frac}, _) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1060 
$ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1061 
 do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1062 
 do_term (t as Const (x as (s, T))) (args as _ :: _) = 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1063 
((if is_constr_like ctxt x then 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1064 
if length args = num_binder_types T then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1065 
case hd args of 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1066 
Const (_, T') $ t' => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1067 
if domain_type T' = body_type T andalso 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1068 
forall (uncurry (is_nth_sel_on t')) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1069 
(index_seq 0 (length args) ~~ args) then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

1072 
raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1073 
 _ => raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1075 
raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1076 
else if is_sel_like_and_no_discr s then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1077 
case strip_comb (hd args) of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1078 
(Const (x' as (s', T')), ts') => 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset

1079 
if is_constr_like ctxt x' andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1080 
constr_name_for_sel_like s = s' andalso 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1081 
not (exists is_pair_type (binder_types T')) then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1082 
list_comb (nth ts' (sel_no_from_name s), tl args) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1084 
raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1085 
 _ => raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1087 
raise SAME ()) 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

1088 
handle SAME () => s_betapplys [] (t, args)) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1089 
 do_term (Abs (s, T, t')) args = 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

1090 
s_betapplys [] (Abs (s, T, do_term t' []), args) 
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37271
diff
changeset

1091 
 do_term t args = s_betapplys [] (t, args) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1092 
in do_term t [] end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1093 

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

1094 
(** Quantifier massaging: Distributing quantifiers **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1095 

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

1096 
fun distribute_quantifiers t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1097 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1098 
(t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1100 
(t10 as @{const HOL.conj}) $ t11 $ t12 => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1101 
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1102 
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1103 
 (t10 as @{const Not}) $ t11 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1104 
t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1105 
$ Abs (s, T1, t11)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1106 
 t1 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1107 
if not (loose_bvar1 (t1, 0)) then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1108 
distribute_quantifiers (incr_boundvars ~1 t1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1110 
t0 $ Abs (s, T1, distribute_quantifiers t1)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1111 
 (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1112 
(case distribute_quantifiers t1 of 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

1113 
(t10 as @{const HOL.disj}) $ t11 $ t12 => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1114 
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1115 
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38240
diff
changeset

1116 
 (t10 as @{const HOL.implies}) $ t11 $ t12 => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1117 
t10 $ distribute_quantifiers (Const (@{const_name All}, T0) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1118 
$ Abs (s, T1, t11)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1119 
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1120 
 (t10 as @{const Not}) $ t11 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1121 
t10 $ distribute_quantifiers (Const (@{const_name All}, T0) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1122 
$ Abs (s, T1, t11)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1123 
 t1 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1124 
if not (loose_bvar1 (t1, 0)) then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1125 
distribute_quantifiers (incr_boundvars ~1 t1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1127 
t0 $ Abs (s, T1, distribute_quantifiers t1)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1128 
 t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1129 
 Abs (s, T, t') => Abs (s, T, distribute_quantifiers t') 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1130 
 _ => t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1131 

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

1132 
(** Quantifier massaging: Pushing quantifiers inward **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1133 

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

1134 
fun renumber_bounds j n f t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1135 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1136 
t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1137 
 Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t') 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1138 
 Bound j' => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1139 
Bound (if j' >= j andalso j' < j + n then f (j'  j) + j else j') 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1140 
 _ => t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1141 

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

1142 
(* Maximum number of quantifiers in a cluster for which the exponential 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1143 
algorithm is used. Larger clusters use a heuristic inspired by Claessen & 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

1144 
Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1145 
paper). *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1146 
val quantifier_cluster_threshold = 7 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1147 

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

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

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

1150 
fun aux quant_s ss Ts t = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1151 
(case t of 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1152 
Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1153 
if s0 = quant_s then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1154 
aux s0 (s1 :: ss) (T1 :: Ts) t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1155 
else if quant_s = "" andalso 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1156 
(s0 = @{const_name All} orelse s0 = @{const_name Ex}) then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1157 
aux s0 [s1] [T1] t1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1159 
raise SAME () 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1160 
 _ => raise SAME ()) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1161 
handle SAME () => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1162 
case t of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1163 
t1 $ t2 => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1164 
if quant_s = "" then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1165 
aux "" [] [] t1 $ aux "" [] [] t2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

1168 
fun big_union proj ps = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1169 
fold (fold (insert (op =)) o proj) ps [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1170 
val (ts, connective) = strip_any_connective t 
41860
49d0fc8c418c
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
blanchet
parents:
41803
diff
changeset

1171 
val T_costs = map typical_card_of_type Ts 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1172 
val t_costs = map size_of_term ts 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1173 
val num_Ts = length Ts 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1174 
val flip = curry (op ) (num_Ts  1) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1175 
val t_boundss = map (map flip o loose_bnos) ts 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1176 
fun merge costly_boundss [] = costly_boundss 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1177 
 merge costly_boundss (j :: js) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1179 
val (yeas, nays) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1180 
List.partition (fn (bounds, _) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1181 
member (op =) bounds j) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1183 
val yeas_bounds = big_union fst yeas 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1184 
val yeas_cost = Integer.sum (map snd yeas) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1185 
* nth T_costs j 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1186 
in merge ((yeas_bounds, yeas_cost) :: nays) js end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1187 
val cost = Integer.sum o map snd oo merge 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1188 
fun heuristically_best_permutation _ [] = [] 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1189 
 heuristically_best_permutation costly_boundss js = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1191 
val (costly_boundss, (j, js)) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1192 
js > map (`(merge costly_boundss o single)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1193 
> sort (int_ord 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1194 
o pairself (Integer.sum o map snd o fst)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1195 
> split_list >> hd > pairf hd tl 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1197 
j :: heuristically_best_permutation costly_boundss js 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1199 
val js = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1200 
if length Ts <= quantifier_cluster_threshold then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1201 
all_permutations (index_seq 0 num_Ts) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1202 
> map (`(cost (t_boundss ~~ t_costs))) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1203 
> sort (int_ord o pairself fst) > hd > snd 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1205 
heuristically_best_permutation (t_boundss ~~ t_costs) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1206 
(index_seq 0 num_Ts) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1207 
val back_js = map (fn j => find_index (curry (op =) j) js) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1208 
(index_seq 0 num_Ts) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1209 
val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1211 
fun mk_connection [] = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1212 
raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\ 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1213 
\mk_connection", "") 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1214 
 mk_connection ts_cum_bounds = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1215 
ts_cum_bounds > map fst 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1216 
> foldr1 (fn (t1, t2) => connective $ t1 $ t2) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1217 
fun build ts_cum_bounds [] = ts_cum_bounds > mk_connection 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1218 
 build ts_cum_bounds (j :: js) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1220 
val (yeas, nays) = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1221 
List.partition (fn (_, bounds) => 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1222 
member (op =) bounds j) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1224 
> map (apfst (incr_boundvars ~1)) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1226 
if null yeas then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1227 
build nays js 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

1229 
let val T = nth Ts (flip j) in 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1230 
build ((Const (quant_s, (T > bool_T) > bool_T) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1231 
$ Abs (nth ss (flip j), T, 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1232 
mk_connection yeas), 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1233 
big_union snd yeas) :: nays) js 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

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

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

1236 
in build (ts ~~ t_boundss) js end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1237 
 Abs (s, T, t') => Abs (s, T, aux "" [] [] t') 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1238 
 _ => t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1239 
in aux "" [] [] end 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1240 

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

1241 
(** Preprocessor entry point **) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1242 

37928
24785fa2416c
do a better job at Skolemizing in Nitpick, for TPTP FOF
blanchet
parents:
37704
diff
changeset

1243 
val max_skolem_depth = 3 
36389
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

1244 

38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1245 
fun preprocess_formulas 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1246 
(hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes, 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41793
diff
changeset

1247 
preconstrs, ...}) assm_ts neg_t = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1248 
let 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

1249 
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1250 
neg_t > unfold_defs_in_term hol_ctxt 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1251 
> close_form 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1252 
> skolemize_term_and_more hol_ctxt max_skolem_depth 
38206  1253 
> specialize_consts_in_term hol_ctxt false 0 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38166
diff
changeset

1254 
> axioms_for_term hol_ctxt assm_ts 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1255 
val binarize = 
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

1256 
is_standard_datatype thy stds nat_T andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1257 
case binary_ints of 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset

1258 
SOME false => false 
35718  1259 
 _ => forall (may_use_binary_ints false) nondef_ts andalso 
1260 
forall (may_use_binary_ints true) def_ts 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

1261 
(binary_ints = SOME true orelse 
35386 