equal
deleted
inserted
replaced
108 definition |
108 definition |
109 SIGN :: "my_int \<Rightarrow> my_int" |
109 SIGN :: "my_int \<Rightarrow> my_int" |
110 where |
110 where |
111 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
111 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
112 |
112 |
|
113 lemma plus_sym_pre: |
|
114 shows "intrel (my_plus a b) (my_plus b a)" |
|
115 apply(cases a) |
|
116 apply(cases b) |
|
117 apply(auto) |
|
118 done |
|
119 |
113 lemma equiv_intrel: "EQUIV intrel" |
120 lemma equiv_intrel: "EQUIV intrel" |
114 sorry |
121 sorry |
115 |
122 |
116 lemma intrel_refl: "intrel a a" |
123 lemma intrel_refl: "intrel a a" |
117 sorry |
124 sorry |
118 |
125 |
119 lemma ho_plus_rsp : "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
126 lemma ho_plus_rsp : |
|
127 "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
120 by (simp) |
128 by (simp) |
121 |
129 |
122 ML {* val consts = [@{const_name "my_plus"}] *} |
130 ML {* val consts = [@{const_name "my_plus"}] *} |
123 ML {* val rty = @{typ "nat \<times> nat"} *} |
131 ML {* val rty = @{typ "nat \<times> nat"} *} |
124 ML {* val qty = @{typ "my_int"} *} |
132 ML {* val qty = @{typ "my_int"} *} |