Commit 2ce70ac4 authored by Christian Sternagel's avatar Christian Sternagel
Browse files

tuned layout; define shows_prec for rat without detour via show_rat

parent 4e0b5dcc2f34
......@@ -24,19 +24,23 @@ imports
"~~/src/HOL/Rat"
begin
text {* For several types, we just derive the show function *}
text {*
For several types, we just derive the show function.
*}
derive "show" bool
derive "show" option
derive "show" sum
text {* The derive-command is not used for @{type unit}, @{type prod}, and numbers:
for @{type unit} and @{type prod}, we do not want to display ``Unity'' and ``Pair'';
for @{type nat}, we do not want to display ``Suc (Suc ... Suc (Zero))''; and neither
@{type int} nor @{type rat} are datatypes. *}
text {*
The derive-command is not used for @{type unit}, @{type prod}, and numbers: for @{type unit} and
@{type prod}, we do not want to display ``Unity'' and ``Pair''; for @{type nat}, we do not want to
display ``Suc (Suc ... Suc (0))''; and neither @{type int} nor @{type rat} are datatypes.
*}
instantiation unit :: "show"
begin
definition "shows_prec d (x::unit) = shows_string ''()''"
lemma assoc_unit:
......@@ -44,77 +48,98 @@ lemma assoc_unit:
by (simp add: shows_prec_unit_def)
standard_shows_list assoc_unit
end
instantiation prod :: ("show", "show") "show"
begin
definition "shows_prec d (p :: 'a \<times> 'b) =
shows_paren (shows (fst p) +@+ '','' +#+ shows (snd p))"
definition "shows_prec d (p :: 'a \<times> 'b) = shows_paren (shows (fst p) +@+ '','' +#+ shows (snd p))"
lemma assoc_prod:
"shows_prec d (p::('a::show \<times> 'b::show)) r @ s = shows_prec d p (r @ s)"
by (cases p) (simp add: shows_prec_prod_def show_defs)
standard_shows_list assoc_prod
end
instantiation nat :: "show" begin
fun
digit2string :: "nat \<Rightarrow> string"
where
"digit2string n =
(if n = 0 then ''0'' else
(if n = 1 then ''1'' else
(if n = 2 then ''2'' else
(if n = 3 then ''3'' else
(if n = 4 then ''4'' else
(if n = 5 then ''5'' else
(if n = 6 then ''6'' else
(if n = 7 then ''7'' else
(if n = 8 then ''8'' else ''9'')))))))))"
fun shows_nat where "shows_nat (n::nat) = (
instantiation nat :: "show"
begin
fun
digit2string :: "nat \<Rightarrow> string"
where
"digit2string n = (
if n = 0 then ''0''
else if n = 1 then ''1''
else if n = 2 then ''2''
else if n = 3 then ''3''
else if n = 4 then ''4''
else if n = 5 then ''5''
else if n = 6 then ''6''
else if n = 7 then ''7''
else if n = 8 then ''8''
else ''9'')"
fun shows_nat :: "nat \<Rightarrow> shows"
where
"shows_nat (n::nat) = (
if n < 10 then shows_string (digit2string n)
else shows_nat (n div 10) \<circ> shows_string (digit2string (n mod 10))
)"
definition "shows_prec (d::nat) (n::nat) \<equiv> shows_nat n"
lemma assoc_nat: "shows_prec d (n::nat) r @ s = shows_prec d n (r @ s)"
proof (induct n arbitrary: r s rule: nat_less_induct)
case (1 n) show ?case
proof (cases "n < 10")
case True thus ?thesis unfolding shows_prec_nat_def by simp
next
let ?m = "n div 10"
case False
hence "?m < n" by simp
with 1 have "\<And>s t. shows_prec d ?m s @ t = shows_prec d ?m (s@t)" by simp
thus ?thesis unfolding shows_prec_nat_def by auto
qed
else shows_nat (n div 10) \<circ> shows_string (digit2string (n mod 10)))"
definition "shows_prec (d::nat) (n::nat) = shows_nat n"
lemma assoc_nat: "shows_prec d (n::nat) r @ s = shows_prec d n (r @ s)"
proof (induct n arbitrary: r s rule: nat_less_induct)
case (1 n)
show ?case
proof (cases "n < 10")
case True thus ?thesis unfolding shows_prec_nat_def by simp
next
let ?m = "n div 10"
case False
hence "?m < n" by simp
with 1 have "\<And>s t. shows_prec d ?m s @ t = shows_prec d ?m (s @ t)" by simp
thus ?thesis unfolding shows_prec_nat_def by auto
qed
standard_shows_list assoc_nat
qed
standard_shows_list assoc_nat
end
instantiation int :: "show" begin
definition "shows_prec (d::nat) (i::int) \<equiv>
(if i < 0
then shows (CHR ''-'') \<circ> shows (nat (- i))
else shows (nat i))"
instantiation int :: "show"
begin
definition "shows_prec (d::nat) (i::int) = (
if i < 0 then shows (CHR ''-'') \<circ> shows (nat (- i))
else shows (nat i))"
lemma assoc_int:
"shows_prec d (i::int) r @ s = shows_prec d i (r @ s)"
by (simp add: shows_prec_int_def)
standard_shows_list assoc_int
lemma assoc_int: "shows_prec d (i::int) r @ s = shows_prec d i (r @ s)"
by (simp add: shows_prec_int_def)
standard_shows_list assoc_int
end
instantiation rat :: "show" begin
definition show_rat :: "rat \<Rightarrow> string"
where "show_rat x \<equiv> case (quotient_of x) of (Pair den num) \<Rightarrow> if num = 1 then shows den '''' else ((shows den \<circ> shows(CHR ''/'') \<circ> shows num) '''')"
definition "shows_prec (d::nat) x \<equiv> shows_string (show_rat x)"
instantiation rat :: "show"
begin
definition "shows_prec (d::nat) (x::rat) =
(case quotient_of x of
Pair den num \<Rightarrow>
if num = 1 then shows den else shows den \<circ> shows (CHR ''/'') \<circ> shows num)"
lemma assoc_rat:
"shows_prec d (x::rat) r @ s = shows_prec d x (r @ s)"
unfolding shows_prec_rat_def by (cases "quotient_of x") auto
standard_shows_list assoc_rat
lemma assoc_rat: "shows_prec d (x::rat) r @ s = shows_prec d x (r @ s)" unfolding shows_prec_rat_def by auto
standard_shows_list assoc_rat
end
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment