# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256417543 -7200
# Node ID 3e53081ad53a9b369df1ab1ac3331ff10e3e1a6f
# Parent  fcacca9588b4bbb184a9d9c1c345229a83dae01a
added another example file about integers (see HOL/Int.thy)

diff -r fcacca9588b4 -r 3e53081ad53a IntEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IntEx.thy	Sat Oct 24 22:52:23 2009 +0200
@@ -0,0 +1,113 @@
+theory IntEx
+imports QuotMain
+begin
+
+fun
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
+where
+  "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient my_int = "nat \<times> nat" / intrel
+  apply(unfold EQUIV_def)
+  apply(auto simp add: mem_def expand_fun_eq)
+  done
+
+typ my_int
+
+local_setup {*
+  make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+*}
+
+term ZERO
+thm ZERO_def
+
+local_setup {*
+  make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+*}
+
+term ONE
+thm ONE_def
+
+fun
+  my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "my_plus (x, y) (u, v) = (x + u, y + v)"
+
+local_setup {*
+  make_const_def @{binding PLUS} @{term "my_plus"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+*}
+
+term PLUS
+thm PLUS_def
+
+fun
+  my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "my_neg (x, y) = (y, x)"
+
+local_setup {*
+  make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+*}
+
+term NEG
+thm NEG_def
+
+definition
+  MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+where
+  "MINUS z w = PLUS z (NEG w)"
+
+fun
+  my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+local_setup {*
+  make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+*}
+
+term MULT
+thm MULT_def
+
+(* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
+fun
+  my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+  "my_le (x, y) (u, v) = (x+v \<le> u+y)"
+
+local_setup {*
+  make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
+*}
+
+term LE
+thm LE_def
+
+definition
+  LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
+where
+  "LESS z w = (LE z w \<and> z \<noteq> w)"
+
+term LESS
+thm LESS_def
+
+
+definition
+  ABS :: "my_int \<Rightarrow> my_int"
+where
+  "ABS i = (if (LESS i ZERO) then (NEG i) else i)"
+
+definition
+  SIGN :: "my_int \<Rightarrow> my_int"
+where
+ "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
+
+ 
+
+lemma 
+  fixes i j k::"my_int"
+  shows "(PLUS (PLUS i j) k) = (PLUS i (PLUS j k))"
+  apply(unfold PLUS_def)
+  apply(simp add: expand_fun_eq)
+  sorry
+
+