adapted to qualified names;
authorwenzelm
Mon Oct 20 11:25:39 1997 +0200 (1997-10-20)
changeset 3947eb707467f8c5
parent 3946 34152864655c
child 3948 3428c0a88449
adapted to qualified names;
src/HOL/Gfp.thy
src/HOL/HOL.thy
src/HOL/Lfp.thy
src/HOL/NatDef.thy
src/HOL/Ord.thy
src/HOL/Prod.thy
src/HOL/ROOT.ML
src/HOL/Set.thy
src/HOL/Sum.thy
src/HOL/Univ.thy
src/HOL/WF.thy
     1.1 --- a/src/HOL/Gfp.thy	Mon Oct 20 11:22:29 1997 +0200
     1.2 +++ b/src/HOL/Gfp.thy	Mon Oct 20 11:25:39 1997 +0200
     1.3 @@ -8,8 +8,12 @@
     1.4  
     1.5  Gfp = Lfp +
     1.6  
     1.7 +global
     1.8 +
     1.9  constdefs
    1.10    gfp :: ['a set=>'a set] => 'a set
    1.11    "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
    1.12  
    1.13 +local
    1.14 +
    1.15  end
     2.1 --- a/src/HOL/HOL.thy	Mon Oct 20 11:22:29 1997 +0200
     2.2 +++ b/src/HOL/HOL.thy	Mon Oct 20 11:25:39 1997 +0200
     2.3 @@ -11,6 +11,8 @@
     2.4  
     2.5  (** Core syntax **)
     2.6  
     2.7 +global
     2.8 +
     2.9  classes
    2.10    term < logic
    2.11  
    2.12 @@ -33,6 +35,7 @@
    2.13    Not           :: bool => bool                     ("~ _" [40] 40)
    2.14    True, False   :: bool
    2.15    If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    2.16 +  arbitrary     :: 'a
    2.17  
    2.18    (* Binders *)
    2.19  
    2.20 @@ -141,6 +144,8 @@
    2.21  
    2.22  (** Rules and definitions **)
    2.23  
    2.24 +local
    2.25 +
    2.26  rules
    2.27  
    2.28    eq_reflection "(x=y) ==> (x==y)"
    2.29 @@ -179,9 +184,6 @@
    2.30    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
    2.31    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
    2.32  
    2.33 -consts
    2.34 -  arbitrary :: 'a
    2.35 -
    2.36  
    2.37  end
    2.38  
     3.1 --- a/src/HOL/Lfp.thy	Mon Oct 20 11:22:29 1997 +0200
     3.2 +++ b/src/HOL/Lfp.thy	Mon Oct 20 11:25:39 1997 +0200
     3.3 @@ -8,8 +8,12 @@
     3.4  
     3.5  Lfp = mono + Prod +
     3.6  
     3.7 +global
     3.8 +
     3.9  constdefs
    3.10    lfp :: ['a set=>'a set] => 'a set
    3.11    "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
    3.12  
    3.13 +local
    3.14 +
    3.15  end
     4.1 --- a/src/HOL/NatDef.thy	Mon Oct 20 11:22:29 1997 +0200
     4.2 +++ b/src/HOL/NatDef.thy	Mon Oct 20 11:25:39 1997 +0200
     4.3 @@ -12,6 +12,8 @@
     4.4  
     4.5  (** type ind **)
     4.6  
     4.7 +global
     4.8 +
     4.9  types
    4.10    ind
    4.11  
    4.12 @@ -59,6 +61,8 @@
    4.13    "case p of 0 => a | Suc y => b" == "nat_case a (%y. b) p"
    4.14  
    4.15  
    4.16 +local
    4.17 +
    4.18  defs
    4.19    Zero_def      "0 == Abs_Nat(Zero_Rep)"
    4.20    Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
     5.1 --- a/src/HOL/Ord.thy	Mon Oct 20 11:22:29 1997 +0200
     5.2 +++ b/src/HOL/Ord.thy	Mon Oct 20 11:25:39 1997 +0200
     5.3 @@ -11,6 +11,8 @@
     5.4  axclass
     5.5    ord < term
     5.6  
     5.7 +global
     5.8 +
     5.9  syntax
    5.10    "op <"        :: ['a::ord, 'a] => bool             ("op <")
    5.11    "op <="       :: ['a::ord, 'a] => bool             ("op <=")
    5.12 @@ -28,6 +30,8 @@
    5.13    "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
    5.14  
    5.15  
    5.16 +local
    5.17 +
    5.18  defs
    5.19    mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
    5.20    min_def       "min a b == (if a <= b then a else b)"
     6.1 --- a/src/HOL/Prod.thy	Mon Oct 20 11:22:29 1997 +0200
     6.2 +++ b/src/HOL/Prod.thy	Mon Oct 20 11:25:39 1997 +0200
     6.3 @@ -18,6 +18,8 @@
     6.4    Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
     6.5    "Pair_Rep == (%a b. %x y. x=a & y=b)"
     6.6  
     6.7 +global
     6.8 +
     6.9  typedef (Prod)
    6.10    ('a, 'b) "*"          (infixr 20)
    6.11      = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
    6.12 @@ -71,6 +73,8 @@
    6.13  
    6.14  (* definitions *)
    6.15  
    6.16 +local
    6.17 +
    6.18  defs
    6.19    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    6.20    fst_def       "fst p == @a. ? b. p = (a, b)"
    6.21 @@ -83,11 +87,15 @@
    6.22  
    6.23  (** unit **)
    6.24  
    6.25 +global
    6.26 +
    6.27  typedef  unit = "{True}"
    6.28  
    6.29  consts
    6.30    "()"          :: unit                           ("'(')")
    6.31  
    6.32 +local
    6.33 +
    6.34  defs
    6.35    Unity_def     "() == Abs_unit True"
    6.36  
     7.1 --- a/src/HOL/ROOT.ML	Mon Oct 20 11:22:29 1997 +0200
     7.2 +++ b/src/HOL/ROOT.ML	Mon Oct 20 11:25:39 1997 +0200
     7.3 @@ -7,9 +7,11 @@
     7.4  Should be executed in the subdirectory HOL.
     7.5  *)
     7.6  
     7.7 -val banner = "Higher-Order Logic with curried functions";
     7.8 +val banner = "Higher-Order Logic";
     7.9  writeln banner;
    7.10  
    7.11 +reset global_names;
    7.12 +
    7.13  print_depth 1;
    7.14  
    7.15  (* Add user sections *)
     8.1 --- a/src/HOL/Set.thy	Mon Oct 20 11:22:29 1997 +0200
     8.2 +++ b/src/HOL/Set.thy	Mon Oct 20 11:25:39 1997 +0200
     8.3 @@ -9,6 +9,8 @@
     8.4  
     8.5  (** Core syntax **)
     8.6  
     8.7 +global
     8.8 +
     8.9  types
    8.10    'a set
    8.11  
    8.12 @@ -121,6 +123,8 @@
    8.13  
    8.14  (** Rules and definitions **)
    8.15  
    8.16 +local
    8.17 +
    8.18  rules
    8.19  
    8.20    (* Isomorphisms between Predicates and Sets *)
     9.1 --- a/src/HOL/Sum.thy	Mon Oct 20 11:22:29 1997 +0200
     9.2 +++ b/src/HOL/Sum.thy	Mon Oct 20 11:25:39 1997 +0200
     9.3 @@ -17,6 +17,8 @@
     9.4    Inr_Rep       :: ['b, 'a, 'b, bool] => bool
     9.5    "Inr_Rep == (%b. %x y p. y=b & ~p)"
     9.6  
     9.7 +global
     9.8 +
     9.9  typedef (Sum)
    9.10    ('a, 'b) "+"          (infixr 10)
    9.11      = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
    9.12 @@ -36,6 +38,8 @@
    9.13  translations
    9.14    "case p of Inl x => a | Inr y => b" == "sum_case (%x. a) (%y. b) p"
    9.15  
    9.16 +local
    9.17 +
    9.18  defs
    9.19    Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
    9.20    Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
    10.1 --- a/src/HOL/Univ.thy	Mon Oct 20 11:22:29 1997 +0200
    10.2 +++ b/src/HOL/Univ.thy	Mon Oct 20 11:25:39 1997 +0200
    10.3 @@ -13,6 +13,8 @@
    10.4  
    10.5  (** lists, trees will be sets of nodes **)
    10.6  
    10.7 +global
    10.8 +
    10.9  typedef (Node)
   10.10    'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
   10.11  
   10.12 @@ -46,6 +48,9 @@
   10.13    "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
   10.14             => ('a item * 'a item)set" (infixr 70)
   10.15  
   10.16 +
   10.17 +local
   10.18 +
   10.19  defs
   10.20  
   10.21    Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    11.1 --- a/src/HOL/WF.thy	Mon Oct 20 11:22:29 1997 +0200
    11.2 +++ b/src/HOL/WF.thy	Mon Oct 20 11:25:39 1997 +0200
    11.3 @@ -8,6 +8,8 @@
    11.4  
    11.5  WF = Trancl +
    11.6  
    11.7 +global
    11.8 +
    11.9  constdefs
   11.10    wf         :: "('a * 'a)set => bool"
   11.11    "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
   11.12 @@ -28,4 +30,6 @@
   11.13    "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
   11.14                              r x)  x)"
   11.15  
   11.16 +local
   11.17 +
   11.18  end