# HG changeset patch # User wenzelm # Date 1234811740 -3600 # Node ID ad4e3a577fd30a0418dba9e4942318ce926cf960 # Parent e2756594c4144e19d45448588808c5438e3050f3 modernized some theory names; diff -r e2756594c414 -r ad4e3a577fd3 doc-src/IsarRef/Thy/Spec.thy --- 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. *} diff -r e2756594c414 -r ad4e3a577fd3 src/FOL/IsaMakefile --- 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 diff -r e2756594c414 -r ad4e3a577fd3 src/FOL/ex/IffOracle.thy --- 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 diff -r e2756594c414 -r ad4e3a577fd3 src/FOL/ex/Iff_Oracle.thy --- /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 diff -r e2756594c414 -r ad4e3a577fd3 src/FOL/ex/NatClass.thy --- 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 \ 'a \ ('a \ 'a \ 'a) \ 'a" - assumes induct: "P(0) \ (\x. P(x) \ P(Suc(x))) \ P(n)" - and Suc_inject: "Suc(m) = Suc(n) \ m = n" - and Suc_neq_Zero: "Suc(m) = 0 \ 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 \ 'a \ 'a" (infixl "+" 60) where - "m + n = rec(m, n, \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: "\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 diff -r e2756594c414 -r ad4e3a577fd3 src/FOL/ex/Nat_Class.thy --- /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 \ 'a \ ('a \ 'a \ 'a) \ 'a" + assumes induct: "P(0) \ (\x. P(x) \ P(Suc(x))) \ P(n)" + and Suc_inject: "Suc(m) = Suc(n) \ m = n" + and Suc_neq_Zero: "Suc(m) = 0 \ 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 \ 'a \ 'a" (infixl "+" 60) where + "m + n = rec(m, n, \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: "\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 diff -r e2756594c414 -r ad4e3a577fd3 src/FOL/ex/ROOT.ML --- 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"; -