--- a/doc-src/IsarRef/Thy/Spec.thy Mon Feb 16 20:07:05 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Mon Feb 16 20:15:40 2009 +0100
@@ -1182,7 +1182,7 @@
\end{description}
- See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
+ See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
defining a new primitive rule as oracle, and turning it into a proof
method.
*}
--- a/src/FOL/IsaMakefile Mon Feb 16 20:07:05 2009 +0100
+++ b/src/FOL/IsaMakefile Mon Feb 16 20:15:40 2009 +0100
@@ -46,12 +46,12 @@
FOL-ex: FOL $(LOG)/FOL-ex.gz
$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \
- ex/IffOracle.thy ex/Nat.thy ex/Natural_Numbers.thy \
- ex/LocaleTest.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/Iff_Oracle.thy ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \
+ ex/LocaleTest.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/IffOracle.thy Mon Feb 16 20:07:05 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-(* Title: FOL/ex/IffOracle.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-*)
-
-header {* Example of Declaring an Oracle *}
-
-theory IffOracle
-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_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 = {*
- Method.simple_args OuterParse.nat (fn n => fn ctxt =>
- Method.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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Iff_Oracle.thy Mon Feb 16 20:15:40 2009 +0100
@@ -0,0 +1,76 @@
+(* 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_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 = {*
+ Method.simple_args OuterParse.nat (fn n => fn ctxt =>
+ Method.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/NatClass.thy Mon Feb 16 20:07:05 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-(* Title: FOL/ex/NatClass.thy
- Author: Markus Wenzel, TU Muenchen
-*)
-
-theory NatClass
-imports FOL
-begin
-
-text {*
- This is an abstract version of theory @{text "Nat"}. Instead of
- axiomatizing a single type @{text nat} we define the class of all
- these types (up to isomorphism).
-
- Note: The @{text rec} operator had to be made \emph{monomorphic},
- because class axioms may not contain more than one type variable.
-*}
-
-class nat =
- fixes Zero :: 'a ("0")
- and Suc :: "'a => 'a"
- and rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
- assumes induct: "P(0) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
- and Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
- and Suc_neq_Zero: "Suc(m) = 0 \<Longrightarrow> R"
- and rec_Zero: "rec(0, a, f) = a"
- and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
-begin
-
-definition
- add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60) where
- "m + n = rec(m, n, \<lambda>x y. Suc(y))"
-
-lemma Suc_n_not_n: "Suc(k) ~= (k::'a)"
- apply (rule_tac n = k in induct)
- apply (rule notI)
- apply (erule Suc_neq_Zero)
- apply (rule notI)
- apply (erule notE)
- apply (erule Suc_inject)
- done
-
-lemma "(k + m) + n = k + (m + n)"
- apply (rule induct)
- back
- back
- back
- back
- back
- oops
-
-lemma add_Zero [simp]: "0 + n = n"
- apply (unfold add_def)
- apply (rule rec_Zero)
- done
-
-lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)"
- apply (unfold add_def)
- apply (rule rec_Suc)
- done
-
-lemma add_assoc: "(k + m) + n = k + (m + n)"
- apply (rule_tac n = k in induct)
- apply simp
- apply simp
- done
-
-lemma add_Zero_right: "m + 0 = m"
- apply (rule_tac n = m in induct)
- apply simp
- apply simp
- done
-
-lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
- apply (rule_tac n = m in induct)
- apply simp_all
- done
-
-lemma
- assumes prem: "\<And>n. f(Suc(n)) = Suc(f(n))"
- shows "f(i + j) = i + f(j)"
- apply (rule_tac n = i in induct)
- apply simp
- apply (simp add: prem)
- done
-
-end
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Nat_Class.thy Mon Feb 16 20:15:40 2009 +0100
@@ -0,0 +1,88 @@
+(* Title: FOL/ex/Nat_Class.thy
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+theory Nat_Class
+imports FOL
+begin
+
+text {*
+ This is an abstract version of theory @{text "Nat"}. Instead of
+ axiomatizing a single type @{text nat} we define the class of all
+ these types (up to isomorphism).
+
+ Note: The @{text rec} operator had to be made \emph{monomorphic},
+ because class axioms may not contain more than one type variable.
+*}
+
+class nat =
+ fixes Zero :: 'a ("0")
+ and Suc :: "'a => 'a"
+ and rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
+ assumes induct: "P(0) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
+ and Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
+ and Suc_neq_Zero: "Suc(m) = 0 \<Longrightarrow> R"
+ and rec_Zero: "rec(0, a, f) = a"
+ and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
+begin
+
+definition
+ add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60) where
+ "m + n = rec(m, n, \<lambda>x y. Suc(y))"
+
+lemma Suc_n_not_n: "Suc(k) ~= (k::'a)"
+ apply (rule_tac n = k in induct)
+ apply (rule notI)
+ apply (erule Suc_neq_Zero)
+ apply (rule notI)
+ apply (erule notE)
+ apply (erule Suc_inject)
+ done
+
+lemma "(k + m) + n = k + (m + n)"
+ apply (rule induct)
+ back
+ back
+ back
+ back
+ back
+ oops
+
+lemma add_Zero [simp]: "0 + n = n"
+ apply (unfold add_def)
+ apply (rule rec_Zero)
+ done
+
+lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)"
+ apply (unfold add_def)
+ apply (rule rec_Suc)
+ done
+
+lemma add_assoc: "(k + m) + n = k + (m + n)"
+ apply (rule_tac n = k in induct)
+ apply simp
+ apply simp
+ done
+
+lemma add_Zero_right: "m + 0 = m"
+ apply (rule_tac n = m in induct)
+ apply simp
+ apply simp
+ done
+
+lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
+ apply (rule_tac n = m in induct)
+ apply simp_all
+ done
+
+lemma
+ assumes prem: "\<And>n. f(Suc(n)) = Suc(f(n))"
+ shows "f(i + j) = i + f(j)"
+ apply (rule_tac n = i in induct)
+ apply simp
+ apply (simp add: prem)
+ done
+
+end
+
+end
--- a/src/FOL/ex/ROOT.ML Mon Feb 16 20:07:05 2009 +0100
+++ b/src/FOL/ex/ROOT.ML Mon Feb 16 20:15:40 2009 +0100
@@ -1,7 +1,4 @@
(* Title: FOL/ex/ROOT.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
Examples for First-Order Logic.
*)
@@ -11,23 +8,19 @@
"Natural_Numbers",
"Intro",
"Nat",
+ "Nat_Class",
"Foundation",
"Prolog",
-
"Intuitionistic",
"Propositional_Int",
"Quantifiers_Int",
-
"Classical",
"Propositional_Cla",
"Quantifiers_Cla",
"Miniscope",
"If",
-
- "NatClass",
- "IffOracle"
+ "Iff_Oracle"
];
(*regression test for locales -- sets several global flags!*)
no_document use_thy "LocaleTest";
-