moved abstract algebra section to the end
authorhaftmann
Tue Jul 21 14:36:26 2009 +0200 (2009-07-21)
changeset 32119a853099fd9ca
parent 32117 0762b9ad83df
child 32120 53a21a5e6889
moved abstract algebra section to the end
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Jul 21 11:09:50 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jul 21 14:36:26 2009 +0200
     1.3 @@ -107,7 +107,6 @@
     1.4  notation (xsymbols)
     1.5    iff  (infixr "\<longleftrightarrow>" 25)
     1.6  
     1.7 -
     1.8  nonterminals
     1.9    letbinds  letbind
    1.10    case_syn  cases_syn
    1.11 @@ -198,96 +197,9 @@
    1.12  axiomatization
    1.13    undefined :: 'a
    1.14  
    1.15 -
    1.16 -subsubsection {* Generic classes and algebraic operations *}
    1.17 -
    1.18  class default =
    1.19    fixes default :: 'a
    1.20  
    1.21 -class zero = 
    1.22 -  fixes zero :: 'a  ("0")
    1.23 -
    1.24 -class one =
    1.25 -  fixes one  :: 'a  ("1")
    1.26 -
    1.27 -hide (open) const zero one
    1.28 -
    1.29 -class plus =
    1.30 -  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    1.31 -
    1.32 -class minus =
    1.33 -  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    1.34 -
    1.35 -class uminus =
    1.36 -  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    1.37 -
    1.38 -class times =
    1.39 -  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    1.40 -
    1.41 -class inverse =
    1.42 -  fixes inverse :: "'a \<Rightarrow> 'a"
    1.43 -    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    1.44 -
    1.45 -class abs =
    1.46 -  fixes abs :: "'a \<Rightarrow> 'a"
    1.47 -begin
    1.48 -
    1.49 -notation (xsymbols)
    1.50 -  abs  ("\<bar>_\<bar>")
    1.51 -
    1.52 -notation (HTML output)
    1.53 -  abs  ("\<bar>_\<bar>")
    1.54 -
    1.55 -end
    1.56 -
    1.57 -class sgn =
    1.58 -  fixes sgn :: "'a \<Rightarrow> 'a"
    1.59 -
    1.60 -class ord =
    1.61 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.62 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.63 -begin
    1.64 -
    1.65 -notation
    1.66 -  less_eq  ("op <=") and
    1.67 -  less_eq  ("(_/ <= _)" [51, 51] 50) and
    1.68 -  less  ("op <") and
    1.69 -  less  ("(_/ < _)"  [51, 51] 50)
    1.70 -  
    1.71 -notation (xsymbols)
    1.72 -  less_eq  ("op \<le>") and
    1.73 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.74 -
    1.75 -notation (HTML output)
    1.76 -  less_eq  ("op \<le>") and
    1.77 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.78 -
    1.79 -abbreviation (input)
    1.80 -  greater_eq  (infix ">=" 50) where
    1.81 -  "x >= y \<equiv> y <= x"
    1.82 -
    1.83 -notation (input)
    1.84 -  greater_eq  (infix "\<ge>" 50)
    1.85 -
    1.86 -abbreviation (input)
    1.87 -  greater  (infix ">" 50) where
    1.88 -  "x > y \<equiv> y < x"
    1.89 -
    1.90 -end
    1.91 -
    1.92 -syntax
    1.93 -  "_index1"  :: index    ("\<^sub>1")
    1.94 -translations
    1.95 -  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    1.96 -
    1.97 -typed_print_translation {*
    1.98 -let
    1.99 -  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
   1.100 -    if (not o null) ts orelse T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
   1.101 -    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
   1.102 -in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
   1.103 -*} -- {* show types that are presumably too general *}
   1.104 -
   1.105  
   1.106  subsection {* Fundamental rules *}
   1.107  
   1.108 @@ -1605,25 +1517,9 @@
   1.109  
   1.110  setup ReorientProc.init
   1.111  
   1.112 -setup {*
   1.113 -  ReorientProc.add
   1.114 -    (fn Const(@{const_name HOL.zero}, _) => true
   1.115 -      | Const(@{const_name HOL.one}, _) => true
   1.116 -      | _ => false)
   1.117 -*}
   1.118 -
   1.119 -simproc_setup reorient_zero ("0 = x") = ReorientProc.proc
   1.120 -simproc_setup reorient_one ("1 = x") = ReorientProc.proc
   1.121 -
   1.122  
   1.123  subsection {* Other simple lemmas and lemma duplicates *}
   1.124  
   1.125 -lemma Let_0 [simp]: "Let 0 f = f 0"
   1.126 -  unfolding Let_def ..
   1.127 -
   1.128 -lemma Let_1 [simp]: "Let 1 f = f 1"
   1.129 -  unfolding Let_def ..
   1.130 -
   1.131  lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
   1.132    by blast+
   1.133  
   1.134 @@ -1643,13 +1539,6 @@
   1.135    apply (drule_tac [3] x = x in fun_cong, simp_all)
   1.136    done
   1.137  
   1.138 -lemma mk_left_commute:
   1.139 -  fixes f (infix "\<otimes>" 60)
   1.140 -  assumes a: "\<And>x y z. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" and
   1.141 -          c: "\<And>x y. x \<otimes> y = y \<otimes> x"
   1.142 -  shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   1.143 -  by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
   1.144 -
   1.145  lemmas eq_sym_conv = eq_commute
   1.146  
   1.147  lemma nnf_simps:
   1.148 @@ -1659,6 +1548,118 @@
   1.149  by blast+
   1.150  
   1.151  
   1.152 +subsection {* Generic classes and algebraic operations *}
   1.153 +
   1.154 +class zero = 
   1.155 +  fixes zero :: 'a  ("0")
   1.156 +
   1.157 +class one =
   1.158 +  fixes one  :: 'a  ("1")
   1.159 +
   1.160 +lemma Let_0 [simp]: "Let 0 f = f 0"
   1.161 +  unfolding Let_def ..
   1.162 +
   1.163 +lemma Let_1 [simp]: "Let 1 f = f 1"
   1.164 +  unfolding Let_def ..
   1.165 +
   1.166 +setup {*
   1.167 +  ReorientProc.add
   1.168 +    (fn Const(@{const_name HOL.zero}, _) => true
   1.169 +      | Const(@{const_name HOL.one}, _) => true
   1.170 +      | _ => false)
   1.171 +*}
   1.172 +
   1.173 +simproc_setup reorient_zero ("0 = x") = ReorientProc.proc
   1.174 +simproc_setup reorient_one ("1 = x") = ReorientProc.proc
   1.175 +
   1.176 +typed_print_translation {*
   1.177 +let
   1.178 +  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
   1.179 +    if (not o null) ts orelse T = dummyT
   1.180 +      orelse not (! show_types) andalso can Term.dest_Type T
   1.181 +    then raise Match
   1.182 +    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
   1.183 +in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
   1.184 +*} -- {* show types that are presumably too general *}
   1.185 +
   1.186 +hide (open) const zero one
   1.187 +
   1.188 +class plus =
   1.189 +  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
   1.190 +
   1.191 +class minus =
   1.192 +  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
   1.193 +
   1.194 +class uminus =
   1.195 +  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
   1.196 +
   1.197 +class times =
   1.198 +  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
   1.199 +
   1.200 +class inverse =
   1.201 +  fixes inverse :: "'a \<Rightarrow> 'a"
   1.202 +    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
   1.203 +
   1.204 +class abs =
   1.205 +  fixes abs :: "'a \<Rightarrow> 'a"
   1.206 +begin
   1.207 +
   1.208 +notation (xsymbols)
   1.209 +  abs  ("\<bar>_\<bar>")
   1.210 +
   1.211 +notation (HTML output)
   1.212 +  abs  ("\<bar>_\<bar>")
   1.213 +
   1.214 +end
   1.215 +
   1.216 +class sgn =
   1.217 +  fixes sgn :: "'a \<Rightarrow> 'a"
   1.218 +
   1.219 +class ord =
   1.220 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.221 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.222 +begin
   1.223 +
   1.224 +notation
   1.225 +  less_eq  ("op <=") and
   1.226 +  less_eq  ("(_/ <= _)" [51, 51] 50) and
   1.227 +  less  ("op <") and
   1.228 +  less  ("(_/ < _)"  [51, 51] 50)
   1.229 +  
   1.230 +notation (xsymbols)
   1.231 +  less_eq  ("op \<le>") and
   1.232 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   1.233 +
   1.234 +notation (HTML output)
   1.235 +  less_eq  ("op \<le>") and
   1.236 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   1.237 +
   1.238 +abbreviation (input)
   1.239 +  greater_eq  (infix ">=" 50) where
   1.240 +  "x >= y \<equiv> y <= x"
   1.241 +
   1.242 +notation (input)
   1.243 +  greater_eq  (infix "\<ge>" 50)
   1.244 +
   1.245 +abbreviation (input)
   1.246 +  greater  (infix ">" 50) where
   1.247 +  "x > y \<equiv> y < x"
   1.248 +
   1.249 +end
   1.250 +
   1.251 +syntax
   1.252 +  "_index1"  :: index    ("\<^sub>1")
   1.253 +translations
   1.254 +  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
   1.255 +
   1.256 +lemma mk_left_commute:
   1.257 +  fixes f (infix "\<otimes>" 60)
   1.258 +  assumes a: "\<And>x y z. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" and
   1.259 +          c: "\<And>x y. x \<otimes> y = y \<otimes> x"
   1.260 +  shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   1.261 +  by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
   1.262 +
   1.263 +
   1.264  subsection {* Basic ML bindings *}
   1.265  
   1.266  ML {*