# HG changeset patch # User wenzelm # Date 1288343241 -7200 # Node ID f99ec71de82db6486451075945df4159f2003863 # Parent 029400b6c8939df698f0333eb1b9c4fb9884e797# Parent bb433b0668b898acaaea1734e8a61af86559dd8d merged diff -r 029400b6c893 -r f99ec71de82d NEWS --- a/NEWS Fri Oct 29 11:04:41 2010 +0200 +++ b/NEWS Fri Oct 29 11:07:21 2010 +0200 @@ -344,6 +344,10 @@ Fail if the argument is false. Due to inlining the source position of failed assertions is included in the error output. +* Discontinued antiquotation @{theory_ref}, which is obsolete since ML +text is in practice always evaluated with a stable theory checkpoint. +Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead. + * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning. diff -r 029400b6c893 -r f99ec71de82d doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Fri Oct 29 11:04:41 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Fri Oct 29 11:07:21 2010 +0200 @@ -226,11 +226,10 @@ text %mlantiq {* \begin{matharray}{rcl} @{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\ - @{ML_antiquotation_def "theory_ref"} & : & @{text ML_antiquotation} \\ \end{matharray} \begin{rail} - ('theory' | 'theory\_ref') nameref? + 'theory' nameref? ; \end{rail} @@ -243,10 +242,6 @@ theory @{text "A"} of the background theory of the current context --- as abstract value. - \item @{text "@{theory_ref}"} is similar to @{text "@{theory}"}, but - produces a @{ML_type theory_ref} via @{ML "Theory.check_thy"} as - explained above. - \end{description} *} diff -r 029400b6c893 -r f99ec71de82d doc-src/IsarImplementation/Thy/document/Prelim.tex --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Oct 29 11:04:41 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Oct 29 11:07:21 2010 +0200 @@ -262,11 +262,10 @@ \begin{isamarkuptext}% \begin{matharray}{rcl} \indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\ - \indexdef{}{ML antiquotation}{theory\_ref}\hypertarget{ML antiquotation.theory-ref}{\hyperlink{ML antiquotation.theory-ref}{\mbox{\isa{theory{\isacharunderscore}ref}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\ \end{matharray} \begin{rail} - ('theory' | 'theory\_ref') nameref? + 'theory' nameref? ; \end{rail} @@ -279,10 +278,6 @@ theory \isa{A} of the background theory of the current context --- as abstract value. - \item \isa{{\isacharat}{\isacharbraceleft}theory{\isacharunderscore}ref{\isacharbraceright}} is similar to \isa{{\isacharat}{\isacharbraceleft}theory{\isacharbraceright}}, but - produces a \verb|theory_ref| via \verb|Theory.check_thy| as - explained above. - \end{description}% \end{isamarkuptext}% \isamarkuptrue% diff -r 029400b6c893 -r f99ec71de82d doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Fri Oct 29 11:04:41 2010 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Fri Oct 29 11:07:21 2010 +0200 @@ -159,7 +159,7 @@ text {* \begin{matharray}{rcll} - @{command_def "axiomatization"} & : & @{text "theory \ theory"} & (axiomatic!)\\ + @{command_def "axiomatization"} & : & @{text "theory \ theory"} & (axiomatic!) \\ @{command_def "definition"} & : & @{text "local_theory \ local_theory"} \\ @{attribute_def "defn"} & : & @{text attribute} \\ @{command_def "abbreviation"} & : & @{text "local_theory \ local_theory"} \\ @@ -1139,8 +1139,8 @@ asserted, and records within the internal derivation object how presumed theorems depend on unproven suppositions. - \begin{matharray}{rcl} - @{command_def "oracle"} & : & @{text "theory \ theory"} \\ + \begin{matharray}{rcll} + @{command_def "oracle"} & : & @{text "theory \ theory"} & (axiomatic!) \\ \end{matharray} \begin{rail} @@ -1159,7 +1159,7 @@ \end{description} - See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of + See @{"file" "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of defining a new primitive rule as oracle, and turning it into a proof method. *} diff -r 029400b6c893 -r f99ec71de82d doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 11:04:41 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 11:07:21 2010 +0200 @@ -179,7 +179,7 @@ % \begin{isamarkuptext}% \begin{matharray}{rcll} - \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!)\\ + \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\ \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isa{attribute} \\ \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ @@ -1179,8 +1179,8 @@ asserted, and records within the internal derivation object how presumed theorems depend on unproven suppositions. - \begin{matharray}{rcl} - \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \begin{matharray}{rcll} + \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\ \end{matharray} \begin{rail} @@ -1199,7 +1199,7 @@ \end{description} - See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of + See \hyperlink{file.~~/src/HOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of defining a new primitive rule as oracle, and turning it into a proof method.% \end{isamarkuptext}% diff -r 029400b6c893 -r f99ec71de82d src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Fri Oct 29 11:04:41 2010 +0200 +++ b/src/FOL/IsaMakefile Fri Oct 29 11:07:21 2010 +0200 @@ -45,14 +45,13 @@ FOL-ex: FOL $(LOG)/FOL-ex.gz $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \ - ex/Iff_Oracle.thy ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \ + ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \ ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \ ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy \ - ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML \ - ex/Classical.thy ex/document/root.tex ex/Foundation.thy \ - ex/Intuitionistic.thy ex/Intro.thy ex/Propositional_Int.thy \ - ex/Propositional_Cla.thy ex/Quantifiers_Int.thy \ - ex/Quantifiers_Cla.thy + ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy \ + ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy \ + ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy \ + ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy @$(ISABELLE_TOOL) usedir $(OUT)/FOL ex diff -r 029400b6c893 -r f99ec71de82d src/FOL/ex/Iff_Oracle.thy --- a/src/FOL/ex/Iff_Oracle.thy Fri Oct 29 11:04:41 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,76 +0,0 @@ -(* Title: FOL/ex/Iff_Oracle.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge -*) - -header {* Example of Declaring an Oracle *} - -theory Iff_Oracle -imports FOL -begin - -subsection {* Oracle declaration *} - -text {* - This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}. - The length is specified by an integer, which is checked to be even - and positive. -*} - -oracle iff_oracle = {* - let - fun mk_iff 1 = Var (("P", 0), @{typ o}) - | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1); - in - fn (thy, n) => - if n > 0 andalso n mod 2 = 0 - then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n)) - else raise Fail ("iff_oracle: " ^ string_of_int n) - end -*} - - -subsection {* Oracle as low-level rule *} - -ML {* iff_oracle (@{theory}, 2) *} -ML {* iff_oracle (@{theory}, 10) *} -ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *} - -text {* These oracle calls had better fail. *} - -ML {* - (iff_oracle (@{theory}, 5); error "?") - handle Fail _ => warning "Oracle failed, as expected" -*} - -ML {* - (iff_oracle (@{theory}, 1); error "?") - handle Fail _ => warning "Oracle failed, as expected" -*} - - -subsection {* Oracle as proof method *} - -method_setup iff = {* - Scan.lift Parse.nat >> (fn n => fn ctxt => - SIMPLE_METHOD - (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) - handle Fail _ => no_tac)) -*} "iff oracle" - - -lemma "A <-> A" - by (iff 2) - -lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A" - by (iff 10) - -lemma "A <-> A <-> A <-> A <-> A" - apply (iff 5)? - oops - -lemma A - apply (iff 1)? - oops - -end diff -r 029400b6c893 -r f99ec71de82d src/FOL/ex/ROOT.ML --- a/src/FOL/ex/ROOT.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/FOL/ex/ROOT.ML Fri Oct 29 11:07:21 2010 +0200 @@ -18,8 +18,7 @@ "Propositional_Cla", "Quantifiers_Cla", "Miniscope", - "If", - "Iff_Oracle" + "If" ]; (*regression test for locales -- sets several global flags!*) diff -r 029400b6c893 -r f99ec71de82d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Oct 29 11:04:41 2010 +0200 +++ b/src/HOL/IsaMakefile Fri Oct 29 11:07:21 2010 +0200 @@ -1016,20 +1016,19 @@ ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ - ex/Induction_Schema.thy ex/InductiveInvariant.thy \ + ex/Iff_Oracle.thy ex/Induction_Schema.thy ex/InductiveInvariant.thy \ ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \ ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ - ex/Normalization_by_Evaluation.thy \ - ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ - ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \ - ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ - ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ - ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \ - ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ - ex/Unification.thy ex/While_Combinator_Example.thy \ - ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \ - ex/svc_test.thy + ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy \ + ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \ + ex/Quickcheck_Lattice_Examples.thy ex/ROOT.ML ex/Recdefs.thy \ + ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ + ex/SAT_Examples.thy ex/SVC_Oracle.thy ex/Serbian.thy ex/Sqrt.thy \ + ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \ + ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \ + ex/While_Combinator_Example.thy ex/document/root.bib \ + ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex diff -r 029400b6c893 -r f99ec71de82d src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Oct 29 11:07:21 2010 +0200 @@ -703,7 +703,7 @@ val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i; val _ = check_nonempty descr handle (exn as Datatype_Empty s) => if #strict config then error ("Nonemptiness check failed for datatype " ^ s) - else raise exn; + else reraise exn; val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names); diff -r 029400b6c893 -r f99ec71de82d src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Oct 29 11:07:21 2010 +0200 @@ -6,10 +6,11 @@ signature QUOTIENT_INFO = sig - exception NotFound + exception NotFound (* FIXME complicates signatures unnecessarily *) type maps_info = {mapfun: string, relmap: string} val maps_defined: theory -> string -> bool + (* FIXME functions called "lookup" must return option, not raise exception *) val maps_lookup: theory -> string -> maps_info (* raises NotFound *) val maps_update_thy: string -> maps_info -> theory -> theory val maps_update: string -> maps_info -> Proof.context -> Proof.context diff -r 029400b6c893 -r f99ec71de82d src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Oct 29 11:07:21 2010 +0200 @@ -67,8 +67,8 @@ fun get_mapfun ctxt s = let val thy = ProofContext.theory_of ctxt - val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") - val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exn + val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => + raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") in Const (mapfun, dummyT) end @@ -104,8 +104,8 @@ fun get_rty_qty ctxt s = let val thy = ProofContext.theory_of ctxt - val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") - val qdata = quotdata_lookup thy s handle NotFound => raise exn + val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => + raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") in (#rtyp qdata, #qtyp qdata) end @@ -127,7 +127,7 @@ val thy = ProofContext.theory_of ctxt in Sign.typ_match thy (ty_pat, ty) Vartab.empty - handle MATCH_TYPE => err ctxt ty_pat ty + handle Type.TYPE_MATCH => err ctxt ty_pat ty end (* produces the rep or abs constant for a qty *) @@ -276,8 +276,8 @@ fun get_relmap ctxt s = let val thy = ProofContext.theory_of ctxt - val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") - val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exn + val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => + raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") in Const (relmap, dummyT) end @@ -299,9 +299,9 @@ fun get_equiv_rel ctxt s = let val thy = ProofContext.theory_of ctxt - val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") in - #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exn + #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => + raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") end fun equiv_match_err ctxt ty_pat ty = @@ -563,7 +563,8 @@ else let val rtrm' = #rconst (qconsts_lookup thy qtrm) - handle NotFound => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm + handle Quotient_Info.NotFound => + term_mismatch "regularize (constant not found)" ctxt rtrm qtrm in if Pattern.matches thy (rtrm', rtrm) then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm diff -r 029400b6c893 -r f99ec71de82d src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Fri Oct 29 11:07:21 2010 +0200 @@ -274,22 +274,6 @@ | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; (* ------------------------------------------------------------------------- *) -(* take_prefix: *) -(* take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *) -(* ------------------------------------------------------------------------- *) - -(* int -> 'a list -> 'a list * 'a list *) - -fun take_prefix n xs = -let - fun take 0 (rxs, xs) = (rev rxs, xs) - | take _ (rxs, []) = (rev rxs, []) - | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs) -in - take n ([], xs) -end; - -(* ------------------------------------------------------------------------- *) (* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) (* a proof from the resulting proof trace of the SAT solver. The *) (* theorem returned is just "False" (with some of the given clauses as *) diff -r 029400b6c893 -r f99ec71de82d src/HOL/ex/Iff_Oracle.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Iff_Oracle.thy Fri Oct 29 11:07:21 2010 +0200 @@ -0,0 +1,76 @@ +(* Title: HOL/ex/Iff_Oracle.thy + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Makarius +*) + +header {* Example of Declaring an Oracle *} + +theory Iff_Oracle +imports Main +begin + +subsection {* Oracle declaration *} + +text {* + This oracle makes tautologies of the form @{prop "P <-> P <-> P <-> P"}. + The length is specified by an integer, which is checked to be even + and positive. +*} + +oracle iff_oracle = {* + let + fun mk_iff 1 = Var (("P", 0), @{typ bool}) + | mk_iff n = HOLogic.mk_eq (Var (("P", 0), @{typ bool}), mk_iff (n - 1)); + in + fn (thy, n) => + if n > 0 andalso n mod 2 = 0 + then Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_iff n)) + else raise Fail ("iff_oracle: " ^ string_of_int n) + end +*} + + +subsection {* Oracle as low-level rule *} + +ML {* iff_oracle (@{theory}, 2) *} +ML {* iff_oracle (@{theory}, 10) *} +ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *} + +text {* These oracle calls had better fail. *} + +ML {* + (iff_oracle (@{theory}, 5); error "Bad oracle") + handle Fail _ => warning "Oracle failed, as expected" +*} + +ML {* + (iff_oracle (@{theory}, 1); error "Bad oracle") + handle Fail _ => warning "Oracle failed, as expected" +*} + + +subsection {* Oracle as proof method *} + +method_setup iff = {* + Scan.lift Parse.nat >> (fn n => fn ctxt => + SIMPLE_METHOD + (HEADGOAL (rtac (iff_oracle (ProofContext.theory_of ctxt, n))) + handle Fail _ => no_tac)) +*} "iff oracle" + + +lemma "A <-> A" + by (iff 2) + +lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A" + by (iff 10) + +lemma "A <-> A <-> A <-> A <-> A" + apply (iff 5)? + oops + +lemma A + apply (iff 1)? + oops + +end diff -r 029400b6c893 -r f99ec71de82d src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/HOL/ex/ROOT.ML Fri Oct 29 11:07:21 2010 +0200 @@ -12,6 +12,7 @@ ]; use_thys [ + "Iff_Oracle", "Numeral", "Higher_Order_Logic", "Abstract_NAT", diff -r 029400b6c893 -r f99ec71de82d src/Pure/Concurrent/simple_thread.ML --- a/src/Pure/Concurrent/simple_thread.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Pure/Concurrent/simple_thread.ML Fri Oct 29 11:07:21 2010 +0200 @@ -32,21 +32,21 @@ fun synchronized name lock e = if Multithreading.available then Exn.release (uninterruptible (fn restore_attributes => fn () => - let - val immediate = - if Mutex.trylock lock then true - else - let - val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ..."); - val time = Multithreading.real_time Mutex.lock lock; - val _ = Multithreading.tracing_time true time - (fn () => name ^ ": locked after " ^ Time.toString time); - in false end; - val result = Exn.capture (restore_attributes e) (); - val _ = - if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ..."); - val _ = Mutex.unlock lock; - in result end) ()) + let + val immediate = + if Mutex.trylock lock then true + else + let + val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ..."); + val time = Multithreading.real_time Mutex.lock lock; + val _ = Multithreading.tracing_time true time + (fn () => name ^ ": locked after " ^ Time.toString time); + in false end; + val result = Exn.capture (restore_attributes e) (); + val _ = + if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ..."); + val _ = Mutex.unlock lock; + in result end) ()) else e (); end; diff -r 029400b6c893 -r f99ec71de82d src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Pure/General/exn.ML Fri Oct 29 11:07:21 2010 +0200 @@ -11,12 +11,13 @@ val get_exn: 'a result -> exn option val capture: ('a -> 'b) -> 'a -> 'b result val release: 'a result -> 'a - val map_result: ('a -> 'a) -> 'a result -> 'a result + val map_result: ('a -> 'b) -> 'a result -> 'b result exception Interrupt val interrupt: unit -> 'a val is_interrupt: exn -> bool val interrupt_exn: 'a result val is_interrupt_exn: 'a result -> bool + val interruptible_capture: ('a -> 'b) -> 'a -> 'b result exception EXCEPTIONS of exn list val flatten: exn -> exn list val flatten_list: exn list -> exn list @@ -45,7 +46,7 @@ | release (Exn e) = reraise e; fun map_result f (Result x) = Result (f x) - | map_result f e = e; + | map_result f (Exn e) = (Exn e); (* interrupts *) @@ -55,7 +56,7 @@ fun interrupt () = raise Interrupt; fun is_interrupt Interrupt = true - | is_interrupt (IO.Io {cause = Interrupt, ...}) = true + | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause | is_interrupt _ = false; val interrupt_exn = Exn Interrupt; @@ -63,6 +64,9 @@ fun is_interrupt_exn (Exn exn) = is_interrupt exn | is_interrupt_exn _ = false; +fun interruptible_capture f x = + Result (f x) handle e => if is_interrupt e then reraise e else Exn e; + (* nested exceptions *) diff -r 029400b6c893 -r f99ec71de82d src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Pure/IsaMakefile Fri Oct 29 11:07:21 2010 +0200 @@ -20,6 +20,7 @@ ## Pure BOOTSTRAP_FILES = \ + General/exn.ML \ ML-Systems/bash.ML \ ML-Systems/compiler_polyml-5.2.ML \ ML-Systems/compiler_polyml-5.3.ML \ @@ -73,7 +74,6 @@ General/basics.ML \ General/binding.ML \ General/buffer.ML \ - General/exn.ML \ General/file.ML \ General/graph.ML \ General/heap.ML \ diff -r 029400b6c893 -r f99ec71de82d src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Pure/Isar/local_defs.ML Fri Oct 29 11:07:21 2010 +0200 @@ -44,8 +44,9 @@ fun cert_def ctxt eq = let - fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ - quote (Syntax.string_of_term ctxt eq)); + fun err msg = + cat_error msg ("The error(s) above occurred in definition:\n" ^ + quote (Syntax.string_of_term ctxt eq)); val ((lhs, _), eq') = eq |> Sign.no_vars ctxt |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true) @@ -245,7 +246,7 @@ (CONVERSION (meta_rewrite_conv ctxt') THEN' MetaSimplifier.rewrite_goal_tac [def] THEN' resolve_tac [Drule.reflexive_thm]))) - handle ERROR msg => cat_error msg "Failed to prove definitional specification." + handle ERROR msg => cat_error msg "Failed to prove definitional specification" end; in (((c, T), rhs), prove) end; diff -r 029400b6c893 -r f99ec71de82d src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Fri Oct 29 11:07:21 2010 +0200 @@ -71,12 +71,6 @@ "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name) || Scan.succeed "ML_Context.the_global_context ()"); -val _ = value "theory_ref" - (Scan.lift Args.name >> (fn name => - "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^ - ML_Syntax.print_string name ^ ")") - || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())"); - val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()"); val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); diff -r 029400b6c893 -r f99ec71de82d src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Fri Oct 29 11:07:21 2010 +0200 @@ -547,7 +547,7 @@ fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts) | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok); - val exn_results = map (Exn.capture ast_of) pts; + val exn_results = map (Exn.interruptible_capture ast_of) pts; val exns = map_filter Exn.get_exn exn_results; val results = map_filter Exn.get_result exn_results in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end; @@ -571,7 +571,7 @@ Term.list_comb (term_of ast, map term_of asts) | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]); - val exn_results = map (Exn.capture term_of) asts; + val exn_results = map (Exn.interruptible_capture term_of) asts; val exns = map_filter Exn.get_exn exn_results; val results = map_filter Exn.get_result exn_results in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end; diff -r 029400b6c893 -r f99ec71de82d src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Pure/more_thm.ML Fri Oct 29 11:07:21 2010 +0200 @@ -12,6 +12,7 @@ structure Ctermtab: TABLE structure Thmtab: TABLE val aconvc: cterm * cterm -> bool + type attribute = Context.generic * thm -> Context.generic * thm end; signature THM = @@ -64,6 +65,7 @@ val close_derivation: thm -> thm val add_axiom: binding * term -> theory -> (string * thm) * theory val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory + type attribute = Context.generic * thm -> Context.generic * thm type binding = binding * attribute list val empty_binding: binding val rule_attribute: (Context.generic -> thm -> thm) -> attribute @@ -382,6 +384,9 @@ (** attributes **) +(*attributes subsume any kind of rules or context modifiers*) +type attribute = Context.generic * thm -> Context.generic * thm; + type binding = binding * attribute list; val empty_binding: binding = (Binding.empty, []); diff -r 029400b6c893 -r f99ec71de82d src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Pure/thm.ML Fri Oct 29 11:07:21 2010 +0200 @@ -39,7 +39,6 @@ (*theorems*) type thm type conv = cterm -> thm - type attribute = Context.generic * thm -> Context.generic * thm val rep_thm: thm -> {thy_ref: theory_ref, tags: Properties.T, @@ -350,9 +349,6 @@ type conv = cterm -> thm; -(*attributes subsume any kind of rules or context modifiers*) -type attribute = Context.generic * thm -> Context.generic * thm; - (*errors involving theorems*) exception THM of string * int * thm list; diff -r 029400b6c893 -r f99ec71de82d src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Tools/Code/code_runtime.ML Fri Oct 29 11:07:21 2010 +0200 @@ -105,7 +105,7 @@ val (program_code, [SOME value_name']) = serializer naming program' [value_name]; val value_code = space_implode " " (value_name' :: "()" :: map (enclose "(" ")") args); - in Exn.capture (value ctxt cookie) (program_code, value_code) end; + in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end; fun partiality_as_none e = SOME (Exn.release e) handle General.Match => NONE diff -r 029400b6c893 -r f99ec71de82d src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/Tools/quickcheck.ML Fri Oct 29 11:07:21 2010 +0200 @@ -170,9 +170,10 @@ fun mk_testers_strict ctxt t = let - val generators = ((map snd o fst o Data.get o Context.Proof) ctxt) - val testers = map (fn generator => Exn.capture (generator ctxt) t) generators; - in if forall (is_none o Exn.get_result) testers + val generators = ((map snd o fst o Data.get o Context.Proof) ctxt) + val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators; + in + if forall (is_none o Exn.get_result) testers then [(Exn.release o snd o split_last) testers] else map_filter Exn.get_result testers end; diff -r 029400b6c893 -r f99ec71de82d src/ZF/simpdata.ML --- a/src/ZF/simpdata.ML Fri Oct 29 11:04:41 2010 +0200 +++ b/src/ZF/simpdata.ML Fri Oct 29 11:07:21 2010 +0200 @@ -59,10 +59,10 @@ in -val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref}) +val defBEX_regroup = Simplifier.simproc_global @{theory} "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex; -val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref}) +val defBALL_regroup = Simplifier.simproc_global @{theory} "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball; end;