--- a/src/HOL/Tools/metis_tools.ML Sun Oct 18 18:08:04 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Sun Oct 18 20:53:40 2009 +0200
@@ -81,11 +81,11 @@
| (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
| _ => error "hol_term_to_fol_FO";
-fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a
- | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) =
- Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist)
- | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
- Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
+fun hol_term_to_fol_HO (ResHolClause.CombVar (a, _)) = Metis.Term.Var a
+ | hol_term_to_fol_HO (ResHolClause.CombConst (a, _, tylist)) =
+ Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
+ | hol_term_to_fol_HO (ResHolClause.CombApp (tm1, tm2)) =
+ Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
(*The fully-typed translation, to avoid type errors*)
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
@@ -122,8 +122,8 @@
fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
| metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
-fun default_sort ctxt (TVar _) = false
- | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
+fun default_sort _ (TVar _) = false
+ | default_sort ctxt (TFree (x, s)) = (s = Option.getOpt (Variable.def_sort ctxt (x, ~1), []));
fun metis_of_tfree tf =
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
@@ -162,7 +162,7 @@
fun m_classrel_cls subclass superclass =
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
-fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) =
+fun classrel_cls (ResClause.ClassrelClause {subclass, superclass, ...}) =
(TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
(* ------------------------------------------------------------------------- *)
@@ -176,10 +176,10 @@
| terms_of (Type _ :: tts) = terms_of tts;
fun types_of [] = []
- | types_of (Term (Term.Var((a,idx), T)) :: tts) =
+ | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
if String.isPrefix "_" a then
(*Variable generated by Metis, which might have been a type variable.*)
- TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts
+ TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
else types_of tts
| types_of (Term _ :: tts) = types_of tts
| types_of (Type T :: tts) = T :: types_of tts;
@@ -210,7 +210,7 @@
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
| strip_happ args x = (x, args);
-fun fol_type_to_isa ctxt (Metis.Term.Var v) =
+fun fol_type_to_isa _ (Metis.Term.Var v) =
(case Recon.strip_prefix ResClause.tvar_prefix v of
SOME w => Recon.make_tvar w
| NONE => Recon.make_tvar v)
@@ -281,11 +281,11 @@
(*Maps fully-typed metis terms to isabelle terms*)
fun fol_term_to_hol_FT ctxt fol_tm =
let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
- fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
+ fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
(case Recon.strip_prefix ResClause.schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
- | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), ty])) =
+ | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
Const ("op =", HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
(case Recon.strip_prefix ResClause.const_prefix x of
@@ -356,7 +356,7 @@
in cterm_instantiate substs th end;
(* INFERENCE RULE: AXIOM *)
-fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th);
+fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th);
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
(* INFERENCE RULE: ASSUME *)
@@ -418,7 +418,6 @@
fun resolve_inf ctxt mode thpairs atm th1 th2 =
let
- val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
@@ -451,17 +450,17 @@
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
-fun get_ty_arg_size thy (Const("op =",_)) = 0 (*equality has no type arguments*)
- | get_ty_arg_size thy (Const(c,_)) = (Recon.num_typargs thy c handle TYPE _ => 0)
- | get_ty_arg_size thy _ = 0;
+fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*)
+ | get_ty_arg_size thy (Const (c, _)) = (Recon.num_typargs thy c handle TYPE _ => 0)
+ | get_ty_arg_size _ _ = 0;
(* INFERENCE RULE: EQUALITY *)
-fun equality_inf ctxt mode thpairs (pos,atm) fp fr =
+fun equality_inf ctxt mode (pos, atm) fp fr =
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis.Term.Fn atm
val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
- fun replace_item_list lx 0 (l::ls) = lx::ls
+ fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
fun path_finder_FO tm [] = (tm, Term.Bound 0)
| path_finder_FO tm (p::ps) =
@@ -479,13 +478,13 @@
end
fun path_finder_HO tm [] = (tm, Term.Bound 0)
| path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
- | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
+ | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
- | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1,t2])) =
+ | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
path_finder_FT tm ps t1
- | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1,t2])) =
+ | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
- | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [t1,t2])) =
+ | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
| path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
space_implode " " (map Int.toString ps) ^
@@ -496,7 +495,7 @@
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
else path_finder_HO tm (p::ps) (*1 selects second operand*)
- | path_finder HO tm (p::ps) (Metis.Term.Fn ("{}", [t1])) =
+ | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
| path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
(Metis.Term.Fn ("=", [t1,t2])) =
@@ -507,7 +506,7 @@
else path_finder_FT tm (p::ps)
(Metis.Term.Fn (".", [metis_eq,t2]))
(*1 selects second operand*)
- | path_finder FT tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
+ | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
(*if not equality, ignore head to skip the hBOOL predicate*)
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
@@ -528,22 +527,19 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step ctxt mode thpairs (fol_th, Metis.Proof.Axiom _) =
- factor (axiom_inf ctxt thpairs fol_th)
- | step ctxt mode thpairs (_, Metis.Proof.Assume f_atm) =
- assume_inf ctxt mode f_atm
- | step ctxt mode thpairs (_, Metis.Proof.Subst(f_subst, f_th1)) =
+fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
+ | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
+ | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
factor (inst_inf ctxt mode thpairs f_subst f_th1)
- | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
+ | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
- | step ctxt mode thpairs (_, Metis.Proof.Refl f_tm) =
- refl_inf ctxt mode f_tm
- | step ctxt mode thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
- equality_inf ctxt mode thpairs f_lit f_p f_r;
+ | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
+ | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
+ equality_inf ctxt mode f_lit f_p f_r;
-fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
+fun real_literal (_, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
-fun translate mode _ thpairs [] = thpairs
+fun translate _ _ thpairs [] = thpairs
| translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
let val _ = trace_msg (fn () => "=============================================")
val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
@@ -551,7 +547,8 @@
val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg (fn () => "=============================================")
- val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
+ val n_metis_lits =
+ length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
in
if nprems_of th = n_metis_lits then ()
else error "Metis: proof reconstruction has gone wrong";
@@ -560,7 +557,7 @@
(*Determining which axiom clauses are actually used*)
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
- | used_axioms axioms _ = NONE;
+ | used_axioms _ _ = NONE;
(* ------------------------------------------------------------------------- *)
(* Translation of HO Clauses *)
@@ -581,8 +578,7 @@
let val subs = ResAtp.tfree_classes_of_terms tms
val supers = ResAtp.tvar_classes_of_terms tms
and tycons = ResAtp.type_consts_of_terms thy tms
- val arity_clauses = ResClause.make_arity_clauses thy tycons supers
- val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
+ val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses
end;
@@ -595,12 +591,12 @@
{axioms : (Metis.Thm.thm * Thm.thm) list,
tfrees : ResClause.type_literal list};
-fun const_in_metis c (pol,(pred,tm_list)) =
+fun const_in_metis c (pred, tm_list) =
let
- fun in_mterm (Metis.Term.Var nm) = false
+ fun in_mterm (Metis.Term.Var _) = false
| in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
| in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
- in c=pred orelse exists in_mterm tm_list end;
+ in c = pred orelse exists in_mterm tm_list end;
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
@@ -641,7 +637,7 @@
{axioms = [], tfrees = init_tfrees ctxt} cls
val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
- fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
+ fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
(*Now check for the existence of certain combinators*)
val thI = if used "c_COMBI" then [comb_I] else []
val thK = if used "c_COMBK" then [comb_K] else []
@@ -697,7 +693,7 @@
and used = map_filter (used_axioms axioms) proof
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
- val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
+ val unused = filter (fn (_, cls) => not (common_thm used cls)) th_cls_pairs
in
if null unused then ()
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));