author  blanchet 
Thu, 16 Sep 2010 17:30:29 +0200  
changeset 39497  fa16349939b7 
parent 39495  bb4fb9ffe2d1 
child 39498  e8aef7ea9cbb 
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 

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

30 
datatype term_or_type = Term of Term.term  Type of Term.typ; 
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 [] = [] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

33 
 terms_of (Term t :: tts) = t :: terms_of tts 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

34 
 terms_of (Type _ :: tts) = terms_of tts; 
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 [] = [] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

37 
 types_of (Term (Term.Var ((a,idx), _)) :: tts) = 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

42 
 types_of (Term _ :: tts) = types_of tts 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

43 
 types_of (Type T :: tts) = T :: types_of tts; 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

47 
in if length trands = nargs then Term (list_comb(rator, trands)) 
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.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

60 
fun mk_var (w,T) = Term.Var((w,1), T); 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

82 
SOME tc => Term.Type (smart_invert_const tc, 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

83 
map (hol_type_from_metis_term ctxt) tys) 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

96 
SOME w => Type (make_tvar w) 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

99 
SOME w => Term (mk_var (w, HOLogic.typeT)) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

100 
 NONE => Term (mk_var (v, HOLogic.typeT)) ) 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

108 
Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) 
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) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

113 
Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) 
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 => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

135 
Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts))) 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

138 
SOME b => Type (mk_tfree ctxt b) 
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 => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

142 
let val opr = Term.Free(b, HOLogic.typeT) 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

147 
Term t => t 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

148 
 _ => raise Fail "fol_tm_to_tt: Term expected" 
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 

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

240 
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

243 
can be inferred from terms.*) 
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 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

247 
val i_th = lookth thpairs th 
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) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

251 
let val v = find_var x 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

252 
(* We call "reveal_skolem_terms" and "infer_types" below. *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

253 
val t = hol_term_from_metis mode ctxt y 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

254 
in SOME (cterm_of thy (Var v), t) end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

256 
(trace_msg (fn() => "\"find_var\" failed for the variable " ^ x ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

257 
" in " ^ Display.string_of_thm ctxt i_th); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

260 
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

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

262 
 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

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

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

265 
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

266 
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

267 
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

268 
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

269 
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

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

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

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

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

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

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

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

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

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

279 

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

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

281 

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

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

283 
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

284 
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

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

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

287 
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

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

289 
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

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

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

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

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

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

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

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

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

298 
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

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

300 
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

301 
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

302 
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

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

304 
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

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

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

307 
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

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

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

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

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

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

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

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

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

316 

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

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

318 
 mk_not b = HOLogic.mk_not b 
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 
(* Match untyped terms. *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

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

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

326 
 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

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

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

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

330 

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

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

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

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

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

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

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

337 
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

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

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

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

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

342 

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

343 
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

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

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

346 
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

347 
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

348 
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

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

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

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

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

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

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

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

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

357 
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

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

359 
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

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

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

362 
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

363 
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

364 
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

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

366 
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

367 
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

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

369 
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

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

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

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

373 

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

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

375 

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

376 
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

377 

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

378 
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

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

380 

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

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

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

383 
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

384 
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

385 
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

386 
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

387 

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

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

389 

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

390 
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

391 
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

392 

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

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

394 

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

395 
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

396 
 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

397 
 get_ty_arg_size _ _ = 0; 
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 equality_inf ctxt mode skolems (pos, atm) fp fr = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

402 
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

403 
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

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

405 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

424 
 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

425 
 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

426 
 path_finder_HO tm ps = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

427 
raise Fail ("equality_inf, path_finder_HO: path = " ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

431 
 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

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

433 
 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

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

435 
 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

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

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

438 
raise Fail ("equality_inf, path_finder_FT: path = " ^ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

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

442 
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

443 
 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

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

445 
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

446 
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

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

448 
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

449 
 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

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

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

452 
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

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

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

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

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

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

458 
 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

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

460 
 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

461 
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

462 
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

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

464 
 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

465 
val (tm_subst, body) = path_finder_lit i_atm fp 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

467 
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

468 
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

469 
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

470 
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

471 
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

472 
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

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

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

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

476 

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

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

478 

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

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

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

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

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

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

484 
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

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

486 
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

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

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

489 
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

490 

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

491 
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

492 

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

493 
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

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

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

496 
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

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

498 
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

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

500 
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

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

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

503 
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

504 
val _ = if nprems_of th = n_metis_lits then () 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset

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

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

507 

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

508 
end; 