Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
authorwenzelm
Thu, 28 Oct 2010 22:39:59 +0200
changeset 40239 c4336e45f199
parent 40238 edcdecd55655
child 40240 a2dde53b15ef
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; tuned;
doc-src/IsarRef/Thy/Spec.thy file | annotate | diff | comparison | revisions
doc-src/IsarRef/Thy/document/Spec.tex file | annotate | diff | comparison | revisions
src/FOL/IsaMakefile file | annotate | diff | comparison | revisions
src/FOL/ex/Iff_Oracle.thy file | annotate | diff | comparison | revisions
src/FOL/ex/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/ex/Iff_Oracle.thy file | annotate | diff | comparison | revisions
src/HOL/ex/ROOT.ML file | annotate | diff | comparison | revisions 
--- 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.
 *}
--- 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}%
--- 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
 
 
--- 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
--- 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!*)
--- 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
 
 
--- /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
--- 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",
isabelle