src/HOL/Tools/Meson/meson.ML
changeset 59165 115965966e15
parent 59164 ff40c53d1af9
child 59171 75ec7271b426
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sat Dec 20 22:23:37 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Dec 21 15:03:45 2014 +0100
     1.3 @@ -14,9 +14,7 @@
     1.4    val first_order_resolve : thm -> thm -> thm
     1.5    val size_of_subgoals: thm -> int
     1.6    val has_too_many_clauses: Proof.context -> term -> bool
     1.7 -  val make_cnf:
     1.8 -    thm list -> thm -> Proof.context
     1.9 -    -> Proof.context -> thm list * Proof.context
    1.10 +  val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
    1.11    val finish_cnf: thm list -> thm list
    1.12    val presimplified_consts : string list
    1.13    val presimplify: Proof.context -> thm -> thm
    1.14 @@ -194,7 +192,7 @@
    1.15              Display.string_of_thm ctxt st ::
    1.16              "Premises:" :: map (Display.string_of_thm ctxt) prems))
    1.17    in
    1.18 -    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS tacf) st) of
    1.19 +    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of
    1.20        SOME (th, _) => th
    1.21      | NONE => raise THM ("forward_res", 0, [st])
    1.22    end;
    1.23 @@ -285,10 +283,11 @@
    1.24  (*** Removal of duplicate literals ***)
    1.25  
    1.26  (*Forward proof, passing extra assumptions as theorems to the tactic*)
    1.27 -fun forward_res2 nf hyps st =
    1.28 +fun forward_res2 ctxt nf hyps st =
    1.29    case Seq.pull
    1.30          (REPEAT
    1.31 -         (Misc_Legacy.METAHYPS (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1)
    1.32 +         (Misc_Legacy.METAHYPS ctxt
    1.33 +           (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1)
    1.34           st)
    1.35    of SOME(th,_) => th
    1.36     | NONE => raise THM("forward_res2", 0, [st]);
    1.37 @@ -297,7 +296,7 @@
    1.38    rls (initially []) accumulates assumptions of the form P==>False*)
    1.39  fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc)
    1.40      handle THM _ => tryres(th,rls)
    1.41 -    handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2),
    1.42 +    handle THM _ => tryres(forward_res2 ctxt (nodups_aux ctxt) rls (th RS disj_forward2),
    1.43                             [disj_FalseD1, disj_FalseD2, asm_rl])
    1.44      handle THM _ => th;
    1.45  
    1.46 @@ -375,18 +374,18 @@
    1.47  (* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    1.48     Strips universal quantifiers and breaks up conjunctions.
    1.49     Eliminates existential quantifiers using Skolemization theorems. *)
    1.50 -fun cnf old_skolem_ths ctxt ctxt0 (th, ths) =
    1.51 -  let val ctxt0r = Unsynchronized.ref ctxt0   (* FIXME ??? *)
    1.52 +fun cnf old_skolem_ths ctxt (th, ths) =
    1.53 +  let val ctxt_ref = Unsynchronized.ref ctxt   (* FIXME ??? *)
    1.54        fun cnf_aux (th,ths) =
    1.55          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
    1.56          else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
    1.57 -        then nodups ctxt0 th :: ths (*no work to do, terminate*)
    1.58 +        then nodups ctxt th :: ths (*no work to do, terminate*)
    1.59          else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
    1.60              Const (@{const_name HOL.conj}, _) => (*conjunction*)
    1.61                  cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
    1.62            | Const (@{const_name All}, _) => (*universal quantifier*)
    1.63 -                let val (th',ctxt0') = freeze_spec th (!ctxt0r)
    1.64 -                in  ctxt0r := ctxt0'; cnf_aux (th', ths) end
    1.65 +                let val (th', ctxt') = freeze_spec th (! ctxt_ref)
    1.66 +                in  ctxt_ref := ctxt'; cnf_aux (th', ths) end
    1.67            | Const (@{const_name Ex}, _) =>
    1.68                (*existential quantifier: Insert Skolem functions*)
    1.69                cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
    1.70 @@ -394,20 +393,21 @@
    1.71                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    1.72                  all combinations of converting P, Q to CNF.*)
    1.73                let val tac =
    1.74 -                  Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
    1.75 -                   (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
    1.76 +                  Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1 THEN
    1.77 +                   (fn st' => st' |> Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1)
    1.78                in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    1.79 -          | _ => nodups ctxt0 th :: ths  (*no work to do*)
    1.80 -      and cnf_nil th = cnf_aux (th,[])
    1.81 +          | _ => nodups ctxt th :: ths  (*no work to do*)
    1.82 +      and cnf_nil th = cnf_aux (th, [])
    1.83        val cls =
    1.84          if has_too_many_clauses ctxt (concl_of th) then
    1.85            (trace_msg ctxt (fn () =>
    1.86 -               "cnf is ignoring: " ^ Display.string_of_thm ctxt0 th); ths)
    1.87 +               "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.88          else
    1.89            cnf_aux (th, ths)
    1.90 -  in (cls, !ctxt0r) end
    1.91 -fun make_cnf old_skolem_ths th ctxt ctxt0 =
    1.92 -  cnf old_skolem_ths ctxt ctxt0 (th, [])
    1.93 +  in (cls, !ctxt_ref) end
    1.94 +
    1.95 +fun make_cnf old_skolem_ths th ctxt =
    1.96 +  cnf old_skolem_ths ctxt (th, [])
    1.97  
    1.98  (*Generalization, removal of redundant equalities, removal of tautologies.*)
    1.99  fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
   1.100 @@ -670,9 +670,11 @@
   1.101    end
   1.102  
   1.103  fun add_clauses ctxt th cls =
   1.104 -  let val ctxt0 = Variable.global_thm_context th
   1.105 -      val (cnfs, ctxt) = make_cnf [] th ctxt ctxt0
   1.106 -  in Variable.export ctxt ctxt0 cnfs @ cls end;
   1.107 +  let
   1.108 +    val (cnfs, ctxt') = ctxt
   1.109 +      |> Variable.declare_thm th
   1.110 +      |> make_cnf [] th;
   1.111 +  in Variable.export ctxt' ctxt cnfs @ cls end;
   1.112  
   1.113  (*Sort clauses by number of literals*)
   1.114  fun fewerlits (th1, th2) = nliterals (prop_of th1) < nliterals (prop_of th2)