--- a/NEWS Wed Apr 25 14:13:44 2018 +0200
+++ b/NEWS Wed Apr 25 16:03:15 2018 +0200
@@ -210,7 +210,7 @@
* Type "String.literal" (for code generation) is now isomorphic
to lists of 7-bit (ASCII) values; concrete values can be written
as "STR ''...''" for sequences of printable characters and
- "ASCII 0x..." for one single ASCII code point given
+ "STR 0x..." for one single ASCII code point given
as hexadecimal numeral.
* Type "String.literal" supports concatenation "... + ..."
--- a/src/Doc/Codegen/Adaptation.thy Wed Apr 25 14:13:44 2018 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Wed Apr 25 16:03:15 2018 +0200
@@ -174,7 +174,7 @@
Literal values of type @{typ String.literal} can be written
as @{text "STR ''\<dots>''"} for sequences of printable characters and
- @{text "ASCII 0x\<dots>"} for one single ASCII code point given
+ @{text "STR 0x\<dots>"} for one single ASCII code point given
as hexadecimal numeral; @{typ String.literal} supports concatenation
@{text "\<dots> + \<dots>"} for all standard target languages.
--- a/src/HOL/Library/Code_Test.thy Wed Apr 25 14:13:44 2018 +0200
+++ b/src/HOL/Library/Code_Test.thy Wed Apr 25 16:03:15 2018 +0200
@@ -84,8 +84,8 @@
definition list where "list f xs = map (node \<circ> f) xs"
-definition X :: yxml_of_term where "X = yot_literal (ASCII 0x05)"
-definition Y :: yxml_of_term where "Y = yot_literal (ASCII 0x06)"
+definition X :: yxml_of_term where "X = yot_literal (STR 0x05)"
+definition Y :: yxml_of_term where "Y = yot_literal (STR 0x06)"
definition XY :: yxml_of_term where "XY = yot_append X Y"
definition XYX :: yxml_of_term where "XYX = yot_append XY X"
--- a/src/HOL/ROOT Wed Apr 25 14:13:44 2018 +0200
+++ b/src/HOL/ROOT Wed Apr 25 16:03:15 2018 +0200
@@ -581,6 +581,7 @@
Records
Reflection_Examples
Refute_Examples
+ Residue_Ring
Rewrite_Examples
SOS
SOS_Cert
--- a/src/HOL/String.thy Wed Apr 25 14:13:44 2018 +0200
+++ b/src/HOL/String.thy Wed Apr 25 16:03:15 2018 +0200
@@ -119,7 +119,7 @@
lemma char_of_nat [simp]:
"char_of (of_nat n) = char_of n"
by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
-
+
end
lemma inj_on_char_of_nat [simp]:
@@ -407,7 +407,7 @@
\<^enum> Printable text as string prefixed with @{text STR};
- \<^enum> A single ascii value as numerical value prefixed with @{text ASCII}.
+ \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
\<close>
instantiation String.literal :: zero
@@ -455,8 +455,8 @@
code_datatype "0 :: String.literal" String.Literal
syntax
- "_Ascii" :: "num_const \<Rightarrow> String.literal" ("ASCII _")
"_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _")
+ "_Ascii" :: "num_const \<Rightarrow> String.literal" ("STR _")
ML_file "Tools/literal.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Residue_Ring.thy Wed Apr 25 16:03:15 2018 +0200
@@ -0,0 +1,89 @@
+(* Author: Florian Haftmann, TUM
+*)
+
+section \<open>Proof of concept for residue rings over int using type numerals\<close>
+
+theory Residue_Ring
+ imports Main "HOL-Library.Type_Length"
+begin
+
+class len2 = len0 +
+ assumes len_ge_2 [iff]: "2 \<le> LENGTH('a)"
+begin
+
+subclass len
+proof
+ show "0 < LENGTH('a)" using len_ge_2
+ by arith
+qed
+
+lemma len_not_eq_Suc_0 [simp]:
+ "LENGTH('a) \<noteq> Suc 0"
+ using len_ge_2 by arith
+
+end
+
+instance bit0 and bit1 :: (len) len2
+ by standard (simp_all add: Suc_le_eq)
+
+quotient_type (overloaded) 'a residue_ring = int / "\<lambda>k l. k mod int (LENGTH('a)) = l mod int (LENGTH('a::len2))"
+ by (auto intro!: equivpI reflpI sympI transpI)
+
+context semiring_1
+begin
+
+lift_definition repr :: "'b::len2 residue_ring \<Rightarrow> 'a"
+ is "\<lambda>k. of_nat (nat (k mod int (LENGTH('b))))"
+ by simp
+
+end
+
+instantiation residue_ring :: (len2) comm_ring_1
+begin
+
+lift_definition zero_residue_ring :: "'a residue_ring"
+ is 0 .
+
+lift_definition one_residue_ring :: "'a residue_ring"
+ is 1 .
+
+lift_definition plus_residue_ring :: "'a residue_ring \<Rightarrow> 'a residue_ring \<Rightarrow> 'a residue_ring"
+ is plus
+ by (fact mod_add_cong)
+
+lift_definition uminus_residue_ring :: "'a residue_ring \<Rightarrow> 'a residue_ring"
+ is uminus
+ by (fact mod_minus_cong)
+
+lift_definition minus_residue_ring :: "'a residue_ring \<Rightarrow> 'a residue_ring \<Rightarrow> 'a residue_ring"
+ is minus
+ by (fact mod_diff_cong)
+
+lift_definition times_residue_ring :: "'a residue_ring \<Rightarrow> 'a residue_ring \<Rightarrow> 'a residue_ring"
+ is times
+ by (fact mod_mult_cong)
+
+instance
+ by (standard; transfer) (simp_all add: algebra_simps mod_eq_0_iff_dvd)
+
+end
+
+context
+ includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+ "((\<longleftrightarrow>) ===> pcr_residue_ring) of_bool of_bool"
+ by (unfold of_bool_def [abs_def]; transfer_prover)
+
+lemma [transfer_rule]:
+ "((=) ===> pcr_residue_ring) numeral numeral"
+ by (rule transfer_rule_numeral; transfer_prover)
+
+lemma [transfer_rule]:
+ "((=) ===> pcr_residue_ring) int of_nat"
+ by (rule transfer_rule_of_nat; transfer_prover)
+
+end
+
+end
--- a/src/Tools/Code/code_scala.ML Wed Apr 25 14:13:44 2018 +0200
+++ b/src/Tools/Code/code_scala.ML Wed Apr 25 16:03:15 2018 +0200
@@ -36,7 +36,7 @@
if i < 32 orelse i > 126
then chr i
else if i >= 128
- then error "non-ASCII byte in Haskell string literal"
+ then error "non-ASCII byte in Scala string literal"
else c
end
in quote o translate_string char end;