author  blanchet 
Fri, 17 Sep 2010 00:35:19 +0200  
changeset 39498  e8aef7ea9cbb 
parent 39497  fa16349939b7 
child 39550  f97fa74c388e 
permissions  rwrr 
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML 
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 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

12 
type mode = Metis_Translate.mode 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

13 

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

14 
val trace: bool Unsynchronized.ref 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

17 
Proof.context > mode > (string * term) list 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

19 
> (Metis_Thm.thm * thm) list 
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset

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

21 

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

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

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

24 

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

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

26 

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

27 
val trace = Unsynchronized.ref false 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

28 
fun trace_msg msg = if !trace then tracing (msg ()) else () 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

29 

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

30 
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

31 

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

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

33 
 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

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

35 

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

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

37 
 types_of (SomeTerm (Var ((a,idx), _)) :: tts) = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

38 
if String.isPrefix "_" a then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

39 
(*Variable generated by Metis, which might have been a type variable.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

40 
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

43 
 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

44 

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

45 
fun apply_list rator nargs rands = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

46 
let val trands = terms_of rands 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

47 
in if length trands = nargs then SomeTerm (list_comb(rator, trands)) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

49 
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

50 
" expected " ^ Int.toString nargs ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

51 
" received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

53 

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

54 
fun infer_types ctxt = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

55 
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

56 

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

57 
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

58 
with variable constraints in the goal...at least, type inference often fails otherwise. 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

59 
SEE ALSO axiom_inf below.*) 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

60 
fun mk_var (w, T) = Var ((w, 1), T) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

61 

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

62 
(*include the default sort, if available*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

63 
fun mk_tfree ctxt w = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

64 
let val ww = "'" ^ w 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

65 
in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

66 

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

67 
(*Remove the "apply" operator from an HO term*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

68 
fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

69 
 strip_happ args x = (x, args); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

70 

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

71 
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

72 

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

73 
fun smart_invert_const "fequal" = @{const_name HOL.eq} 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

74 
 smart_invert_const s = invert_const s 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

75 

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

76 
fun hol_type_from_metis_term _ (Metis_Term.Var v) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

77 
(case strip_prefix_and_unascii tvar_prefix v of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

78 
SOME w => make_tvar w 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

79 
 NONE => make_tvar v) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

80 
 hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

81 
(case strip_prefix_and_unascii type_const_prefix x of 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

82 
SOME tc => Type (smart_invert_const tc, 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

83 
map (hol_type_from_metis_term ctxt) tys) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

84 
 NONE => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

85 
case strip_prefix_and_unascii tfree_prefix x of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

86 
SOME tf => mk_tfree ctxt tf 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

87 
 NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

88 

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

89 
(*Maps metis terms to isabelle terms*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

90 
fun hol_term_from_metis_PT ctxt fol_tm = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

91 
let val thy = ProofContext.theory_of ctxt 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

92 
val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

93 
Metis_Term.toString fol_tm) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

94 
fun tm_to_tt (Metis_Term.Var v) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

95 
(case strip_prefix_and_unascii tvar_prefix v of 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

96 
SOME w => SomeType (make_tvar w) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

99 
SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

100 
 NONE => SomeTerm (mk_var (v, HOLogic.typeT)) ) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

101 
(*Var from Metis with a name like _nnn; possibly a type variable*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

102 
 tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

103 
 tm_to_tt (t as Metis_Term.Fn (".",_)) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

104 
let val (rator,rands) = strip_happ [] t 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

106 
Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

107 
 _ => case tm_to_tt rator of 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

108 
SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands))) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

109 
 _ => raise Fail "tm_to_tt: HO application" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

111 
 tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

112 
and applic_to_tt ("=",ts) = 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

113 
SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

114 
 applic_to_tt (a,ts) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

115 
case strip_prefix_and_unascii const_prefix a of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

116 
SOME b => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

117 
let val c = smart_invert_const b 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

118 
val ntypes = num_type_args thy c 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

119 
val nterms = length ts  ntypes 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

120 
val tts = map tm_to_tt ts 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

121 
val tys = types_of (List.take(tts,ntypes)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

122 
in if length tys = ntypes then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

123 
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

125 
raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

126 
" but gets " ^ Int.toString (length tys) ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

127 
" type arguments\n" ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

128 
cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

129 
" the terms are \n" ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

130 
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

132 
 NONE => (*Not a constant. Is it a type constructor?*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

133 
case strip_prefix_and_unascii type_const_prefix a of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

135 
SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts))) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

136 
 NONE => (*Maybe a TFree. Should then check that ts=[].*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

138 
SOME b => SomeType (mk_tfree ctxt b) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

139 
 NONE => (*a fixed variable? They are Skolem functions.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

140 
case strip_prefix_and_unascii fixed_var_prefix a of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

142 
let val opr = Free (b, HOLogic.typeT) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

143 
in apply_list opr (length ts) (map tm_to_tt ts) end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

144 
 NONE => raise Fail ("unexpected metis function: " ^ a) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

148 
 SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

150 

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

151 
(*Maps fullytyped metis terms to isabelle terms*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

152 
fun hol_term_from_metis_FT ctxt fol_tm = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

153 
let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

154 
Metis_Term.toString fol_tm) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

155 
fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

156 
(case strip_prefix_and_unascii schematic_var_prefix v of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

157 
SOME w => mk_var(w, dummyT) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

158 
 NONE => mk_var(v, dummyT)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

159 
 cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

160 
Const (@{const_name HOL.eq}, HOLogic.typeT) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

161 
 cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

162 
(case strip_prefix_and_unascii const_prefix x of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

163 
SOME c => Const (smart_invert_const c, dummyT) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

164 
 NONE => (*Not a constant. Is it a fixed variable??*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

165 
case strip_prefix_and_unascii fixed_var_prefix x of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

166 
SOME v => Free (v, hol_type_from_metis_term ctxt ty) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

167 
 NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

168 
 cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

169 
cvt tm1 $ cvt tm2 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

170 
 cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

171 
cvt tm1 $ cvt tm2 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

172 
 cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

173 
 cvt (Metis_Term.Fn ("=", [tm1,tm2])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

174 
list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

175 
 cvt (t as Metis_Term.Fn (x, [])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

176 
(case strip_prefix_and_unascii const_prefix x of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

177 
SOME c => Const (smart_invert_const c, dummyT) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

178 
 NONE => (*Not a constant. Is it a fixed variable??*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

179 
case strip_prefix_and_unascii fixed_var_prefix x of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

180 
SOME v => Free (v, dummyT) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

181 
 NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

182 
hol_term_from_metis_PT ctxt t)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

183 
 cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

184 
hol_term_from_metis_PT ctxt t) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

185 
in fol_tm > cvt end 
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 
fun hol_term_from_metis FT = hol_term_from_metis_FT 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

188 
 hol_term_from_metis _ = hol_term_from_metis_PT 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

189 

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

190 
fun hol_terms_from_fol ctxt mode skolems fol_tms = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

191 
let val ts = map (hol_term_from_metis mode ctxt) fol_tms 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

192 
val _ = trace_msg (fn () => " calling type inference:") 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

193 
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

194 
val ts' = ts > map (reveal_skolem_terms skolems) > infer_types ctxt 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

196 
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

197 
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

200 

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

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

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

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

204 

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

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

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

207 
fun print_thpair (fth,th) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

208 
(trace_msg (fn () => "============================================="); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

209 
trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

212 

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

213 
fun lookth thpairs (fth : Metis_Thm.thm) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

214 
the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

216 
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

217 

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

218 
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

219 

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

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

221 

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

222 
fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

223 
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

224 

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

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

226 

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

227 
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

228 

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

229 
fun inst_excluded_middle thy i_atm = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

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

234 

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

235 
fun assume_inf ctxt mode skolems atm = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

237 
(ProofContext.theory_of ctxt) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

238 
(singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

239 

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

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

241 
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

242 
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

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

244 

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

245 
fun inst_inf ctxt mode skolems thpairs fsubst th = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

246 
let val thy = ProofContext.theory_of ctxt 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

247 
val i_th = lookth thpairs th 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

248 
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

249 
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

250 
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

251 
let val v = find_var x 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

252 
(* We call "reveal_skolem_terms" and "infer_types" below. *) 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

253 
val t = hol_term_from_metis mode ctxt y 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

254 
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

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

256 
(trace_msg (fn () => "\"find_var\" failed for " ^ x ^ 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

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

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

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

260 
(trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

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

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

263 
fun remove_typeinst (a, t) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

264 
case strip_prefix_and_unascii schematic_var_prefix a of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

265 
SOME b => SOME (b, t) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

266 
 NONE => case strip_prefix_and_unascii tvar_prefix a of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

267 
SOME _ => NONE (*type instantiations are forbidden!*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

268 
 NONE => SOME (a,t) (*internal Metis var?*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

270 
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

271 
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

272 
val tms = rawtms > map (reveal_skolem_terms skolems) > infer_types ctxt 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

273 
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

274 
val substs' = ListPair.zip (vars, map ctm_of tms) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

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

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

280 
in cterm_instantiate substs' i_th end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

281 
handle THM (msg, _, _) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

282 
error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

283 

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

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

285 

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

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

287 
have an index of 1, and the use of RSN would increase this typically to 3. 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

291 
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

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

293 
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

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

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

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

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

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

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

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

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

302 
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

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

304 
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

305 
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

306 
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

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

308 
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

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

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

311 
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

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

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

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

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

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

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

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

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

320 

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

321 
fun mk_not (Const (@{const_name Not}, _) $ b) = b 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

322 
 mk_not b = HOLogic.mk_not b 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

323 

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

324 
(* Match untyped terms. *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

325 
fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

326 
 untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

327 
 untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

328 
(a = b) (* The index is ignored, for some reason. *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

329 
 untyped_aconv (Bound i) (Bound j) = (i = j) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

330 
 untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

331 
 untyped_aconv (t1 $ t2) (u1 $ u2) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

332 
untyped_aconv t1 u1 andalso untyped_aconv t2 u2 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

333 
 untyped_aconv _ _ = false 
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 
(* Finding the relative location of an untyped term within a list of terms *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

336 
fun literal_index lit = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

338 
val lit = Envir.eta_contract lit 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

339 
fun get _ [] = raise Empty 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

340 
 get n (x :: xs) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

341 
if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

344 
get (n+1) xs 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

345 
in get 1 end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

346 

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

347 
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

349 
val thy = ProofContext.theory_of ctxt 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

350 
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

351 
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

352 
val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

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

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

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

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

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

361 
val i_atm = singleton (hol_terms_from_fol ctxt mode skolems) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

363 
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

364 
val prems_th1 = prems_of i_th1 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

365 
val prems_th2 = prems_of i_th2 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

366 
val index_th1 = literal_index (mk_not i_atm) prems_th1 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

367 
handle Empty => raise Fail "Failed to find literal in th1" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

368 
val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

369 
val index_th2 = literal_index i_atm prems_th2 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

370 
handle Empty => raise Fail "Failed to find literal in th2" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

371 
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

373 
resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

377 

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

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

379 

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

380 
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

381 

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

382 
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

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

384 

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

385 
fun refl_inf ctxt mode skolems t = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

386 
let val thy = ProofContext.theory_of ctxt 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

387 
val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

389 
val c_t = cterm_incr_types thy refl_idx i_t 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

390 
in cterm_instantiate [(refl_x, c_t)] REFL_THM end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

391 

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

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

393 

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

394 
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

395 
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

396 

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

397 
val metis_eq = Metis_Term.Fn ("=", []); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

398 

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

399 
fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

400 
 get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

401 
 get_ty_arg_size _ _ = 0; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

402 

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

403 
fun equality_inf ctxt mode skolems (pos, atm) fp fr = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

404 
let val thy = ProofContext.theory_of ctxt 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

405 
val m_tm = Metis_Term.Fn atm 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

406 
val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

409 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

410 
fun path_finder_FO tm [] = (tm, Bound 0) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

411 
 path_finder_FO tm (p::ps) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

412 
let val (tm1,args) = strip_comb tm 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

413 
val adjustment = get_ty_arg_size thy tm1 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

414 
val p' = if adjustment > p then p else padjustment 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

415 
val tm_p = List.nth(args,p') 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

416 
handle Subscript => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

417 
error ("Cannot replay Metis proof in Isabelle:\n" ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

418 
"equality_inf: " ^ Int.toString p ^ " adj " ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

419 
Int.toString adjustment ^ " term " ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

420 
Syntax.string_of_term ctxt tm) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

421 
val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

422 
" " ^ Syntax.string_of_term ctxt tm_p) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

423 
val (r,t) = path_finder_FO tm_p ps 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

425 
(r, list_comb (tm1, replace_item_list t p' args)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

427 
fun path_finder_HO tm [] = (tm, Bound 0) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

428 
 path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

429 
 path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

431 
raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

432 
"equality_inf, path_finder_HO: path = " ^ 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

433 
space_implode " " (map Int.toString ps) ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

434 
" isaterm: " ^ Syntax.string_of_term ctxt tm) 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

435 
fun path_finder_FT tm [] _ = (tm, Bound 0) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

436 
 path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

437 
path_finder_FT tm ps t1 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

438 
 path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

439 
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

440 
 path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

441 
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

443 
raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ 
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

444 
"equality_inf, path_finder_FT: path = " ^ 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

445 
space_implode " " (map Int.toString ps) ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

446 
" isaterm: " ^ Syntax.string_of_term ctxt tm ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

447 
" folterm: " ^ Metis_Term.toString t) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

448 
fun path_finder FO tm ps _ = path_finder_FO tm ps 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

449 
 path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

450 
(*equality: not curried, as other predicates are*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

451 
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

452 
else path_finder_HO tm (p::ps) (*1 selects second operand*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

453 
 path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

454 
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

455 
 path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

456 
(Metis_Term.Fn ("=", [t1,t2])) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

457 
(*equality: not curried, as other predicates are*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

458 
if p=0 then path_finder_FT tm (0::1::ps) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

459 
(Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2])) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

460 
(*select first operand*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

461 
else path_finder_FT tm (p::ps) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

462 
(Metis_Term.Fn (".", [metis_eq,t2])) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

463 
(*1 selects second operand*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

464 
 path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

465 
(*if not equality, ignore head to skip the hBOOL predicate*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

466 
 path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

467 
fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

468 
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

469 
in (tm, nt $ tm_rslt) end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

470 
 path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

471 
val (tm_subst, body) = path_finder_lit i_atm fp 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

472 
val tm_abs = Abs ("x", type_of tm_subst, body) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

473 
val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

476 
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

477 
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

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

482 

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

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

484 

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

485 
fun step ctxt mode skolems thpairs p = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

487 
(fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

488 
 (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

489 
 (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

490 
factor (inst_inf ctxt mode skolems thpairs f_subst f_th1) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

491 
 (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

492 
factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

493 
 (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

494 
 (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

495 
equality_inf ctxt mode skolems f_lit f_p f_r 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

496 

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

497 
fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

498 

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

499 
fun replay_one_inference ctxt mode skolems (fol_th, inf) thpairs = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

502 
val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

503 
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

504 
val th = Meson.flexflex_first_order (step ctxt mode skolems 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

505 
thpairs (fol_th, inf)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

508 
val n_metis_lits = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

509 
length (filter is_real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

510 
val _ = if nprems_of th = n_metis_lits then () 
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 > 'a}
blanchet
parents:
39497
diff
changeset

511 
else error "Cannot replay Metis proof in Isabelle: Out of sync." 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

512 
in (fol_th, th) :: thpairs end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

513 

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

514 
end; 