--- 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";
-
--- 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
--- 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);
--- 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
--- 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";
-
--- 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
--- 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);
--- 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
--- 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.";
--- 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