1 theory IntEx

     2 imports QuotMain

     3 begin

     4 

     5 fun

     6   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 

     7 where

     8   "intrel (x, y) (u, v) = (x + v = u + y)"

     9 

    10 quotient my_int = "nat \<times> nat" / intrel

    11   apply(unfold EQUIV_def)

    12   apply(auto simp add: mem_def expand_fun_eq)

    13   done

    14 

    15 typ my_int

    16 

    17 local_setup {*

    18   make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd

    19 *}

    20 

    21 term ZERO

    22 thm ZERO_def

    23 

    24 local_setup {*

    25   make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd

    26 *}

    27 

    28 term ONE

    29 thm ONE_def

    30 

    31 fun

    32   my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    33 where

    34   "my_plus (x, y) (u, v) = (x + u, y + v)"

    35 

    36 local_setup {*

    37   make_const_def @{binding PLUS} @{term "my_plus"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd

    38 *}

    39 

    40 term PLUS

    41 thm PLUS_def

    42 

    43 fun

    44   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    45 where

    46   "my_neg (x, y) = (y, x)"

    47 

    48 local_setup {*

    49   make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd

    50 *}

    51 

    52 term NEG

    53 thm NEG_def

    54 

    55 definition

    56   MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"

    57 where

    58   "MINUS z w = PLUS z (NEG w)"

    59 

    60 fun

    61   my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    62 where

    63   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

    64 

    65 local_setup {*

    66   make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd

    67 *}

    68 

    69 term MULT

    70 thm MULT_def

    71 

    72 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *)

    73 fun

    74   my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"

    75 where

    76   "my_le (x, y) (u, v) = (x+v \<le> u+y)"

    77 

    78 local_setup {*

    79   make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd

    80 *}

    81 

    82 term LE

    83 thm LE_def

    84 

    85 definition

    86   LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"

    87 where

    88   "LESS z w = (LE z w \<and> z \<noteq> w)"

    89 

    90 term LESS

    91 thm LESS_def

    92 

    93 

    94 definition

    95   ABS :: "my_int \<Rightarrow> my_int"

    96 where

    97   "ABS i = (if (LESS i ZERO) then (NEG i) else i)"

    98 

    99 definition

   100   SIGN :: "my_int \<Rightarrow> my_int"

   101 where

   102  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"

   103 

   104  

   105 

   106 lemma 

   107   fixes i j k::"my_int"

   108   shows "(PLUS (PLUS i j) k) = (PLUS i (PLUS j k))"

   109   apply(unfold PLUS_def)

   110   apply(simp add: expand_fun_eq)

   111   sorry

   112 

   113