# HG changeset patch # User wenzelm # Date 1288298399 -7200 # Node ID c4336e45f199c7a828422cd13b3b4247c85d2dba # Parent edcdecd556556668acdce206c363ab05762fbeb7 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; tuned; diff -r edcdecd55655 -r c4336e45f199 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Thu Oct 28 22:23:11 2010 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Oct 28 22:39:59 2010 +0200 @@ -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 edcdecd55655 -r c4336e45f199 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Oct 28 22:23:11 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Oct 28 22:39:59 2010 +0200 @@ -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 edcdecd55655 -r c4336e45f199 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Thu Oct 28 22:23:11 2010 +0200 +++ b/src/FOL/IsaMakefile Thu Oct 28 22:39:59 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 edcdecd55655 -r c4336e45f199 src/FOL/ex/Iff_Oracle.thy --- a/src/FOL/ex/Iff_Oracle.thy Thu Oct 28 22:23:11 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 edcdecd55655 -r c4336e45f199 src/FOL/ex/ROOT.ML --- a/src/FOL/ex/ROOT.ML Thu Oct 28 22:23:11 2010 +0200 +++ b/src/FOL/ex/ROOT.ML Thu Oct 28 22:39:59 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 edcdecd55655 -r c4336e45f199 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Oct 28 22:23:11 2010 +0200 +++ b/src/HOL/IsaMakefile Thu Oct 28 22:39:59 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 edcdecd55655 -r c4336e45f199 src/HOL/ex/Iff_Oracle.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Iff_Oracle.thy Thu Oct 28 22:39:59 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 edcdecd55655 -r c4336e45f199 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Thu Oct 28 22:23:11 2010 +0200 +++ b/src/HOL/ex/ROOT.ML Thu Oct 28 22:39:59 2010 +0200 @@ -12,6 +12,7 @@ ]; use_thys [ + "Iff_Oracle", "Numeral", "Higher_Order_Logic", "Abstract_NAT",