signature ARGO_TACTIC = sig val trace: string Config.T val timeout: real Config.T
(* extending the tactic *) type trans_context =
Name.context * Argo_Expr.typ Typtab.table * (string * Argo_Expr.typ) Termtab.table type ('a, 'b) trans = 'a -> trans_context -> 'b * trans_context type ('a, 'b) trans' = 'a -> trans_context -> ('b * trans_context) option type extension = {
trans_type: (typ, Argo_Expr.typ) trans -> (typ, Argo_Expr.typ) trans',
trans_term: (term, Argo_Expr.expr) trans -> (term, Argo_Expr.expr) trans',
term_of: (Argo_Expr.expr -> term) -> Argo_Expr.expr -> term option,
replay_rewr: Proof.context -> Argo_Proof.rewrite -> conv,
replay: (Argo_Expr.expr -> cterm) -> Proof.context -> Argo_Proof.rule -> thm list -> thm option} val add_extension: extension -> theory -> theory
(* proof utilities *) val discharges: thm -> thm list -> thm list val flatten_conv: conv -> thm -> conv
(* interface to the tactic as well as the underlying checker and prover *) datatype result = Satisfiable of term -> booloption | Unsatisfiable val check: term list -> Proof.context -> result * Proof.context val prove: thm list -> Proof.context -> thm option * Proof.context val argo_tac: Proof.context -> thm list -> int -> tactic end
structure Argo_Tactic: ARGO_TACTIC = struct
(* readable fresh names for terms *)
fun fresh_name n = Name.variant (case Long_Name.base_name n of"" => "x" | n' => n')
fun fresh_type_name (Type (n, _)) = fresh_name n
| fresh_type_name (TFree (n, _)) = fresh_name n
| fresh_type_name (TVar ((n, i), _)) = fresh_name (n ^ "." ^ string_of_int i)
fun string_of_mode None = "none"
| string_of_mode Basic = "basic"
| string_of_mode Full = "full"
fun requires_mode None = []
| requires_mode Basic = [Basic, Full]
| requires_mode Full = [Full]
val trace = Attrib.setup_config_string \<^binding>\<open>argo_trace\<close> (K (string_of_mode None))
fun allows_mode ctxt = exists (equal (Config.get ctxt trace) o string_of_mode) o requires_mode
fun output mode ctxt msg = if allows_mode ctxt mode then Output.tracing ("Argo: " ^ msg) else () val tracing = output Basic val full_tracing = output Full
fun with_mode mode ctxt f = if allows_mode ctxt mode then f ctxt else () val with_tracing = with_mode Basic val with_full_tracing = with_mode Full
(* timeout *)
val timeout = Attrib.setup_config_real \<^binding>\<open>argo_timeout\<close> (K 10.0)
val timeout_seconds = seconds o Config.apply timeout
fun with_timeout f ctxt = Timeout.apply (timeout_seconds ctxt) f ctxt
type ('a, 'b) trans = 'a -> trans_context -> 'b * trans_context type ('a, 'b) trans' = 'a -> trans_context -> ('b * trans_context) option
type extension = {
trans_type: (typ, Argo_Expr.typ) trans -> (typ, Argo_Expr.typ) trans',
trans_term: (term, Argo_Expr.expr) trans -> (term, Argo_Expr.expr) trans',
term_of: (Argo_Expr.expr -> term) -> Argo_Expr.expr -> term option,
replay_rewr: Proof.context -> Argo_Proof.rewrite -> conv,
replay: (Argo_Expr.expr -> cterm) -> Proof.context -> Argo_Proof.rule -> thm list -> thm option}
fun eq_extension ((serial1, _), (serial2, _)) = (serial1 = serial2)
structure Extensions = Theory_Data
( type T = (serial * extension) list val empty = [] val merge = merge eq_extension
)
fun add_extension ext = Extensions.map (insert eq_extension (serial (), ext)) fun get_extensions ctxt = Extensions.get (Proof_Context.theory_of ctxt) fun apply_first ctxt f = get_first (fn (_, e) => f e) (get_extensions ctxt)
fun ext_trans sel ctxt f x tcx = apply_first ctxt (fn ext => sel ext f x tcx)
val ext_trans_type = ext_trans (fn {trans_type, ...}: extension => trans_type) val ext_trans_term = ext_trans (fn {trans_term, ...}: extension => trans_term)
fun ext_term_of ctxt f e = apply_first ctxt (fn {term_of, ...}: extension => term_of f e)
fun ext_replay_rewr ctxt r =
get_extensions ctxt
|> map (fn (_, {replay_rewr, ...}: extension) => replay_rewr ctxt r)
|> Conv.first_conv
fun ext_replay cprop_of ctxt rule prems =
(case apply_first ctxt (fn {replay, ...}: extension => replay cprop_of ctxt rule prems) of
SOME thm => thm
| NONE => raise THM ("failed to replay " ^ quote (Argo_Proof.string_of_rule rule), 0, []))
(* translating input terms *)
fun add_new_type T (names, types, terms) = let val (n, names') = fresh_type_name T names val ty = Argo_Expr.Type n in (ty, (names', Typtab.update (T, ty) types, terms)) end
fun add_type T (tcx as (_, types, _)) =
(case Typtab.lookup types T of
SOME ty => (ty, tcx)
| NONE => add_new_type T tcx)
fun trans_type _ \<^Type>\<open>bool\<close> = pair Argo_Expr.Bool
| trans_type ctxt \<^Type>\<open>fun T1 T2\<close> =
trans_type ctxt T1 ##>> trans_type ctxt T2 #>> Argo_Expr.Func
| trans_type ctxt T = (fn tcx =>
(case ext_trans_type ctxt (trans_type ctxt) T tcx of
SOME result => result
| NONE => add_type T tcx))
fun add_new_term ctxt t T tcx = let val (ty, (names, types, terms)) = trans_type ctxt T tcx val (n, names') = fresh_term_name t names val c = (n, ty) in (Argo_Expr.mk_con c, (names', types, Termtab.update (t, c) terms)) end
fun add_term ctxt t (tcx as (_, _, terms)) =
(case Termtab.lookup terms t of
SOME c => (Argo_Expr.mk_con c, tcx)
| NONE => add_new_term ctxt t (Term.fastype_of t) tcx)
fun mk_eq \<^Type>\<open>bool\<close> = Argo_Expr.mk_iff
| mk_eq _ = Argo_Expr.mk_eq
fun trans_term _ \<^Const_>\<open>True\<close> = pair Argo_Expr.true_expr
| trans_term _ \<^Const_>\<open>False\<close> = pair Argo_Expr.false_expr
| trans_term ctxt \<^Const_>\<open>Not for t\<close> = trans_term ctxt t #>> Argo_Expr.mk_not
| trans_term ctxt \<^Const_>\<open>conj for t1 t2\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_and2
| trans_term ctxt \<^Const_>\<open>disj for t1 t2\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_or2
| trans_term ctxt \<^Const_>\<open>implies for t1 t2\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_imp
| trans_term ctxt \<^Const_>\<open>If _ for t1 t2 t3\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 ##>> trans_term ctxt t3 #>>
(fn ((u1, u2), u3) => Argo_Expr.mk_ite u1 u2 u3)
| trans_term ctxt \<^Const_>\<open>HOL.eq T for t1 t2\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq T)
| trans_term ctxt (t as (t1 $ t2)) = (fn tcx =>
(case ext_trans_term ctxt (trans_term ctxt) t tcx of
SOME result => result
| NONE => tcx |> trans_term ctxt t1 ||>> trans_term ctxt t2 |>> uncurry Argo_Expr.mk_app))
| trans_term ctxt t = (fn tcx =>
(case ext_trans_term ctxt (trans_term ctxt) t tcx of
SOME result => result
| NONE => add_term ctxt t tcx))
fun translate ctxt prop = trans_term ctxt (HOLogic.dest_Trueprop prop)
(* invoking the solver *)
type data = {
names: Name.context,
types: Argo_Expr.typ Typtab.table,
terms: (string * Argo_Expr.typ) Termtab.table,
argo: Argo_Solver.context}
fun mk_data names types terms argo: data = {names=names, types=types, terms=terms, argo=argo} val empty_data = mk_data Name.context Typtab.empty Termtab.empty Argo_Solver.context
structure Solver_Data = Proof_Data
( type T = data option fun init _ = SOME empty_data
)
datatype ('m, 'p) solver_result = Model of'm | Proof of 'p
fun raw_solve es argo = Model (Argo_Solver.assert es argo) handle Argo_Proof.UNSAT proof => Proof proof
fun value_of terms model t =
(case Termtab.lookup terms t of
SOME c => model c
| _ => NONE)
fun trace_props props ctxt =
tracing ctxt (Pretty.string_of (Pretty.big_list "using these propositions:"
(map (Pretty.item o single o Syntax.pretty_term ctxt) props)))
fun trace_result ctxt ({elapsed, ...}: Timing.timing) msg =
tracing ctxt ("found a " ^ msg ^ " in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")
fun solve props ctxt =
(case Solver_Data.get ctxt of
NONE => error "bad Argo solver context"
| SOME {names, types, terms, argo} => let val _ = with_tracing ctxt (trace_props props) val (es, (names', types', terms')) = fold_map (translate ctxt) props (names, types, terms) val _ = tracing ctxt "starting the prover" in
(case Timing.timing (raw_solve es) argo of
(time, Proof proof) => letval _ = trace_result ctxt time "proof" in (Proof (terms', proof), Solver_Data.put NONE ctxt) end
| (time, Model argo') => let val _ = trace_result ctxt time "model" val model = value_of terms' (Argo_Solver.model_of argo') in (Model model, Solver_Data.put (SOME (mk_data names' types' terms' argo')) ctxt) end) end)
fun with_frees ctxt n mk = let val ns = map (fn i => "P" ^ string_of_int i) (0 upto (n - 1)) val ts = map (Free o rpair \<^Type>\<open>bool\<close>) ns val t = mk_nary HOLogic.mk_disj (mk ts) in prove_taut ctxt ns t end
fun taut_and1_term ts = mk_nary HOLogic.mk_conj ts :: map HOLogic.mk_not ts fun taut_and2_term i ts = [HOLogic.mk_not (mk_nary HOLogic.mk_conj ts), nth ts i] fun taut_or1_term i ts = [mk_nary HOLogic.mk_disj ts, HOLogic.mk_not (nth ts i)] fun taut_or2_term ts = HOLogic.mk_not (mk_nary HOLogic.mk_disj ts) :: ts
val iff_1_taut = @{lemma "P = Q \ P \ Q" by fast} val iff_2_taut = @{lemma "P = Q \ (\P) \ (\Q)" by fast} val iff_3_taut = @{lemma "\(P = Q) \ (\P) \ Q" by fast} val iff_4_taut = @{lemma "\(P = Q) \ P \ (\Q)" by fast} val ite_then_taut = @{lemma "\P \ (if P then t else u) = t" by auto} val ite_else_taut = @{lemma "P \ (if P then t else u) = u" by auto}
fun pick_dual rule (i1, i2) thms =
rule OF [nth thms i1, nth thms i2] handle THM _ => rule OF [nth thms i2, nth thms i1] val pick_dual_conj = pick_dual @{lemma "\P \ P \ False" by auto} val pick_dual_ndis = pick_dual @{lemma "\P \ P \ \True" by auto}
fun join thm0 rule is thms = let val l = length thms val thms' = fold (fn i => cons (if 0 <= i andalso i < l then nth thms i else thm0)) is [] in fold (fn thm => fn thm' => discharge2 thm thm' rule) (tl thms') (hd thms') end
val join_conj = join @{lemma "True" by auto} @{lemma "P \ Q \ P \ Q" by auto} val join_ndis = join @{lemma "\False" by auto} @{lemma "\P \ \Q \ \(P \ Q)" by auto}
val false_thm = @{lemma "False \ P" by auto} val ntrue_thm = @{lemma "\True \ P" by auto} val iff_conj_thm = @{lemma "(P \ Q) \ (Q \ P) \ P = Q" by auto} val iff_ndis_thm = @{lemma "(\P \ \Q) \ (\Q \ \P) \ P = Q" by auto}
fun iff_intro rule lf rf ct = let val lhs = under_assumption lf ct val rhs = rf (Thm.dest_arg (snd (Thm.dest_implies (Thm.cprop_of lhs)))) in mk_rewr (discharge2 lhs rhs rule) end
fun with_conj f g ct = iff_intro iff_conj_thm (f o explode_conj) g ct fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply \<^cterm>\<open>Not\<close> ct)
fun swap_indices n iss = map (fn i => find_index (fn is => member (op =) is i) iss) (0 upto (n - 1)) fun sort_nary w f g (n, iss) = w (f (map hd iss)) (under_assumption (f (swap_indices n iss) o g)) val sort_conj = sort_nary with_conj join_conj explode_conj val sort_ndis = sort_nary with_ndis join_ndis explode_ndis
val not_true_thm = mk_rewr @{lemma "(\True) = False" by auto} val not_false_thm = mk_rewr @{lemma "(\False) = True" by auto} val not_not_thm = mk_rewr @{lemma "(\\P) = P" by auto} val not_and_thm = mk_rewr @{lemma "(\(P \ Q)) = (\P \ \Q)" by auto} val not_or_thm = mk_rewr @{lemma "(\(P \ Q)) = (\P \ \Q)" by auto} val not_iff_thms = map mk_rewr
@{lemma "(\((\P) = Q)) = (P = Q)""(\(P = (\Q))) = (P = Q)""(\(P = Q)) = ((\P) = Q)" by auto} val iff_true_thms = map mk_rewr @{lemma "(True = P) = P""(P = True) = P" by auto} val iff_false_thms = map mk_rewr @{lemma "(False = P) = (\P)""(P = False) = (\P)" by auto} val iff_not_not_thm = mk_rewr @{lemma "((\P) = (\Q)) = (P = Q)" by auto} val iff_refl_thm = mk_rewr @{lemma "(P = P) = True" by auto} val iff_symm_thm = mk_rewr @{lemma "(P = Q) = (Q = P)" by auto} val iff_dual_thms = map mk_rewr @{lemma "(P = (\P)) = False""((\P) = P) = False" by auto} val imp_thm = mk_rewr @{lemma "(P \ Q) = (\P \ Q)" by auto} val ite_prop_thm = mk_rewr @{lemma "(If P Q R) = ((\P \ Q) \ (P \ R) \ (Q \ R))" by auto} val ite_true_thm = mk_rewr @{lemma "(If True t u) = t" by auto} val ite_false_thm = mk_rewr @{lemma "(If False t u) = u" by auto} val ite_eq_thm = mk_rewr @{lemma "(If P t t) = t" by auto} val eq_refl_thm = mk_rewr @{lemma "(t = t) = True" by auto} val eq_symm_thm = mk_rewr @{lemma "(t1 = t2) = (t2 = t1)" by auto}
fun replay_with_lits [] thm lits = (thm, lits)
| replay_with_lits is thm lits =
extract_lits is (discharge thm prep_clause_rule, lits)
||> Ord_List.make lit_ord
fun replay_clause is thm = replay_with_lits is thm []
(* proof replay for unit resolution *)
val bogus_ct = \<^cterm>\<open>True\<close>
fun replay_unit_res lit (pthm, plits) (nthm, nlits) = let val plit = the (AList.lookup (op =) plits lit) val nlit = the (AList.lookup (op =) nlits (~lit)) val prune = Ord_List.remove lit_ord (lit, bogus_ct) in
\<^instantiate>\<open>P = \<open>Thm.dest_arg plit\<close> in
lemma "(P \ False) \ (\P \ False) \ False" by fast\<close>
|> Thm.elim_implies (Thm.implies_intr plit pthm)
|> Thm.elim_implies (Thm.implies_intr nlit nthm)
|> rpair (Ord_List.union lit_ord (prune nlits) (prune plits)) end
(* proof replay for hypothesis *)
val dneg_rule = @{lemma "\\P \ P" by auto}
fun replay_hyp i ct = if i < 0 then (Thm.assume ct, [(~i, ct)]) else letval cu = HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct))) in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
(* proof replay for lemma *)
fun replay_lemma is (thm, lits) = replay_with_lits is thm lits
(* proof replay for reflexivity *)
fun replay_refl x =
\<^instantiate>\<open>'a = \Thm.ctyp_of_cterm x\ and x in lemma \x = x\ by (rule refl)\
(* proof replay for symmetry *)
val symm_rules = @{lemma "a = b ==> b = a""\(a = b) \ \(b = a)" by simp_all}
fun replay_symm thm = hd (discharges thm symm_rules)
(* proof replay for transitivity *)
val trans_rules = @{lemma "\(a = b) \ b = c \ \(a = c)" "a = b \ \(b = c) \ \(a = c)" "a = b \ b = c ==> a = c"
by simp_all}
fun replay_trans thm1 thm2 = hd (discharges thm2 (discharges thm1 trans_rules))
val unclausify_rule1 = @{lemma "(\P \ False) \ P" by auto} val unclausify_rule2 = @{lemma "(P \ False) \ \P" by auto}
fun unclausify (thm, lits) ls =
(case (Thm.prop_of thm, lits) of
(\<^Const_>\<open>Trueprop for \<^Const_>\<open>False\<close>\<close>, [(_, ct)]) => letval thm = Thm.implies_intr ct thm in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
| _ => (thm, Ord_List.union lit_ord lits ls))
fun with_thms f tps = fold_map unclausify tps [] |>> f
fun bad_premises () = raise Fail "bad number of premises" fun with_thms1 f = with_thms (fn [thm] => f thm | _ => bad_premises ()) fun with_thms2 f = with_thms (fn [thm1, thm2] => f thm1 thm2 | _ => bad_premises ()) fun with_thms3 f = with_thms (fn [thm1, thm2, thm3] => f thm1 thm2 thm3 | _ => bad_premises ())
fun replay_rule (ctxt, cons, facts) prems rule =
(case rule of
Argo_Proof.Axiom i => (nth facts i, [])
| Argo_Proof.Taut (k, concl) => (replay_taut ctxt k (cprop_of ctxt cons concl), [])
| Argo_Proof.Conjunct (i, n) => with_thms1 (replay_conjunct i n) prems
| Argo_Proof.Rewrite c => with_thms1 (replay_rewrite ctxt c) prems
| Argo_Proof.Clause is => replay_clause is (fst (hd prems))
| Argo_Proof.Unit_Res i => replay_unit_res i (hd prems) (hd (tl prems))
| Argo_Proof.Hyp (i, concl) => replay_hyp i (cprop_of ctxt cons concl)
| Argo_Proof.Lemma is => replay_lemma is (hd prems)
| Argo_Proof.Refl concl => (replay_refl (cterm_of ctxt cons concl), [])
| Argo_Proof.Symm => with_thms1 replay_symm prems
| Argo_Proof.Trans => with_thms2 replay_trans prems
| Argo_Proof.Cong => with_thms2 replay_cong prems
| Argo_Proof.Subst => with_thms3 replay_subst prems
| _ => with_thms (ext_replay (cprop_of ctxt cons) ctxt rule) prems)
fun with_cache f proof thm_cache =
(case Thm_Cache.lookup thm_cache (Argo_Proof.id_of proof) of
SOME thm => (thm, thm_cache)
| NONE => letval (thm, thm_cache') = f proof thm_cache in (thm, Thm_Cache.update (Argo_Proof.id_of proof, thm) thm_cache') end)
fun trace_step ctxt proof_id rule proofs = with_full_tracing ctxt (fn ctxt' => let val id = Argo_Proof.string_of_proof_id proof_id val ids = map (Argo_Proof.string_of_proof_id o Argo_Proof.id_of) proofs val rule_string = Argo_Proof.string_of_rule rule in full_tracing ctxt' (" " ^ id ^ " <- " ^ implode_space ids ^ " . " ^ rule_string) end)
fun replay_bottom_up (env as (ctxt, _, _)) proof thm_cache = let val (proof_id, rule, proofs) = Argo_Proof.dest proof val (prems, thm_cache) = fold_map (with_cache (replay_bottom_up env)) proofs thm_cache val _ = trace_step ctxt proof_id rule proofs in (replay_rule env prems rule, thm_cache) end
fun replay_proof env proof = with_cache (replay_bottom_up env) proof Thm_Cache.empty
fun replay ctxt terms facts proof = let val env = (ctxt, Termtab.fold (Contab.update o swap) terms Contab.empty, facts) val _ = tracing ctxt "replaying the proof" val ({elapsed=t, ...}, ((thm, _), _)) = Timing.timing (replay_proof env) proof val _ = tracing ctxt ("replayed the proof in " ^ string_of_int (Time.toMilliseconds t) ^ " ms") in thm end
(* normalizing goals *)
fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make1 (v, ct))
fun instantiate_elim_rule thm = let val ct = Drule.strip_imp_concl (Thm.cprop_of thm) in
(case Thm.term_of ct of
\<^Const_>\<open>Trueprop for \<open>Var (v as (_, \<^Type>\<open>bool\<close>))\<close>\<close> => instantiate v \<^cterm>\<open>False\<close> thm
| Var v => instantiate v \<^cprop>\<open>False\<close> thm
| _ => thm) end
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
\<^Const_>\<open>Trueprop for _\<close> => Conv.all_conv
| \<^Const_>\<open>Pure.imp for _ _\<close> =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_imp}
| \<^Const>\<open>Pure.eq _ for _ _\<close> =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_eq}
| \<^Const>\<open>Pure.all _ for \<open>Abs _\<close>\<close> =>
Conv.binder_conv (atomize_conv o snd) ctxt then_conv
Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.18Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
