# HG changeset patch # User wenzelm # Date 780154841 -7200 # Node ID a9f7ff3a464ca42bfa5d660f552ec2eedaf84a8a # Parent 6254f50e5ec959f80a288ad36dfc71094573b9cd minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; diff -r 6254f50e5ec9 -r a9f7ff3a464c Arith.thy --- a/Arith.thy Fri Sep 16 15:48:20 1994 +0200 +++ b/Arith.thy Wed Sep 21 15:40:41 1994 +0200 @@ -1,24 +1,26 @@ -(* Title: HOL/arith.thy +(* Title: HOL/Arith.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Arithmetic operators and their definitions *) Arith = Nat + -arities nat::plus - nat::minus - nat::times + +instance + nat :: {plus, minus, times} + consts - pred :: "nat => nat" - div,mod :: "[nat,nat]=>nat" (infixl 70) -rules + pred :: "nat => nat" + div, mod :: "[nat, nat] => nat" (infixl 70) + +defs pred_def "pred(m) == nat_rec(m, 0, %n r.n)" - add_def "m+n == nat_rec(m, n, %u v. Suc(v))" - diff_def "m-n == nat_rec(n, m, %u v. pred(v))" - mult_def "m*n == nat_rec(m, 0, %u v. n + v)" - mod_def "m mod n == wfrec(trancl(pred_nat), m, %j f. if(jn. Also, nat_rec(m, 0, %z w.z) is pred(m). *) + diff -r 6254f50e5ec9 -r a9f7ff3a464c HOL.thy --- a/HOL.thy Fri Sep 16 15:48:20 1994 +0200 +++ b/HOL.thy Wed Sep 21 15:40:41 1994 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/hol.thy +(* Title: HOL/HOL.thy ID: $Id$ Author: Tobias Nipkow Copyright 1993 University of Cambridge @@ -10,8 +10,14 @@ classes term < logic + +axclass plus < term + +axclass minus < term + +axclass times < term default @@ -19,8 +25,6 @@ types bool - letbinds letbind - case_syn cases_syn arities fun :: (term, term) term @@ -43,31 +47,13 @@ All :: "('a => bool) => bool" (binder "! " 10) Ex :: "('a => bool) => bool" (binder "? " 10) Ex1 :: "('a => bool) => bool" (binder "?! " 10) - Let :: "['a, 'a => 'b] => 'b" - "_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10) - "" :: "letbind => letbinds" ("_") - "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") - "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) - - (* Case expressions *) - - "@case" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) - "@case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) - "" :: "case_syn => cases_syn" ("_") - "@case2" :: "[case_syn,cases_syn] => cases_syn" ("_/ | _") - - (* Alternative Quantifiers *) - - "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) - "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) - "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) (* Infixes *) o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) "=" :: "['a, 'a] => bool" (infixl 50) - "~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [50, 51] 50) +(*"~=" :: "['a, 'a] => bool" (infixl 50)*) "&" :: "[bool, bool] => bool" (infixr 35) "|" :: "[bool, bool] => bool" (infixr 30) "-->" :: "[bool, bool] => bool" (infixr 25) @@ -79,13 +65,42 @@ "*" :: "['a::times, 'a] => 'a" (infixl 70) +types + letbinds letbind + case_syn cases_syn + +syntax + + "~=" :: "['a, 'a] => bool" (infixl 50) + + (* Alternative Quantifiers *) + + "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) + "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) + "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) + + (* Let expressions *) + + "_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10) + "" :: "letbind => letbinds" ("_") + "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") + "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) + + (* Case expressions *) + + "@case" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) + "@case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) + "" :: "case_syn => cases_syn" ("_") + "@case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") + translations + "x ~= y" == "~ (x = y)" "ALL xs. P" => "! xs. P" "EX xs. P" => "? xs. P" "EX! xs. P" => "?! xs. P" - "x ~= y" == "~ (x = y)" - "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" - "let x = a in e" == "Let(a, %x. e)" + "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" + "let x = a in e" == "Let(a, %x. e)" + rules @@ -103,15 +118,15 @@ (* Definitions *) - True_def "True == ((%x::bool.x)=(%x.x))" - All_def "All(P) == (P = (%x.True))" - Ex_def "Ex(P) == P(@x.P(x))" - False_def "False == (!P.P)" - not_def "~ P == P-->False" - and_def "P & Q == !R. (P-->Q-->R) --> R" - or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R" - Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" - Let_def "Let(s,f) == f(s)" + True_def "True == ((%x::bool.x)=(%x.x))" + All_def "All(P) == (P = (%x.True))" + Ex_def "Ex(P) == P(@x.P(x))" + False_def "False == (!P.P)" + not_def "~ P == P-->False" + and_def "P & Q == !R. (P-->Q-->R) --> R" + or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R" + Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" + Let_def "Let(s, f) == f(s)" (* Axioms *) diff -r 6254f50e5ec9 -r a9f7ff3a464c Nat.thy --- a/Nat.thy Fri Sep 16 15:48:20 1994 +0200 +++ b/Nat.thy Wed Sep 21 15:40:41 1994 +0200 @@ -1,6 +1,6 @@ -(* Title: HOL/nat +(* Title: HOL/Nat.thy ID: $Id$ - Author: Tobias Nipkow, Cambridge University Computer Laboratory + Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Definition of types ind and nat. @@ -15,45 +15,48 @@ nat arities - ind,nat :: term - nat :: ord + ind, nat :: term + +instance + nat :: ord consts - Zero_Rep :: "ind" - Suc_Rep :: "ind => ind" - Nat :: "ind set" - Rep_Nat :: "nat => ind" - Abs_Nat :: "ind => nat" - Suc :: "nat => nat" - nat_case :: "['a, nat=>'a, nat] =>'a" - pred_nat :: "(nat*nat) set" - nat_rec :: "[nat, 'a, [nat, 'a]=>'a] => 'a" - "0" :: "nat" ("0") + Zero_Rep :: "ind" + Suc_Rep :: "ind => ind" + Nat :: "ind set" + Rep_Nat :: "nat => ind" + Abs_Nat :: "ind => nat" + Suc :: "nat => nat" + nat_case :: "['a, nat=>'a, nat] =>'a" + pred_nat :: "(nat * nat) set" + nat_rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" + "0" :: "nat" ("0") translations "case p of 0 => a | Suc(y) => b" == "nat_case(a, %y.b, p)" rules (*the axiom of infinity in 2 parts*) - inj_Suc_Rep "inj(Suc_Rep)" - Suc_Rep_not_Zero_Rep "~(Suc_Rep(x) = Zero_Rep)" - Nat_def "Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" + inj_Suc_Rep "inj(Suc_Rep)" + Suc_Rep_not_Zero_Rep "~(Suc_Rep(x) = Zero_Rep)" + Nat_def "Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" (*faking a type definition...*) - Rep_Nat "Rep_Nat(n): Nat" - Rep_Nat_inverse "Abs_Nat(Rep_Nat(n)) = n" - Abs_Nat_inverse "i: Nat ==> Rep_Nat(Abs_Nat(i)) = i" + Rep_Nat "Rep_Nat(n): Nat" + Rep_Nat_inverse "Abs_Nat(Rep_Nat(n)) = n" + Abs_Nat_inverse "i: Nat ==> Rep_Nat(Abs_Nat(i)) = i" (*defining the abstract constants*) - Zero_def "0 == Abs_Nat(Zero_Rep)" - Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" + Zero_def "0 == Abs_Nat(Zero_Rep)" + Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" (*nat operations and recursion*) - nat_case_def "nat_case(a,f,n) == @z. (n=0 --> z=a) \ + nat_case_def "nat_case(a,f,n) == @z. (n=0 --> z=a) \ \ & (!x. n=Suc(x) --> z=f(x))" - pred_nat_def "pred_nat == {p. ? n. p = }" + pred_nat_def "pred_nat == {p. ? n. p = }" less_def "m:trancl(pred_nat)" le_def "m<=(n::nat) == ~(n bool" (infixl 50) - mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) - min,max :: "['a::ord,'a] => 'a" + mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) + min, max :: "['a::ord, 'a] => 'a" -rules - -mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" -min_def "min(a,b) == if(a <= b, a, b)" -max_def "max(a,b) == if(a <= b, b, a)" +defs + mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" + min_def "min(a, b) == if(a <= b, a, b)" + max_def "max(a, b) == if(a <= b, b, a)" end + diff -r 6254f50e5ec9 -r a9f7ff3a464c Set.thy --- a/Set.thy Fri Sep 16 15:48:20 1994 +0200 +++ b/Set.thy Wed Sep 21 15:40:41 1994 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/set.thy +(* Title: HOL/Set.thy ID: $Id$ Author: Tobias Nipkow Copyright 1993 University of Cambridge @@ -11,14 +11,13 @@ arities set :: (term) term - set :: (term) ord - set :: (term) minus +instance + set :: (term) {ord, minus} consts - - (* Constants *) - + "{}" :: "'a set" ("{}") + insert :: "['a, 'a set] => 'a set" Collect :: "('a => bool) => 'a set" (*comprehension*) Compl :: "('a set) => 'a set" (*complement*) Int :: "['a set, 'a set] => 'a set" (infixl 70) @@ -27,23 +26,20 @@ UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10) INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10) Union, Inter :: "(('a set)set) => 'a set" (*of a set*) - Pow :: "'a set => 'a set set" (*powerset*) + Pow :: "'a set => 'a set set" (*powerset*) range :: "('a => 'b) => 'b set" (*of function*) Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*) inj, surj :: "('a => 'b) => bool" (*inj/surjective*) inj_onto :: "['a => 'b, 'a set] => bool" "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90) ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*) - "~:" :: "['a, 'a set] => bool" ("(_ ~:/ _)" [50, 51] 50) - - (* Finite Sets *) - - insert :: "['a, 'a set] => 'a set" - "{}" :: "'a set" ("{}") - "@Finset" :: "args => 'a set" ("{(_)}") - (** Binding Constants **) +syntax + + "~:" :: "['a, 'a set] => bool" (infixl 50) + + "@Finset" :: "args => 'a set" ("{(_)}") "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") "@SetCompr" :: "['a, idts, bool] => 'a set" ("(1{_ |/_./ _})") @@ -60,7 +56,6 @@ "*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) "*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) - translations "x ~: y" == "~ (x : y)" "{x, xs}" == "insert(x, {xs})" @@ -89,14 +84,14 @@ Compl_def "Compl(A) == {x. ~x:A}" Un_def "A Un B == {x.x:A | x:B}" Int_def "A Int B == {x.x:A & x:B}" - set_diff_def "A-B == {x. x:A & ~x:B}" + set_diff_def "A - B == {x. x:A & ~x:B}" INTER_def "INTER(A, B) == {y. ! x:A. y: B(x)}" UNION_def "UNION(A, B) == {y. ? x:A. y: B(x)}" INTER1_def "INTER1(B) == INTER({x.True}, B)" UNION1_def "UNION1(B) == UNION({x.True}, B)" Inter_def "Inter(S) == (INT x:S. x)" Union_def "Union(S) == (UN x:S. x)" - Pow_def "Pow(A) == {B. B <= A}" + Pow_def "Pow(A) == {B. B <= A}" empty_def "{} == {x. False}" insert_def "insert(a, B) == {x.x=a} Un B" range_def "range(f) == {y. ? x. y=f(x)}" @@ -113,18 +108,16 @@ (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *) -fun dummyC(s) = Const(s,dummyT); - val ex_tr = snd(mk_binder_tr("? ","Ex")); fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1 | nvars(_) = 1; fun setcompr_tr[e,idts,b] = - let val eq = dummyC("op =") $ Bound(nvars(idts)) $ e - val P = dummyC("op &") $ eq $ b + let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e + val P = Syntax.const("op &") $ eq $ b val exP = ex_tr [idts,P] - in dummyC("Collect") $ Abs("",dummyT,exP) end; + in Syntax.const("Collect") $ Abs("",dummyT,exP) end; val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY")); @@ -135,14 +128,13 @@ fun tr'(_ $ abs) = let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs] - in dummyC("@SetCompr") $ e $ idts $ Q end + in Syntax.const("@SetCompr") $ e $ idts $ Q end in ok(P,0); tr'(P) end; in -val parse_translation = [("@SetCompr",setcompr_tr)]; -val print_translation = [("Collect",setcompr_tr')]; - +val parse_translation = [("@SetCompr", setcompr_tr)]; +val print_translation = [("Collect", setcompr_tr')]; val print_ast_translation = map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];