equal
deleted
inserted
replaced
380 |
380 |
381 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*} |
381 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*} |
382 |
382 |
383 (* PROBLEM: this has to be a definition, not an abbreviation *) |
383 (* PROBLEM: this has to be a definition, not an abbreviation *) |
384 (* otherwise the lemma nat_le_eq_zle cannot be lifted *) |
384 (* otherwise the lemma nat_le_eq_zle cannot be lifted *) |
385 fun |
385 |
386 nat_aux |
386 abbreviation |
387 where |
387 "nat_aux \<equiv> \<lambda>(x, y).x - (y::nat)" |
388 "nat_aux (x, y) = x - (y::nat)" |
|
389 |
388 |
390 quotient_def |
389 quotient_def |
391 "nat2::int\<Rightarrow>nat" |
390 "nat2::int\<Rightarrow>nat" |
392 as |
391 as |
393 "nat_aux" |
392 "nat_aux" |
403 lemma [quot_respect]: |
402 lemma [quot_respect]: |
404 shows "(intrel ===> op =) nat_aux nat_aux" |
403 shows "(intrel ===> op =) nat_aux nat_aux" |
405 apply(auto) |
404 apply(auto) |
406 done |
405 done |
407 |
406 |
|
407 ML {* |
|
408 let |
|
409 val parser = Args.context -- Scan.lift Args.name_source |
|
410 fun term_pat (ctxt, str) = |
|
411 str |> ProofContext.read_term_pattern ctxt |
|
412 |> ML_Syntax.print_term |
|
413 |> ML_Syntax.atomic |
|
414 in |
|
415 ML_Antiquote.inline "term_pat" (parser >> term_pat) |
|
416 end |
|
417 |
|
418 *} |
|
419 |
|
420 consts test::"'b \<Rightarrow> 'b \<Rightarrow> 'b" |
|
421 |
|
422 |
408 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)" |
423 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)" |
409 unfolding less_int_def |
424 unfolding less_int_def |
410 apply(lifting nat_le_eq_zle_aux) |
425 apply(lifting nat_le_eq_zle_aux) |
411 apply(injection) |
426 apply(injection) |
412 apply(simp_all only: quot_respect) |
427 apply(simp_all only: quot_respect) |
413 done |
428 done |
414 (* PROBLEM *) |
|
415 |
429 |
416 end |
430 end |