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 "../QuotMain" |
5 imports Nat "../QuotMain" "../QuotProd" |
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" |
10 where |
10 where |
359 lemma [quot_respect]: |
359 lemma [quot_respect]: |
360 shows "(intrel ===> op =) nat_raw nat_raw" |
360 shows "(intrel ===> op =) nat_raw nat_raw" |
361 apply(auto iff: nat_raw_def) |
361 apply(auto iff: nat_raw_def) |
362 done |
362 done |
363 |
363 |
364 ML {* |
|
365 let |
|
366 val parser = Args.context -- Scan.lift Args.name_source |
|
367 fun term_pat (ctxt, str) = |
|
368 str |> ProofContext.read_term_pattern ctxt |
|
369 |> ML_Syntax.print_term |
|
370 |> ML_Syntax.atomic |
|
371 in |
|
372 ML_Antiquote.inline "term_pat" (parser >> term_pat) |
|
373 end |
|
374 |
|
375 *} |
|
376 |
|
377 consts test::"'b \<Rightarrow> 'b \<Rightarrow> 'b" |
|
378 |
|
379 |
|
380 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)" |
364 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)" |
381 unfolding less_int_def |
365 unfolding less_int_def |
382 apply(lifting nat_le_eq_zle_raw) |
366 apply(lifting nat_le_eq_zle_raw) |
383 done |
367 done |
384 |
368 |