equal
deleted
inserted
replaced
1 |
1 |
2 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} |
2 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} |
3 |
3 |
4 theory LarryInt |
4 theory LarryInt |
5 imports Nat "../Quotient" "../Quotient_Product" |
5 imports Nat "../Quotient" "../Quotient_Product" |
6 begin |
6 begin |
7 |
7 |
8 fun |
8 fun |
9 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
9 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
371 "nat2::int \<Rightarrow> nat" |
371 "nat2::int \<Rightarrow> nat" |
372 is |
372 is |
373 "nat_raw" |
373 "nat_raw" |
374 |
374 |
375 abbreviation |
375 abbreviation |
376 "less_raw x y \<equiv> (le_raw x y \<and> \<not>(x = y))" |
376 "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))" |
377 |
377 |
378 lemma nat_le_eq_zle_raw: |
378 lemma nat_le_eq_zle_raw: |
379 shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)" |
379 shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)" |
380 apply(auto) |
380 apply (cases w) |
381 sorry |
381 apply (cases z) |
|
382 apply (simp add: nat_raw_def le_raw_def) |
|
383 by auto |
382 |
384 |
383 lemma [quot_respect]: |
385 lemma [quot_respect]: |
384 shows "(intrel ===> op =) nat_raw nat_raw" |
386 shows "(intrel ===> op =) nat_raw nat_raw" |
385 by (auto iff: nat_raw_def) |
387 by (auto iff: nat_raw_def) |
386 |
388 |