proper context;
authorwenzelm
Sun Dec 21 15:03:45 2014 +0100 (2014-12-21)
changeset 59165115965966e15
parent 59164 ff40c53d1af9
child 59166 4e43651235b2
proper context;
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/Tools/misc_legacy.ML
     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)
     2.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Dec 20 22:23:37 2014 +0100
     2.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sun Dec 21 15:03:45 2014 +0100
     2.3 @@ -370,9 +370,10 @@
     2.4      val (opt, (nnf_th, ctxt)) =
     2.5        nnf_axiom choice_ths new_skolem ax_no th ctxt0
     2.6      fun clausify th =
     2.7 -      make_cnf (if new_skolem orelse null choice_ths then []
     2.8 -                else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th))
     2.9 -               th ctxt ctxt
    2.10 +      make_cnf
    2.11 +       (if new_skolem orelse null choice_ths then []
    2.12 +        else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th))
    2.13 +       th ctxt
    2.14      val (cnf_ths, ctxt) = clausify nnf_th
    2.15      fun intr_imp ct th =
    2.16        Thm.instantiate ([], map (apply2 (cterm_of thy))
     3.1 --- a/src/Tools/misc_legacy.ML	Sat Dec 20 22:23:37 2014 +0100
     3.2 +++ b/src/Tools/misc_legacy.ML	Sun Dec 21 15:03:45 2014 +0100
     3.3 @@ -22,7 +22,7 @@
     3.4    val term_frees: term -> term list
     3.5    val mk_defpair: term * term -> string * term
     3.6    val get_def: theory -> xstring -> thm
     3.7 -  val METAHYPS: (thm list -> tactic) -> int -> tactic
     3.8 +  val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic
     3.9    val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
    3.10    val freeze_thaw: thm -> thm * (thm -> thm)
    3.11  end;
    3.12 @@ -158,7 +158,7 @@
    3.13        val (params,hyps,concl) = strip_context prem'
    3.14    in (insts,params,hyps,concl)  end;
    3.15  
    3.16 -fun metahyps_aux_tac tacf (prem,gno) state =
    3.17 +fun metahyps_aux_tac ctxt tacf (prem,gno) state =
    3.18    let val (insts,params,hyps,concl) = metahyps_split_prem prem
    3.19        val maxidx = Thm.maxidx_of state
    3.20        val cterm = Thm.cterm_of (Thm.theory_of_thm state)
    3.21 @@ -204,15 +204,13 @@
    3.22          end
    3.23        (*function to replace the current subgoal*)
    3.24        fun next st =
    3.25 -        Thm.bicompose NONE {flatten = true, match = false, incremented = false}
    3.26 +        Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
    3.27            (false, relift st, nprems_of st) gno state
    3.28    in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
    3.29  
    3.30 -fun print_vars_terms n thm =
    3.31 +fun print_vars_terms ctxt n thm =
    3.32    let
    3.33 -    val thy = theory_of_thm thm
    3.34 -    fun typed s ty =
    3.35 -      "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
    3.36 +    fun typed s ty = "  " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty;
    3.37      fun find_vars (Const (c, ty)) =
    3.38            if null (Term.add_tvarsT ty []) then I
    3.39            else insert (op =) (typed c ty)
    3.40 @@ -228,8 +226,8 @@
    3.41  
    3.42  in
    3.43  
    3.44 -fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
    3.45 -  handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
    3.46 +fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm
    3.47 +  handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty)
    3.48  
    3.49  end;
    3.50