# HG changeset patch # User wenzelm # Date 909167313 -7200 # Node ID c90b5f7d0c613025d49bea5c83b9105b3fffe0df # Parent c3df312f34a2bed017cec7cc550e2534849f031d tuned; diff -r c3df312f34a2 -r c90b5f7d0c61 src/HOL/ex/Points.ML --- a/src/HOL/ex/Points.ML Fri Oct 23 19:40:00 1998 +0200 +++ b/src/HOL/ex/Points.ML Fri Oct 23 20:28:33 1998 +0200 @@ -1,32 +1,40 @@ -(** some basic simplifiactions **) +(*Note: any of these goals may be solved by a single stroke of + auto(); or force 1;*) + + +(* some basic simplifications *) Goal "!!m n p. 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 |)"; by (Simp_tac 1); +result(); - -(** splitting **) +(* splitting quantifiers *) Goal "!!r m n. 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 |)"; by (record_split_tac 1); by (Simp_tac 1); +result(); - -(** Equality **) +(* record equality *) Goal "!!r. (| x = n, y = p |) = (| x = n', y = p' |) & n = 0 ==> n' = 0"; by (Asm_full_simp_tac 1); -by (Fast_tac 1); +by (Blast_tac 1); +result(); Goalw [getX_def, setX_def, incX_def] "!!r n. incX r = setX r (Suc (getX r))"; by (record_split_tac 1); -by (Simp_tac 1); \ No newline at end of file +by (Simp_tac 1); +result(); diff -r c3df312f34a2 -r c90b5f7d0c61 src/HOL/ex/Points.thy --- a/src/HOL/ex/Points.thy Fri Oct 23 19:40:00 1998 +0200 +++ b/src/HOL/ex/Points.thy Fri Oct 23 20:28:33 1998 +0200 @@ -1,28 +1,41 @@ +(* Title: HOL/ex/Points.thy + ID: $Id$ + Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen -Points = Main + +Basic use of extensible records in HOL, including the famous points +and coloured points. +*) + +Points = Main + -(** To find out, which theorems are produced by the record delaration, **) -(** type the following commands in Isabelle **) -(** - thms "point.simps"; **) -(** - thms "point.iffs"; **) -(** - thms "point.update_defs"; **) -(** **) -(** The set of theorems "point.simps" is added automatically **) -(** to the standard simpset **) - +(** points **) record point = x :: nat y :: nat +(* + To find out, which theorems are produced by the record declaration, + type the following commands: + + thms "point.simps"; + thms "point.iffs"; + thms "point.update_defs"; + + The set of theorems "point.simps" is added automatically to the + standard simpset, "point.iffs" is added to the claset and simpset. +*) -(** Record declarations define new type constructors: **) -(** point = (| x :: nat, y :: nat |) **) -(** 'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |) **) -(** **) -(** Extensions must be in type class 'more'!!! **) +(* + Record declarations define new type abbreviations: + + point = (| x :: nat, y :: nat |) + 'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |) + + Extensions `...' must be in type class `more'! +*) consts foo1 :: point consts foo2 :: "(| x :: nat, y :: nat |)" @@ -30,48 +43,43 @@ consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)" +(* Introducing concrete records and record schemes *) -(** Introducing concrete records and record schemes **) - -defs +defs foo1_def "foo1 == (| x = 1, y = 0 |)" foo3_def "foo3 ext == (| x = 1, y = 0, ... = ext |)" +(* Record selection and record update *) -(** Record selection and record update **) - -constdefs +constdefs getX :: ('a::more) point_scheme => nat "getX r == x r" setX :: ('a::more) point_scheme => nat => 'a point_scheme "setX r n == r (| x := n |)" - -(** Concrete records are type instances of record schemes **) +(* concrete records are type instances of record schemes *) constdefs foo5 :: nat - "foo5 == getX (| x = 1, y = 0 |)" + "foo5 == getX (| x = 1, y = 0 |)" - -(** Binding the "..." (more-part) **) +(* manipulating the `...' (more-part) *) constdefs incX :: ('a::more) point_scheme => 'a point_scheme - "incX r == (| x = Suc (x r), y = (y r), ... = (point.more r) |)" + "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)" -(* Alternative *) - +(*alternative definition*) constdefs incX' :: ('a::more) point_scheme => 'a point_scheme "incX' r == r (| x := Suc (x r) |)" -(** Record extension **) +(** coloured points: record extension **) datatype colour = Red | Green | Blue @@ -79,10 +87,12 @@ colour :: colour +(* + The record declaration defines new type constructors: -(** The record declaration defines new type constructors: **) -(** cpoint = (| x :: nat, y :: nat, colour :: colour |) **) -(** 'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |) **) + cpoint = (| x :: nat, y :: nat, colour :: colour |) + 'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |) +*) consts foo6 :: cpoint consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)" @@ -90,25 +100,25 @@ consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)" +(* functions on point schemes work for cpoints as well *) -(** Functions on point schemes work for cpoints as well **) - -constdefs +constdefs foo10 :: nat "foo10 == getX (| x = 2, y = 0, colour = Blue |)" - -(** Subtyping is _not_ destructive !! **) -(** foo11 hast type cpoint, not type point **) +(* non-coercive structural subtyping *) -constdefs +(*foo11 has type cpoint, not type point*) (*Great!*) +constdefs foo11 :: cpoint - "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0" + "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0" -(** Field names contribute to identity **) +(** other features **) + +(* field names contribute to record identity *) record point' = x' :: nat @@ -116,29 +126,18 @@ consts foo12 :: nat -(* invalid *) -(* "foo12 == getX (| x' = 2, y' = 0 |)" *) +(*"foo12 == getX (| x' = 2, y' = 0 |)"*) (*invalid*) - -(** Polymorphic records **) +(* polymorphic records *) record 'a point'' = point + content :: 'a - - -(** Instantiating type variables **) - types cpoint'' = colour point'' -(** Have a lot of fun !!! **) +(*Have a lot of fun!*) end - - - - - diff -r c3df312f34a2 -r c90b5f7d0c61 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Fri Oct 23 19:40:00 1998 +0200 +++ b/src/HOL/ex/ROOT.ML Fri Oct 23 20:28:33 1998 +0200 @@ -11,7 +11,7 @@ writeln "Root file for HOL examples"; set proof_timing; -(**Some examples of recursive function definitions: the TFL package**) +(*some examples of recursive function definitions: the TFL package*) time_use_thy "Recdefs"; time_use_thy "Primes"; time_use_thy "Fib"; @@ -35,14 +35,15 @@ time_use_thy "StringEx"; time_use_thy "BinEx"; -(*Monoids and Groups as predicates over record schemes*) +(*basic use of extensible records*) time_use_thy "MonoidGroup"; +time_use_thy "Points"; -(*Groups via locales*) +(*groups via locales*) time_use_thy "PiSets"; time_use_thy "LocaleGroup"; -(*Expressions with quote / antiquote*) +(*expressions with quote / antiquote syntax*) time_use_thy "Antiquote";