--- a/src/HOL/ex/LocaleGroup.thy Wed Nov 11 15:44:24 1998 +0100
+++ b/src/HOL/ex/LocaleGroup.thy Wed Nov 11 15:45:32 1998 +0100
@@ -15,24 +15,27 @@
constdefs
Group :: "('a, 'more) grouptype_scheme set"
- "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G & inverse G : carrier G -> carrier G
+ "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G &
+ inverse G : carrier G -> carrier G
& unit G : carrier G &
(! x: carrier G. ! y: carrier G. !z: carrier G.
(bin_op G (inverse G x) x = unit G)
& (bin_op G (unit G) x = x)
- & (bin_op G (bin_op G x y) z = bin_op G (x) (bin_op G y z)))}"
+ & (bin_op G (bin_op G x y) z =
+ bin_op G (x) (bin_op G y z)))}"
locale groups =
fixes
G ::"('a, 'more :: more) grouptype_scheme"
e :: "'a"
binop :: "'a => 'a => 'a" (infixr "#" 80)
- inv :: "'a => 'a" ("_ -|" [90]91)
+ (*INV renamed from inv temporarily to avoid clash with Fun.inv*)
+ INV :: "'a => 'a" ("_ -|" [90]91)
assumes
Group_G "G: Group"
defines
- e_def "e == unit G"
- binop_def "x # y == bin_op G x y"
- inv_def "x -| == inverse G x"
+ e_def "e == unit G"
+ binop_def "x # y == bin_op G x y"
+ inv_def "INV == inverse G"
end
--- a/src/HOL/ex/PiSets.thy Wed Nov 11 15:44:24 1998 +0100
+++ b/src/HOL/ex/PiSets.thy Wed Nov 11 15:45:32 1998 +0100
@@ -7,60 +7,42 @@
PiSets = Univ + Finite +
-consts
- Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
+
-consts
- restrict :: "['a => 'b, 'a set] => ('a => 'b)"
+constdefs
+ Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
+ "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
-defs
- restrict_def "restrict f A == (%x. if x : A then f x else (@ y. True))"
+ restrict :: "['a => 'b, 'a set] => ('a => 'b)"
+ "restrict f A == (%x. if x : A then f x else (@ y. True))"
syntax
- "@Pi" :: "[idt, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
- "@->" :: "['a set, 'b set] => ('a => 'b) set" ("_ -> _" [91,90]90)
+ "@Pi" :: "[idt, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
+ "@->" :: "['a set, 'b set] => ('a => 'b) set" ("_ -> _" [91,90]90)
(* or "->" ... (infixr 60) and at the end print_translation (... op ->) *)
- "@lam" :: "[idt, 'a set, 'a => 'b] => ('a => 'b)" ("(3lam _:_./ _)" 10)
-(* Could as well take pttrn *)
+ "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3lam _:_./ _)" 10)
translations
"PI x:A. B" => "Pi A (%x. B)"
- "A -> B" => "Pi A (_K B)"
+ "A -> B" => "Pi A (_K B)"
"lam x:A. f" == "restrict (%x. f) A"
-(* Larry fragen: "lam (x,y): A. f" == "restrict (%(x,y). f) A" *)
-defs
- Pi_def "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
-
-consts
- Fset_apply :: "[('a => 'b) set, 'a]=> 'b set" ("_ @@ _" [90,91]90)
-defs
- Fset_apply_def "F @@ a == (%f. f a) `` F"
+constdefs
+ Fset_apply :: "[('a => 'b) set, 'a]=> 'b set" ("_ @@ _" [90,91]90)
+ "F @@ a == (%f. f a) `` F"
-consts
compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
-
-defs
- compose_def "compose A g f == lam x : A. g(f x)"
+ "compose A g f == lam x : A. g(f x)"
-consts
Inv :: "['a set, 'a => 'b] => ('b => 'a)"
+ "Inv A f == (% x. (@ y. y : A & f y = x))"
-defs
- Inv_def "Inv A f == (% x. (@ y. y : A & f y = x))"
-
-(* new: bijection between Pi_sig and Pi_=> *)
-consts
+(* bijection between Pi_sig and Pi_=> *)
PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
-
-defs
- PiBij_def "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
+ "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
-consts
Graph :: "['a set, 'a => 'b set] => ('a * 'b) set set"
-
-defs
- Graph_def "Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}"
+ "Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}"
end
--- a/src/HOL/ex/Points.ML Wed Nov 11 15:44:24 1998 +0100
+++ b/src/HOL/ex/Points.ML Wed Nov 11 15:45:32 1998 +0100
@@ -1,27 +1,33 @@
+(* Title: HOL/ex/Points.thy
+ ID: $Id$
+ Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
-(*Note: any of these goals may be solved by a single stroke of
- auto(); or force 1;*)
+Basic use of extensible records in HOL, including the famous points
+and coloured points.
+
+Note: any of these goals may be solved at a stroke by Auto_tac or Force_tac
+*)
(* some basic simplifications *)
-Goal "!!m n p. x (| x = m, y = n, ... = p |) = m";
+Goal "x (| x = m, y = n, ... = p |) = m";
by (Simp_tac 1);
result();
-Goal "!!m n p. (| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
+Goal "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
by (Simp_tac 1);
result();
-(* splitting quantifiers *)
+(* splitting quantifiers: the !!r is NECESSARY *)
-Goal "!!r m n. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
+Goal "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
by (record_split_tac 1);
by (Simp_tac 1);
result();
-Goal "!!r m n. r (| x := n |) (| x := m |) = r (| x := m |)";
+Goal "!!r. r (| x := n |) (| x := m |) = r (| x := m |)";
by (record_split_tac 1);
by (Simp_tac 1);
result();
@@ -29,7 +35,7 @@
(* record equality *)
-Goal "!!r. (| x = n, y = p |) = (| x = n', y = p' |) & n = 0 ==> n' = 0";
+Goal "(| x = n, y = p |) = (| x = n', y = p' |) & n = 0 ==> n' = 0";
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
result();