src/HOL/HOL.thy
changeset 10432 3dfbc913d184
parent 10383 a092ae7bb2a6
child 10489 a4684cf28edf
     1.1 --- a/src/HOL/HOL.thy	Fri Nov 10 19:01:33 2000 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Nov 10 19:02:37 2000 +0100
     1.3 @@ -24,7 +24,6 @@
     1.4    bool :: "term"
     1.5    fun :: ("term", "term") "term"
     1.6  
     1.7 -
     1.8  consts
     1.9  
    1.10    (* Constants *)
    1.11 @@ -51,6 +50,8 @@
    1.12    "|"           :: "[bool, bool] => bool"           (infixr 30)
    1.13    -->           :: "[bool, bool] => bool"           (infixr 25)
    1.14  
    1.15 +local
    1.16 +
    1.17  
    1.18  (* Overloaded Constants *)
    1.19  
    1.20 @@ -58,21 +59,28 @@
    1.21  axclass plus  < "term"
    1.22  axclass minus < "term"
    1.23  axclass times < "term"
    1.24 -axclass power < "term"
    1.25 +axclass inverse < "term"
    1.26 +
    1.27 +global
    1.28  
    1.29  consts
    1.30 -  "0"           :: "('a::zero)"                     ("0")
    1.31 +  "0"           :: "'a::zero"                       ("0")
    1.32    "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    1.33    -             :: "['a::minus, 'a] => 'a"          (infixl 65)
    1.34    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
    1.35 -  abs           :: "('a::minus) => 'a"
    1.36    *             :: "['a::times, 'a] => 'a"          (infixl 70)
    1.37 -  (*See Nat.thy for "^"*)
    1.38 +
    1.39 +local
    1.40 +
    1.41 +consts
    1.42 +  abs           :: "'a::minus => 'a"
    1.43 +  inverse       :: "'a::inverse => 'a"
    1.44 +  divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)
    1.45  
    1.46  axclass plus_ac0 < plus, zero
    1.47 -    commute: "x + y = y + x"
    1.48 -    assoc:   "(x + y) + z = x + (y + z)"
    1.49 -    zero:    "0 + x = x"
    1.50 +  commute: "x + y = y + x"
    1.51 +  assoc:   "(x + y) + z = x + (y + z)"
    1.52 +  zero:    "0 + x = x"
    1.53  
    1.54  
    1.55  (** Additional concrete syntax **)
    1.56 @@ -110,28 +118,28 @@
    1.57    "op ~="       :: "['a, 'a] => bool"                    ("(_ ~=/ _)" [51, 51] 50)
    1.58  
    1.59  syntax (symbols)
    1.60 -  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
    1.61 -  "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
    1.62 -  "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
    1.63 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.64 -  "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
    1.65 -  "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
    1.66 -  "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
    1.67 -  "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.68 -  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
    1.69 +  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    1.70 +  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    1.71 +  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    1.72 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\<midarrow>\<rightarrow>" 25)
    1.73 +  "op ~="       :: "['a, 'a] => bool"                    (infixl "\<noteq>" 50)
    1.74 +  "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    1.75 +  "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    1.76 +  "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
    1.77 +  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    1.78  (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
    1.79  
    1.80  syntax (input)
    1.81 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
    1.82 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
    1.83  
    1.84  syntax (symbols output)
    1.85 -  "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)
    1.86 +  "op ~="       :: "['a, 'a] => bool"                    ("(_ \<noteq>/ _)" [51, 51] 50)
    1.87  
    1.88  syntax (xsymbols)
    1.89 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<longrightarrow>" 25)
    1.90 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    1.91  
    1.92  syntax (HTML output)
    1.93 -  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
    1.94 +  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    1.95  
    1.96  syntax (HOL)
    1.97    "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
    1.98 @@ -143,8 +151,6 @@
    1.99  
   1.100  (** Rules and definitions **)
   1.101  
   1.102 -local
   1.103 -
   1.104  axioms
   1.105  
   1.106    eq_reflection: "(x=y) ==> (x==y)"
   1.107 @@ -159,7 +165,7 @@
   1.108      rule, and similar to the ABS rule of HOL.*)
   1.109    ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
   1.110  
   1.111 -  someI:        "P (x::'a) ==> P (@x. P x)"
   1.112 +  someI:        "P (x::'a) ==> P (SOME x. P x)"
   1.113  
   1.114    impI:         "(P ==> Q) ==> P-->Q"
   1.115    mp:           "[| P-->Q;  P |] ==> Q"
   1.116 @@ -168,7 +174,7 @@
   1.117  
   1.118    True_def:     "True      == ((%x::bool. x) = (%x. x))"
   1.119    All_def:      "All(P)    == (P = (%x. True))"
   1.120 -  Ex_def:       "Ex(P)     == P(@x. P(x))"
   1.121 +  Ex_def:       "Ex(P)     == P (SOME x. P x)"
   1.122    False_def:    "False     == (!P. P)"
   1.123    not_def:      "~ P       == P-->False"
   1.124    and_def:      "P & Q     == !R. (P-->Q-->R) --> R"
   1.125 @@ -184,11 +190,11 @@
   1.126  defs
   1.127    (*misc definitions*)
   1.128    Let_def:      "Let s f == f(s)"
   1.129 -  if_def:       "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
   1.130 +  if_def:       "If P x y == SOME z::'a. (P=True --> z=x) & (P=False --> z=y)"
   1.131  
   1.132    (*arbitrary is completely unspecified, but is made to appear as a
   1.133      definition syntactically*)
   1.134 -  arbitrary_def:  "False ==> arbitrary == (@x. False)"
   1.135 +  arbitrary_def:  "False ==> arbitrary == (SOME x. False)"
   1.136  
   1.137  
   1.138  
   1.139 @@ -196,7 +202,7 @@
   1.140  
   1.141  use "HOL_lemmas.ML"
   1.142  
   1.143 -lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
   1.144 +lemma atomize_all: "(!!x. P x) == Trueprop (ALL x. P x)"
   1.145  proof (rule equal_intr_rule)
   1.146    assume "!!x. P x"
   1.147    show "ALL x. P x" by (rule allI)
   1.148 @@ -205,7 +211,7 @@
   1.149    thus "!!x. P x" by (rule allE)
   1.150  qed
   1.151  
   1.152 -lemma imp_eq: "(A ==> B) == Trueprop (A --> B)"
   1.153 +lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)"
   1.154  proof (rule equal_intr_rule)
   1.155    assume r: "A ==> B"
   1.156    show "A --> B" by (rule impI) (rule r)
   1.157 @@ -214,7 +220,17 @@
   1.158    thus B by (rule mp)
   1.159  qed
   1.160  
   1.161 -lemmas atomize = all_eq imp_eq
   1.162 +lemma atomize_eq: "(x == y) == Trueprop (x = y)"
   1.163 +proof (rule equal_intr_rule)
   1.164 +  assume "x == y"
   1.165 +  show "x = y" by (unfold prems) (rule refl)
   1.166 +next
   1.167 +  assume "x = y"
   1.168 +  thus "x == y" by (rule eq_reflection)
   1.169 +qed
   1.170 +
   1.171 +lemmas atomize = atomize_all atomize_imp
   1.172 +lemmas atomize' = atomize atomize_eq
   1.173  
   1.174  use "cladata.ML"
   1.175  setup hypsubst_setup