author  wenzelm 
Wed, 29 May 2013 18:25:11 +0200  
changeset 52223  5bb6ae8acb87 
parent 52178  6228806b2605 
child 52225  568b2cd65d50 
permissions  rwrr 
39958  1 
(* Title: HOL/Tools/Metis/metis_reconstruct.ML 
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

2 
Author: Kong W. Susanto, Cambridge University Computer Laboratory 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

3 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

4 
Author: Jasmin Blanchette, TU Muenchen 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

5 
Copyright Cambridge University 2007 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

6 

bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

7 
Proof reconstruction for Metis. 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

8 
*) 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

9 

bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

10 
signature METIS_RECONSTRUCT = 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

11 
sig 
46320  12 
type type_enc = ATP_Problem_Generate.type_enc 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset

13 

50875
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

14 
exception METIS_RECONSTRUCT of string * string 
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis"  I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset

15 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

16 
val hol_clause_of_metis : 
45508  17 
Proof.context > type_enc > int Symtab.table 
18 
> (string * term) list * (string * term) list > Metis_Thm.thm > term 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

19 
val lookth : (Metis_Thm.thm * 'a) list > Metis_Thm.thm > 'a 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

20 
val replay_one_inference : 
45508  21 
Proof.context > type_enc 
22 
> (string * term) list * (string * term) list > int Symtab.table 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

23 
> Metis_Thm.thm * Metis_Proof.inference > (Metis_Thm.thm * thm) list 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

24 
> (Metis_Thm.thm * thm) list 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

25 
val discharge_skolem_premises : 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

26 
Proof.context > (thm * term) option list > thm > thm 
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

27 
end; 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

28 

bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

29 
structure Metis_Reconstruct : METIS_RECONSTRUCT = 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

30 
struct 
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

31 

43094  32 
open ATP_Problem 
46320  33 
open ATP_Problem_Generate 
34 
open ATP_Proof_Reconstruct 

35 
open Metis_Generate 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

36 

50875
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

37 
exception METIS_RECONSTRUCT of string * string 
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis"  I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset

38 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

39 
fun atp_name_of_metis type_enc s = 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset

40 
case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

41 
SOME ((s, _), (_, swap)) => (s, swap) 
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

42 
 _ => (s, false) 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

43 
fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) = 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

44 
let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

45 
ATerm ((s, []), tms > map (atp_term_of_metis type_enc) > swap ? rev) 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

46 
end 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

47 
 atp_term_of_metis _ (Metis_Term.Var s) = 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
46708
diff
changeset

48 
ATerm ((Metis_Name.toString s, []), []) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

49 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

50 
fun hol_term_of_metis ctxt type_enc sym_tab = 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

51 
atp_term_of_metis type_enc #> term_of_atp ctxt false sym_tab NONE 
43094  52 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

53 
fun atp_literal_of_metis type_enc (pos, atom) = 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

54 
atom > Metis_Term.Fn > atp_term_of_metis type_enc 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset

55 
> AAtom > not pos ? mk_anot 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

56 
fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), [])) 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

57 
 atp_clause_of_metis type_enc lits = 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

58 
lits > map (atp_literal_of_metis type_enc) > mk_aconns AOr 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

59 

45508  60 
fun polish_hol_terms ctxt (lifted, old_skolems) = 
45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45511
diff
changeset

61 
map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems) 
43212  62 
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) 
43184  63 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

64 
fun hol_clause_of_metis ctxt type_enc sym_tab concealed = 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

65 
Metis_Thm.clause 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

66 
#> Metis_LiteralSet.toList 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

67 
#> atp_clause_of_metis type_enc 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

68 
#> prop_of_atp ctxt false sym_tab 
45508  69 
#> singleton (polish_hol_terms ctxt concealed) 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

70 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

71 
fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms = 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

72 
let val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

73 
val _ = trace_msg ctxt (fn () => " calling type inference:") 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

74 
val _ = app (fn t => trace_msg ctxt 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

75 
(fn () => Syntax.string_of_term ctxt t)) ts 
45508  76 
val ts' = ts > polish_hol_terms ctxt concealed 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

77 
val _ = app (fn t => trace_msg ctxt 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

78 
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ 
43128  79 
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

80 
ts' 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

81 
in ts' end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

82 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

83 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

84 
(* FOL step Inference Rules *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

85 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

86 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

87 
(*for debugging only*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

88 
(* 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

89 
fun print_thpair ctxt (fth,th) = 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

90 
(trace_msg ctxt (fn () => "============================================="); 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

91 
trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth); 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

92 
trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

93 
*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

94 

43094  95 
fun lookth th_pairs fth = 
96 
the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

97 
handle Option.Option => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

98 
raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

99 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

100 
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

101 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

102 
(* INFERENCE RULE: AXIOM *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

103 

43212  104 
(* This causes variables to have an index of 1 by default. See also 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

105 
"term_of_atp" in "ATP_Proof_Reconstruct". *) 
43212  106 
val axiom_inference = Thm.incr_indexes 1 oo lookth 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

107 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

108 
(* INFERENCE RULE: ASSUME *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

109 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

110 
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

111 

43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

112 
fun inst_excluded_middle thy i_atom = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

113 
let val th = EXCLUDED_MIDDLE 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

114 
val [vx] = Term.add_vars (prop_of th) [] 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

115 
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)] 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

116 
in cterm_instantiate substs th end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

117 

45508  118 
fun assume_inference ctxt type_enc concealed sym_tab atom = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

119 
inst_excluded_middle 
42361  120 
(Proof_Context.theory_of ctxt) 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

121 
(singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

122 
(Metis_Term.Fn atom)) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

123 

39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

124 
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

125 
to reconstruct them admits new possibilities of errors, e.g. concerning 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

126 
sorts. Instead we try to arrange that new TVars are distinct and that types 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

127 
can be inferred from terms. *) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

128 

45508  129 
fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th = 
42361  130 
let val thy = Proof_Context.theory_of ctxt 
43094  131 
val i_th = lookth th_pairs th 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

132 
val i_th_vars = Term.add_vars (prop_of i_th) [] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

133 
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

134 
fun subst_translation (x,y) = 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

135 
let val v = find_var x 
45508  136 
(* We call "polish_hol_terms" below. *) 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

137 
val t = hol_term_of_metis ctxt type_enc sym_tab y 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

138 
in SOME (cterm_of thy (Var v), t) end 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

139 
handle Option.Option => 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

140 
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^ 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

141 
" in " ^ Display.string_of_thm ctxt i_th); 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

142 
NONE) 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

143 
 TYPE _ => 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

144 
(trace_msg ctxt (fn () => "\"hol_term_of_metis\" failed for " ^ x ^ 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

145 
" in " ^ Display.string_of_thm ctxt i_th); 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

146 
NONE) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

147 
fun remove_typeinst (a, t) = 
43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

148 
let val a = Metis_Name.toString a in 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

149 
case unprefix_and_unascii schematic_var_prefix a of 
43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

150 
SOME b => SOME (b, t) 
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

151 
 NONE => 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

152 
case unprefix_and_unascii tvar_prefix a of 
43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

153 
SOME _ => NONE (* type instantiations are forbidden *) 
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

154 
 NONE => SOME (a, t) (* internal Metis var? *) 
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

155 
end 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

156 
val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

157 
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) 
43184  158 
val (vars, tms) = 
159 
ListPair.unzip (map_filter subst_translation substs) 

45508  160 
> polish_hol_terms ctxt concealed 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

161 
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

162 
val substs' = ListPair.zip (vars, map ctm_of tms) 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

163 
val _ = trace_msg ctxt (fn () => 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

164 
cat_lines ("subst_translations:" :: 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

165 
(substs' > map (fn (x, y) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

166 
Syntax.string_of_term ctxt (term_of x) ^ " > " ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

167 
Syntax.string_of_term ctxt (term_of y))))); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

168 
in cterm_instantiate substs' i_th end 
50875
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

169 
handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg) 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

170 
 ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

171 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

172 
(* INFERENCE RULE: RESOLVE *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

173 

43330  174 
(*Increment the indexes of only the type variables*) 
175 
fun incr_type_indexes inc th = 

176 
let val tvs = Term.add_tvars (Thm.full_prop_of th) [] 

177 
and thy = Thm.theory_of_thm th 

178 
fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s)) 

179 
in Thm.instantiate (map inc_tvar tvs, []) th end; 

180 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

181 
(* Like RSN, but we rename apart only the type variables. Vars here typically 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

182 
have an index of 1, and the use of RSN would increase this typically to 3. 
43300  183 
Instantiations of those Vars could then fail. *) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

184 
fun resolve_inc_tyvars thy tha i thb = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

185 
let 
43330  186 
val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha 
43359  187 
fun aux (tha, thb) = 
52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52178
diff
changeset

188 
case Thm.bicompose {flatten = true, match = false, incremented = false} 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52178
diff
changeset

189 
(false, tha, nprems_of tha) i thb 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

190 
> Seq.list_of > distinct Thm.eq_thm of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

191 
[th] => th 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

192 
 _ => raise THM ("resolve_inc_tyvars: unique result expected", i, 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

193 
[tha, thb]) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

194 
in 
43359  195 
aux (tha, thb) 
52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52178
diff
changeset

196 
handle TERM z => (* FIXME obsolete!? *) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

197 
(* The unifier, which is invoked from "Thm.bicompose", will sometimes 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

198 
refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

199 
"TERM" exception (with "add_ffpair" as first argument). We then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

200 
perform unification of the types of variables by hand and try 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

201 
again. We could do this the first time around but this error 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

202 
occurs seldom and we don't want to break existing proofs in subtle 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

203 
ways or slow them down needlessly. *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

204 
case [] > fold (Term.add_vars o prop_of) [tha, thb] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

205 
> AList.group (op =) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

206 
> maps (fn ((s, _), T :: Ts) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

207 
map (fn T' => (Free (s, T), Free (s, T'))) Ts) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

208 
> rpair (Envir.empty ~1) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

209 
> fold (Pattern.unify thy) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

210 
> Envir.type_env > Vartab.dest 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

211 
> map (fn (x, (S, T)) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

212 
pairself (ctyp_of thy) (TVar (x, S), T)) of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

213 
[] => raise TERM z 
43359  214 
 ps => (tha, thb) > pairself (Drule.instantiate_normalize (ps, [])) 
215 
> aux 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

216 
end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

217 

40221
d10b68c6e6d4
do not let Metis be confused by higherorder reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset

218 
fun s_not (@{const Not} $ t) = t 
d10b68c6e6d4
do not let Metis be confused by higherorder reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset

219 
 s_not t = HOLogic.mk_not t 
43195
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

220 
fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t 
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

221 
 simp_not_not (@{const Not} $ t) = s_not (simp_not_not t) 
40221
d10b68c6e6d4
do not let Metis be confused by higherorder reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset

222 
 simp_not_not t = t 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

223 

43195
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

224 
val normalize_literal = simp_not_not o Envir.eta_contract 
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

225 

43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

226 
(* Find the relative location of an untyped term within a list of terms as a 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

227 
1based index. Returns 0 in case of failure. *) 
40221
d10b68c6e6d4
do not let Metis be confused by higherorder reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset

228 
fun index_of_literal lit haystack = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

229 
let 
43195
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

230 
fun match_lit normalize = 
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

231 
HOLogic.dest_Trueprop #> normalize 
43301
8d7fc4a5b502
removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents:
43300
diff
changeset

232 
#> curry Term.aconv_untyped (lit > normalize) 
43195
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

233 
in 
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

234 
(case find_index (match_lit I) haystack of 
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

235 
~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack 
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

236 
 j => j) + 1 
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

237 
end 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

238 

39893  239 
(* Permute a rule's premises to move the ith premise to the last position. *) 
240 
fun make_last i th = 

241 
let val n = nprems_of th 

242 
in if 1 <= i andalso i <= n 

243 
then Thm.permute_prems (i1) 1 th 

244 
else raise THM("select_literal", i, [th]) 

245 
end; 

246 

42348
187354e22c7d
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
blanchet
parents:
42344
diff
changeset

247 
(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding 
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

248 
to create double negations. The "select" wrapper is a trick to ensure that 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

249 
"P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

250 
don't use this trick in general because it makes the proof object uglier than 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

251 
necessary. FIXME. *) 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

252 
fun negate_head th = 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

253 
if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

254 
(th RS @{thm select_FalseI}) 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

255 
> fold (rewrite_rule o single) 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

256 
@{thms not_atomize_select atomize_not_select} 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

257 
else 
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset

258 
th > fold (rewrite_rule o single) @{thms not_atomize atomize_not} 
39893  259 

260 
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i1),P(i+1),...Pn] ==> ~P *) 

42348
187354e22c7d
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
blanchet
parents:
42344
diff
changeset

261 
val select_literal = negate_head oo make_last 
39893  262 

45508  263 
fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

264 
let 
43094  265 
val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2) 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

266 
val _ = trace_msg ctxt (fn () => 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

267 
" isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\ 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

268 
\ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

269 
in 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

270 
(* Trivial cases where one operand is type info *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

271 
if Thm.eq_thm (TrueI, i_th1) then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

272 
i_th2 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

273 
else if Thm.eq_thm (TrueI, i_th2) then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

274 
i_th1 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

275 
else 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

276 
let 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

277 
val thy = Proof_Context.theory_of ctxt 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

278 
val i_atom = 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

279 
singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

280 
(Metis_Term.Fn atom) 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

281 
val _ = trace_msg ctxt (fn () => 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

282 
" atom: " ^ Syntax.string_of_term ctxt i_atom) 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

283 
in 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

284 
case index_of_literal (s_not i_atom) (prems_of i_th1) of 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

285 
0 => 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

286 
(trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

287 
i_th1) 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

288 
 j1 => 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

289 
(trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1); 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

290 
case index_of_literal i_atom (prems_of i_th2) of 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

291 
0 => 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

292 
(trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

293 
i_th2) 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

294 
 j2 => 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

295 
(trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2); 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

296 
resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2 
50875
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

297 
handle TERM (s, _) => 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

298 
raise METIS_RECONSTRUCT ("resolve_inference", s))) 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

299 
end 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

300 
end 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

301 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

302 
(* INFERENCE RULE: REFL *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

303 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

304 
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

305 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

306 
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

307 
val refl_idx = 1 + Thm.maxidx_of REFL_THM; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

308 

45508  309 
fun refl_inference ctxt type_enc concealed sym_tab t = 
43094  310 
let 
311 
val thy = Proof_Context.theory_of ctxt 

44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset

312 
val i_t = 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

313 
singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t 
43094  314 
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) 
315 
val c_t = cterm_incr_types thy refl_idx i_t 

316 
in cterm_instantiate [(refl_x, c_t)] REFL_THM end 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

317 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

318 
(* INFERENCE RULE: EQUALITY *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

319 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

320 
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

321 
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

322 

45508  323 
fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr = 
42361  324 
let val thy = Proof_Context.theory_of ctxt 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

325 
val m_tm = Metis_Term.Fn atom 
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

326 
val [i_atom, i_tm] = 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

327 
hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr] 
51951
fab4ab92e812
more standard Isabelle/ML operations  avoid inaccurate Bool.fromString;
wenzelm
parents:
51929
diff
changeset

328 
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Markup.print_bool pos) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

329 
fun replace_item_list lx 0 (_::ls) = lx::ls 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

330 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
43205  331 
fun path_finder_fail tm ps t = 
50875
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

332 
raise METIS_RECONSTRUCT ("equality_inference (path_finder)", 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

333 
"path = " ^ space_implode " " (map string_of_int ps) ^ 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

334 
" isaterm: " ^ Syntax.string_of_term ctxt tm ^ 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

335 
(case t of 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

336 
SOME t => " folterm: " ^ Metis_Term.toString t 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

337 
 NONE => "")) 
43212  338 
fun path_finder tm [] _ = (tm, Bound 0) 
339 
 path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = 

43177  340 
let 
43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

341 
val s = s > Metis_Name.toString 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

342 
> perhaps (try (unprefix_and_unascii const_prefix 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46320
diff
changeset

343 
#> the #> unmangled_const_name #> hd)) 
43177  344 
in 
345 
if s = metis_predicator orelse s = predicator_name orelse 

44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset

346 
s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag 
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset

347 
orelse s = type_tag_name then 
43212  348 
path_finder tm ps (nth ts p) 
43177  349 
else if s = metis_app_op orelse s = app_op_name then 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

350 
let 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

351 
val (tm1, tm2) = dest_comb tm 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

352 
val p' = p  (length ts  2) 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

353 
in 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

354 
if p' = 0 then 
43212  355 
path_finder tm1 ps (nth ts p) > (fn y => y $ tm2) 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

356 
else 
43212  357 
path_finder tm2 ps (nth ts p) > (fn y => tm1 $ y) 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

358 
end 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

359 
else 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

360 
let 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

361 
val (tm1, args) = strip_comb tm 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

362 
val adjustment = length ts  length args 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

363 
val p' = if adjustment > p then p else p  adjustment 
43205  364 
val tm_p = 
365 
nth args p' 

43278  366 
handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t) 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

367 
val _ = trace_msg ctxt (fn () => 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

368 
"path_finder: " ^ string_of_int p ^ " " ^ 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

369 
Syntax.string_of_term ctxt tm_p) 
43212  370 
val (r, t) = path_finder tm_p ps (nth ts p) 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

371 
in (r, list_comb (tm1, replace_item_list t p' args)) end 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset

372 
end 
43212  373 
 path_finder tm ps t = path_finder_fail tm ps (SOME t) 
374 
val (tm_subst, body) = path_finder i_atom fp m_tm 

39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

375 
val tm_abs = Abs ("x", type_of tm_subst, body) 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

376 
val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

377 
val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

378 
val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

379 
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

380 
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

381 
val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

382 
val eq_terms = map (pairself (cterm_of thy)) 
44121  383 
(ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

384 
in cterm_instantiate eq_terms subst' end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

385 

43094  386 
val factor = Seq.hd o distinct_subgoals_tac 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

387 

45508  388 
fun one_step ctxt type_enc concealed sym_tab th_pairs p = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

389 
case p of 
43186  390 
(fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th > factor 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

391 
 (_, Metis_Proof.Assume f_atom) => 
45508  392 
assume_inference ctxt type_enc concealed sym_tab f_atom 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

393 
 (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => 
45508  394 
inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 
43186  395 
> factor 
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset

396 
 (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) => 
45508  397 
resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset

398 
f_th2 
43094  399 
> factor 
43186  400 
 (_, Metis_Proof.Refl f_tm) => 
45508  401 
refl_inference ctxt type_enc concealed sym_tab f_tm 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

402 
 (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => 
45508  403 
equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

404 

39893  405 
fun flexflex_first_order th = 
406 
case Thm.tpairs_of th of 

407 
[] => th 

408 
 pairs => 

409 
let val thy = theory_of_thm th 

52178
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

410 
val cert = cterm_of thy 
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

411 
val certT = ctyp_of thy 
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

412 
val (tyenv, tenv) = 
39893  413 
fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) 
52178
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

414 
fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T) 
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

415 
fun mk (v, (T, t)) = 
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

416 
let val T' = Envir.subst_type tyenv T 
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

417 
in (cert (Var (v, T')), cert t) end 
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

418 
val instsT = Vartab.fold (cons o mkT) tyenv [] 
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

419 
val insts = Vartab.fold (cons o mk) tenv [] 
6228806b2605
instantiate types as well (see also Thm.first_order_match);
wenzelm
parents:
52031
diff
changeset

420 
val th' = Thm.instantiate (instsT, insts) th 
39893  421 
in th' end 
422 
handle THM _ => th; 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

423 

43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

424 
fun is_metis_literal_genuine (_, (s, _)) = 
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

425 
not (String.isPrefix class_prefix (Metis_Name.toString s)) 
39895
a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync  generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset

426 
fun is_isabelle_literal_genuine t = 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39946
diff
changeset

427 
case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false  _ => true 
39895
a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync  generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset

428 

a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync  generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset

429 
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 
a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync  generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset

430 

42333  431 
(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate 
432 
disjuncts are impossible. In the Isabelle proof, in spite of efforts to 

433 
eliminate them, duplicates sometimes appear with slightly different (but 

434 
unifiable) types. *) 

435 
fun resynchronize ctxt fol_th th = 

436 
let 

437 
val num_metis_lits = 

438 
count is_metis_literal_genuine 

439 
(Metis_LiteralSet.toList (Metis_Thm.clause fol_th)) 

440 
val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th) 

441 
in 

442 
if num_metis_lits >= num_isabelle_lits then 

443 
th 

444 
else 

445 
let 

446 
val (prems0, concl) = th > prop_of > Logic.strip_horn 

43195
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

447 
val prems = prems0 > map normalize_literal 
43301
8d7fc4a5b502
removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents:
43300
diff
changeset

448 
> distinct Term.aconv_untyped 
42333  449 
val goal = Logic.list_implies (prems, concl) 
46708
b138dee7bed3
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
wenzelm
parents:
46392
diff
changeset

450 
val tac = cut_tac th 1 
43195
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

451 
THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]} 
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

452 
THEN ALLGOALS assume_tac 
42333  453 
in 
454 
if length prems = length prems0 then 

50875
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset

455 
raise METIS_RECONSTRUCT ("resynchronize", "Out of sync") 
42333  456 
else 
43195
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

457 
Goal.prove ctxt [] [] goal (K tac) 
42333  458 
> resynchronize ctxt fol_th 
459 
end 

460 
end 

461 

45508  462 
fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf) 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset

463 
th_pairs = 
43094  464 
if not (null th_pairs) andalso 
465 
prop_of (snd (hd th_pairs)) aconv @{prop False} then 

40868
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

466 
(* Isabelle sometimes identifies literals (premises) that are distinct in 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

467 
Metis (e.g., because of type variables). We give the Isabelle proof the 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

468 
benefice of the doubt. *) 
43094  469 
th_pairs 
40868
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

470 
else 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

471 
let 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

472 
val _ = trace_msg ctxt 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

473 
(fn () => "=============================================") 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

474 
val _ = trace_msg ctxt 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

475 
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

476 
val _ = trace_msg ctxt 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

477 
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) 
45508  478 
val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf) 
40868
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

479 
> flexflex_first_order 
42333  480 
> resynchronize ctxt fol_th 
40868
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

481 
val _ = trace_msg ctxt 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

482 
(fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

483 
val _ = trace_msg ctxt 
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset

484 
(fn () => "=============================================") 
43094  485 
in (fol_th, th) :: th_pairs end 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

486 

42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

487 
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

488 
one of the premises. Unfortunately, this sometimes yields "Variable 
51701
1e29891759c4
tuned exceptions  avoid composing error messages in lowlevel situations;
wenzelm
parents:
50875
diff
changeset

489 
has two distinct types" errors. To avoid this, we instantiate the 
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

490 
variables before applying "assume_tac". Typical constraints are of the form 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

491 
?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x, 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

492 
where the nonvariables are goal parameters. *) 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

493 
fun unify_first_prem_with_concl thy i th = 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

494 
let 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

495 
val goal = Logic.get_goal (prop_of th) i > Envir.beta_eta_contract 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

496 
val prem = goal > Logic.strip_assums_hyp > hd 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

497 
val concl = goal > Logic.strip_assums_concl 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

498 
fun pair_untyped_aconv (t1, t2) (u1, u2) = 
43301
8d7fc4a5b502
removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents:
43300
diff
changeset

499 
Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2) 
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

500 
fun add_terms tp inst = 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

501 
if exists (pair_untyped_aconv tp) inst then inst 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

502 
else tp :: map (apsnd (subst_atomic [tp])) inst 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

503 
fun is_flex t = 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

504 
case strip_comb t of 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

505 
(Var _, args) => forall is_Bound args 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

506 
 _ => false 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

507 
fun unify_flex flex rigid = 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

508 
case strip_comb flex of 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

509 
(Var (z as (_, T)), args) => 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

510 
add_terms (Var z, 
44241  511 
fold_rev absdummy (take (length args) (binder_types T)) rigid) 
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

512 
 _ => I 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

513 
fun unify_potential_flex comb atom = 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

514 
if is_flex comb then unify_flex comb atom 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

515 
else if is_Var atom then add_terms (atom, comb) 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

516 
else I 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

517 
fun unify_terms (t, u) = 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

518 
case (t, u) of 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

519 
(t1 $ t2, u1 $ u2) => 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

520 
if is_flex t then unify_flex t u 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

521 
else if is_flex u then unify_flex u t 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

522 
else fold unify_terms [(t1, u1), (t2, u2)] 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

523 
 (_ $ _, _) => unify_potential_flex t u 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

524 
 (_, _ $ _) => unify_potential_flex u t 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

525 
 (Var _, _) => add_terms (t, u) 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

526 
 (_, Var _) => add_terms (u, t) 
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

527 
 _ => I 
42344
4a58173ffb99
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed  catch the exception for now
blanchet
parents:
42342
diff
changeset

528 
val t_inst = 
4a58173ffb99
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed  catch the exception for now
blanchet
parents:
42342
diff
changeset

529 
[] > try (unify_terms (prem, concl) #> map (pairself (cterm_of thy))) 
4a58173ffb99
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed  catch the exception for now
blanchet
parents:
42342
diff
changeset

530 
> the_default [] (* FIXME *) 
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

531 
in th > cterm_instantiate t_inst end 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

532 

8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

533 
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

534 

8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

535 
fun copy_prems_tac [] ns i = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

536 
if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

537 
 copy_prems_tac (1 :: ms) ns i = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

538 
rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

539 
 copy_prems_tac (m :: ms) ns i = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

540 
etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

541 

42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

542 
(* Metis generates variables of the form _nnn. *) 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

543 
val is_metis_fresh_variable = String.isPrefix "_" 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

544 

40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

545 
fun instantiate_forall_tac thy t i st = 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

546 
let 
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

547 
val params = Logic.strip_params (Logic.get_goal (prop_of st) i) > rev 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

548 
fun repair (t as (Var ((s, _), _))) = 
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

549 
(case find_index (fn (s', _) => s' = s) params of 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

550 
~1 => t 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

551 
 j => Bound j) 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

552 
 repair (t $ u) = 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

553 
(case (repair t, repair u) of 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

554 
(t as Bound j, u as Bound k) => 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

555 
(* This is a rather subtle trick to repair the discrepancy between 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

556 
the fully skolemized term that MESON gives us (where existentials 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

557 
were pulled out) and the reality. *) 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

558 
if k > j then t else t $ u 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

559 
 (t, u) => t $ u) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

560 
 repair t = t 
44241  561 
val t' = t > repair > fold (absdummy o snd) params 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

562 
fun do_instantiate th = 
42270  563 
case Term.add_vars (prop_of th) [] 
42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

564 
> filter_out ((Meson_Clausify.is_zapped_var_name orf 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

565 
is_metis_fresh_variable) o fst o fst) of 
42270  566 
[] => th 
42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

567 
 [var as (_, T)] => 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

568 
let 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

569 
val var_binder_Ts = T > binder_types > take (length params) > rev 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

570 
val var_body_T = T > funpow (length params) range_type 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

571 
val tyenv = 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

572 
Vartab.empty > Type.raw_unifys (fastype_of t :: map snd params, 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

573 
var_body_T :: var_binder_Ts) 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

574 
val env = 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

575 
Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0, 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

576 
tenv = Vartab.empty, tyenv = tyenv} 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

577 
val ty_inst = 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

578 
Vartab.fold (fn (x, (S, T)) => 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

579 
cons (pairself (ctyp_of thy) (TVar (x, S), T))) 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

580 
tyenv [] 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

581 
val t_inst = 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

582 
[pairself (cterm_of thy o Envir.norm_term env) (Var var, t')] 
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
43330
diff
changeset

583 
in th > Drule.instantiate_normalize (ty_inst, t_inst) end 
42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

584 
 _ => raise Fail "expected a single nonzapped, nonMetis Var" 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

585 
in 
42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

586 
(DETERM (etac @{thm allE} i THEN rotate_tac ~1 i) 
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

587 
THEN PRIMITIVE do_instantiate) st 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

588 
end 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

589 

41135  590 
fun fix_exists_tac t = 
43162
9a8acc5adfa3
added Metis examples to test the new type encodings
blanchet
parents:
43159
diff
changeset

591 
etac @{thm exE} THEN' rename_tac [t > dest_Var > fst > fst] 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

592 

7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

593 
fun release_quantifier_tac thy (skolem, t) = 
41135  594 
(if skolem then fix_exists_tac else instantiate_forall_tac thy) t 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

595 

40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

596 
fun release_clusters_tac _ _ _ [] = K all_tac 
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

597 
 release_clusters_tac thy ax_counts substs 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

598 
((ax_no, cluster_no) :: clusters) = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

599 
let 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

600 
val cluster_of_var = 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

601 
Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

602 
fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

603 
val cluster_substs = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

604 
substs 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

605 
> map_filter (fn (ax_no', (_, (_, tsubst))) => 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

606 
if ax_no' = ax_no then 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

607 
tsubst > map (apfst cluster_of_var) 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

608 
> filter (in_right_cluster o fst) 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

609 
> map (apfst snd) 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

610 
> SOME 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

611 
else 
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

612 
NONE) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

613 
fun do_cluster_subst cluster_subst = 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset

614 
map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1] 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

615 
val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

616 
in 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

617 
rotate_tac first_prem 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

618 
THEN' (EVERY' (maps do_cluster_subst cluster_substs)) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

619 
THEN' rotate_tac (~ first_prem  length cluster_substs) 
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

620 
THEN' release_clusters_tac thy ax_counts substs clusters 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

621 
end 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

622 

40264
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset

623 
fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) = 
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset

624 
(ax_no, (cluster_no, (skolem, index_no))) 
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset

625 
fun cluster_ord p = 
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset

626 
prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) 
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset

627 
(pairself cluster_key p) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

628 

8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

629 
val tysubst_ord = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

630 
list_ord (prod_ord Term_Ord.fast_indexname_ord 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

631 
(prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

632 

8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

633 
structure Int_Tysubst_Table = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

634 
Table(type key = int * (indexname * (sort * typ)) list 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

635 
val ord = prod_ord int_ord tysubst_ord) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

636 

8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

637 
structure Int_Pair_Graph = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

638 
Graph(type key = int * int val ord = prod_ord int_ord int_ord) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

639 

42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

640 
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no) 
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

641 
fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p) 
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

642 

39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

643 
(* Attempts to derive the theorem "False" from a theorem of the form 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

644 
"P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

645 
specified axioms. The axioms have leading "All" and "Ex" quantifiers, which 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

646 
must be eliminated first. *) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

647 
fun discharge_skolem_premises ctxt axioms prems_imp_false = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

648 
if prop_of prems_imp_false aconv @{prop False} then 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

649 
prems_imp_false 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

650 
else 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

651 
let 
42361  652 
val thy = Proof_Context.theory_of ctxt 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

653 
fun match_term p = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

654 
let 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

655 
val (tyenv, tenv) = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

656 
Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

657 
val tsubst = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

658 
tenv > Vartab.dest 
42099
447fa058ab22
avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents:
42098
diff
changeset

659 
> filter (Meson_Clausify.is_zapped_var_name o fst o fst) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

660 
> sort (cluster_ord 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

661 
o pairself (Meson_Clausify.cluster_of_zapped_var_name 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

662 
o fst o fst)) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

663 
> map (Meson.term_pair_of 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

664 
#> pairself (Envir.subst_term_types tyenv)) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

665 
val tysubst = tyenv > Vartab.dest 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

666 
in (tysubst, tsubst) end 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset

667 
fun subst_info_of_prem subgoal_no prem = 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

668 
case prem of 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

669 
_ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) => 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

670 
let val ax_no = HOLogic.dest_nat num in 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

671 
(ax_no, (subgoal_no, 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

672 
match_term (nth axioms ax_no > the > snd, t))) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

673 
end 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

674 
 _ => raise TERM ("discharge_skolem_premises: Malformed premise", 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

675 
[prem]) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

676 
fun cluster_of_var_name skolem s = 
42098
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset

677 
case try Meson_Clausify.cluster_of_zapped_var_name s of 
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset

678 
NONE => NONE 
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset

679 
 SOME ((ax_no, (cluster_no, _)), skolem') => 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

680 
if skolem' = skolem andalso cluster_no > 0 then 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

681 
SOME (ax_no, cluster_no) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

682 
else 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

683 
NONE 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

684 
fun clusters_in_term skolem t = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

685 
Term.add_var_names t [] > map_filter (cluster_of_var_name skolem o fst) 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset

686 
fun deps_of_term_subst (var, t) = 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

687 
case clusters_in_term false var of 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

688 
[] => NONE 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

689 
 [(ax_no, cluster_no)] => 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

690 
SOME ((ax_no, cluster_no), 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

691 
clusters_in_term true t 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

692 
> cluster_no > 1 ? cons (ax_no, cluster_no  1)) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

693 
 _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

694 
val prems = Logic.strip_imp_prems (prop_of prems_imp_false) 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset

695 
val substs = prems > map2 subst_info_of_prem (1 upto length prems) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

696 
> sort (int_ord o pairself fst) 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset

697 
val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

698 
val clusters = maps (op ::) depss 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

699 
val ordered_clusters = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

700 
Int_Pair_Graph.empty 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

701 
> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

702 
> fold Int_Pair_Graph.add_deps_acyclic depss 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

703 
> Int_Pair_Graph.topological_order 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

704 
handle Int_Pair_Graph.CYCLES _ => 
40158  705 
error "Cannot replay Metis proof in Isabelle without \ 
706 
\\"Hilbert_Choice\"." 

39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

707 
val ax_counts = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

708 
Int_Tysubst_Table.empty 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

709 
> fold (fn (ax_no, (_, (tysubst, _))) => 
43262  710 
Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

711 
(Integer.add 1)) substs 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

712 
> Int_Tysubst_Table.dest 
42339
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

713 
val needed_axiom_props = 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

714 
0 upto length axioms  1 ~~ axioms 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

715 
> map_filter (fn (_, NONE) => NONE 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

716 
 (ax_no, SOME (_, t)) => 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

717 
if exists (fn ((ax_no', _), n) => 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

718 
ax_no' = ax_no andalso n > 0) 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

719 
ax_counts then 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

720 
SOME t 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

721 
else 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

722 
NONE) 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

723 
val outer_param_names = 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

724 
[] > fold Term.add_var_names needed_axiom_props 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

725 
> filter (Meson_Clausify.is_zapped_var_name o fst) 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

726 
> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst)) 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

727 
> filter (fn (((_, (cluster_no, _)), skolem), _) => 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

728 
cluster_no = 0 andalso skolem) 
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

729 
> sort shuffle_ord > map (fst o snd) 
42270  730 
(* for debugging only: 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset

731 
fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

732 
"ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ 
51929  733 
"; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^ 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

734 
commas (map ((fn (s, t) => s ^ " > " ^ t) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

735 
o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" 
51929  736 
val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters) 
737 
val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts) 

738 
val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names) 

39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

739 
val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset

740 
cat_lines (map string_of_subst_info substs)) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

741 
*) 
42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

742 
fun cut_and_ex_tac axiom = 
46708
b138dee7bed3
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
wenzelm
parents:
46392
diff
changeset

743 
cut_tac axiom 1 
42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

744 
THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset

745 
fun rotation_of_subgoal i = 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

746 
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

747 
in 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

748 
Goal.prove ctxt [] [] @{prop False} 
42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

749 
(K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

750 
o fst) ax_counts) 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

751 
THEN rename_tac outer_param_names 1 
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

752 
THEN copy_prems_tac (map snd ax_counts) [] 1) 
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset

753 
THEN release_clusters_tac thy ax_counts substs ordered_clusters 1 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

754 
THEN match_tac [prems_imp_false] 1 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

755 
THEN ALLGOALS (fn i => 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

756 
rtac @{thm Meson.skolem_COMBK_I} i 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset

757 
THEN rotate_tac (rotation_of_subgoal i) i 
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances of the same fact are needed by Metis, cf. example in "Clausify.thy")  the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset

758 
THEN PRIMITIVE (unify_first_prem_with_concl thy i) 
42271
7d08265f181d
further development of new Skolemizer  make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset

759 
THEN assume_tac i 
42270  760 
THEN flexflex_tac))) 
40158  761 
handle ERROR _ => 
762 
error ("Cannot replay Metis proof in Isabelle:\n\ 

763 
\Error when discharging Skolem assumptions.") 

39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

764 
end 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

765 

39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

766 
end; 