author  blanchet 
Wed, 08 Jun 2011 16:20:18 +0200  
changeset 43294  0271fda2a83a 
parent 43268  c0eaa8b9bff5 
child 43297  e77baf329f48 
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 
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

12 
exception METIS of string * string 
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

13 

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

14 
val hol_clause_from_metis : 
43184  15 
Proof.context > int Symtab.table > (string * term) list > Metis_Thm.thm 
16 
> term 

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

17 
val lookth : (Metis_Thm.thm * 'a) list > Metis_Thm.thm > 'a 
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

18 
val untyped_aconv : term * term > bool 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

19 
val replay_one_inference : 
43212  20 
Proof.context > (string * term) list > int Symtab.table 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

21 
> 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

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

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

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

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

26 

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

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

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

29 

43094  30 
open ATP_Problem 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
42650
diff
changeset

31 
open ATP_Translate 
43094  32 
open ATP_Reconstruct 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

34 

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

35 
exception METIS of string * string 
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

36 

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

37 
datatype term_or_type = SomeTerm of term  SomeType of typ 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

38 

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

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

40 
 terms_of (SomeTerm t :: tts) = t :: terms_of tts 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

41 
 terms_of (SomeType _ :: tts) = terms_of tts; 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

42 

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

43 
fun types_of [] = [] 
43135
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

44 
 types_of (SomeTerm (Var ((a, idx), _)) :: tts) = 
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

45 
types_of tts 
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

46 
> (if String.isPrefix metis_generated_var_prefix a then 
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

47 
(* Variable generated by Metis, which might have been a type 
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

48 
variable. *) 
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

49 
cons (TVar (("'" ^ a, idx), HOLogic.typeS)) 
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

50 
else 
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

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

52 
 types_of (SomeTerm _ :: tts) = types_of tts 
43135
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

53 
 types_of (SomeType T :: tts) = T :: types_of tts 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

54 

43094  55 
fun atp_name_from_metis s = 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

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

57 
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

58 
 _ => (s, false) 
43094  59 
fun atp_term_from_metis (Metis_Term.Fn (s, tms)) = 
43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

60 
let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset

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

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

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

64 

43212  65 
fun hol_term_from_metis ctxt sym_tab = 
66 
atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE 

43094  67 

43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

68 
fun atp_literal_from_metis (pos, atom) = 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

69 
atom > Metis_Term.Fn > atp_term_from_metis > AAtom > not pos ? mk_anot 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

70 
fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, [])) 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

71 
 atp_clause_from_metis lits = 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

72 
lits > map atp_literal_from_metis > mk_aconns AOr 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

73 

43184  74 
fun reveal_old_skolems_and_infer_types ctxt old_skolems = 
75 
map (reveal_old_skolem_terms old_skolems) 

43212  76 
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) 
43184  77 

78 
fun hol_clause_from_metis ctxt sym_tab old_skolems = 

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

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

80 
#> Metis_LiteralSet.toList 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

81 
#> atp_clause_from_metis 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

82 
#> prop_from_atp ctxt false sym_tab 
43184  83 
#> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems) 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

84 

43212  85 
fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms = 
86 
let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms 

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

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

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

89 
(fn () => Syntax.string_of_term ctxt t)) ts 
43184  90 
val ts' = 
91 
ts > reveal_old_skolems_and_infer_types ctxt old_skolems 

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

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

93 
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ 
43128  94 
" 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

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

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

97 

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

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

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

100 
(*  *) 
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 
(*for debugging only*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

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

107 
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

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

109 

43094  110 
fun lookth th_pairs fth = 
111 
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

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

113 
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

114 

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

115 
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

116 

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

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

118 

43212  119 
(* This causes variables to have an index of 1 by default. See also 
120 
"term_from_atp" in "ATP_Reconstruct". *) 

121 
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

122 

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

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

124 

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

125 
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

126 

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

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

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

129 
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

130 
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

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

132 

43212  133 
fun assume_inference ctxt old_skolems sym_tab atom = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

134 
inst_excluded_middle 
42361  135 
(Proof_Context.theory_of ctxt) 
43212  136 
(singleton (hol_terms_from_metis ctxt old_skolems 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

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

138 

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

139 
(* 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

140 
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

141 
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

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

143 

43212  144 
fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th = 
42361  145 
let val thy = Proof_Context.theory_of ctxt 
43094  146 
val i_th = lookth th_pairs th 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

147 
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

148 
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

149 
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

150 
let val v = find_var x 
43184  151 
(* We call "reveal_old_skolems_and_infer_types" below. *) 
43212  152 
val t = hol_term_from_metis ctxt sym_tab y 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

153 
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

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

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

156 
" 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

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

158 
 TYPE _ => 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

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

160 
" 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

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

162 
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

163 
let val a = Metis_Name.toString a in 
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

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

165 
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

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

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

168 
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

169 
 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

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

171 
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

172 
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) 
43184  173 
val (vars, tms) = 
174 
ListPair.unzip (map_filter subst_translation substs) 

175 
> reveal_old_skolems_and_infer_types ctxt old_skolems 

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

176 
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

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

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

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

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

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

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

183 
in cterm_instantiate substs' i_th end 
43186  184 
handle THM (msg, _, _) => raise METIS ("inst_inference", msg) 
185 
 ERROR msg => raise METIS ("inst_inference", msg) 

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

186 

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

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

188 

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

189 
(* 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

190 
have an index of 1, and the use of RSN would increase this typically to 3. 
43135
8c32a0160b0d
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
blanchet
parents:
43134
diff
changeset

191 
Instantiations of those Vars could then fail. See comment on "make_var". *) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

194 
val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

195 
fun aux tha thb = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

196 
case Thm.bicompose false (false, tha, nprems_of tha) i thb 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

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

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

202 
aux tha thb 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

203 
handle TERM z => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

204 
(* 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

205 
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

206 
"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

207 
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

208 
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

209 
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

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

211 
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

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

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

214 
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

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

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

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

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

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

220 
[] => raise TERM z 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

221 
 ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

223 

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

224 
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

225 
 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

226 
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

227 
 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

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

229 

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

230 
(* Match untyped terms. *) 
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

231 
fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b) 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

232 
 untyped_aconv (Free (a, _), Free (b, _)) = (a = b) 
43294  233 
 untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = 
234 
(a = b) (* ignore variable numbers *) 

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

235 
 untyped_aconv (Bound i, Bound j) = (i = j) 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

236 
 untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u) 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

237 
 untyped_aconv (t1 $ t2, u1 $ u2) = 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

238 
untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2) 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

239 
 untyped_aconv _ = false 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

240 

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

241 
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

242 

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

243 
(* 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

244 
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

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

246 
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

247 
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

248 
HOLogic.dest_Trueprop #> normalize 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

249 
#> curry untyped_aconv (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

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

251 
(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

252 
~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

253 
 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

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

255 

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

258 
let val n = nprems_of th 

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

260 
then Thm.permute_prems (i1) 1 th 

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

262 
end; 

263 

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

264 
(* 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

265 
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

266 
"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

267 
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

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

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

270 
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

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

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

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

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

275 
th > fold (rewrite_rule o single) @{thms not_atomize atomize_not} 
39893  276 

277 
(* 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

278 
val select_literal = negate_head oo make_last 
39893  279 

43212  280 
fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

281 
let 
43094  282 
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

283 
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

284 
" 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

285 
\ 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

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

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

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

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

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

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

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

293 
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

294 
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

295 
val i_atom = 
43212  296 
singleton (hol_terms_from_metis ctxt old_skolems 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

297 
(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

298 
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

299 
" 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

300 
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

301 
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

302 
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

303 
(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

304 
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

305 
 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

306 
(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

307 
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

308 
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

309 
(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

310 
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

311 
 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

312 
(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

313 
resolve_inc_tyvars thy (select_literal j1 i_th1) j2 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

314 
handle TERM (s, _) => raise METIS ("resolve_inference", s))) 
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

315 
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

316 
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: REFL *) 
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 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

321 

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

322 
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

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

324 

43212  325 
fun refl_inference ctxt old_skolems sym_tab t = 
43094  326 
let 
327 
val thy = Proof_Context.theory_of ctxt 

43212  328 
val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t 
43094  329 
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) 
330 
val c_t = cterm_incr_types thy refl_idx i_t 

331 
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

332 

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

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

334 

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

335 
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

336 
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

337 

43212  338 
fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr = 
42361  339 
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

340 
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

341 
val [i_atom, i_tm] = 
43212  342 
hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr] 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

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

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

345 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
43205  346 
fun path_finder_fail tm ps t = 
43209
007117fed183
fall back in case path finder fails  these errors are sometimes salvageable
blanchet
parents:
43205
diff
changeset

347 
raise METIS ("equality_inference (path_finder)", 
007117fed183
fall back in case path finder fails  these errors are sometimes salvageable
blanchet
parents:
43205
diff
changeset

348 
"path = " ^ space_implode " " (map string_of_int ps) ^ 
007117fed183
fall back in case path finder fails  these errors are sometimes salvageable
blanchet
parents:
43205
diff
changeset

349 
" isaterm: " ^ Syntax.string_of_term ctxt tm ^ 
007117fed183
fall back in case path finder fails  these errors are sometimes salvageable
blanchet
parents:
43205
diff
changeset

350 
(case t of 
007117fed183
fall back in case path finder fails  these errors are sometimes salvageable
blanchet
parents:
43205
diff
changeset

351 
SOME t => " folterm: " ^ Metis_Term.toString t 
007117fed183
fall back in case path finder fails  these errors are sometimes salvageable
blanchet
parents:
43205
diff
changeset

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

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

356 
val s = s > Metis_Name.toString 
c0eaa8b9bff5
removed yet another hack in "make_metis" script  respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset

357 
> perhaps (try (strip_prefix_and_unascii const_prefix 
43177  358 
#> the #> unmangled_const_name)) 
359 
in 

360 
if s = metis_predicator orelse s = predicator_name orelse 

361 
s = metis_type_tag orelse s = type_tag_name then 

43212  362 
path_finder tm ps (nth ts p) 
43177  363 
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

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

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

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

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

368 
if p' = 0 then 
43212  369 
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

370 
else 
43212  371 
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

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

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

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

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

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

377 
val p' = if adjustment > p then p else p  adjustment 
43205  378 
val tm_p = 
379 
nth args p' 

380 
handle 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

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

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

383 
Syntax.string_of_term ctxt tm_p) 
43212  384 
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

385 
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

386 
end 
43212  387 
 path_finder tm ps t = path_finder_fail tm ps (SOME t) 
388 
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

389 
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

390 
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

391 
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

392 
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

393 
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

394 
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

395 
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

396 
val eq_terms = map (pairself (cterm_of thy)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

397 
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

399 

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

401 

43212  402 
fun one_step ctxt old_skolems sym_tab th_pairs p = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

403 
case p of 
43186  404 
(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

405 
 (_, Metis_Proof.Assume f_atom) => 
43212  406 
assume_inference ctxt old_skolems sym_tab f_atom 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

407 
 (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => 
43212  408 
inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1 
43186  409 
> 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

410 
 (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) => 
43212  411 
resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2 
43094  412 
> factor 
43186  413 
 (_, Metis_Proof.Refl f_tm) => 
43212  414 
refl_inference ctxt old_skolems sym_tab f_tm 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

415 
 (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => 
43212  416 
equality_inference ctxt old_skolems sym_tab f_lit f_p f_r 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

417 

39893  418 
fun flexflex_first_order th = 
419 
case Thm.tpairs_of th of 

420 
[] => th 

421 
 pairs => 

422 
let val thy = theory_of_thm th 

423 
val (_, tenv) = 

424 
fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) 

425 
val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) 

426 
val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th 

427 
in th' end 

428 
handle THM _ => th; 

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

429 

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

430 
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

431 
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

432 
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

433 
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

434 

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

435 
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

436 

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

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

440 
unifiable) types. *) 

441 
fun resynchronize ctxt fol_th th = 

442 
let 

443 
val num_metis_lits = 

444 
count is_metis_literal_genuine 

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

446 
val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th) 

447 
in 

448 
if num_metis_lits >= num_isabelle_lits then 

449 
th 

450 
else 

451 
let 

452 
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

453 
val prems = prems0 > map normalize_literal 
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

454 
> distinct untyped_aconv 
42333  455 
val goal = Logic.list_implies (prems, concl) 
43195
6dc58b3b73b5
improved correctness of handling of higherorder occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset

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

457 
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

458 
THEN ALLGOALS assume_tac 
42333  459 
in 
460 
if length prems = length prems0 then 

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

461 
raise METIS ("resynchronize", "Out of sync") 
42333  462 
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

463 
Goal.prove ctxt [] [] goal (K tac) 
42333  464 
> resynchronize ctxt fol_th 
465 
end 

466 
end 

467 

43212  468 
fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs = 
43094  469 
if not (null th_pairs) andalso 
470 
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

471 
(* 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

472 
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

473 
benefice of the doubt. *) 
43094  474 
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

475 
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

476 
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

477 
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

478 
(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

479 
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

480 
(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

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 () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) 
43212  483 
val th = one_step ctxt old_skolems 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

484 
> flexflex_first_order 
42333  485 
> 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

486 
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

487 
(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

488 
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

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

491 

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

492 
(* 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

493 
one of the premises. Unfortunately, this sometimes yields "Variable 
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 
?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the 
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 
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

496 
?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

497 
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

498 
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

499 
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

500 
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

501 
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

502 
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

503 
fun pair_untyped_aconv (t1, t2) (u1, u2) = 
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset

504 
untyped_aconv (t1, u1) andalso untyped_aconv (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

505 
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

506 
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

507 
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

508 
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

509 
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

510 
(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

511 
 _ => 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

512 
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

513 
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

514 
(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

515 
add_terms (Var z, 
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 
fold_rev (curry absdummy) (take (length args) (binder_types T)) 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

517 
 _ => 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

518 
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

519 
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

520 
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

521 
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

522 
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

523 
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

524 
(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

525 
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

526 
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

527 
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

528 
 (_ $ _, _) => 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

529 
 (_, _ $ _) => 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

530 
 (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

531 
 (_, 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

532 
 _ => 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

533 
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

534 
[] > 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

535 
> 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

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

537 

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

538 
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

539 

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

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

541 
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

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

543 
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

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

545 
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

546 

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

547 
(* 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

548 
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

549 

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

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

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

552 
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

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

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

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

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

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

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

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

560 
(* 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

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

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

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

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

565 
 repair t = t 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

566 
val t' = t > repair > fold (curry absdummy) (map snd params) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

567 
fun do_instantiate th = 
42270  568 
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

569 
> 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

570 
is_metis_fresh_variable) o fst o fst) of 
42270  571 
[] => 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

572 
 [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

573 
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

574 
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

575 
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

576 
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

577 
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

578 
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

579 
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

580 
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

581 
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

582 
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

583 
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

584 
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

585 
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

586 
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

587 
[pairself (cterm_of thy o Envir.norm_term env) (Var var, t')] 
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

588 
in th > instantiate (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

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

590 
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

591 
(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

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

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

594 

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

596 
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

597 

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

598 
fun release_quantifier_tac thy (skolem, t) = 
41135  599 
(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

600 

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

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

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

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

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

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

606 
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

607 
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

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

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

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

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

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

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

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

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

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

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

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

619 
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

620 
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

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

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

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

624 
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

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

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

627 

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

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

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

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

631 
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

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

633 

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

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

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

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

637 

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

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

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

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

641 

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

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

643 
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

644 

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

645 
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

646 
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

647 

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

648 
(* 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

649 
"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

650 
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

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

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

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

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

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

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

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

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

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

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

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

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

664 
> 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

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

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

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

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

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

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

671 
in (tysubst, tsubst) end 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

672 
fun subst_info_for_prem subgoal_no prem = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

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

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

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

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

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

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

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

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

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

682 
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

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

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

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

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

687 
else 
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 
fun clusters_in_term skolem t = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

690 
Term.add_var_names t [] > map_filter (cluster_of_var_name skolem o fst) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

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

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

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

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

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

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

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

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

699 
val prems = Logic.strip_imp_prems (prop_of prems_imp_false) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

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

701 
> sort (int_ord o pairself fst) 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

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

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

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

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

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

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

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

709 
handle Int_Pair_Graph.CYCLES _ => 
40158  710 
error "Cannot replay Metis proof in Isabelle without \ 
711 
\\"Hilbert_Choice\"." 

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

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

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

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

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

717 
> 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

718 
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

719 
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

720 
> 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

721 
 (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

722 
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

723 
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

724 
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

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

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

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

728 
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

729 
[] > 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

730 
> 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

731 
> 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

732 
> 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

733 
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

734 
> sort shuffle_ord > map (fst o snd) 
42270  735 
(* for debugging only: 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

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

737 
"ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

738 
"; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^ 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

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

740 
o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" 
40264
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset

741 
val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters) 
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset

742 
val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts) 
42339
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset

743 
val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

744 
val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

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

746 
*) 
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

747 
fun cut_and_ex_tac axiom = 
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

748 
cut_rules_tac [axiom] 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

749 
THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) 
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

750 
fun rotation_for_subgoal i = 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

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

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

753 
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

754 
(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

755 
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

756 
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

757 
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

758 
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

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

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

761 
rtac @{thm Meson.skolem_COMBK_I} i 
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset

762 
THEN rotate_tac (rotation_for_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

763 
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

764 
THEN assume_tac i 
42270  765 
THEN flexflex_tac))) 
40158  766 
handle ERROR _ => 
767 
error ("Cannot replay Metis proof in Isabelle:\n\ 

768 
\Error when discharging Skolem assumptions.") 

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

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

770 

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

771 
end; 