1.1 --- a/doc-src/IsarRef/Thy/Spec.thy Mon Feb 16 20:07:05 2009 +0100
1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy Mon Feb 16 20:15:40 2009 +0100
1.3 @@ -1182,7 +1182,7 @@
1.4
1.5 \end{description}
1.6
1.7 - See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
1.8 + See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
1.9 defining a new primitive rule as oracle, and turning it into a proof
1.10 method.
1.11 *}
2.1 --- a/src/FOL/IsaMakefile Mon Feb 16 20:07:05 2009 +0100
2.2 +++ b/src/FOL/IsaMakefile Mon Feb 16 20:15:40 2009 +0100
2.3 @@ -46,12 +46,12 @@
2.4 FOL-ex: FOL $(LOG)/FOL-ex.gz
2.5
2.6 $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \
2.7 - ex/IffOracle.thy ex/Nat.thy ex/Natural_Numbers.thy \
2.8 - ex/LocaleTest.thy \
2.9 - ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy \
2.10 - ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy \
2.11 - ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy \
2.12 - ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
2.13 + ex/Iff_Oracle.thy ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \
2.14 + ex/LocaleTest.thy ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML \
2.15 + ex/Classical.thy ex/document/root.tex ex/Foundation.thy \
2.16 + ex/Intuitionistic.thy ex/Intro.thy ex/Propositional_Int.thy \
2.17 + ex/Propositional_Cla.thy ex/Quantifiers_Int.thy \
2.18 + ex/Quantifiers_Cla.thy
2.19 @$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
2.20
2.21
3.1 --- a/src/FOL/ex/IffOracle.thy Mon Feb 16 20:07:05 2009 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,77 +0,0 @@
3.4 -(* Title: FOL/ex/IffOracle.thy
3.5 - ID: $Id$
3.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3.7 - Copyright 1996 University of Cambridge
3.8 -*)
3.9 -
3.10 -header {* Example of Declaring an Oracle *}
3.11 -
3.12 -theory IffOracle
3.13 -imports FOL
3.14 -begin
3.15 -
3.16 -subsection {* Oracle declaration *}
3.17 -
3.18 -text {*
3.19 - This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}.
3.20 - The length is specified by an integer, which is checked to be even
3.21 - and positive.
3.22 -*}
3.23 -
3.24 -oracle iff_oracle = {*
3.25 - let
3.26 - fun mk_iff 1 = Var (("P", 0), @{typ o})
3.27 - | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
3.28 - in
3.29 - fn (thy, n) =>
3.30 - if n > 0 andalso n mod 2 = 0
3.31 - then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
3.32 - else raise Fail ("iff_oracle: " ^ string_of_int n)
3.33 - end
3.34 -*}
3.35 -
3.36 -
3.37 -subsection {* Oracle as low-level rule *}
3.38 -
3.39 -ML {* iff_oracle (@{theory}, 2) *}
3.40 -ML {* iff_oracle (@{theory}, 10) *}
3.41 -ML {* Thm.proof_of (iff_oracle (@{theory}, 10)) *}
3.42 -
3.43 -text {* These oracle calls had better fail. *}
3.44 -
3.45 -ML {*
3.46 - (iff_oracle (@{theory}, 5); error "?")
3.47 - handle Fail _ => warning "Oracle failed, as expected"
3.48 -*}
3.49 -
3.50 -ML {*
3.51 - (iff_oracle (@{theory}, 1); error "?")
3.52 - handle Fail _ => warning "Oracle failed, as expected"
3.53 -*}
3.54 -
3.55 -
3.56 -subsection {* Oracle as proof method *}
3.57 -
3.58 -method_setup iff = {*
3.59 - Method.simple_args OuterParse.nat (fn n => fn ctxt =>
3.60 - Method.SIMPLE_METHOD
3.61 - (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
3.62 - handle Fail _ => no_tac))
3.63 -*} "iff oracle"
3.64 -
3.65 -
3.66 -lemma "A <-> A"
3.67 - by (iff 2)
3.68 -
3.69 -lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
3.70 - by (iff 10)
3.71 -
3.72 -lemma "A <-> A <-> A <-> A <-> A"
3.73 - apply (iff 5)?
3.74 - oops
3.75 -
3.76 -lemma A
3.77 - apply (iff 1)?
3.78 - oops
3.79 -
3.80 -end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/FOL/ex/Iff_Oracle.thy Mon Feb 16 20:15:40 2009 +0100
4.3 @@ -0,0 +1,76 @@
4.4 +(* Title: FOL/ex/Iff_Oracle.thy
4.5 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4.6 + Copyright 1996 University of Cambridge
4.7 +*)
4.8 +
4.9 +header {* Example of Declaring an Oracle *}
4.10 +
4.11 +theory Iff_Oracle
4.12 +imports FOL
4.13 +begin
4.14 +
4.15 +subsection {* Oracle declaration *}
4.16 +
4.17 +text {*
4.18 + This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}.
4.19 + The length is specified by an integer, which is checked to be even
4.20 + and positive.
4.21 +*}
4.22 +
4.23 +oracle iff_oracle = {*
4.24 + let
4.25 + fun mk_iff 1 = Var (("P", 0), @{typ o})
4.26 + | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
4.27 + in
4.28 + fn (thy, n) =>
4.29 + if n > 0 andalso n mod 2 = 0
4.30 + then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
4.31 + else raise Fail ("iff_oracle: " ^ string_of_int n)
4.32 + end
4.33 +*}
4.34 +
4.35 +
4.36 +subsection {* Oracle as low-level rule *}
4.37 +
4.38 +ML {* iff_oracle (@{theory}, 2) *}
4.39 +ML {* iff_oracle (@{theory}, 10) *}
4.40 +ML {* Thm.proof_of (iff_oracle (@{theory}, 10)) *}
4.41 +
4.42 +text {* These oracle calls had better fail. *}
4.43 +
4.44 +ML {*
4.45 + (iff_oracle (@{theory}, 5); error "?")
4.46 + handle Fail _ => warning "Oracle failed, as expected"
4.47 +*}
4.48 +
4.49 +ML {*
4.50 + (iff_oracle (@{theory}, 1); error "?")
4.51 + handle Fail _ => warning "Oracle failed, as expected"
4.52 +*}
4.53 +
4.54 +
4.55 +subsection {* Oracle as proof method *}
4.56 +
4.57 +method_setup iff = {*
4.58 + Method.simple_args OuterParse.nat (fn n => fn ctxt =>
4.59 + Method.SIMPLE_METHOD
4.60 + (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
4.61 + handle Fail _ => no_tac))
4.62 +*} "iff oracle"
4.63 +
4.64 +
4.65 +lemma "A <-> A"
4.66 + by (iff 2)
4.67 +
4.68 +lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
4.69 + by (iff 10)
4.70 +
4.71 +lemma "A <-> A <-> A <-> A <-> A"
4.72 + apply (iff 5)?
4.73 + oops
4.74 +
4.75 +lemma A
4.76 + apply (iff 1)?
4.77 + oops
4.78 +
4.79 +end
5.1 --- a/src/FOL/ex/NatClass.thy Mon Feb 16 20:07:05 2009 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,88 +0,0 @@
5.4 -(* Title: FOL/ex/NatClass.thy
5.5 - Author: Markus Wenzel, TU Muenchen
5.6 -*)
5.7 -
5.8 -theory NatClass
5.9 -imports FOL
5.10 -begin
5.11 -
5.12 -text {*
5.13 - This is an abstract version of theory @{text "Nat"}. Instead of
5.14 - axiomatizing a single type @{text nat} we define the class of all
5.15 - these types (up to isomorphism).
5.16 -
5.17 - Note: The @{text rec} operator had to be made \emph{monomorphic},
5.18 - because class axioms may not contain more than one type variable.
5.19 -*}
5.20 -
5.21 -class nat =
5.22 - fixes Zero :: 'a ("0")
5.23 - and Suc :: "'a => 'a"
5.24 - and rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
5.25 - assumes induct: "P(0) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
5.26 - and Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
5.27 - and Suc_neq_Zero: "Suc(m) = 0 \<Longrightarrow> R"
5.28 - and rec_Zero: "rec(0, a, f) = a"
5.29 - and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
5.30 -begin
5.31 -
5.32 -definition
5.33 - add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60) where
5.34 - "m + n = rec(m, n, \<lambda>x y. Suc(y))"
5.35 -
5.36 -lemma Suc_n_not_n: "Suc(k) ~= (k::'a)"
5.37 - apply (rule_tac n = k in induct)
5.38 - apply (rule notI)
5.39 - apply (erule Suc_neq_Zero)
5.40 - apply (rule notI)
5.41 - apply (erule notE)
5.42 - apply (erule Suc_inject)
5.43 - done
5.44 -
5.45 -lemma "(k + m) + n = k + (m + n)"
5.46 - apply (rule induct)
5.47 - back
5.48 - back
5.49 - back
5.50 - back
5.51 - back
5.52 - oops
5.53 -
5.54 -lemma add_Zero [simp]: "0 + n = n"
5.55 - apply (unfold add_def)
5.56 - apply (rule rec_Zero)
5.57 - done
5.58 -
5.59 -lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)"
5.60 - apply (unfold add_def)
5.61 - apply (rule rec_Suc)
5.62 - done
5.63 -
5.64 -lemma add_assoc: "(k + m) + n = k + (m + n)"
5.65 - apply (rule_tac n = k in induct)
5.66 - apply simp
5.67 - apply simp
5.68 - done
5.69 -
5.70 -lemma add_Zero_right: "m + 0 = m"
5.71 - apply (rule_tac n = m in induct)
5.72 - apply simp
5.73 - apply simp
5.74 - done
5.75 -
5.76 -lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
5.77 - apply (rule_tac n = m in induct)
5.78 - apply simp_all
5.79 - done
5.80 -
5.81 -lemma
5.82 - assumes prem: "\<And>n. f(Suc(n)) = Suc(f(n))"
5.83 - shows "f(i + j) = i + f(j)"
5.84 - apply (rule_tac n = i in induct)
5.85 - apply simp
5.86 - apply (simp add: prem)
5.87 - done
5.88 -
5.89 -end
5.90 -
5.91 -end
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/FOL/ex/Nat_Class.thy Mon Feb 16 20:15:40 2009 +0100
6.3 @@ -0,0 +1,88 @@
6.4 +(* Title: FOL/ex/Nat_Class.thy
6.5 + Author: Markus Wenzel, TU Muenchen
6.6 +*)
6.7 +
6.8 +theory Nat_Class
6.9 +imports FOL
6.10 +begin
6.11 +
6.12 +text {*
6.13 + This is an abstract version of theory @{text "Nat"}. Instead of
6.14 + axiomatizing a single type @{text nat} we define the class of all
6.15 + these types (up to isomorphism).
6.16 +
6.17 + Note: The @{text rec} operator had to be made \emph{monomorphic},
6.18 + because class axioms may not contain more than one type variable.
6.19 +*}
6.20 +
6.21 +class nat =
6.22 + fixes Zero :: 'a ("0")
6.23 + and Suc :: "'a => 'a"
6.24 + and rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
6.25 + assumes induct: "P(0) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
6.26 + and Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
6.27 + and Suc_neq_Zero: "Suc(m) = 0 \<Longrightarrow> R"
6.28 + and rec_Zero: "rec(0, a, f) = a"
6.29 + and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
6.30 +begin
6.31 +
6.32 +definition
6.33 + add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60) where
6.34 + "m + n = rec(m, n, \<lambda>x y. Suc(y))"
6.35 +
6.36 +lemma Suc_n_not_n: "Suc(k) ~= (k::'a)"
6.37 + apply (rule_tac n = k in induct)
6.38 + apply (rule notI)
6.39 + apply (erule Suc_neq_Zero)
6.40 + apply (rule notI)
6.41 + apply (erule notE)
6.42 + apply (erule Suc_inject)
6.43 + done
6.44 +
6.45 +lemma "(k + m) + n = k + (m + n)"
6.46 + apply (rule induct)
6.47 + back
6.48 + back
6.49 + back
6.50 + back
6.51 + back
6.52 + oops
6.53 +
6.54 +lemma add_Zero [simp]: "0 + n = n"
6.55 + apply (unfold add_def)
6.56 + apply (rule rec_Zero)
6.57 + done
6.58 +
6.59 +lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)"
6.60 + apply (unfold add_def)
6.61 + apply (rule rec_Suc)
6.62 + done
6.63 +
6.64 +lemma add_assoc: "(k + m) + n = k + (m + n)"
6.65 + apply (rule_tac n = k in induct)
6.66 + apply simp
6.67 + apply simp
6.68 + done
6.69 +
6.70 +lemma add_Zero_right: "m + 0 = m"
6.71 + apply (rule_tac n = m in induct)
6.72 + apply simp
6.73 + apply simp
6.74 + done
6.75 +
6.76 +lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
6.77 + apply (rule_tac n = m in induct)
6.78 + apply simp_all
6.79 + done
6.80 +
6.81 +lemma
6.82 + assumes prem: "\<And>n. f(Suc(n)) = Suc(f(n))"
6.83 + shows "f(i + j) = i + f(j)"
6.84 + apply (rule_tac n = i in induct)
6.85 + apply simp
6.86 + apply (simp add: prem)
6.87 + done
6.88 +
6.89 +end
6.90 +
6.91 +end
7.1 --- a/src/FOL/ex/ROOT.ML Mon Feb 16 20:07:05 2009 +0100
7.2 +++ b/src/FOL/ex/ROOT.ML Mon Feb 16 20:15:40 2009 +0100
7.3 @@ -1,7 +1,4 @@
7.4 (* Title: FOL/ex/ROOT.ML
7.5 - ID: $Id$
7.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7.7 - Copyright 1992 University of Cambridge
7.8
7.9 Examples for First-Order Logic.
7.10 *)
7.11 @@ -11,23 +8,19 @@
7.12 "Natural_Numbers",
7.13 "Intro",
7.14 "Nat",
7.15 + "Nat_Class",
7.16 "Foundation",
7.17 "Prolog",
7.18 -
7.19 "Intuitionistic",
7.20 "Propositional_Int",
7.21 "Quantifiers_Int",
7.22 -
7.23 "Classical",
7.24 "Propositional_Cla",
7.25 "Quantifiers_Cla",
7.26 "Miniscope",
7.27 "If",
7.28 -
7.29 - "NatClass",
7.30 - "IffOracle"
7.31 + "Iff_Oracle"
7.32 ];
7.33
7.34 (*regression test for locales -- sets several global flags!*)
7.35 no_document use_thy "LocaleTest";
7.36 -