1.1 --- a/src/HOL/Tools/meson.ML Fri Aug 25 18:46:24 2006 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Fri Aug 25 18:47:36 2006 +0200
1.3 @@ -15,6 +15,7 @@
1.4 sig
1.5 val size_of_subgoals : thm -> int
1.6 val make_cnf : thm list -> thm -> thm list
1.7 + val finish_cnf : thm list -> thm list
1.8 val make_nnf : thm -> thm
1.9 val make_nnf1 : thm -> thm
1.10 val skolemize : thm -> thm
1.11 @@ -36,7 +37,6 @@
1.12 val select_literal : int -> thm -> thm
1.13 val skolemize_tac : int -> tactic
1.14 val make_clauses_tac : int -> tactic
1.15 - val check_is_fol_term : term -> term
1.16 end
1.17
1.18
1.19 @@ -66,13 +66,29 @@
1.20
1.21 (**** Operators for forward proof ****)
1.22
1.23 -(*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*)
1.24 -fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb);
1.25 +
1.26 +(** First-order Resolution **)
1.27 +
1.28 +fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
1.29 +fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
1.30 +
1.31 +val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
1.32 +
1.33 +(*FIXME: currently does not "rename variables apart"*)
1.34 +fun first_order_resolve thA thB =
1.35 + let val thy = theory_of_thm thA
1.36 + val tmA = concl_of thA
1.37 + fun match pat = Pattern.first_order_match thy (pat,tmA) (tyenv0,tenv0)
1.38 + val Const("==>",_) $ tmB $ _ = prop_of thB
1.39 + val (tyenv,tenv) = match tmB
1.40 + val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
1.41 + in thA RS (cterm_instantiate ct_pairs thB) end
1.42 + handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
1.43
1.44 (*raises exception if no rules apply -- unlike RL*)
1.45 fun tryres (th, rls) =
1.46 let fun tryall [] = raise THM("tryres", 0, th::rls)
1.47 - | tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls)
1.48 + | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
1.49 in tryall rls end;
1.50
1.51 (*Permits forward proof from rules that discharge assumptions*)
1.52 @@ -189,6 +205,11 @@
1.53
1.54 val has_meta_conn =
1.55 exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
1.56 +
1.57 +fun apply_skolem_ths (th, rls) =
1.58 + let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
1.59 + | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
1.60 + in tryall rls end;
1.61
1.62 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
1.63 Strips universal quantifiers and breaks up conjunctions.
1.64 @@ -200,13 +221,12 @@
1.65 then th::ths (*no work to do, terminate*)
1.66 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
1.67 Const ("op &", _) => (*conjunction*)
1.68 - cnf_aux (th RS conjunct1,
1.69 - cnf_aux (th RS conjunct2, ths))
1.70 + cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
1.71 | Const ("All", _) => (*universal quantifier*)
1.72 cnf_aux (freeze_spec th, ths)
1.73 | Const ("Ex", _) =>
1.74 (*existential quantifier: Insert Skolem functions*)
1.75 - cnf_aux (tryres (th,skoths), ths)
1.76 + cnf_aux (apply_skolem_ths (th,skoths), ths)
1.77 | Const ("op |", _) => (*disjunction*)
1.78 let val tac =
1.79 (METAHYPS (resop cnf_nil) 1) THEN
1.80 @@ -224,9 +244,10 @@
1.81 but don't discharge assumptions.*)
1.82 fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
1.83
1.84 -fun make_cnf skoths th =
1.85 - filter (not o is_taut)
1.86 - (map (refl_clause o generalize) (cnf skoths (th, [])));
1.87 +fun make_cnf skoths th = cnf skoths (th, []);
1.88 +
1.89 +(*Generalization, removal of redundant equalities, removal of tautologies.*)
1.90 +fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
1.91
1.92
1.93 (**** Removal of duplicate literals ****)
1.94 @@ -303,13 +324,6 @@
1.95 has_bool_arg_const t orelse
1.96 has_meta_conn t);
1.97
1.98 -(*FIXME: replace this by the boolean-valued version above!*)
1.99 -fun check_is_fol_term t =
1.100 - if is_fol_term t then t else raise TERM("check_is_fol_term",[t]);
1.101 -
1.102 -fun check_is_fol th = (check_is_fol_term (prop_of th); th);
1.103 -
1.104 -
1.105 (*Create a meta-level Horn clause*)
1.106 fun make_horn crules th = make_horn crules (tryres(th,crules))
1.107 handle THM _ => th;
1.108 @@ -426,7 +440,6 @@
1.109 fun make_clauses ths =
1.110 (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
1.111
1.112 -
1.113 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
1.114 fun make_horns ths =
1.115 name_thms "Horn#"
1.116 @@ -461,7 +474,7 @@
1.117 EVERY1 [skolemize_prems_tac negs,
1.118 METAHYPS (cltac o make_clauses)]) 1,
1.119 expand_defs_tac]) i st
1.120 - handle TERM _ => no_tac st; (*probably from check_is_fol*)
1.121 + handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
1.122
1.123 (** Best-first search versions **)
1.124
1.125 @@ -531,7 +544,9 @@
1.126
1.127 (*Converting one clause*)
1.128 fun make_meta_clause th =
1.129 - negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
1.130 + if is_fol_term (prop_of th)
1.131 + then negated_asm_of_head (make_horn resolution_clause_rules th)
1.132 + else raise THM("make_meta_clause", 0, [th]);
1.133
1.134 fun make_meta_clauses ths =
1.135 name_thms "MClause#"