author | desharna |
Mon, 20 Sep 2021 15:30:03 +0200 | |
changeset 74328 | 404ce20efc4c |
parent 69597 | ff784d5a5bfb |
child 74379 | 9ea507f63bcb |
permissions | -rw-r--r-- |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/ATP/atp_util.ML |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
3 |
|
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
4 |
General-purpose functions used by the ATP module. |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
5 |
*) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
6 |
|
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
7 |
signature ATP_UTIL = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
8 |
sig |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
9 |
val timestamp : unit -> string |
53514 | 10 |
val hashw : word * word -> word |
11 |
val hashw_string : string * word -> word |
|
43827
62d64709af3b
added option to control which lambda translation to use (for experiments)
blanchet
parents:
43572
diff
changeset
|
12 |
val hash_string : string -> int |
48323 | 13 |
val chunk_list : int -> 'a list -> 'a list list |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48247
diff
changeset
|
14 |
val stringN_of_int : int -> int -> string |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
15 |
val strip_spaces : bool -> (char -> bool) -> string -> string |
44784 | 16 |
val strip_spaces_except_between_idents : string -> string |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48251
diff
changeset
|
17 |
val elide_string : int -> string -> string |
52077 | 18 |
val find_enclosed : string -> string -> string -> string list |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
19 |
val nat_subscript : int -> string |
52076
bfa28e1cba77
freeze types in Sledgehammer goal, not just terms
blanchet
parents:
52031
diff
changeset
|
20 |
val unquote_tvar : string -> string |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58919
diff
changeset
|
21 |
val maybe_quote : Keyword.keywords -> string -> string |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51209
diff
changeset
|
22 |
val string_of_ext_time : bool * Time.time -> string |
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51209
diff
changeset
|
23 |
val string_of_time : Time.time -> string |
47150 | 24 |
val type_instance : theory -> typ -> typ -> bool |
25 |
val type_generalization : theory -> typ -> typ -> bool |
|
26 |
val type_intersect : theory -> typ -> typ -> bool |
|
27 |
val type_equiv : theory -> typ * typ -> bool |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
28 |
val varify_type : Proof.context -> typ -> typ |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
29 |
val instantiate_type : theory -> typ -> typ -> typ -> typ |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
30 |
val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ |
44393 | 31 |
val is_type_surely_finite : Proof.context -> typ -> bool |
44399 | 32 |
val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool |
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
33 |
val s_not : term -> term |
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
34 |
val s_conj : term * term -> term |
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
35 |
val s_disj : term * term -> term |
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
36 |
val s_imp : term * term -> term |
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
37 |
val s_iff : term * term -> term |
49983
33e18e9916a8
use metaquantification when possible in Isar proofs
blanchet
parents:
49982
diff
changeset
|
38 |
val close_form : term -> term |
49982 | 39 |
val hol_close_form_prefix : string |
40 |
val hol_close_form : term -> term |
|
41 |
val hol_open_form : (string -> string) -> term -> term |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
42 |
val eta_expand : typ list -> term -> int -> term |
59632 | 43 |
val cong_extensionalize_term : Proof.context -> term -> term |
47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47718
diff
changeset
|
44 |
val abs_extensionalize_term : Proof.context -> term -> term |
47991
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
45 |
val unextensionalize_def : term -> term |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
46 |
val transform_elim_prop : term -> term |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
47 |
val specialize_type : theory -> (string * typ) -> term -> term |
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
48 |
val strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term |
57541 | 49 |
val extract_lambda_def : (term -> string * typ) -> term -> string * term |
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
50 |
val short_thm_name : Proof.context -> thm -> string |
74328 | 51 |
val map_prod : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
52 |
end; |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
53 |
|
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
54 |
structure ATP_Util : ATP_UTIL = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
55 |
struct |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
56 |
|
53800 | 57 |
fun timestamp_format time = |
58 |
Date.fmt "%Y-%m-%d %H:%M:%S." (Date.fromTimeLocal time) ^ |
|
59 |
(StringCvt.padLeft #"0" 3 (string_of_int (Time.toMilliseconds time - 1000 * Time.toSeconds time))) |
|
60 |
||
61 |
val timestamp = timestamp_format o Time.now |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
62 |
|
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
63 |
(* This hash function is recommended in "Compilers: Principles, Techniques, and |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
64 |
Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
65 |
particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
66 |
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
67 |
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
68 |
fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s |
43827
62d64709af3b
added option to control which lambda translation to use (for experiments)
blanchet
parents:
43572
diff
changeset
|
69 |
fun hash_string s = Word.toInt (hashw_string (s, 0w0)) |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
70 |
|
48323 | 71 |
fun chunk_list _ [] = [] |
72 |
| chunk_list k xs = |
|
73 |
let val (xs1, xs2) = chop k xs in xs1 :: chunk_list k xs2 end |
|
74 |
||
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48247
diff
changeset
|
75 |
fun stringN_of_int 0 _ = "" |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48247
diff
changeset
|
76 |
| stringN_of_int k n = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48247
diff
changeset
|
77 |
stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48247
diff
changeset
|
78 |
|
57728
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
79 |
fun is_spaceish c = Char.isSpace c orelse c = #"\127" (* DEL -- no idea where these come from *) |
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
80 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
81 |
fun strip_spaces skip_comments is_evil = |
44935
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
82 |
let |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
83 |
fun strip_c_style_comment [] accum = accum |
57728
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
84 |
| strip_c_style_comment (#"*" :: #"/" :: cs) accum = strip_spaces_in_list true cs accum |
44935
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
85 |
| strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum |
48766
553ad5f99968
fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end
blanchet
parents:
48323
diff
changeset
|
86 |
and strip_spaces_in_list _ [] accum = accum |
44935
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
87 |
| strip_spaces_in_list true (#"%" :: cs) accum = |
67522 | 88 |
strip_spaces_in_list true (cs |> drop_prefix (not_equal #"\n")) accum |
57728
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
89 |
| strip_spaces_in_list true (#"/" :: #"*" :: cs) accum = strip_c_style_comment cs accum |
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
90 |
| strip_spaces_in_list _ [c1] accum = accum |> not (is_spaceish c1) ? cons c1 |
44935
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
91 |
| strip_spaces_in_list skip_comments (cs as [_, _]) accum = |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
92 |
accum |> fold (strip_spaces_in_list skip_comments o single) cs |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
93 |
| strip_spaces_in_list skip_comments (c1 :: c2 :: c3 :: cs) accum = |
57728
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
94 |
if is_spaceish c1 then |
44935
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
95 |
strip_spaces_in_list skip_comments (c2 :: c3 :: cs) accum |
57728
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
96 |
else if is_spaceish c2 then |
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
97 |
if is_spaceish c3 then |
44935
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
98 |
strip_spaces_in_list skip_comments (c1 :: c3 :: cs) accum |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
99 |
else |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
100 |
strip_spaces_in_list skip_comments (c3 :: cs) |
57728
c21e7bdb40ad
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet
parents:
57547
diff
changeset
|
101 |
(c1 :: accum |> forall is_evil [c1, c3] ? cons #" ") |
44935
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
102 |
else |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
103 |
strip_spaces_in_list skip_comments (c2 :: c3 :: cs) (cons c1 accum) |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
104 |
in |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
105 |
String.explode |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
106 |
#> rpair [] #-> strip_spaces_in_list skip_comments |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
107 |
#> rev #> String.implode |
2e812384afa8
tail recursive proof preprocessing (needed for huge proofs)
blanchet
parents:
44893
diff
changeset
|
108 |
end |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
109 |
|
44784 | 110 |
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
111 |
val strip_spaces_except_between_idents = strip_spaces true is_ident_char |
|
112 |
||
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48251
diff
changeset
|
113 |
fun elide_string threshold s = |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48251
diff
changeset
|
114 |
if size s > threshold then |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48251
diff
changeset
|
115 |
String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48251
diff
changeset
|
116 |
String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48251
diff
changeset
|
117 |
else |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48251
diff
changeset
|
118 |
s |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48251
diff
changeset
|
119 |
|
52077 | 120 |
fun find_enclosed left right s = |
121 |
case first_field left s of |
|
122 |
SOME (_, s) => |
|
123 |
(case first_field right s of |
|
124 |
SOME (enclosed, s) => enclosed :: find_enclosed left right s |
|
125 |
| NONE => []) |
|
126 |
| NONE => [] |
|
127 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52196
diff
changeset
|
128 |
val subscript = implode o map (prefix "\<^sub>") o raw_explode (* FIXME Symbol.explode (?) *) |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
129 |
fun nat_subscript n = |
66020 | 130 |
n |> string_of_int |> not (print_mode_active Print_Mode.ASCII) ? subscript |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
131 |
|
52076
bfa28e1cba77
freeze types in Sledgehammer goal, not just terms
blanchet
parents:
52031
diff
changeset
|
132 |
val unquote_tvar = perhaps (try (unprefix "'")) |
bfa28e1cba77
freeze types in Sledgehammer goal, not just terms
blanchet
parents:
52031
diff
changeset
|
133 |
val unquery_var = perhaps (try (unprefix "?")) |
bfa28e1cba77
freeze types in Sledgehammer goal, not just terms
blanchet
parents:
52031
diff
changeset
|
134 |
|
50239 | 135 |
val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58919
diff
changeset
|
136 |
fun maybe_quote keywords y = |
59433 | 137 |
let val s = YXML.content_of y in |
52076
bfa28e1cba77
freeze types in Sledgehammer goal, not just terms
blanchet
parents:
52031
diff
changeset
|
138 |
y |> ((not (is_long_identifier (unquote_tvar s)) andalso |
bfa28e1cba77
freeze types in Sledgehammer goal, not just terms
blanchet
parents:
52031
diff
changeset
|
139 |
not (is_long_identifier (unquery_var s))) orelse |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58919
diff
changeset
|
140 |
Keyword.is_literal keywords s) ? quote |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
141 |
end |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
142 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51209
diff
changeset
|
143 |
fun string_of_ext_time (plus, time) = |
58081
aa239fee063a
show microseconds as well (useful when playing with Isar proofs)
blanchet
parents:
57728
diff
changeset
|
144 |
let val us = Time.toMicroseconds time in |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
145 |
(if plus then "> " else "") ^ |
58088 | 146 |
(if us < 1000 then string_of_real (Real.fromInt (us div 100) / 10.0) ^ " ms" |
58081
aa239fee063a
show microseconds as well (useful when playing with Isar proofs)
blanchet
parents:
57728
diff
changeset
|
147 |
else if us < 1000000 then signed_string_of_int (us div 1000) ^ " ms" |
58088 | 148 |
else string_of_real (Real.fromInt (us div 100000) / 10.0) ^ " s") |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
149 |
end |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
150 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51209
diff
changeset
|
151 |
val string_of_time = string_of_ext_time o pair false |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
152 |
|
47150 | 153 |
fun type_instance thy T T' = Sign.typ_instance thy (T, T') |
154 |
fun type_generalization thy T T' = Sign.typ_instance thy (T', T) |
|
48247
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
155 |
|
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
156 |
fun type_intersect _ (TVar _) _ = true |
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
157 |
| type_intersect _ _ (TVar _) = true |
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
158 |
| type_intersect thy T T' = |
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
159 |
let |
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
160 |
val tvars = Term.add_tvar_namesT T [] |
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
161 |
val tvars' = Term.add_tvar_namesT T' [] |
50968
3686bc0d4df2
pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier
blanchet
parents:
50239
diff
changeset
|
162 |
val maxidx' = maxidx_of_typ T' |
48247
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
163 |
val T = |
50968
3686bc0d4df2
pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier
blanchet
parents:
50239
diff
changeset
|
164 |
T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1) |
3686bc0d4df2
pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier
blanchet
parents:
50239
diff
changeset
|
165 |
val maxidx = Integer.max (maxidx_of_typ T) maxidx' |
3686bc0d4df2
pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier
blanchet
parents:
50239
diff
changeset
|
166 |
in can (Sign.typ_unify thy (T, T')) (Vartab.empty, maxidx) end |
48247
8f37d2ddabc8
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
blanchet
parents:
48238
diff
changeset
|
167 |
|
47150 | 168 |
val type_equiv = Sign.typ_equiv |
44399 | 169 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
170 |
fun varify_type ctxt T = |
69593 | 171 |
Variable.polymorphic_types ctxt [Const (\<^const_name>\<open>undefined\<close>, T)] |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
172 |
|> snd |> the_single |> dest_Const |> snd |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
173 |
|
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
174 |
(* TODO: use "Term_Subst.instantiateT" instead? *) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
175 |
fun instantiate_type thy T1 T1' T2 = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
176 |
Same.commit (Envir.subst_type_same |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
177 |
(Sign.typ_match thy (T1, T1') Vartab.empty)) T2 |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
178 |
handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], []) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
179 |
|
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
180 |
fun varify_and_instantiate_type ctxt T1 T1' T2 = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
181 |
let val thy = Proof_Context.theory_of ctxt in |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
182 |
instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
183 |
end |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
184 |
|
54554
b8d0d8407c3b
eliminated Sledgehammer's dependency on old-style datatypes
blanchet
parents:
53800
diff
changeset
|
185 |
fun free_constructors_of ctxt (Type (s, Ts)) = |
b8d0d8407c3b
eliminated Sledgehammer's dependency on old-style datatypes
blanchet
parents:
53800
diff
changeset
|
186 |
(case Ctr_Sugar.ctr_sugar_of ctxt s of |
b8d0d8407c3b
eliminated Sledgehammer's dependency on old-style datatypes
blanchet
parents:
53800
diff
changeset
|
187 |
SOME {ctrs, ...} => map_filter (try dest_Const o Ctr_Sugar.mk_ctr Ts) ctrs |
b8d0d8407c3b
eliminated Sledgehammer's dependency on old-style datatypes
blanchet
parents:
53800
diff
changeset
|
188 |
| NONE => []) |
b8d0d8407c3b
eliminated Sledgehammer's dependency on old-style datatypes
blanchet
parents:
53800
diff
changeset
|
189 |
| free_constructors_of _ _ = [] |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
190 |
|
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
191 |
(* Similar to "Nitpick_HOL.bounded_exact_card_of_type". |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
192 |
0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
193 |
cardinality 2 or more. The specified default cardinality is returned if the |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
194 |
cardinality of the type can't be determined. *) |
44500 | 195 |
fun tiny_card_of_type ctxt sound assigns default_card T = |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
196 |
let |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
197 |
val thy = Proof_Context.theory_of ctxt |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
198 |
val max = 2 (* 1 would be too small for the "fun" case *) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
199 |
fun aux slack avoid T = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
200 |
if member (op =) avoid T then |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
201 |
0 |
47150 | 202 |
else case AList.lookup (type_equiv thy) assigns T of |
44393 | 203 |
SOME k => k |
204 |
| NONE => |
|
44392
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
205 |
case T of |
69593 | 206 |
Type (\<^type_name>\<open>fun\<close>, [T1, T2]) => |
44392
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
207 |
(case (aux slack avoid T1, aux slack avoid T2) of |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
208 |
(k, 1) => if slack andalso k = 0 then 0 else 1 |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
209 |
| (0, _) => 0 |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
210 |
| (_, 0) => 0 |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
211 |
| (k1, k2) => |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
212 |
if k1 >= max orelse k2 >= max then max |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
213 |
else Int.min (max, Integer.pow k2 k1)) |
69593 | 214 |
| Type (\<^type_name>\<open>set\<close>, [T']) => aux slack avoid (T' --> \<^typ>\<open>bool\<close>) |
215 |
| \<^typ>\<open>prop\<close> => 2 |
|
216 |
| \<^typ>\<open>bool\<close> => 2 (* optimization *) |
|
217 |
| \<^typ>\<open>nat\<close> => 0 (* optimization *) |
|
44392
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
218 |
| Type ("Int.int", []) => 0 (* optimization *) |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
219 |
| Type (s, _) => |
54554
b8d0d8407c3b
eliminated Sledgehammer's dependency on old-style datatypes
blanchet
parents:
53800
diff
changeset
|
220 |
(case free_constructors_of ctxt T of |
44392
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
221 |
constrs as _ :: _ => |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
222 |
let |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
223 |
val constr_cards = |
54554
b8d0d8407c3b
eliminated Sledgehammer's dependency on old-style datatypes
blanchet
parents:
53800
diff
changeset
|
224 |
map (Integer.prod o map (aux slack (T :: avoid)) o binder_types o snd) constrs |
44392
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
225 |
in |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
226 |
if exists (curry (op =) 0) constr_cards then 0 |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
227 |
else Int.min (max, Integer.sum constr_cards) |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
228 |
end |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
229 |
| [] => |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
230 |
case Typedef.get_info ctxt s of |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
231 |
({abs_type, rep_type, ...}, _) :: _ => |
45299
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
232 |
if not sound then |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
233 |
(* We cheat here by assuming that typedef types are infinite if |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
234 |
their underlying type is infinite. This is unsound in |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
235 |
general but it's hard to think of a realistic example where |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
236 |
this would not be the case. We are also slack with |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
237 |
representation types: If a representation type has the form |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
238 |
"sigma => tau", we consider it enough to check "sigma" for |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
239 |
infiniteness. *) |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
240 |
(case varify_and_instantiate_type ctxt |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
241 |
(Logic.varifyT_global abs_type) T |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
242 |
(Logic.varifyT_global rep_type) |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
243 |
|> aux true avoid of |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
244 |
0 => 0 |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
245 |
| 1 => 1 |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
246 |
| _ => default_card) |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
247 |
else |
ee584ff987c3
check "sound" flag before doing something unsound...
blanchet
parents:
44935
diff
changeset
|
248 |
default_card |
44392
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
249 |
| [] => default_card) |
54554
b8d0d8407c3b
eliminated Sledgehammer's dependency on old-style datatypes
blanchet
parents:
53800
diff
changeset
|
250 |
| TFree _ => |
44392
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
251 |
(* Very slightly unsound: Type variables are assumed not to be |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
252 |
constrained to cardinality 1. (In practice, the user would most |
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
253 |
likely have used "unit" directly anyway.) *) |
44500 | 254 |
if not sound andalso default_card = 1 then 2 else default_card |
44392
6750b4297691
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
blanchet
parents:
43864
diff
changeset
|
255 |
| TVar _ => default_card |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
256 |
in Int.min (max, aux false [] T) end |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
257 |
|
44500 | 258 |
fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt true [] 0 T <> 0 |
259 |
fun is_type_surely_infinite ctxt sound infinite_Ts T = |
|
260 |
tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
261 |
|
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
262 |
(* Simple simplifications to ensure that sort annotations don't leave a trail of |
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
263 |
spurious "True"s. *) |
69593 | 264 |
fun s_not (Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', t')) = |
265 |
Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', s_not t') |
|
266 |
| s_not (Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', t')) = |
|
267 |
Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', s_not t') |
|
69597 | 268 |
| s_not (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) = \<^const>\<open>HOL.conj\<close> $ t1 $ s_not t2 |
269 |
| s_not (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) = |
|
270 |
\<^const>\<open>HOL.disj\<close> $ s_not t1 $ s_not t2 |
|
271 |
| s_not (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) = |
|
272 |
\<^const>\<open>HOL.conj\<close> $ s_not t1 $ s_not t2 |
|
273 |
| s_not (\<^const>\<open>False\<close>) = \<^const>\<open>True\<close> |
|
274 |
| s_not (\<^const>\<open>True\<close>) = \<^const>\<open>False\<close> |
|
275 |
| s_not (\<^const>\<open>Not\<close> $ t) = t |
|
276 |
| s_not t = \<^const>\<open>Not\<close> $ t |
|
54758 | 277 |
|
69597 | 278 |
fun s_conj (\<^const>\<open>True\<close>, t2) = t2 |
279 |
| s_conj (t1, \<^const>\<open>True\<close>) = t1 |
|
280 |
| s_conj (\<^const>\<open>False\<close>, _) = \<^const>\<open>False\<close> |
|
281 |
| s_conj (_, \<^const>\<open>False\<close>) = \<^const>\<open>False\<close> |
|
51197 | 282 |
| s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2) |
54758 | 283 |
|
69597 | 284 |
fun s_disj (\<^const>\<open>False\<close>, t2) = t2 |
285 |
| s_disj (t1, \<^const>\<open>False\<close>) = t1 |
|
286 |
| s_disj (\<^const>\<open>True\<close>, _) = \<^const>\<open>True\<close> |
|
287 |
| s_disj (_, \<^const>\<open>True\<close>) = \<^const>\<open>True\<close> |
|
51197 | 288 |
| s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2) |
54757
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54554
diff
changeset
|
289 |
|
69597 | 290 |
fun s_imp (\<^const>\<open>True\<close>, t2) = t2 |
291 |
| s_imp (t1, \<^const>\<open>False\<close>) = s_not t1 |
|
292 |
| s_imp (\<^const>\<open>False\<close>, _) = \<^const>\<open>True\<close> |
|
293 |
| s_imp (_, \<^const>\<open>True\<close>) = \<^const>\<open>True\<close> |
|
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
294 |
| s_imp p = HOLogic.mk_imp p |
54757
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54554
diff
changeset
|
295 |
|
69597 | 296 |
fun s_iff (\<^const>\<open>True\<close>, t2) = t2 |
297 |
| s_iff (t1, \<^const>\<open>True\<close>) = t1 |
|
298 |
| s_iff (\<^const>\<open>False\<close>, t2) = s_not t2 |
|
299 |
| s_iff (t1, \<^const>\<open>False\<close>) = s_not t1 |
|
300 |
| s_iff (t1, t2) = if t1 aconv t2 then \<^const>\<open>True\<close> else HOLogic.eq_const HOLogic.boolT $ t1 $ t2 |
|
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43827
diff
changeset
|
301 |
|
49983
33e18e9916a8
use metaquantification when possible in Isar proofs
blanchet
parents:
49982
diff
changeset
|
302 |
fun close_form t = |
33e18e9916a8
use metaquantification when possible in Isar proofs
blanchet
parents:
49982
diff
changeset
|
303 |
fold (fn ((s, i), T) => fn t' => |
54757
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54554
diff
changeset
|
304 |
Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54554
diff
changeset
|
305 |
(Term.add_vars t []) t |
49983
33e18e9916a8
use metaquantification when possible in Isar proofs
blanchet
parents:
49982
diff
changeset
|
306 |
|
58091 | 307 |
val hol_close_form_prefix = "ATP." |
46385
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
45896
diff
changeset
|
308 |
|
49982 | 309 |
fun hol_close_form t = |
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45511
diff
changeset
|
310 |
fold (fn ((s, i), T) => fn t' => |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45299
diff
changeset
|
311 |
HOLogic.all_const T |
49982 | 312 |
$ Abs (hol_close_form_prefix ^ s, T, |
46385
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
45896
diff
changeset
|
313 |
abstract_over (Var ((s, i), T), t'))) |
43864
58a7b3fdc193
fixed lambda-liftg: must ensure the formulas are in close form
blanchet
parents:
43863
diff
changeset
|
314 |
(Term.add_vars t []) t |
58a7b3fdc193
fixed lambda-liftg: must ensure the formulas are in close form
blanchet
parents:
43863
diff
changeset
|
315 |
|
49982 | 316 |
fun hol_open_form unprefix |
69593 | 317 |
(t as Const (\<^const_name>\<open>All\<close>, _) $ Abs (s, T, t')) = |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
318 |
(case try unprefix s of |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
319 |
SOME s => |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
320 |
let |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
321 |
val names = Name.make_context (map fst (Term.add_var_names t' [])) |
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
322 |
val (s, _) = Name.variant s names |
49982 | 323 |
in hol_open_form unprefix (subst_bound (Var ((s, 0), T), t')) end |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
324 |
| NONE => t) |
49982 | 325 |
| hol_open_form _ t = t |
47718
39229c760636
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents:
47715
diff
changeset
|
326 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
327 |
fun eta_expand _ t 0 = t |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
328 |
| eta_expand Ts (Abs (s, T, t')) n = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
329 |
Abs (s, T, eta_expand (T :: Ts) t' (n - 1)) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
330 |
| eta_expand Ts t n = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
331 |
fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t')) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
332 |
(List.take (binder_types (fastype_of1 (Ts, t)), n)) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
333 |
(list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
334 |
|
59632 | 335 |
fun cong_extensionalize_term ctxt t = |
69593 | 336 |
if exists_Const (fn (s, _) => s = \<^const_name>\<open>Not\<close>) t then |
59632 | 337 |
t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
338 |
|> Meson.cong_extensionalize_thm ctxt |
|
59582 | 339 |
|> Thm.prop_of |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
340 |
else |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
341 |
t |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
342 |
|
69593 | 343 |
fun is_fun_equality (\<^const_name>\<open>HOL.eq\<close>, |
344 |
Type (_, [Type (\<^type_name>\<open>fun\<close>, _), _])) = true |
|
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47150
diff
changeset
|
345 |
| is_fun_equality _ = false |
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47150
diff
changeset
|
346 |
|
47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47718
diff
changeset
|
347 |
fun abs_extensionalize_term ctxt t = |
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47150
diff
changeset
|
348 |
if exists_Const is_fun_equality t then |
59632 | 349 |
t |> Thm.cterm_of ctxt |> Meson.abs_extensionalize_conv ctxt |
350 |
|> Thm.prop_of |> Logic.dest_equals |> snd |
|
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47150
diff
changeset
|
351 |
else |
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47150
diff
changeset
|
352 |
t |
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47150
diff
changeset
|
353 |
|
47991
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
354 |
fun unextensionalize_def t = |
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
355 |
case t of |
69597 | 356 |
\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) => |
47991
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
357 |
(case strip_comb lhs of |
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
358 |
(c as Const (_, T), args) => |
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
359 |
if forall is_Var args andalso not (has_duplicates (op =) args) then |
69597 | 360 |
\<^const>\<open>Trueprop\<close> |
69593 | 361 |
$ (Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> \<^typ>\<open>bool\<close>) |
47991
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
362 |
$ c $ fold_rev lambda args rhs) |
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
363 |
else |
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
364 |
t |
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
365 |
| _ => t) |
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
366 |
| _ => t |
3eb598b044ad
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents:
47954
diff
changeset
|
367 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
368 |
(* Converts an elim-rule into an equivalent theorem that does not have the |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
369 |
predicate variable. Leaves other theorems unchanged. We simply instantiate |
44460 | 370 |
the conclusion variable to "False". (Cf. "transform_elim_theorem" in |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
371 |
"Meson_Clausify".) *) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
372 |
fun transform_elim_prop t = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
373 |
case Logic.strip_imp_concl t of |
69597 | 374 |
\<^const>\<open>Trueprop\<close> $ Var (z, \<^typ>\<open>bool\<close>) => |
375 |
subst_Vars [(z, \<^const>\<open>False\<close>)] t |
|
69593 | 376 |
| Var (z, \<^typ>\<open>prop\<close>) => subst_Vars [(z, \<^prop>\<open>False\<close>)] t |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
377 |
| _ => t |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
378 |
|
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
379 |
fun specialize_type thy (s, T) t = |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
380 |
let |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
381 |
fun subst_for (Const (s', T')) = |
61769 | 382 |
if s = s' then |
383 |
SOME (Sign.typ_match thy (T', T) Vartab.empty) |
|
384 |
handle Type.TYPE_MATCH => NONE |
|
385 |
else |
|
386 |
NONE |
|
387 |
| subst_for (t1 $ t2) = (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2) |
|
388 |
| subst_for (Abs (_, _, t')) = subst_for t' |
|
389 |
| subst_for _ = NONE |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
390 |
in |
61769 | 391 |
(case subst_for t of |
61770 | 392 |
SOME subst => Envir.subst_term_types subst t |
61769 | 393 |
| NONE => raise Type.TYPE_MATCH) |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
394 |
end |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
395 |
|
52125
ac7830871177
improved handling of free variables' types in Isar proofs
blanchet
parents:
52077
diff
changeset
|
396 |
fun strip_subgoal goal i ctxt = |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
397 |
let |
52196
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52125
diff
changeset
|
398 |
val (t, (frees, params)) = |
59582 | 399 |
Logic.goal_params (Thm.prop_of goal) i |
52196
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52125
diff
changeset
|
400 |
||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free)) |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
401 |
val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
402 |
val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees |
52196
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52125
diff
changeset
|
403 |
in (rev params, hyp_ts, concl_t) end |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
404 |
|
69593 | 405 |
fun extract_lambda_def dest_head (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u) = |
57541 | 406 |
let val (head, args) = strip_comb t in |
407 |
(head |> dest_head |> fst, |
|
408 |
fold_rev (fn t as Var ((s, _), T) => |
|
409 |
(fn u => Abs (s, T, abstract_over (t, u))) |
|
410 |
| _ => raise Fail "expected \"Var\"") args u) |
|
411 |
end |
|
412 |
| extract_lambda_def _ _ = raise Fail "malformed lifted lambda" |
|
413 |
||
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
414 |
fun short_thm_name ctxt th = |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
415 |
let |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
416 |
val long = Thm.get_name_hint th |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
417 |
val short = Long_Name.base_name long |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
418 |
in |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
419 |
if Thm.eq_thm_prop (th, singleton (Attrib.eval_thms ctxt) (Facts.named short, [])) then short |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
420 |
else long |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
421 |
end |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
54768
diff
changeset
|
422 |
|
74328 | 423 |
val map_prod = Ctr_Sugar_Util.map_prod |
424 |
||
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
diff
changeset
|
425 |
end; |