equal
deleted
inserted
replaced
1 theory IntEx |
1 theory IntEx |
2 imports QuotMain |
2 imports QuotMain |
3 begin |
3 begin |
4 |
4 |
5 fun |
5 fun |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
7 where |
7 where |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
9 |
9 |
10 quotient my_int = "nat \<times> nat" / intrel |
10 quotient my_int = "nat \<times> nat" / intrel |
11 apply(unfold EQUIV_def) |
11 apply(unfold EQUIV_def) |
121 sorry |
121 sorry |
122 |
122 |
123 lemma intrel_refl: "intrel a a" |
123 lemma intrel_refl: "intrel a a" |
124 sorry |
124 sorry |
125 |
125 |
126 lemma ho_plus_rsp : |
126 lemma ho_plus_rsp: |
127 "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
127 "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
128 by (simp) |
128 by (simp) |
129 |
129 |
130 ML {* val consts = [@{const_name "my_plus"}] *} |
130 ML {* val consts = [@{const_name "my_plus"}] *} |
131 ML {* val rty = @{typ "nat \<times> nat"} *} |
131 ML {* val rty = @{typ "nat \<times> nat"} *} |