# HG changeset patch # User wenzelm # Date 1419170625 -3600 # Node ID 115965966e15c9acc3c5e594207562c9e95e629c # Parent ff40c53d1af99f25eb2687f86e6403ad7f595a4a proper context; diff -r ff40c53d1af9 -r 115965966e15 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Sat Dec 20 22:23:37 2014 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Sun Dec 21 15:03:45 2014 +0100 @@ -14,9 +14,7 @@ val first_order_resolve : thm -> thm -> thm val size_of_subgoals: thm -> int val has_too_many_clauses: Proof.context -> term -> bool - val make_cnf: - thm list -> thm -> Proof.context - -> Proof.context -> thm list * Proof.context + val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context val finish_cnf: thm list -> thm list val presimplified_consts : string list val presimplify: Proof.context -> thm -> thm @@ -194,7 +192,7 @@ Display.string_of_thm ctxt st :: "Premises:" :: map (Display.string_of_thm ctxt) prems)) in - case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS tacf) st) of + case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of SOME (th, _) => th | NONE => raise THM ("forward_res", 0, [st]) end; @@ -285,10 +283,11 @@ (*** Removal of duplicate literals ***) (*Forward proof, passing extra assumptions as theorems to the tactic*) -fun forward_res2 nf hyps st = +fun forward_res2 ctxt nf hyps st = case Seq.pull (REPEAT - (Misc_Legacy.METAHYPS (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1) + (Misc_Legacy.METAHYPS ctxt + (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1) st) of SOME(th,_) => th | NONE => raise THM("forward_res2", 0, [st]); @@ -297,7 +296,7 @@ rls (initially []) accumulates assumptions of the form P==>False*) fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc) handle THM _ => tryres(th,rls) - handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2), + handle THM _ => tryres(forward_res2 ctxt (nodups_aux ctxt) rls (th RS disj_forward2), [disj_FalseD1, disj_FalseD2, asm_rl]) handle THM _ => th; @@ -375,18 +374,18 @@ (* Conjunctive normal form, adding clauses from th in front of ths (for foldr). Strips universal quantifiers and breaks up conjunctions. Eliminates existential quantifiers using Skolemization theorems. *) -fun cnf old_skolem_ths ctxt ctxt0 (th, ths) = - let val ctxt0r = Unsynchronized.ref ctxt0 (* FIXME ??? *) +fun cnf old_skolem_ths ctxt (th, ths) = + let val ctxt_ref = Unsynchronized.ref ctxt (* FIXME ??? *) fun cnf_aux (th,ths) = if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th)) - then nodups ctxt0 th :: ths (*no work to do, terminate*) + then nodups ctxt th :: ths (*no work to do, terminate*) else case head_of (HOLogic.dest_Trueprop (concl_of th)) of Const (@{const_name HOL.conj}, _) => (*conjunction*) cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) | Const (@{const_name All}, _) => (*universal quantifier*) - let val (th',ctxt0') = freeze_spec th (!ctxt0r) - in ctxt0r := ctxt0'; cnf_aux (th', ths) end + let val (th', ctxt') = freeze_spec th (! ctxt_ref) + in ctxt_ref := ctxt'; cnf_aux (th', ths) end | Const (@{const_name Ex}, _) => (*existential quantifier: Insert Skolem functions*) cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) @@ -394,20 +393,21 @@ (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using all combinations of converting P, Q to CNF.*) let val tac = - Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN - (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1) + Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1 THEN + (fn st' => st' |> Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1) in Seq.list_of (tac (th RS disj_forward)) @ ths end - | _ => nodups ctxt0 th :: ths (*no work to do*) - and cnf_nil th = cnf_aux (th,[]) + | _ => nodups ctxt th :: ths (*no work to do*) + and cnf_nil th = cnf_aux (th, []) val cls = if has_too_many_clauses ctxt (concl_of th) then (trace_msg ctxt (fn () => - "cnf is ignoring: " ^ Display.string_of_thm ctxt0 th); ths) + "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) else cnf_aux (th, ths) - in (cls, !ctxt0r) end -fun make_cnf old_skolem_ths th ctxt ctxt0 = - cnf old_skolem_ths ctxt ctxt0 (th, []) + in (cls, !ctxt_ref) end + +fun make_cnf old_skolem_ths th ctxt = + cnf old_skolem_ths ctxt (th, []) (*Generalization, removal of redundant equalities, removal of tautologies.*) fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths); @@ -670,9 +670,11 @@ end fun add_clauses ctxt th cls = - let val ctxt0 = Variable.global_thm_context th - val (cnfs, ctxt) = make_cnf [] th ctxt ctxt0 - in Variable.export ctxt ctxt0 cnfs @ cls end; + let + val (cnfs, ctxt') = ctxt + |> Variable.declare_thm th + |> make_cnf [] th; + in Variable.export ctxt' ctxt cnfs @ cls end; (*Sort clauses by number of literals*) fun fewerlits (th1, th2) = nliterals (prop_of th1) < nliterals (prop_of th2) diff -r ff40c53d1af9 -r 115965966e15 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Dec 20 22:23:37 2014 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun Dec 21 15:03:45 2014 +0100 @@ -370,9 +370,10 @@ val (opt, (nnf_th, ctxt)) = nnf_axiom choice_ths new_skolem ax_no th ctxt0 fun clausify th = - make_cnf (if new_skolem orelse null choice_ths then [] - else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th)) - th ctxt ctxt + make_cnf + (if new_skolem orelse null choice_ths then [] + else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th)) + th ctxt val (cnf_ths, ctxt) = clausify nnf_th fun intr_imp ct th = Thm.instantiate ([], map (apply2 (cterm_of thy)) diff -r ff40c53d1af9 -r 115965966e15 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Sat Dec 20 22:23:37 2014 +0100 +++ b/src/Tools/misc_legacy.ML Sun Dec 21 15:03:45 2014 +0100 @@ -22,7 +22,7 @@ val term_frees: term -> term list val mk_defpair: term * term -> string * term val get_def: theory -> xstring -> thm - val METAHYPS: (thm list -> tactic) -> int -> tactic + val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) val freeze_thaw: thm -> thm * (thm -> thm) end; @@ -158,7 +158,7 @@ val (params,hyps,concl) = strip_context prem' in (insts,params,hyps,concl) end; -fun metahyps_aux_tac tacf (prem,gno) state = +fun metahyps_aux_tac ctxt tacf (prem,gno) state = let val (insts,params,hyps,concl) = metahyps_split_prem prem val maxidx = Thm.maxidx_of state val cterm = Thm.cterm_of (Thm.theory_of_thm state) @@ -204,15 +204,13 @@ end (*function to replace the current subgoal*) fun next st = - Thm.bicompose NONE {flatten = true, match = false, incremented = false} + Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} (false, relift st, nprems_of st) gno state in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end; -fun print_vars_terms n thm = +fun print_vars_terms ctxt n thm = let - val thy = theory_of_thm thm - fun typed s ty = - " " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty; + fun typed s ty = " " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty; fun find_vars (Const (c, ty)) = if null (Term.add_tvarsT ty []) then I else insert (op =) (typed c ty) @@ -228,8 +226,8 @@ in -fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm - handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty) +fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm + handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty) end;