1.1 --- a/NEWS Thu Sep 18 14:06:58 2008 +0200
1.2 +++ b/NEWS Thu Sep 18 19:39:44 2008 +0200
1.3 @@ -22,6 +22,13 @@
1.4
1.5 *** Pure ***
1.6
1.7 +* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
1.8 +to 'a -> thm, at the cost of internal tagging of results with an
1.9 +authentic oracle name. The Isar command 'oracle' is now polymorphic,
1.10 +no argument type is specified. INCOMPATIBILITY, need to simplify
1.11 +existing oracle code accordingly. Note that extra performance may be
1.12 +gained by producing the cterm carefully, not via Thm.cterm_of.
1.13 +
1.14 * Changed defaults for unify configuration options:
1.15
1.16 unify_trace_bound = 50 (formerly 25)
2.1 --- a/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 18 14:06:58 2008 +0200
2.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 18 19:39:44 2008 +0200
2.3 @@ -595,12 +595,12 @@
2.4 @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
2.5 @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
2.6 @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
2.7 - @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
2.8 + @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
2.9 + -> (string * ('a -> thm)) * theory"} \\
2.10 \end{mldecls}
2.11 \begin{mldecls}
2.12 @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
2.13 @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
2.14 - @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
2.15 @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
2.16 \end{mldecls}
2.17
2.18 @@ -651,16 +651,13 @@
2.19 \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
2.20 axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
2.21
2.22 - \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a
2.23 - named oracle function, cf.\ @{text "axiom"} in
2.24 - \figref{fig:prim-rules}.
2.25 + \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
2.26 + oracle rule, essentially generating arbitrary axioms on the fly,
2.27 + cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
2.28
2.29 \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
2.30 arbitrary propositions as axioms.
2.31
2.32 - \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
2.33 - function for generating arbitrary axioms on the fly.
2.34 -
2.35 \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
2.36 \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
2.37 for constant @{text "c\<^isub>\<tau>"}, relative to existing
3.1 --- a/doc-src/IsarRef/Thy/Spec.thy Thu Sep 18 14:06:58 2008 +0200
3.2 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Sep 18 19:39:44 2008 +0200
3.3 @@ -1136,9 +1136,8 @@
3.4 @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
3.5 \end{matharray}
3.6
3.7 - The oracle interface promotes a given ML function @{ML_text
3.8 - "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some
3.9 - type @{ML_text T} given by the user. This acts like an infinitary
3.10 + The oracle interface promotes a given ML function @{ML_text "'a -> cterm"}
3.11 + to @{ML_text "'a -> thm"}. This acts like an infinitary
3.12 specification of axioms -- there is no internal check of the
3.13 correctness of the results! The inference kernel records oracle
3.14 invocations within the internal derivation object of theorems, and
3.15 @@ -1146,18 +1145,16 @@
3.16 that are not fully checked by Isabelle inferences.
3.17
3.18 \begin{rail}
3.19 - 'oracle' name '(' type ')' '=' text
3.20 + 'oracle' name '=' text
3.21 ;
3.22 \end{rail}
3.23
3.24 \begin{descr}
3.25
3.26 - \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
3.27 - given ML expression @{text "text"} of type
3.28 - @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an
3.29 - ML function of type
3.30 - @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is
3.31 - bound to the global identifier @{ML_text name}.
3.32 + \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
3.33 + expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
3.34 + ML function of type @{ML_text "'a -> thm"}, which is bound to the
3.35 + global identifier @{ML_text name}.
3.36
3.37 \end{descr}
3.38 *}
4.1 --- a/src/FOL/ex/IffOracle.thy Thu Sep 18 14:06:58 2008 +0200
4.2 +++ b/src/FOL/ex/IffOracle.thy Thu Sep 18 19:39:44 2008 +0200
4.3 @@ -18,14 +18,14 @@
4.4 and positive.
4.5 *}
4.6
4.7 -oracle iff_oracle (int) = {*
4.8 +oracle iff_oracle = {*
4.9 let
4.10 fun mk_iff 1 = Var (("P", 0), @{typ o})
4.11 | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
4.12 in
4.13 - fn thy => fn n =>
4.14 + fn (thy, n) =>
4.15 if n > 0 andalso n mod 2 = 0
4.16 - then FOLogic.mk_Trueprop (mk_iff n)
4.17 + then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
4.18 else raise Fail ("iff_oracle: " ^ string_of_int n)
4.19 end
4.20 *}
4.21 @@ -33,19 +33,19 @@
4.22
4.23 subsection {* Oracle as low-level rule *}
4.24
4.25 -ML {* iff_oracle @{theory} 2 *}
4.26 -ML {* iff_oracle @{theory} 10 *}
4.27 -ML {* #der (Thm.rep_thm (iff_oracle @{theory} 10)) *}
4.28 +ML {* iff_oracle (@{theory}, 2) *}
4.29 +ML {* iff_oracle (@{theory}, 10) *}
4.30 +ML {* #der (Thm.rep_thm (iff_oracle (@{theory}, 10))) *}
4.31
4.32 text {* These oracle calls had better fail. *}
4.33
4.34 ML {*
4.35 - (iff_oracle @{theory} 5; error "?")
4.36 + (iff_oracle (@{theory}, 5); error "?")
4.37 handle Fail _ => warning "Oracle failed, as expected"
4.38 *}
4.39
4.40 ML {*
4.41 - (iff_oracle @{theory} 1; error "?")
4.42 + (iff_oracle (@{theory}, 1); error "?")
4.43 handle Fail _ => warning "Oracle failed, as expected"
4.44 *}
4.45
4.46 @@ -55,7 +55,7 @@
4.47 method_setup iff = {*
4.48 Method.simple_args OuterParse.nat (fn n => fn ctxt =>
4.49 Method.SIMPLE_METHOD
4.50 - (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
4.51 + (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
4.52 handle Fail _ => no_tac))
4.53 *} "iff oracle"
4.54
5.1 --- a/src/HOL/ATP_Linkup.thy Thu Sep 18 14:06:58 2008 +0200
5.2 +++ b/src/HOL/ATP_Linkup.thy Thu Sep 18 19:39:44 2008 +0200
5.3 @@ -101,9 +101,9 @@
5.4
5.5 use "Tools/res_atp_provers.ML"
5.6
5.7 -oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
5.8 -oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
5.9 -oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
5.10 +oracle vampire_oracle = {* ResAtpProvers.vampire_o *}
5.11 +oracle eprover_oracle = {* ResAtpProvers.eprover_o *}
5.12 +oracle spass_oracle = {* ResAtpProvers.spass_o *}
5.13
5.14 use "Tools/res_atp_methods.ML"
5.15 setup ResAtpMethods.setup --{*Oracle ATP methods: still useful?*}
6.1 --- a/src/HOL/Code_Setup.thy Thu Sep 18 14:06:58 2008 +0200
6.2 +++ b/src/HOL/Code_Setup.thy Thu Sep 18 19:39:44 2008 +0200
6.3 @@ -129,17 +129,22 @@
6.4 end;
6.5 *}
6.6
6.7 -oracle eval_oracle ("term") = {* fn thy => fn t =>
6.8 - if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
6.9 - (HOLogic.dest_Trueprop t) []
6.10 - then t
6.11 - else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
6.12 +oracle eval_oracle = {* fn ct =>
6.13 + let
6.14 + val thy = Thm.theory_of_cterm ct;
6.15 + val t = Thm.term_of ct;
6.16 + in
6.17 + if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
6.18 + (HOLogic.dest_Trueprop t) []
6.19 + then ct
6.20 + else @{cprop True} (*dummy*)
6.21 + end
6.22 *}
6.23
6.24 method_setup eval = {*
6.25 let
6.26 fun eval_tac thy =
6.27 - SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
6.28 + CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
6.29 in
6.30 Method.ctxt_args (fn ctxt =>
6.31 Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
7.1 --- a/src/HOL/Complex/ex/MIR.thy Thu Sep 18 14:06:58 2008 +0200
7.2 +++ b/src/HOL/Complex/ex/MIR.thy Thu Sep 18 19:39:44 2008 +0200
7.3 @@ -5791,7 +5791,7 @@
7.4 (*export_code mircfrqe mirlfrqe
7.5 in SML module_name Mir file "raw_mir.ML"*)
7.6
7.7 -oracle mirfr_oracle ("bool * term") = {*
7.8 +oracle mirfr_oracle = {* fn (proofs, ct) =>
7.9 let
7.10
7.11 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
7.12 @@ -5891,13 +5891,15 @@
7.13 | term_of_fm vs (@{code Iff} (t1, t2)) =
7.14 @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm vs t1 $ term_of_fm vs t2;
7.15
7.16 -in fn thy => fn (proofs, t) =>
7.17 +in
7.18 let
7.19 + val thy = Thm.theory_of_cterm ct;
7.20 + val t = Thm.term_of ct;
7.21 val fs = term_frees t;
7.22 val vs = fs ~~ (0 upto (length fs - 1));
7.23 val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
7.24 val t' = (term_of_fm vs o qe o fm_of_term vs) t;
7.25 - in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
7.26 + in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
7.27 end;
7.28 *}
7.29
8.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Sep 18 14:06:58 2008 +0200
8.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Sep 18 19:39:44 2008 +0200
8.3 @@ -1997,7 +1997,7 @@
8.4
8.5 ML {* @{code ferrack_test} () *}
8.6
8.7 -oracle linr_oracle ("term") = {*
8.8 +oracle linr_oracle = {*
8.9 let
8.10
8.11 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
8.12 @@ -2066,11 +2066,14 @@
8.13 term_of_fm vs t1 $ term_of_fm vs t2
8.14 | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
8.15
8.16 -in fn thy => fn t =>
8.17 +in fn ct =>
8.18 let
8.19 + val thy = Thm.theory_of_cterm ct;
8.20 + val t = Thm.term_of ct;
8.21 val fs = term_frees t;
8.22 val vs = fs ~~ (0 upto (length fs - 1));
8.23 - in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))) end
8.24 + val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
8.25 + in Thm.cterm_of thy res end
8.26 end;
8.27 *}
8.28
9.1 --- a/src/HOL/Complex/ex/linrtac.ML Thu Sep 18 14:06:58 2008 +0200
9.2 +++ b/src/HOL/Complex/ex/linrtac.ML Thu Sep 18 19:39:44 2008 +0200
9.3 @@ -86,7 +86,7 @@
9.4 (* The result of the quantifier elimination *)
9.5 val (th, tac) = case (prop_of pre_thm) of
9.6 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
9.7 - let val pth = linr_oracle thy (Pattern.eta_long [] t1)
9.8 + let val pth = linr_oracle (cterm_of thy (Pattern.eta_long [] t1))
9.9 in
9.10 (trace_msg ("calling procedure with term:\n" ^
9.11 Syntax.string_of_term ctxt t1);
10.1 --- a/src/HOL/Complex/ex/mirtac.ML Thu Sep 18 14:06:58 2008 +0200
10.2 +++ b/src/HOL/Complex/ex/mirtac.ML Thu Sep 18 19:39:44 2008 +0200
10.3 @@ -87,9 +87,9 @@
10.4
10.5 fun mir_tac ctxt q i =
10.6 (ObjectLogic.atomize_prems_tac i)
10.7 - THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
10.8 - THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
10.9 - THEN (fn st =>
10.10 + THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
10.11 + THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
10.12 + THEN (fn st =>
10.13 let
10.14 val g = List.nth (prems_of st, i - 1)
10.15 val thy = ProofContext.theory_of ctxt
10.16 @@ -97,13 +97,13 @@
10.17 val (t,np,nh) = prepare_for_mir thy q g
10.18 (* Some simpsets for dealing with mod div abs and nat*)
10.19 val mod_div_simpset = HOL_basic_ss
10.20 - addsimps [refl,nat_mod_add_eq,
10.21 - @{thm "mod_self"}, @{thm "zmod_self"},
10.22 - @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
10.23 - @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
10.24 - @{thm "Suc_plus1"}]
10.25 - addsimps @{thms add_ac}
10.26 - addsimprocs [cancel_div_mod_proc]
10.27 + addsimps [refl,nat_mod_add_eq,
10.28 + @{thm "mod_self"}, @{thm "zmod_self"},
10.29 + @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
10.30 + @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
10.31 + @{thm "Suc_plus1"}]
10.32 + addsimps @{thms add_ac}
10.33 + addsimprocs [cancel_div_mod_proc]
10.34 val simpset0 = HOL_basic_ss
10.35 addsimps [mod_div_equality', Suc_plus1]
10.36 addsimps comp_ths
10.37 @@ -131,11 +131,11 @@
10.38 (* The result of the quantifier elimination *)
10.39 val (th, tac) = case (prop_of pre_thm) of
10.40 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
10.41 - let val pth =
10.42 + let val pth =
10.43 (* If quick_and_dirty then run without proof generation as oracle*)
10.44 - if !quick_and_dirty
10.45 - then mirfr_oracle thy (false, Pattern.eta_long [] t1)
10.46 - else mirfr_oracle thy (true, Pattern.eta_long [] t1)
10.47 + if !quick_and_dirty
10.48 + then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
10.49 + else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
10.50 in
10.51 (trace_msg ("calling procedure with term:\n" ^
10.52 Syntax.string_of_term ctxt t1);
11.1 --- a/src/HOL/Library/Eval_Witness.thy Thu Sep 18 14:06:58 2008 +0200
11.2 +++ b/src/HOL/Library/Eval_Witness.thy Thu Sep 18 19:39:44 2008 +0200
11.3 @@ -55,8 +55,10 @@
11.4 end;
11.5 *}
11.6
11.7 -oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) =>
11.8 +oracle eval_witness_oracle = {* fn (cgoal, ws) =>
11.9 let
11.10 + val thy = Thm.theory_of_cterm cgoal;
11.11 + val goal = Thm.term_of cgoal;
11.12 fun check_type T =
11.13 if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
11.14 then T
11.15 @@ -69,8 +71,8 @@
11.16 val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
11.17 in
11.18 if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
11.19 - then goal
11.20 - else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
11.21 + then Thm.cterm_of thy goal
11.22 + else @{cprop True} (*dummy*)
11.23 end
11.24 *}
11.25
11.26 @@ -78,12 +80,11 @@
11.27 method_setup eval_witness = {*
11.28 let
11.29
11.30 -fun eval_tac ws thy =
11.31 - SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i)
11.32 +fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
11.33
11.34 -in
11.35 - Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt =>
11.36 - Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt)))
11.37 +in
11.38 + Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
11.39 + Method.SIMPLE_METHOD' (eval_tac ws))
11.40 end
11.41 *} "Evaluation with ML witnesses"
11.42
12.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy Thu Sep 18 14:06:58 2008 +0200
12.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy Thu Sep 18 19:39:44 2008 +0200
12.3 @@ -30,7 +30,7 @@
12.4 val trace_eindhoven = ref false;
12.5 *}
12.6
12.7 -oracle mc_eindhoven_oracle ("term") =
12.8 +oracle mc_eindhoven_oracle =
12.9 {*
12.10 let
12.11 val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
12.12 @@ -43,15 +43,17 @@
12.13 else eindhoven_home ^ "/pmu";
12.14 in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
12.15 in
12.16 - fn thy => fn goal =>
12.17 + fn cgoal =>
12.18 let
12.19 + val thy = Thm.theory_of_cterm cgoal;
12.20 + val goal = Thm.term_of cgoal;
12.21 val s = eindhoven_term thy goal;
12.22 val debug = tracing ("MC debugger: " ^ s);
12.23 val result = call_mc s;
12.24 in
12.25 if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
12.26 (case result of
12.27 - "TRUE\n" => goal |
12.28 + "TRUE\n" => cgoal |
12.29 "FALSE\n" => error "MC oracle yields FALSE" |
12.30 _ => error ("MC syntax error: " ^ result))
12.31 end
12.32 @@ -62,7 +64,7 @@
12.33 fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
12.34 let
12.35 val thy = Thm.theory_of_thm state;
12.36 - val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
12.37 + val assertion = mc_eindhoven_oracle (Thm.cterm_of thy (Logic.strip_imp_concl goal));
12.38 in cut_facts_tac [assertion] i THEN atac i end) i state;
12.39
12.40 val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
13.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy Thu Sep 18 14:06:58 2008 +0200
13.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Thu Sep 18 19:39:44 2008 +0200
13.3 @@ -68,8 +68,7 @@
13.4 will be replaced by the expression between the two asterisks
13.5 following "case" and the asterisk after esac will be deleted *)
13.6
13.7 -oracle mc_mucke_oracle ("term") =
13.8 - mk_mc_mucke_oracle
13.9 +oracle mc_mucke_oracle = mk_mc_mucke_oracle
13.10
13.11 ML {*
13.12 (* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
13.13 @@ -154,12 +153,9 @@
13.14 end;
13.15
13.16
13.17 -fun call_mucke_tac i state =
13.18 -let val thy = Thm.theory_of_thm state;
13.19 - val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
13.20 -in
13.21 -(cut_facts_tac [OraAss] i) state
13.22 -end;
13.23 +val call_mucke_tac = CSUBGOAL (fn (cgoal, i) =>
13.24 +let val OraAss = mc_mucke_oracle cgoal
13.25 +in cut_facts_tac [OraAss] i end);
13.26
13.27
13.28 (* transforming fun-defs into lambda-defs *)
14.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML Thu Sep 18 14:06:58 2008 +0200
14.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Sep 18 19:39:44 2008 +0200
14.3 @@ -1012,8 +1012,12 @@
14.4
14.5 (**********************************************************)
14.6
14.7 -fun mk_mc_mucke_oracle sign subgoal =
14.8 - let val Freesubgoal = freeze_thaw subgoal;
14.9 +fun mk_mc_mucke_oracle csubgoal =
14.10 + let
14.11 + val sign = Thm.theory_of_cterm csubgoal;
14.12 + val subgoal = Thm.term_of csubgoal;
14.13 +
14.14 + val Freesubgoal = freeze_thaw subgoal;
14.15
14.16 val prems = Logic.strip_imp_prems Freesubgoal;
14.17 val concl = Logic.strip_imp_concl Freesubgoal;
14.18 @@ -1047,6 +1051,6 @@
14.19 (writeln ("\nmodelchecker input:\n" ^ MCstr ^ "\n/**** end ****/"))
14.20 else ();
14.21 (case (extract_result concl_str result) of
14.22 - true => (Logic.strip_imp_concl subgoal) |
14.23 + true => cterm_of sign (Logic.strip_imp_concl subgoal) |
14.24 false => (error ("Mucke couldn't solve subgoal: \n" ^result))))
14.25 end;
15.1 --- a/src/HOL/Presburger.thy Thu Sep 18 14:06:58 2008 +0200
15.2 +++ b/src/HOL/Presburger.thy Thu Sep 18 19:39:44 2008 +0200
15.3 @@ -440,7 +440,7 @@
15.4 by simp_all
15.5
15.6 use "Tools/Qelim/cooper.ML"
15.7 -oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
15.8 +oracle linzqe_oracle = Coopereif.cooper_oracle
15.9
15.10 use "Tools/Qelim/presburger.ML"
15.11
16.1 --- a/src/HOL/Tools/Qelim/cooper.ML Thu Sep 18 14:06:58 2008 +0200
16.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu Sep 18 19:39:44 2008 +0200
16.3 @@ -633,12 +633,14 @@
16.4 | NClosed n => term_of_qf ps vs (Nota (Closed n))
16.5 | _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
16.6
16.7 -fun cooper_oracle thy t =
16.8 +fun cooper_oracle ct =
16.9 let
16.10 + val thy = Thm.theory_of_cterm ct;
16.11 + val t = Thm.term_of ct;
16.12 val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
16.13 in
16.14 - Logic.mk_equals (HOLogic.mk_Trueprop t,
16.15 - HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
16.16 + Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
16.17 + HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))))
16.18 end;
16.19
16.20 end;
17.1 --- a/src/HOL/Tools/Qelim/presburger.ML Thu Sep 18 14:06:58 2008 +0200
17.2 +++ b/src/HOL/Tools/Qelim/presburger.ML Thu Sep 18 19:39:44 2008 +0200
17.3 @@ -152,8 +152,8 @@
17.4 let
17.5 val cpth =
17.6 if !quick_and_dirty
17.7 - then linzqe_oracle (ProofContext.theory_of ctxt)
17.8 - (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
17.9 + then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
17.10 + (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
17.11 else arg_conv (Cooper.cooper_conv ctxt) p
17.12 val p' = Thm.rhs_of cpth
17.13 val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
18.1 --- a/src/HOL/Tools/res_atp_methods.ML Thu Sep 18 14:06:58 2008 +0200
18.2 +++ b/src/HOL/Tools/res_atp_methods.ML Thu Sep 18 19:39:44 2008 +0200
18.3 @@ -27,7 +27,7 @@
18.4 Meson.skolemize_tac,
18.5 METAHYPS (fn negs =>
18.6 HEADGOAL (Tactic.rtac
18.7 - (res_atp_oracle (ProofContext.theory_of ctxt)
18.8 + (res_atp_oracle
18.9 (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty;
18.10
18.11
19.1 --- a/src/HOL/Tools/res_atp_provers.ML Thu Sep 18 14:06:58 2008 +0200
19.2 +++ b/src/HOL/Tools/res_atp_provers.ML Thu Sep 18 19:39:44 2008 +0200
19.3 @@ -40,19 +40,19 @@
19.4 in seek_line "SPASS beiseite: Proof found.\n" instr
19.5 end;
19.6
19.7 -fun vampire_o _ (file,time) =
19.8 +fun vampire_o (file,time) =
19.9 if call_vampire (file,time)
19.10 - then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
19.11 + then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
19.12 else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
19.13
19.14 -fun eprover_o _ (file,time) =
19.15 +fun eprover_o (file,time) =
19.16 if call_eprover (file,time)
19.17 - then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
19.18 + then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
19.19 else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
19.20
19.21 -fun spass_o _ (file,time) =
19.22 +fun spass_o (file,time) =
19.23 if call_spass (file,time)
19.24 - then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
19.25 + then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
19.26 else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
19.27
19.28 end;
20.1 --- a/src/HOL/ex/Reflected_Presburger.thy Thu Sep 18 14:06:58 2008 +0200
20.2 +++ b/src/HOL/ex/Reflected_Presburger.thy Thu Sep 18 19:39:44 2008 +0200
20.3 @@ -1920,7 +1920,7 @@
20.4 export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"
20.5 *)
20.6
20.7 -oracle linzqe_oracle ("term") = {*
20.8 +oracle linzqe_oracle = {*
20.9 let
20.10
20.11 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
20.12 @@ -2035,14 +2035,16 @@
20.13 | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
20.14 end;
20.15
20.16 -in fn thy => fn t =>
20.17 - let
20.18 +in fn ct =>
20.19 + let
20.20 + val thy = Thm.theory_of_cterm ct;
20.21 + val t = Thm.term_of ct;
20.22 val fs = term_frees t;
20.23 val bs = term_bools [] t;
20.24 val vs = fs ~~ (0 upto (length fs - 1))
20.25 val ps = bs ~~ (0 upto (length bs - 1))
20.26 val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
20.27 - in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
20.28 + in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
20.29 end;
20.30 *}
20.31
21.1 --- a/src/HOL/ex/SVC_Oracle.thy Thu Sep 18 14:06:58 2008 +0200
21.2 +++ b/src/HOL/ex/SVC_Oracle.thy Thu Sep 18 19:39:44 2008 +0200
21.3 @@ -19,8 +19,7 @@
21.4
21.5 hide const iff_keep iff_unfold
21.6
21.7 -oracle
21.8 - svc_oracle ("term") = Svc.oracle
21.9 +oracle svc_oracle = Svc.oracle
21.10
21.11 ML {*
21.12 (*
21.13 @@ -110,12 +109,13 @@
21.14 abstracted. Use via compose_tac, which performs no lifting but will
21.15 instantiate variables.*)
21.16
21.17 -fun svc_tac i st =
21.18 +val svc_tac = CSUBGOAL (fn (ct, i) =>
21.19 let
21.20 - val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
21.21 - val th = svc_oracle (Thm.theory_of_thm st) abs_goal
21.22 - in compose_tac (false, th, 0) i st end
21.23 - handle TERM _ => no_tac st;
21.24 + val thy = Thm.theory_of_cterm ct;
21.25 + val (abs_goal, _) = svc_abstract (Thm.term_of ct);
21.26 + val th = svc_oracle (Thm.cterm_of thy abs_goal);
21.27 + in compose_tac (false, th, 0) i end
21.28 + handle TERM _ => no_tac);
21.29 *}
21.30
21.31 end
22.1 --- a/src/HOL/ex/coopertac.ML Thu Sep 18 14:06:58 2008 +0200
22.2 +++ b/src/HOL/ex/coopertac.ML Thu Sep 18 19:39:44 2008 +0200
22.3 @@ -104,7 +104,7 @@
22.4 (* The result of the quantifier elimination *)
22.5 val (th, tac) = case (prop_of pre_thm) of
22.6 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
22.7 - let val pth = linzqe_oracle thy (Pattern.eta_long [] t1)
22.8 + let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
22.9 in
22.10 ((pth RS iffD2) RS pre_thm,
22.11 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
23.1 --- a/src/HOL/ex/svc_funcs.ML Thu Sep 18 14:06:58 2008 +0200
23.2 +++ b/src/HOL/ex/svc_funcs.ML Thu Sep 18 19:39:44 2008 +0200
23.3 @@ -237,10 +237,14 @@
23.4 end;
23.5
23.6
23.7 - (*The oracle proves the given formula t, if possible*)
23.8 - fun oracle thy t =
23.9 - (if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
23.10 - else ();
23.11 - if valid (expr_of false t) then t else fail t);
23.12 + (*The oracle proves the given formula, if possible*)
23.13 + fun oracle ct =
23.14 + let
23.15 + val thy = Thm.theory_of_cterm ct;
23.16 + val t = Thm.term_of ct;
23.17 + val _ =
23.18 + if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
23.19 + else ();
23.20 + in if valid (expr_of false t) then ct else fail t end;
23.21
23.22 end;
24.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Sep 18 14:06:58 2008 +0200
24.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Sep 18 19:39:44 2008 +0200
24.3 @@ -178,8 +178,12 @@
24.4
24.5 in
24.6
24.7 -fun mk_sim_oracle sign (subgoal, thl) = (
24.8 +fun mk_sim_oracle (csubgoal, thl) =
24.9 let
24.10 + val sign = Thm.theory_of_cterm csubgoal;
24.11 + val subgoal = Thm.term_of csubgoal;
24.12 + in
24.13 + (let
24.14 val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
24.15 val concl = Logic.strip_imp_concl subgoal;
24.16 val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
24.17 @@ -287,11 +291,12 @@
24.18 by (atac 1);
24.19 result();
24.20 OldGoals.pop_proof();
24.21 -Logic.strip_imp_concl subgoal
24.22 +Thm.cterm_of sign (Logic.strip_imp_concl subgoal)
24.23 )
24.24 end)
24.25 handle malformed =>
24.26 -error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal));
24.27 +error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal))
24.28 +end;
24.29
24.30 end
24.31
25.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Thu Sep 18 14:06:58 2008 +0200
25.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Thu Sep 18 19:39:44 2008 +0200
25.3 @@ -5,16 +5,13 @@
25.4 imports MuIOA
25.5 begin
25.6
25.7 -oracle sim_oracle ("term * thm list") =
25.8 - mk_sim_oracle
25.9 +oracle sim_oracle = mk_sim_oracle
25.10
25.11 ML {*
25.12 (* call_sim_tac invokes oracle "Sim" *)
25.13 -fun call_sim_tac thm_list i state =
25.14 -let val thy = Thm.theory_of_thm state;
25.15 - val (subgoal::_) = Library.drop(i-1,prems_of state);
25.16 - val OraAss = sim_oracle thy (subgoal,thm_list);
25.17 -in cut_facts_tac [OraAss] i state end;
25.18 +fun call_sim_tac thm_list = CSUBGOAL (fn (csubgoal, i) =>
25.19 +let val OraAss = sim_oracle (csubgoal,thm_list);
25.20 +in cut_facts_tac [OraAss] i end);
25.21
25.22
25.23 val ioa_implements_def = thm "ioa_implements_def";
26.1 --- a/src/Pure/Isar/isar_cmd.ML Thu Sep 18 14:06:58 2008 +0200
26.2 +++ b/src/Pure/Isar/isar_cmd.ML Thu Sep 18 19:39:44 2008 +0200
26.3 @@ -13,8 +13,7 @@
26.4 val print_translation: bool * (string * Position.T) -> theory -> theory
26.5 val typed_print_translation: bool * (string * Position.T) -> theory -> theory
26.6 val print_ast_translation: bool * (string * Position.T) -> theory -> theory
26.7 - val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
26.8 - theory -> theory
26.9 + val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
26.10 val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
26.11 val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory
26.12 val declaration: string * Position.T -> local_theory -> local_theory
26.13 @@ -152,22 +151,15 @@
26.14
26.15 (* oracles *)
26.16
26.17 -fun oracle name typ_pos (oracle_txt, pos) =
26.18 +fun oracle name (oracle_txt, pos) =
26.19 let
26.20 - val typ = SymbolPos.content (SymbolPos.explode typ_pos);
26.21 val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
26.22 val txt =
26.23 - "local\
26.24 - \ type T = " ^ typ ^ ";\
26.25 - \ val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
26.26 + "local\n\
26.27 \ val name = " ^ quote name ^ ";\n\
26.28 - \ exception Arg of T;\n\
26.29 - \ val _ = Context.>> (Context.map_theory\n\
26.30 - \ (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
26.31 - \ val thy = ML_Context.the_global_context ();\n\
26.32 - \ val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
26.33 + \ val oracle = " ^ oracle ^ ";\n\
26.34 \in\n\
26.35 - \ fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
26.36 + \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (name, oracle))));\n\
26.37 \end;\n";
26.38 in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
26.39
27.1 --- a/src/Pure/Isar/isar_syn.ML Thu Sep 18 14:06:58 2008 +0200
27.2 +++ b/src/Pure/Isar/isar_syn.ML Thu Sep 18 19:39:44 2008 +0200
27.3 @@ -371,8 +371,7 @@
27.4
27.5 val _ =
27.6 OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
27.7 - (P.name -- (P.$$$ "(" |-- P.ML_source --| P.$$$ ")" --| P.$$$ "=")
27.8 - -- P.ML_source >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
27.9 + (P.name -- (P.$$$ "=" |-- P.ML_source) >> (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
27.10
27.11
27.12 (* local theories *)
28.1 --- a/src/Pure/Isar/skip_proof.ML Thu Sep 18 14:06:58 2008 +0200
28.2 +++ b/src/Pure/Isar/skip_proof.ML Thu Sep 18 19:39:44 2008 +0200
28.3 @@ -20,20 +20,15 @@
28.4
28.5 (* oracle setup *)
28.6
28.7 -exception SkipProof of term;
28.8 -
28.9 -fun skip_proof (_, SkipProof prop) =
28.10 - if ! quick_and_dirty then prop
28.11 - else error "Proof may be skipped in quick_and_dirty mode only!";
28.12 -
28.13 -val _ = Context.>> (Context.map_theory
28.14 - (Theory.add_oracle ("skip_proof", skip_proof)));
28.15 +val (_, skip_proof) = Context.>>> (Context.map_theory_result
28.16 + (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
28.17 + if ! quick_and_dirty then Thm.cterm_of thy prop
28.18 + else error "Proof may be skipped in quick_and_dirty mode only!")));
28.19
28.20
28.21 (* basic cheating *)
28.22
28.23 -fun make_thm thy prop =
28.24 - Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
28.25 +fun make_thm thy prop = skip_proof (thy, prop);
28.26
28.27 fun cheat_tac thy st =
28.28 ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
29.1 --- a/src/Pure/display.ML Thu Sep 18 14:06:58 2008 +0200
29.2 +++ b/src/Pure/display.ML Thu Sep 18 19:39:44 2008 +0200
29.3 @@ -178,7 +178,6 @@
29.4 Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
29.5
29.6 val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
29.7 - val oracles = (Theory.oracle_space thy, Theory.oracle_table thy);
29.8 val defs = Theory.defs_of thy;
29.9 val {restricts, reducts} = Defs.dest defs;
29.10 val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
29.11 @@ -202,7 +201,6 @@
29.12 val cnstrs = NameSpace.extern_table constraints;
29.13
29.14 val axms = NameSpace.extern_table axioms;
29.15 - val oras = NameSpace.extern_table oracles;
29.16
29.17 val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
29.18 |> map (fn (lhs, rhs) =>
29.19 @@ -223,7 +221,7 @@
29.20 Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
29.21 Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
29.22 Pretty.big_list "axioms:" (map pretty_axm axms),
29.23 - Pretty.strs ("oracles:" :: (map #1 oras)),
29.24 + Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
29.25 Pretty.big_list "definitions:"
29.26 [pretty_finals reds0,
29.27 Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
30.1 --- a/src/Pure/theory.ML Thu Sep 18 14:06:58 2008 +0200
30.2 +++ b/src/Pure/theory.ML Thu Sep 18 19:39:44 2008 +0200
30.3 @@ -2,7 +2,7 @@
30.4 ID: $Id$
30.5 Author: Lawrence C Paulson and Markus Wenzel
30.6
30.7 -Logical theory content: axioms, definitions, oracles.
30.8 +Logical theory content: axioms, definitions, and begin/end wrappers.
30.9 *)
30.10
30.11 signature THEORY =
30.12 @@ -22,8 +22,6 @@
30.13 val requires: theory -> string -> string -> unit
30.14 val axiom_space: theory -> NameSpace.T
30.15 val axiom_table: theory -> term Symtab.table
30.16 - val oracle_space: theory -> NameSpace.T
30.17 - val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table
30.18 val axioms_of: theory -> (string * term) list
30.19 val all_axioms_of: theory -> (string * term) list
30.20 val defs_of: theory -> Defs.T
30.21 @@ -39,7 +37,6 @@
30.22 val add_finals: bool -> string list -> theory -> theory
30.23 val add_finals_i: bool -> term list -> theory -> theory
30.24 val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
30.25 - val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
30.26 end
30.27
30.28 structure Theory: THEORY =
30.29 @@ -86,55 +83,41 @@
30.30 datatype thy = Thy of
30.31 {axioms: term NameSpace.table,
30.32 defs: Defs.T,
30.33 - oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
30.34 wrappers: wrapper list * wrapper list};
30.35
30.36 -fun make_thy (axioms, defs, oracles, wrappers) =
30.37 - Thy {axioms = axioms, defs = defs, oracles = oracles, wrappers = wrappers};
30.38 +fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
30.39
30.40 fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
30.41 -fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
30.42
30.43 structure ThyData = TheoryDataFun
30.44 (
30.45 type T = thy;
30.46 - val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, ([], []));
30.47 + val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
30.48 val copy = I;
30.49
30.50 - fun extend (Thy {axioms, defs, oracles, wrappers}) =
30.51 - make_thy (NameSpace.empty_table, defs, oracles, wrappers);
30.52 + fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
30.53
30.54 fun merge pp (thy1, thy2) =
30.55 let
30.56 - val Thy {axioms = _, defs = defs1, oracles = oracles1, wrappers = (bgs1, ens1)} = thy1;
30.57 - val Thy {axioms = _, defs = defs2, oracles = oracles2, wrappers = (bgs2, ens2)} = thy2;
30.58 + val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
30.59 + val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
30.60
30.61 val axioms' = NameSpace.empty_table;
30.62 val defs' = Defs.merge pp (defs1, defs2);
30.63 - val oracles' = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
30.64 - handle Symtab.DUP dup => err_dup_ora dup;
30.65 val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
30.66 val ens' = Library.merge (eq_snd op =) (ens1, ens2);
30.67 - in make_thy (axioms', defs', oracles', (bgs', ens')) end;
30.68 + in make_thy (axioms', defs', (bgs', ens')) end;
30.69 );
30.70
30.71 fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
30.72
30.73 -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, wrappers}) =>
30.74 - make_thy (f (axioms, defs, oracles, wrappers)));
30.75 +fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
30.76 + make_thy (f (axioms, defs, wrappers)));
30.77
30.78
30.79 -fun map_axioms f = map_thy
30.80 - (fn (axioms, defs, oracles, wrappers) => (f axioms, defs, oracles, wrappers));
30.81 -
30.82 -fun map_defs f = map_thy
30.83 - (fn (axioms, defs, oracles, wrappers) => (axioms, f defs, oracles, wrappers));
30.84 -
30.85 -fun map_oracles f = map_thy
30.86 - (fn (axioms, defs, oracles, wrappers) => (axioms, defs, f oracles, wrappers));
30.87 -
30.88 -fun map_wrappers f = map_thy
30.89 - (fn (axioms, defs, oracles, wrappers) => (axioms, defs, oracles, f wrappers));
30.90 +fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
30.91 +fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
30.92 +fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
30.93
30.94
30.95 (* basic operations *)
30.96 @@ -142,9 +125,6 @@
30.97 val axiom_space = #1 o #axioms o rep_theory;
30.98 val axiom_table = #2 o #axioms o rep_theory;
30.99
30.100 -val oracle_space = #1 o #oracles o rep_theory;
30.101 -val oracle_table = #2 o #oracles o rep_theory;
30.102 -
30.103 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
30.104 fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
30.105
30.106 @@ -323,13 +303,4 @@
30.107
30.108 end;
30.109
30.110 -
30.111 -
30.112 -(** add oracle **)
30.113 -
30.114 -fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
30.115 - NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
30.116 - handle Symtab.DUP dup => err_dup_ora dup);
30.117 -
30.118 end;
30.119 -
31.1 --- a/src/Pure/thm.ML Thu Sep 18 14:06:58 2008 +0200
31.2 +++ b/src/Pure/thm.ML Thu Sep 18 19:39:44 2008 +0200
31.3 @@ -112,8 +112,8 @@
31.4 val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
31.5 val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
31.6 val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
31.7 - val invoke_oracle: theory -> xstring -> theory * Object.T -> thm
31.8 - val invoke_oracle_i: theory -> string -> theory * Object.T -> thm
31.9 + val extern_oracles: theory -> xstring list
31.10 + val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
31.11 end;
31.12
31.13 signature THM =
31.14 @@ -1557,36 +1557,53 @@
31.15
31.16 (*** Oracles ***)
31.17
31.18 -fun invoke_oracle_i thy1 name =
31.19 - let
31.20 - val oracle =
31.21 - (case Symtab.lookup (Theory.oracle_table thy1) name of
31.22 - NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
31.23 - | SOME (f, _) => f);
31.24 - val thy_ref1 = Theory.check_thy thy1;
31.25 - in
31.26 - fn (thy2, data) =>
31.27 - let
31.28 - val thy' = Theory.merge (Theory.deref thy_ref1, thy2);
31.29 - val (prop, T, maxidx) = Sign.certify_term thy' (oracle (thy', data));
31.30 - val shyps' = Sorts.insert_term prop [];
31.31 - val der = Deriv.oracle name prop;
31.32 - in
31.33 - if T <> propT then
31.34 - raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
31.35 - else
31.36 - Thm {thy_ref = Theory.check_thy thy', der = der, tags = [],
31.37 - maxidx = maxidx, shyps = shyps', hyps = [], tpairs = [], prop = prop}
31.38 - end
31.39 +(* oracle rule *)
31.40 +
31.41 +fun invoke_oracle thy_ref1 name oracle arg =
31.42 + let val {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = rep_cterm (oracle arg) in
31.43 + if T <> propT then
31.44 + raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
31.45 + else
31.46 + Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
31.47 + der = Deriv.oracle name prop,
31.48 + tags = [],
31.49 + maxidx = maxidx,
31.50 + shyps = sorts,
31.51 + hyps = [],
31.52 + tpairs = [],
31.53 + prop = prop}
31.54 end;
31.55
31.56 -fun invoke_oracle thy =
31.57 - invoke_oracle_i thy o NameSpace.intern (Theory.oracle_space thy);
31.58 +end;
31.59 +end;
31.60 +end;
31.61
31.62
31.63 -end;
31.64 -end;
31.65 -end;
31.66 +(* authentic derivation names *)
31.67 +
31.68 +fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
31.69 +
31.70 +structure Oracles = TheoryDataFun
31.71 +(
31.72 + type T = stamp NameSpace.table;
31.73 + val empty = NameSpace.empty_table;
31.74 + val copy = I;
31.75 + val extend = I;
31.76 + fun merge _ oracles = NameSpace.merge_tables (op =) oracles
31.77 + handle Symtab.DUP dup => err_dup_ora dup;
31.78 +);
31.79 +
31.80 +val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
31.81 +
31.82 +fun add_oracle (bname, oracle) thy =
31.83 + let
31.84 + val naming = Sign.naming_of thy;
31.85 + val name = NameSpace.full naming bname;
31.86 + val thy' = thy |> Oracles.map (fn (space, tab) =>
31.87 + (NameSpace.declare naming name space,
31.88 + Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
31.89 + in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
31.90 +
31.91 end;
31.92
31.93 structure BasicThm: BASIC_THM = Thm;
32.1 --- a/src/Tools/Compute_Oracle/Compute_Oracle.thy Thu Sep 18 14:06:58 2008 +0200
32.2 +++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy Thu Sep 18 19:39:44 2008 +0200
32.3 @@ -9,6 +9,4 @@
32.4 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
32.5 begin
32.6
32.7 -setup {* Compute.setup_compute *}
32.8 -
32.9 end
32.10 \ No newline at end of file
33.1 --- a/src/Tools/Compute_Oracle/compute.ML Thu Sep 18 14:06:58 2008 +0200
33.2 +++ b/src/Tools/Compute_Oracle/compute.ML Thu Sep 18 19:39:44 2008 +0200
33.3 @@ -35,8 +35,6 @@
33.4 (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem
33.5 (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem
33.6
33.7 - val setup_compute : theory -> theory
33.8 -
33.9 end
33.10
33.11 structure Compute :> COMPUTE = struct
33.12 @@ -362,8 +360,6 @@
33.13 (* An oracle for exporting theorems; must only be accessible from inside this structure! *)
33.14 (* ------------------------------------------------------------------------------------- *)
33.15
33.16 -exception ExportThm of term list * sort list * term
33.17 -
33.18 fun merge_hyps hyps1 hyps2 =
33.19 let
33.20 fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab
33.21 @@ -375,7 +371,8 @@
33.22
33.23 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
33.24
33.25 -fun export_oracle (thy, ExportThm (hyps, shyps, prop)) =
33.26 +val (_, export_oracle) = Context.>>> (Context.map_theory_result
33.27 + (Thm.add_oracle ("compute", fn (thy, hyps, shyps, prop) =>
33.28 let
33.29 val shyptab = add_shyps shyps Sorttab.empty
33.30 fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
33.31 @@ -385,15 +382,12 @@
33.32 val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
33.33 val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
33.34 in
33.35 - fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop
33.36 - end
33.37 - | export_oracle _ = raise Match
33.38 -
33.39 -val setup_compute = (fn thy => Theory.add_oracle ("compute", export_oracle) thy)
33.40 + Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
33.41 + end)));
33.42
33.43 fun export_thm thy hyps shyps prop =
33.44 let
33.45 - val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop))
33.46 + val th = export_oracle (thy, hyps, shyps, prop)
33.47 val hyps = map (fn h => assume (cterm_of thy h)) hyps
33.48 in
33.49 fold (fn h => fn p => implies_elim p h) hyps th
34.1 --- a/src/Tools/nbe.ML Thu Sep 18 14:06:58 2008 +0200
34.2 +++ b/src/Tools/nbe.ML Thu Sep 18 19:39:44 2008 +0200
34.3 @@ -403,15 +403,9 @@
34.4
34.5 (* evaluation oracle *)
34.6
34.7 -exception Norm of term * Code_Thingol.program
34.8 - * (Code_Thingol.typscheme * Code_Thingol.iterm) * string list;
34.9 -
34.10 -fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
34.11 - Logic.mk_equals (t, eval thy t program vs_ty_t deps);
34.12 -
34.13 -fun norm_invoke thy t program vs_ty_t deps =
34.14 - Thm.invoke_oracle_i thy "HOL.norm" (thy, Norm (t, program, vs_ty_t, deps));
34.15 - (*FIXME get rid of hardwired theory name*)
34.16 +val (_, norm_oracle) = Context.>>> (Context.map_theory_result
34.17 + (Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) =>
34.18 + Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps)))));
34.19
34.20 fun add_triv_classes thy =
34.21 let
34.22 @@ -425,7 +419,7 @@
34.23 fun norm_conv ct =
34.24 let
34.25 val thy = Thm.theory_of_cterm ct;
34.26 - fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
34.27 + fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
34.28 fun evaluator t = (add_triv_classes thy t, evaluator' t);
34.29 in Code_Thingol.eval_conv thy evaluator ct end;
34.30
34.31 @@ -455,8 +449,8 @@
34.32 let val ctxt = Toplevel.context_of state
34.33 in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
34.34
34.35 -val setup = Theory.add_oracle ("norm", norm_oracle)
34.36 - #> Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
34.37 +val setup =
34.38 + Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
34.39
34.40 local structure P = OuterParse and K = OuterKeyword in
34.41