systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char
--- a/src/Doc/Codegen/Adaptation.thy Fri Feb 15 15:22:16 2013 +0100
+++ b/src/Doc/Codegen/Adaptation.thy Fri Feb 15 11:47:33 2013 +0100
@@ -150,10 +150,6 @@
containing both @{text "Code_Target_Nat"} and
@{text "Code_Target_Int"}.
- \item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, but
- also offers treatment of character codes; includes @{text
- "Code_Char"}.
-
\item[@{text "Efficient_Nat"}] \label{eff_nat} implements
natural numbers by integers, which in general will result in
higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
--- a/src/HOL/Code_Evaluation.thy Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy Fri Feb 15 11:47:33 2013 +0100
@@ -119,11 +119,10 @@
= Code_Evaluation.term_of" ..
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
- "Code_Evaluation.term_of c =
- (let (n, m) = nibble_pair_of_char c
- in Code_Evaluation.App (Code_Evaluation.App
+ "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
+ Code_Evaluation.App (Code_Evaluation.App
(Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
- (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
+ (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
by (subst term_of_anything) rule
code_type "term"
--- a/src/HOL/Codegenerator_Test/Candidates.thy Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Fri Feb 15 11:47:33 2013 +0100
@@ -6,7 +6,7 @@
theory Candidates
imports
Complex_Main
- Library
+ "~~/src/HOL/Library/Library"
"~~/src/HOL/Library/Sublist"
"~~/src/HOL/Number_Theory/Primes"
"~~/src/HOL/ex/Records"
--- a/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Fri Feb 15 11:47:33 2013 +0100
@@ -4,7 +4,7 @@
header {* Generating code using pretty literals and natural number literals *}
theory Candidates_Pretty
-imports Candidates Code_Char_ord Code_Target_Numeral
+imports Candidates Code_Char Code_Target_Numeral
begin
end
--- a/src/HOL/Library/Char_nat.thy Fri Feb 15 15:22:16 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,199 +0,0 @@
-(* Title: HOL/Library/Char_nat.thy
- Author: Norbert Voelker, Florian Haftmann
-*)
-
-header {* Mapping between characters and natural numbers *}
-
-theory Char_nat
-imports List Main
-begin
-
-text {* Conversions between nibbles and natural numbers in [0..15]. *}
-
-primrec
- nat_of_nibble :: "nibble \<Rightarrow> nat" where
- "nat_of_nibble Nibble0 = 0"
- | "nat_of_nibble Nibble1 = 1"
- | "nat_of_nibble Nibble2 = 2"
- | "nat_of_nibble Nibble3 = 3"
- | "nat_of_nibble Nibble4 = 4"
- | "nat_of_nibble Nibble5 = 5"
- | "nat_of_nibble Nibble6 = 6"
- | "nat_of_nibble Nibble7 = 7"
- | "nat_of_nibble Nibble8 = 8"
- | "nat_of_nibble Nibble9 = 9"
- | "nat_of_nibble NibbleA = 10"
- | "nat_of_nibble NibbleB = 11"
- | "nat_of_nibble NibbleC = 12"
- | "nat_of_nibble NibbleD = 13"
- | "nat_of_nibble NibbleE = 14"
- | "nat_of_nibble NibbleF = 15"
-
-definition
- nibble_of_nat :: "nat \<Rightarrow> nibble" where
- "nibble_of_nat x = (let y = x mod 16 in
- if y = 0 then Nibble0 else
- if y = 1 then Nibble1 else
- if y = 2 then Nibble2 else
- if y = 3 then Nibble3 else
- if y = 4 then Nibble4 else
- if y = 5 then Nibble5 else
- if y = 6 then Nibble6 else
- if y = 7 then Nibble7 else
- if y = 8 then Nibble8 else
- if y = 9 then Nibble9 else
- if y = 10 then NibbleA else
- if y = 11 then NibbleB else
- if y = 12 then NibbleC else
- if y = 13 then NibbleD else
- if y = 14 then NibbleE else
- NibbleF)"
-
-lemma nibble_of_nat_norm:
- "nibble_of_nat (n mod 16) = nibble_of_nat n"
- unfolding nibble_of_nat_def mod_mod_trivial ..
-
-lemma nibble_of_nat_simps [simp]:
- "nibble_of_nat 0 = Nibble0"
- "nibble_of_nat 1 = Nibble1"
- "nibble_of_nat 2 = Nibble2"
- "nibble_of_nat 3 = Nibble3"
- "nibble_of_nat 4 = Nibble4"
- "nibble_of_nat 5 = Nibble5"
- "nibble_of_nat 6 = Nibble6"
- "nibble_of_nat 7 = Nibble7"
- "nibble_of_nat 8 = Nibble8"
- "nibble_of_nat 9 = Nibble9"
- "nibble_of_nat 10 = NibbleA"
- "nibble_of_nat 11 = NibbleB"
- "nibble_of_nat 12 = NibbleC"
- "nibble_of_nat 13 = NibbleD"
- "nibble_of_nat 14 = NibbleE"
- "nibble_of_nat 15 = NibbleF"
- unfolding nibble_of_nat_def by auto
-
-lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
- by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
-
-lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
-proof -
- have nibble_nat_enum:
- "n mod 16 \<in> {15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0}"
- proof -
- have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
- have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
- (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))}" by simp
- from this [simplified set_unfold atLeastAtMost_singleton]
- show ?thesis by (simp add: numeral_2_eq_2 [symmetric])
- qed
- then show ?thesis unfolding nibble_of_nat_def
- by auto
-qed
-
-lemma inj_nat_of_nibble: "inj nat_of_nibble"
- by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
-
-lemma nat_of_nibble_eq: "nat_of_nibble n = nat_of_nibble m \<longleftrightarrow> n = m"
- by (rule inj_eq) (rule inj_nat_of_nibble)
-
-lemma nat_of_nibble_less_16: "nat_of_nibble n < 16"
- by (cases n) auto
-
-lemma nat_of_nibble_div_16: "nat_of_nibble n div 16 = 0"
- by (cases n) auto
-
-
-text {* Conversion between chars and nats. *}
-
-definition
- nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
- "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
-
-lemma nibble_of_pair [code]:
- "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
- unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
-
-primrec
- nat_of_char :: "char \<Rightarrow> nat" where
- "nat_of_char (Char n m) = nat_of_nibble n * 16 + nat_of_nibble m"
-
-lemmas [simp del] = nat_of_char.simps
-
-definition
- char_of_nat :: "nat \<Rightarrow> char" where
- char_of_nat_def: "char_of_nat n = split Char (nibble_pair_of_nat n)"
-
-lemma Char_char_of_nat:
- "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
- unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
- by (auto simp add: div_add1_eq mod_add_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
-
-lemma char_of_nat_of_char:
- "char_of_nat (nat_of_char c) = c"
- by (cases c) (simp add: nat_of_char.simps, simp add: Char_char_of_nat)
-
-lemma nat_of_char_of_nat:
- "nat_of_char (char_of_nat n) = n mod 256"
-proof -
- from mod_div_equality [of n, symmetric, of 16]
- have mod_mult_self3: "\<And>m k n \<Colon> nat. (k * n + m) mod n = m mod n"
- proof -
- fix m k n :: nat
- show "(k * n + m) mod n = m mod n"
- by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
- qed
- from mod_div_decomp [of n 256] obtain k l where n: "n = k * 256 + l"
- and k: "k = n div 256" and l: "l = n mod 256" by blast
- have 16: "(0::nat) < 16" by auto
- have 256: "(256 :: nat) = 16 * 16" by auto
- have l_256: "l mod 256 = l" using l by auto
- have l_div_256: "l div 16 * 16 mod 256 = l div 16 * 16"
- using l by auto
- have aux2: "(k * 256 mod 16 + l mod 16) div 16 = 0"
- unfolding 256 mult_assoc [symmetric] mod_mult_self2_is_0 by simp
- have aux3: "(k * 256 + l) div 16 = k * 16 + l div 16"
- unfolding div_add1_eq [of "k * 256" l 16] aux2 256
- mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
- have aux4: "(k * 256 + l) mod 16 = l mod 16"
- unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
- show ?thesis
- by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
- nat_of_nibble_of_nat mult_mod_left
- n aux3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
-qed
-
-lemma nibble_pair_of_nat_char:
- "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"
-proof -
- have nat_of_nibble_256:
- "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 =
- nat_of_nibble n * 16 + nat_of_nibble m"
- proof -
- fix n m
- have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
- using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: eval_nat_numeral)
- have less_eq_240: "nat_of_nibble n * 16 \<le> 240"
- using nat_of_nibble_less_eq_15 by auto
- have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
- by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
- then have "nat_of_nibble n * 16 + nat_of_nibble m < 256" (is "?rhs < _") by auto
- then show "?rhs mod 256 = ?rhs" by auto
- qed
- show ?thesis
- unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
- by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
-qed
-
-
-text {* Code generator setup *}
-
-code_modulename SML
- Char_nat String
-
-code_modulename OCaml
- Char_nat String
-
-code_modulename Haskell
- Char_nat String
-
-end
\ No newline at end of file
--- a/src/HOL/Library/Char_ord.thy Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Library/Char_ord.thy Fri Feb 15 11:47:33 2013 +0100
@@ -5,43 +5,20 @@
header {* Order on characters *}
theory Char_ord
-imports Char_nat
+imports Main
begin
instantiation nibble :: linorder
begin
definition
- nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
+ "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
definition
- nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
+ "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
instance proof
- fix n :: nibble
- show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
-next
- fix n m q :: nibble
- assume "n \<le> m"
- and "m \<le> q"
- then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
-next
- fix n m :: nibble
- assume "n \<le> m"
- and "m \<le> n"
- then show "n = m"
- unfolding nibble_less_eq_def nibble_less_def
- by (auto simp add: nat_of_nibble_eq)
-next
- fix n m :: nibble
- show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
- unfolding nibble_less_eq_def nibble_less_def less_le
- by (auto simp add: nat_of_nibble_eq)
-next
- fix n m :: nibble
- show "n \<le> m \<or> m \<le> n"
- unfolding nibble_less_eq_def by auto
-qed
+qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
end
@@ -54,8 +31,8 @@
definition
"(sup \<Colon> nibble \<Rightarrow> _) = max"
-instance by default (auto simp add:
- inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
+instance proof
+qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
end
@@ -63,18 +40,46 @@
begin
definition
- char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
- n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
+ "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
definition
- char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
- n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
+ "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
-instance
- by default (auto simp: char_less_eq_def char_less_def split: char.splits)
+instance proof
+qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
end
+lemma less_eq_char_Char:
+ "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
+proof -
+ {
+ assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
+ \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
+ then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
+ using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
+ }
+ note * = this
+ show ?thesis
+ using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
+ by (auto simp add: less_eq_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
+qed
+
+lemma less_char_Char:
+ "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
+proof -
+ {
+ assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
+ < nat_of_nibble n2 * 16 + nat_of_nibble m2"
+ then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
+ using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
+ }
+ note * = this
+ show ?thesis
+ using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
+ by (auto simp add: less_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
+qed
+
instantiation char :: distrib_lattice
begin
@@ -84,14 +89,19 @@
definition
"(sup \<Colon> char \<Rightarrow> _) = max"
-instance by default (auto simp add:
- inf_char_def sup_char_def min_max.sup_inf_distrib1)
+instance proof
+qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
end
-lemma [simp, code]:
- shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
- and char_less_simp: "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
- unfolding char_less_eq_def char_less_def by simp_all
+text {* Legacy aliasses *}
+
+lemmas nibble_less_eq_def = less_eq_nibble_def
+lemmas nibble_less_def = less_nibble_def
+lemmas char_less_eq_def = less_eq_char_def
+lemmas char_less_def = less_char_def
+lemmas char_less_eq_simp = less_eq_char_Char
+lemmas char_less_simp = less_char_Char
end
+
--- a/src/HOL/Library/Code_Char.thy Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Library/Code_Char.thy Fri Feb 15 11:47:33 2013 +0100
@@ -5,7 +5,7 @@
header {* Code generation of pretty characters (and strings) *}
theory Code_Char
-imports List Code_Evaluation Main
+imports Main "~~/src/HOL/Library/Char_ord"
begin
code_type char
@@ -58,4 +58,47 @@
(Haskell "_")
(Scala "!(_.toList)")
+
+definition integer_of_char :: "char \<Rightarrow> integer"
+where
+ "integer_of_char = integer_of_nat o nat_of_char"
+
+definition char_of_integer :: "integer \<Rightarrow> char"
+where
+ "char_of_integer = char_of_nat \<circ> nat_of_integer"
+
+lemma [code]:
+ "nat_of_char = nat_of_integer o integer_of_char"
+ by (simp add: integer_of_char_def fun_eq_iff)
+
+lemma [code]:
+ "char_of_nat = char_of_integer o integer_of_nat"
+ by (simp add: char_of_integer_def fun_eq_iff)
+
+code_const integer_of_char and char_of_integer
+ (SML "!(IntInf.fromInt o Char.ord)"
+ and "!(Char.chr o IntInf.toInt)")
+ (OCaml "Big'_int.big'_int'_of'_int (Char.code _)"
+ and "Char.chr (Big'_int.int'_of'_big'_int _)")
+ (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
+ and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
+ (Scala "BigInt(_.toInt)"
+ and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
+
+
+code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+ (SML "!((_ : char) <= _)")
+ (OCaml "!((_ : char) <= _)")
+ (Haskell infix 4 "<=")
+ (Scala infixl 4 "<=")
+ (Eval infixl 6 "<=")
+
+code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+ (SML "!((_ : char) < _)")
+ (OCaml "!((_ : char) < _)")
+ (Haskell infix 4 "<")
+ (Scala infixl 4 "<")
+ (Eval infixl 6 "<")
+
end
+
--- a/src/HOL/Library/Code_Char_chr.thy Fri Feb 15 15:22:16 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* Title: HOL/Library/Code_Char_chr.thy
- Author: Florian Haftmann
-*)
-
-header {* Code generation of pretty characters with character codes *}
-
-theory Code_Char_chr
-imports Char_nat Code_Char Code_Target_Int Main
-begin
-
-definition
- "int_of_char = int o nat_of_char"
-
-lemma [code]:
- "nat_of_char = nat o int_of_char"
- unfolding int_of_char_def by (simp add: fun_eq_iff)
-
-definition
- "char_of_int = char_of_nat o nat"
-
-lemma [code]:
- "char_of_nat = char_of_int o int"
- unfolding char_of_int_def by (simp add: fun_eq_iff)
-
-code_const int_of_char and char_of_int
- (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
- (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
- (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
- (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
-
-end
--- a/src/HOL/Library/Code_Char_ord.thy Fri Feb 15 15:22:16 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Title: HOL/Library/Code_Char_ord.thy
- Author: Lukas Bulwahn, Florian Haftmann, Rene Thiemann
-*)
-
-header {* Code generation of orderings for pretty characters *}
-
-theory Code_Char_ord
-imports Code_Char Char_ord
-begin
-
-code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
- (SML "!((_ : char) <= _)")
- (OCaml "!((_ : char) <= _)")
- (Haskell infix 4 "<=")
- (Scala infixl 4 "<=")
- (Eval infixl 6 "<=")
-
-code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
- (SML "!((_ : char) < _)")
- (OCaml "!((_ : char) < _)")
- (Haskell infix 4 "<")
- (Scala infixl 4 "<")
- (Eval infixl 6 "<")
-
-end
\ No newline at end of file
--- a/src/HOL/List.thy Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/List.thy Fri Feb 15 11:47:33 2013 +0100
@@ -1626,6 +1626,35 @@
lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
by(auto simp:set_conv_nth)
+lemma nth_equal_first_eq:
+ assumes "x \<notin> set xs"
+ assumes "n \<le> length xs"
+ shows "(x # xs) ! n = x \<longleftrightarrow> n = 0" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ assume ?lhs
+ show ?rhs
+ proof (rule ccontr)
+ assume "n \<noteq> 0"
+ then have "n > 0" by simp
+ with `?lhs` have "xs ! (n - 1) = x" by simp
+ moreover from `n > 0` `n \<le> length xs` have "n - 1 < length xs" by simp
+ ultimately have "\<exists>i<length xs. xs ! i = x" by auto
+ with `x \<notin> set xs` in_set_conv_nth [of x xs] show False by simp
+ qed
+next
+ assume ?rhs then show ?lhs by simp
+qed
+
+lemma nth_non_equal_first_eq:
+ assumes "x \<noteq> y"
+ shows "(x # xs) ! n = y \<longleftrightarrow> xs ! (n - 1) = y \<and> n > 0" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ assume "?lhs" with assms have "n > 0" by (cases n) simp_all
+ with `?lhs` show ?rhs by simp
+next
+ assume "?rhs" then show "?lhs" by simp
+qed
+
lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
by (auto simp add: set_conv_nth)
@@ -2614,6 +2643,22 @@
"set (List.product xs ys) = set xs \<times> set ys"
by (induct xs) auto
+lemma length_product [simp]:
+ "length (List.product xs ys) = length xs * length ys"
+ by (induct xs) simp_all
+
+lemma product_nth:
+ assumes "n < length xs * length ys"
+ shows "List.product xs ys ! n = (xs ! (n div length ys), ys ! (n mod length ys))"
+using assms proof (induct xs arbitrary: n)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs n)
+ then have "length ys > 0" by auto
+ with Cons show ?case
+ by (auto simp add: nth_append not_less le_mod_geq le_div_geq)
+qed
+
subsubsection {* @{const fold} with natural argument order *}
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 15 11:47:33 2013 +0100
@@ -230,8 +230,7 @@
"nibble"]
val forbidden_consts =
- [@{const_name nibble_pair_of_char}, @{const_name "TYPE"},
- @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
+ [@{const_name "TYPE"}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
fun is_forbidden_theorem (s, th) =
let val consts = Term.add_const_names (prop_of th) [] in
--- a/src/HOL/ROOT Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/ROOT Fri Feb 15 11:47:33 2013 +0100
@@ -24,8 +24,7 @@
List_lexord
Sublist_Order
Finite_Lattice
- Code_Char_chr
- Code_Char_ord
+ Code_Char
Product_Lexorder
Product_Order
(* Code_Prolog FIXME cf. 76965c356d2a *)
--- a/src/HOL/String.thy Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/String.thy Fri Feb 15 11:47:33 2013 +0100
@@ -49,6 +49,72 @@
"card (UNIV :: nibble set) = 16"
by (simp add: card_UNIV_length_enum enum_nibble_def)
+primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
+where
+ "nat_of_nibble Nibble0 = 0"
+| "nat_of_nibble Nibble1 = 1"
+| "nat_of_nibble Nibble2 = 2"
+| "nat_of_nibble Nibble3 = 3"
+| "nat_of_nibble Nibble4 = 4"
+| "nat_of_nibble Nibble5 = 5"
+| "nat_of_nibble Nibble6 = 6"
+| "nat_of_nibble Nibble7 = 7"
+| "nat_of_nibble Nibble8 = 8"
+| "nat_of_nibble Nibble9 = 9"
+| "nat_of_nibble NibbleA = 10"
+| "nat_of_nibble NibbleB = 11"
+| "nat_of_nibble NibbleC = 12"
+| "nat_of_nibble NibbleD = 13"
+| "nat_of_nibble NibbleE = 14"
+| "nat_of_nibble NibbleF = 15"
+
+definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
+ "nibble_of_nat n = Enum.enum ! (n mod 16)"
+
+lemma nibble_of_nat_simps [simp]:
+ "nibble_of_nat 0 = Nibble0"
+ "nibble_of_nat 1 = Nibble1"
+ "nibble_of_nat 2 = Nibble2"
+ "nibble_of_nat 3 = Nibble3"
+ "nibble_of_nat 4 = Nibble4"
+ "nibble_of_nat 5 = Nibble5"
+ "nibble_of_nat 6 = Nibble6"
+ "nibble_of_nat 7 = Nibble7"
+ "nibble_of_nat 8 = Nibble8"
+ "nibble_of_nat 9 = Nibble9"
+ "nibble_of_nat 10 = NibbleA"
+ "nibble_of_nat 11 = NibbleB"
+ "nibble_of_nat 12 = NibbleC"
+ "nibble_of_nat 13 = NibbleD"
+ "nibble_of_nat 14 = NibbleE"
+ "nibble_of_nat 15 = NibbleF"
+ unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
+
+lemma nibble_of_nat_of_nibble [simp]:
+ "nibble_of_nat (nat_of_nibble x) = x"
+ by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
+
+lemma nat_of_nibble_of_nat [simp]:
+ "nat_of_nibble (nibble_of_nat n) = n mod 16"
+ by (cases "nibble_of_nat n")
+ (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
+
+lemma inj_nat_of_nibble:
+ "inj nat_of_nibble"
+ by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
+
+lemma nat_of_nibble_eq_iff:
+ "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
+ by (rule inj_eq) (rule inj_nat_of_nibble)
+
+lemma nat_of_nibble_less_16:
+ "nat_of_nibble x < 16"
+ by (cases x) auto
+
+lemma nibble_of_nat_mod_16:
+ "nibble_of_nat (n mod 16) = nibble_of_nat n"
+ by (simp add: nibble_of_nat_def)
+
datatype char = Char nibble nibble
-- "Note: canonical order of character encoding coincides with standard term ordering"
@@ -154,13 +220,15 @@
definition
"Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
+lemma enum_char_product_enum_nibble:
+ "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
+ by (simp add: enum_char_def enum_nibble_def)
+
instance proof
- have enum: "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
- by (simp add: enum_char_def enum_nibble_def)
show UNIV: "UNIV = set (Enum.enum :: char list)"
- by (simp add: enum UNIV_char product_list_set enum_UNIV)
+ by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
show "distinct (Enum.enum :: char list)"
- by (auto intro: inj_onI simp add: enum distinct_map distinct_product enum_distinct)
+ by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
by (simp add: UNIV enum_all_char_def list_all_iff)
show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
@@ -173,30 +241,115 @@
"card (UNIV :: char set) = 256"
by (simp add: card_UNIV_length_enum enum_char_def)
-primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
- "nibble_pair_of_char (Char n m) = (n, m)"
+definition nat_of_char :: "char \<Rightarrow> nat"
+where
+ "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
+
+lemma nat_of_char_Char:
+ "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
+ by (simp add: nat_of_char_def)
setup {*
let
val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
- val thms = map_product
- (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
- nibbles nibbles;
+ val simpset = HOL_ss addsimps
+ @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
+ fun mk_code_eqn x y =
+ Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
+ |> simplify simpset;
+ val code_eqns = map_product mk_code_eqn nibbles nibbles;
in
Global_Theory.note_thmss ""
- [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
- #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
+ [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
+ #> snd
end
*}
-lemma char_case_nibble_pair [code, code_unfold]:
- "char_case f = split f o nibble_pair_of_char"
+declare nat_of_char_simps [code]
+
+lemma nibble_of_nat_of_char_div_16:
+ "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
+ by (cases c)
+ (simp add: nat_of_char_def add_commute nat_of_nibble_less_16)
+
+lemma nibble_of_nat_nat_of_char:
+ "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
+proof (cases c)
+ case (Char x y)
+ then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
+ by (simp add: nibble_of_nat_mod_16)
+ then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
+ by (simp only: nibble_of_nat_mod_16)
+ with Char show ?thesis by (simp add: nat_of_char_def add_commute)
+qed
+
+code_datatype Char -- {* drop case certificate for char *}
+
+lemma char_case_code [code]:
+ "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
+ by (cases c)
+ (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
+
+lemma [code]:
+ "char_rec = char_case"
by (simp add: fun_eq_iff split: char.split)
-lemma char_rec_nibble_pair [code, code_unfold]:
- "char_rec f = split f o nibble_pair_of_char"
- unfolding char_case_nibble_pair [symmetric]
- by (simp add: fun_eq_iff split: char.split)
+definition char_of_nat :: "nat \<Rightarrow> char" where
+ "char_of_nat n = Enum.enum ! (n mod 256)"
+
+lemma char_of_nat_Char_nibbles:
+ "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
+proof -
+ from mod_mult2_eq [of n 16 16]
+ have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
+ then show ?thesis
+ by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
+ card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute)
+qed
+
+lemma char_of_nat_of_char [simp]:
+ "char_of_nat (nat_of_char c) = c"
+ by (cases c)
+ (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
+
+lemma nat_of_char_of_nat [simp]:
+ "nat_of_char (char_of_nat n) = n mod 256"
+proof -
+ have "n mod 256 = n mod (16 * 16)" by simp
+ then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
+ then show ?thesis
+ by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
+qed
+
+lemma inj_nat_of_char:
+ "inj nat_of_char"
+ by (rule inj_on_inverseI) (rule char_of_nat_of_char)
+
+lemma nat_of_char_eq_iff:
+ "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
+ by (rule inj_eq) (rule inj_nat_of_char)
+
+lemma nat_of_char_less_256:
+ "nat_of_char c < 256"
+proof (cases c)
+ case (Char x y)
+ with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
+ show ?thesis by (simp add: nat_of_char_def)
+qed
+
+lemma char_of_nat_mod_256:
+ "char_of_nat (n mod 256) = char_of_nat n"
+proof -
+ from nibble_of_nat_mod_16 [of "n mod 256"]
+ have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
+ with nibble_of_nat_mod_16 [of n]
+ have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
+ have "n mod 256 = n mod (16 * 16)" by simp
+ then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
+ show ?thesis
+ by (simp add: char_of_nat_Char_nibbles *)
+ (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
+qed
subsection {* Strings as dedicated type *}
@@ -228,8 +381,9 @@
end
-lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
-by(simp add: STR_inject)
+lemma STR_inject' [simp]:
+ "STR xs = STR ys \<longleftrightarrow> xs = ys"
+ by (simp add: STR_inject)
subsection {* Code generator *}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Feb 15 11:47:33 2013 +0100
@@ -155,7 +155,7 @@
fun multi_base_blacklist ctxt ho_atp =
["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
"ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
- "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
+ "weak_case_cong", "nat_of_char_simps", "nibble.simps",
"nibble.distinct"]
|> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
append ["induct", "inducts"]
--- a/src/HOL/Tools/string_code.ML Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Tools/string_code.ML Fri Feb 15 11:47:33 2013 +0100
@@ -27,14 +27,14 @@
| _ => NONE
end;
-fun implode_string char' nibbles' mk_char mk_string ts =
+fun implode_string literals char' nibbles' ts =
let
fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
if c = char' then decode_char nibbles' (t1, t2) else NONE
| implode_char _ = NONE;
val ts' = map_filter implode_char ts;
in if length ts = length ts'
- then (SOME o Code_Printer.str o mk_string o implode) ts'
+ then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
else NONE
end;
@@ -50,10 +50,9 @@
fun add_literal_list_string target =
let
- fun pretty literals (nil' :: cons' :: char' :: nibbles') pr thm vars fxy [(t1, _), (t2, _)] =
+ fun pretty literals (nil' :: cons' :: char' :: nibbles') pr _ vars fxy [(t1, _), (t2, _)] =
case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
- of SOME ts => (case implode_string char' nibbles'
- (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
+ of SOME ts => (case implode_string literals char' nibbles' ts
of SOME p => p
| NONE =>
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
@@ -77,8 +76,7 @@
let
fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
case List_Code.implode_list nil' cons' t
- of SOME ts => (case implode_string char' nibbles'
- (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
+ of SOME ts => (case implode_string literals char' nibbles' ts
of SOME p => p
| NONE => Code_Printer.eqn_error thm "Illegal message expression")
| NONE => Code_Printer.eqn_error thm "Illegal message expression";
--- a/src/HOL/Tools/string_syntax.ML Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Tools/string_syntax.ML Fri Feb 15 11:47:33 2013 +0100
@@ -81,7 +81,7 @@
fun list_ast_tr' [args] =
Ast.Appl [Ast.Constant @{syntax_const "_String"},
syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
- | list_ast_tr' ts = raise Match;
+ | list_ast_tr' _ = raise Match;
(* theory setup *)