# HG changeset patch
# User wenzelm
# Date 1125760551 -7200
# Node ID 1c519a3cca5917802bf02de176f38d4562e68bdb
# Parent  0b2ff9541727b10c5a121e8a9a5db18653f3c028
converted to Isar theory format;

diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/List.ML
--- a/src/FOL/ex/List.ML	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/List.ML	Sat Sep 03 17:15:51 2005 +0200
@@ -2,13 +2,9 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
-
-For ex/list.thy.  Examples of simplification and induction on lists
 *)
 
-open List;
-
-val prems = goal List.thy "[| P([]);  !!x l. P(x . l) |] ==> All(P)";
+val prems = goal (the_context ()) "[| P([]);  !!x l. P(x . l) |] ==> All(P)";
 by (rtac list_ind 1);
 by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
 qed "list_exh";
@@ -62,4 +58,3 @@
 Goal "at(l1++(x . l2), len(l1)) = x";
 by (IND_TAC list_ind Simp_tac "l1" 1);
 qed "at_app_hd2";
-
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/List.thy
--- a/src/FOL/ex/List.thy	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/List.thy	Sat Sep 03 17:15:51 2005 +0200
@@ -2,48 +2,52 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
-
-Examples of simplification and induction on lists
 *)
 
-List = Nat2 +
+header {* Examples of simplification and induction on lists *}
 
-types 'a list
-arities list :: (term)term
+theory List
+imports Nat2
+begin
+
+typedecl 'a list
+arities list :: ("term") "term"
 
 consts
-   hd           :: 'a list => 'a  
-   tl           :: 'a list => 'a list
-   forall       :: ['a list, 'a => o] => o  
-   len          :: 'a list => nat  
-   at           :: ['a list, nat] => 'a  
-   Nil          :: ('a list)                         ("[]")
-   Cons         :: ['a, 'a list] => 'a list          (infixr "." 80)
-   "++"         :: ['a list, 'a list] => 'a list     (infixr 70)
+   hd           :: "'a list => 'a"
+   tl           :: "'a list => 'a list"
+   forall       :: "['a list, 'a => o] => o"
+   len          :: "'a list => nat"
+   at           :: "['a list, nat] => 'a"
+   Nil          :: "'a list"                          ("[]")
+   Cons         :: "['a, 'a list] => 'a list"         (infixr "." 80)
+   app          :: "['a list, 'a list] => 'a list"    (infixr "++" 70)
 
-rules
- list_ind "[| P([]);  ALL x l. P(l)-->P(x . l) |] ==> All(P)"
+axioms
+ list_ind: "[| P([]);  ALL x l. P(l)-->P(x . l) |] ==> All(P)"
 
- forall_cong 
+ forall_cong:
   "[| l = l';  !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
 
- list_distinct1 "~[] = x . l"
- list_distinct2 "~x . l = []"
+ list_distinct1: "~[] = x . l"
+ list_distinct2: "~x . l = []"
+
+ list_free:      "x . l = x' . l' <-> x=x' & l=l'"
 
- list_free      "x . l = x' . l' <-> x=x' & l=l'"
+ app_nil:        "[]++l = l"
+ app_cons:       "(x . l)++l' = x .(l++l')"
+ tl_eq:  "tl(m . q) = q"
+ hd_eq:  "hd(m . q) = m"
 
- app_nil        "[]++l = l"
- app_cons       "(x . l)++l' = x .(l++l')"
- tl_eq  "tl(m . q) = q"
- hd_eq  "hd(m . q) = m"
+ forall_nil: "forall([],P)"
+ forall_cons: "forall(x . l,P) <-> P(x) & forall(l,P)"
 
- forall_nil "forall([],P)"
- forall_cons "forall(x . l,P) <-> P(x) & forall(l,P)"
+ len_nil: "len([]) = 0"
+ len_cons: "len(m . q) = succ(len(q))"
 
- len_nil "len([]) = 0"
- len_cons "len(m . q) = succ(len(q))"
+ at_0: "at(m . q,0) = m"
+ at_succ: "at(m . q,succ(n)) = at(q,n)"
 
- at_0 "at(m . q,0) = m"
- at_succ "at(m . q,succ(n)) = at(q,n)"
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/Nat.ML
--- a/src/FOL/ex/Nat.ML	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/Nat.ML	Sat Sep 03 17:15:51 2005 +0200
@@ -9,8 +9,6 @@
     Pretty.setmargin 72; print_depth 0;
 *)
 
-open Nat;
-
 Goal "Suc(k) ~= k";
 by (res_inst_tac [("n","k")] induct 1);
 by (rtac notI 1);
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/Nat.thy	Sat Sep 03 17:15:51 2005 +0200
@@ -2,23 +2,31 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
-Examples for the manuals.
-
-Theory of the natural numbers: Peano's axioms, primitive recursion
 *)
 
-Nat = FOL +
-types   nat
-arities nat :: term
-consts  "0" :: nat      ("0")
-        Suc :: nat=>nat  
-        rec :: [nat, 'a, [nat,'a]=>'a] => 'a  
-        "+" :: [nat, nat] => nat                (infixl 60)
-rules   induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
-        Suc_inject  "Suc(m)=Suc(n) ==> m=n"
-        Suc_neq_0   "Suc(m)=0      ==> R"
-        rec_0       "rec(0,a,f) = a"
-        rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-        add_def     "m+n == rec(m, n, %x y. Suc(y))"
+header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
+
+theory Nat
+imports FOL
+begin
+
+typedecl nat
+arities nat :: "term"
+
+consts
+  0 :: nat    ("0")
+  Suc :: "nat => nat"
+  rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
+  add :: "[nat, nat] => nat"    (infixl "+" 60)
+
+axioms
+  induct:      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
+  Suc_inject:  "Suc(m)=Suc(n) ==> m=n"
+  Suc_neq_0:   "Suc(m)=0      ==> R"
+  rec_0:       "rec(0,a,f) = a"
+  rec_Suc:     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
+  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/Nat2.ML
--- a/src/FOL/ex/Nat2.ML	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/Nat2.ML	Sat Sep 03 17:15:51 2005 +0200
@@ -2,20 +2,15 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
-
-For ex/nat.thy.  
-Examples of simplification and induction on the natural numbers
 *)
 
-open Nat2;
-
-Addsimps [pred_0, pred_succ, plus_0, plus_succ, 
-	  nat_distinct1, nat_distinct2, succ_inject,
-	  leq_0, leq_succ_succ, leq_succ_0, 
-	  lt_0_succ, lt_succ_succ, lt_0];
+Addsimps [pred_0, pred_succ, plus_0, plus_succ,
+          nat_distinct1, nat_distinct2, succ_inject,
+          leq_0, leq_succ_succ, leq_succ_0,
+          lt_0_succ, lt_succ_succ, lt_0];
 
 
-val prems = goal Nat2.thy 
+val prems = goal (the_context ())
     "[| P(0);  !!x. P(succ(x)) |] ==> All(P)";
 by (rtac nat_ind 1);
 by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
@@ -115,7 +110,7 @@
 by (Fast_tac 1);
 qed "plus_le";
 
-val prems = goal Nat2.thy "[| ~m=0;  m <= n |] ==> ~n=0";
+val prems = goal (the_context ()) "[| ~m=0;  m <= n |] ==> ~n=0";
 by (cut_facts_tac prems 1);
 by (REPEAT (etac rev_mp 1));
 by (IND_TAC nat_exh Simp_tac "m" 1);
@@ -162,4 +157,3 @@
 by (ALL_IND_TAC nat_exh Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "less_succ";
-
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/Nat2.thy
--- a/src/FOL/ex/Nat2.thy	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/Nat2.thy	Sat Sep 03 17:15:51 2005 +0200
@@ -2,39 +2,46 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1994  University of Cambridge
-
-Theory for examples of simplification and induction on the natural numbers
 *)
 
-Nat2 = FOL +
+header {* Theory for examples of simplification and induction on the natural numbers *}
 
-types nat
-arities nat :: term
+theory Nat2
+imports FOL
+begin
+
+typedecl nat
+arities nat :: "term"
 
 consts
- succ,pred :: nat => nat  
-       "0" :: nat       ("0")
-       "+" :: [nat,nat] => nat   (infixr 90)
-  "<","<=" :: [nat,nat] => o     (infixr 70)
+  succ :: "nat => nat"
+  pred :: "nat => nat"
+  0 :: nat    ("0")
+  add :: "[nat,nat] => nat"    (infixr "+" 90)
+  lt :: "[nat,nat] => o"    (infixr "<" 70)
+  leq :: "[nat,nat] => o"    (infixr "<=" 70)
 
-rules
- pred_0         "pred(0) = 0"
- pred_succ      "pred(succ(m)) = m"
+axioms
+ pred_0:         "pred(0) = 0"
+ pred_succ:      "pred(succ(m)) = m"
 
- plus_0         "0+n = n"
- plus_succ      "succ(m)+n = succ(m+n)"
+ plus_0:         "0+n = n"
+ plus_succ:      "succ(m)+n = succ(m+n)"
 
- nat_distinct1  "~ 0=succ(n)"
- nat_distinct2  "~ succ(m)=0"
- succ_inject    "succ(m)=succ(n) <-> m=n"
+ nat_distinct1:  "~ 0=succ(n)"
+ nat_distinct2:  "~ succ(m)=0"
+ succ_inject:    "succ(m)=succ(n) <-> m=n"
+
+ leq_0:          "0 <= n"
+ leq_succ_succ:  "succ(m)<=succ(n) <-> m<=n"
+ leq_succ_0:     "~ succ(m) <= 0"
 
- leq_0          "0 <= n"
- leq_succ_succ  "succ(m)<=succ(n) <-> m<=n"
- leq_succ_0     "~ succ(m) <= 0"
+ lt_0_succ:      "0 < succ(n)"
+ lt_succ_succ:   "succ(m)<succ(n) <-> m<n"
+ lt_0:           "~ m < 0"
 
- lt_0_succ      "0 < succ(n)"
- lt_succ_succ   "succ(m)<succ(n) <-> m<n"
- lt_0 "~ m < 0"
+ nat_ind:        "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
 
- nat_ind        "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/NatClass.ML
--- a/src/FOL/ex/NatClass.ML	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/NatClass.ML	Sat Sep 03 17:15:51 2005 +0200
@@ -5,8 +5,6 @@
 This is Nat.ML trivially modified to make it work with NatClass.thy.
 *)
 
-open NatClass;
-
 Goal "Suc(k) ~= (k::'a::nat)";
 by (res_inst_tac [("n","k")] induct 1);
 by (rtac notI 1);
@@ -54,7 +52,7 @@
 by (ALLGOALS (Asm_simp_tac));
 qed "add_Suc_right";
 
-val [prem] = goal NatClass.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
+val [prem] = goal (the_context ()) "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
 by (res_inst_tac [("n","i")] induct 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [prem]) 1);
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/NatClass.thy
--- a/src/FOL/ex/NatClass.thy	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/NatClass.thy	Sat Sep 03 17:15:51 2005 +0200
@@ -1,34 +1,39 @@
 (*  Title:      FOL/ex/NatClass.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
-
-This is an abstract version of Nat.thy. Instead of axiomatizing a
-single type "nat" we define the class of all these types (up to
-isomorphism).
-
-Note: The "rec" operator had to be made 'monomorphic', because class
-axioms may not contain more than one type variable.
 *)
 
-NatClass = FOL +
+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.
+*}
 
 consts
-  "0"           :: 'a                                   ("0")
-  Suc           :: 'a => 'a  
-  rec           :: ['a, 'a, ['a, 'a] => 'a] => 'a  
+  0 :: 'a    ("0")
+  Suc :: "'a => 'a"
+  rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"
 
 axclass
-  nat < term
-  induct        "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
-  Suc_inject    "Suc(m) = Suc(n) ==> m = n"
-  Suc_neq_0     "Suc(m) = 0 ==> R"
-  rec_0         "rec(0, a, f) = a"
-  rec_Suc       "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
+  nat < "term"
+  induct:        "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
+  Suc_inject:    "Suc(m) = Suc(n) ==> m = n"
+  Suc_neq_0:     "Suc(m) = 0 ==> R"
+  rec_0:         "rec(0, a, f) = a"
+  rec_Suc:       "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
 
-consts
-  "+"           :: "['a::nat, 'a] => 'a"                (infixl 60)
+constdefs
+  add :: "['a::nat, 'a] => 'a"    (infixl "+" 60)
+  "m + n == rec(m, n, %x y. Suc(y))"
 
-defs
-  add_def       "m + n == rec(m, n, %x y. Suc(y))"
+ML {* use_legacy_bindings (the_context ()) *}
+ML {* open nat *}
 
 end
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/Prolog.ML
--- a/src/FOL/ex/Prolog.ML	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/Prolog.ML	Sat Sep 03 17:15:51 2005 +0200
@@ -2,12 +2,8 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
-For ex/prolog.thy.  First-Order Logic: PROLOG examples
 *)
 
-open Prolog;
-
 Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
 by (resolve_tac [appNil,appCons] 1);
 by (resolve_tac [appNil,appCons] 1);
@@ -70,5 +66,3 @@
 by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
 (*Poly/ML: 29 secs >> 20 lips*)
 result();
-
-writeln"Reached end of file.";
diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/Prolog.thy	Sat Sep 03 17:15:51 2005 +0200
@@ -2,21 +2,27 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
-First-Order Logic: PROLOG examples
-
-Inherits from FOL the class term, the type o, and the coercion Trueprop
 *)
 
-Prolog = FOL +
-types   'a list
-arities list    :: (term)term
-consts  Nil     :: 'a list
-        ":"     :: ['a, 'a list]=> 'a list              (infixr 60)
-        app     :: ['a list, 'a list, 'a list] => o  
-        rev     :: ['a list, 'a list] => o  
-rules   appNil  "app(Nil,ys,ys)"
-        appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
-        revNil  "rev(Nil,Nil)"
-        revCons "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
+header {* First-Order Logic: PROLOG examples *}
+
+theory Prolog
+imports FOL
+begin
+
+typedecl 'a list
+arities list :: ("term") "term"
+consts
+  Nil     :: "'a list"
+  Cons    :: "['a, 'a list]=> 'a list"    (infixr ":" 60)
+  app     :: "['a list, 'a list, 'a list] => o"
+  rev     :: "['a list, 'a list] => o"
+axioms
+  appNil:  "app(Nil,ys,ys)"
+  appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
+  revNil:  "rev(Nil,Nil)"
+  revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end