--- a/CONTRIBUTORS Fri Sep 25 14:11:48 2020 +0100
+++ b/CONTRIBUTORS Fri Sep 25 14:12:01 2020 +0100
@@ -20,9 +20,6 @@
and @{scala} to invoke Scala from ML.
* May 2020: Florian Haftmann
- HOL-Word based on library theory of generic bit operations.
-
-* May 2020: Florian Haftmann
Generic algebraically founded bit operations NOT, AND, OR, XOR.
* Sept. 2020: Florian Haftmann
--- a/NEWS Fri Sep 25 14:11:48 2020 +0100
+++ b/NEWS Fri Sep 25 14:12:01 2020 +0100
@@ -78,6 +78,9 @@
* Library theory "Bit_Operations" with generic bit operations.
+* Library theory "Signed_Division" provides operations for signed
+division, instantiated for type int.
+
* Session HOL-Word: Type word is restricted to bit strings consisting
of at least one bit. INCOMPATIBILITY.
@@ -100,13 +103,6 @@
* Session HOL-Word: Theory "Word_Bitwise" has been moved to AFP entry
Word_Lib as theory "Bitwise". INCOMPATIBILITY.
-* Session HOL-Word: Misc ancient material has been factored out into
-separate theories. INCOMPATIBILITY, prefer theory "More_Word"
-over "Word" to use it.
-
-* Session HOL-Word: Ancient int numeral representation has been
-factored out in separate theory "Ancient_Numeral". INCOMPATIBILITY.
-
* Session HOL-Word: Compound operation "bin_split" simplifies by default
into its components "drop_bit" and "take_bit". INCOMPATIBILITY.
@@ -117,6 +113,13 @@
into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
INCOMPATIBILITY.
+* Session HOL-Word: Misc ancient material has been factored out into
+separate theories. INCOMPATIBILITY, prefer theory "More_Word"
+over "Word" to use it.
+
+* Session HOL-Word: Ancient int numeral representation has been
+factored out in separate theory "Ancient_Numeral". INCOMPATIBILITY.
+
* Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth",
"bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now
mere input abbreviations. Minor INCOMPATIBILITY.
--- a/src/HOL/Data_Structures/Leftist_Heap.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Fri Sep 25 14:12:01 2020 +0100
@@ -97,34 +97,20 @@
subsection "Functional Correctness"
-lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2"
-by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps)
+lemma mset_merge: "mset_tree (merge t1 t2) = mset_tree t1 + mset_tree t2"
+by (induction t1 t2 rule: merge.induct) (auto simp add: node_def ac_simps)
lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
by (auto simp add: insert_def mset_merge)
-lemma get_min: "\<lbrakk> heap h; h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min(set_tree h)"
-by (induction h) (auto simp add: eq_Min_iff)
+lemma get_min: "\<lbrakk> heap t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min t = Min(set_tree t)"
+by (cases t) (auto simp add: eq_Min_iff)
-lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
-by (cases h) (auto simp: mset_merge)
+lemma mset_del_min: "mset_tree (del_min t) = mset_tree t - {# get_min t #}"
+by (cases t) (auto simp: mset_merge)
lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
-proof(induction l r rule: merge.induct)
- case (3 l1 a1 n1 r1 l2 a2 n2 r2)
- show ?case (is "ltree(merge ?t1 ?t2)")
- proof cases
- assume "a1 \<le> a2"
- hence "ltree (merge ?t1 ?t2) = ltree (node l1 a1 (merge r1 ?t2))" by simp
- also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
- by(simp add: ltree_node)
- also have "..." using "3.prems" "3.IH"(1)[OF \<open>a1 \<le> a2\<close>] by (simp)
- finally show ?thesis .
- next (* analogous but automatic *)
- assume "\<not> a1 \<le> a2"
- thus ?thesis using 3 by(simp)(auto simp: ltree_node)
- qed
-qed simp_all
+by(induction l r rule: merge.induct)(auto simp: ltree_node)
lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"
proof(induction l r rule: merge.induct)
@@ -147,10 +133,10 @@
to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
interpretation lheap: Priority_Queue_Merge
-where empty = empty and is_empty = "\<lambda>h. h = Leaf"
+where empty = empty and is_empty = "\<lambda>t. t = Leaf"
and insert = insert and del_min = del_min
and get_min = get_min and merge = merge
-and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+and invar = "\<lambda>t. heap t \<and> ltree t" and mset = mset_tree
proof(standard, goal_cases)
case 1 show ?case by (simp add: empty_def)
next
--- a/src/HOL/Library/Bit_Operations.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy Fri Sep 25 14:12:01 2020 +0100
@@ -159,6 +159,10 @@
by (rule bit_eqI)
(auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)
+lemma or_eq_0_iff:
+ \<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
+ by (auto simp add: bit_eq_iff bit_or_iff)
+
lemma disjunctive_add:
\<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
by (rule bit_eqI) (use that in \<open>simp add: bit_disjunctive_add_iff bit_or_iff\<close>)
@@ -249,6 +253,30 @@
\<open>NOT (a - b) = NOT a + b\<close>
using not_add_distrib [of a \<open>- b\<close>] by simp
+lemma (in ring_bit_operations) and_eq_minus_1_iff:
+ \<open>a AND b = - 1 \<longleftrightarrow> a = - 1 \<and> b = - 1\<close>
+proof
+ assume \<open>a = - 1 \<and> b = - 1\<close>
+ then show \<open>a AND b = - 1\<close>
+ by simp
+next
+ assume \<open>a AND b = - 1\<close>
+ have *: \<open>bit a n\<close> \<open>bit b n\<close> if \<open>2 ^ n \<noteq> 0\<close> for n
+ proof -
+ from \<open>a AND b = - 1\<close>
+ have \<open>bit (a AND b) n = bit (- 1) n\<close>
+ by (simp add: bit_eq_iff)
+ then show \<open>bit a n\<close> \<open>bit b n\<close>
+ using that by (simp_all add: bit_and_iff)
+ qed
+ have \<open>a = - 1\<close>
+ by (rule bit_eqI) (simp add: *)
+ moreover have \<open>b = - 1\<close>
+ by (rule bit_eqI) (simp add: *)
+ ultimately show \<open>a = - 1 \<and> b = - 1\<close>
+ by simp
+qed
+
lemma disjunctive_diff:
\<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
proof -
--- a/src/HOL/Library/Library.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Library/Library.thy Fri Sep 25 14:12:01 2020 +0100
@@ -86,6 +86,7 @@
Saturated
Set_Algebras
Set_Idioms
+ Signed_Division
State_Monad
Stirling
Stream
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Signed_Division.thy Fri Sep 25 14:12:01 2020 +0100
@@ -0,0 +1,27 @@
+(* Author: Stefan Berghofer et al.
+*)
+
+subsection \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close>
+
+theory Signed_Division
+ imports Main
+begin
+
+class signed_division =
+ fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "sdiv" 70)
+ and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "smod" 70)
+
+instantiation int :: signed_division
+begin
+
+definition signed_divide_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>k sdiv l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)\<close> for k l :: int
+
+definition signed_modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>k smod l = k - (k sdiv l) * l\<close> for k l :: int
+
+instance ..
+
+end
+
+end
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Fri Sep 25 14:12:01 2020 +0100
@@ -41,8 +41,8 @@
val (output, rc) =
Isabelle_System.bash_output
("\"$ISABELLE_CSDP\" " ^
- Bash.string (File.platform_path in_path) ^ " " ^
- Bash.string (File.platform_path out_path));
+ File.bash_platform_path in_path ^ " " ^
+ File.bash_platform_path out_path);
val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
val result = if File.exists out_path then File.read out_path else ""
--- a/src/HOL/Library/Type_Length.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Library/Type_Length.thy Fri Sep 25 14:12:01 2020 +0100
@@ -117,4 +117,12 @@
end
+lemma less_eq_decr_length_iff [simp]:
+ \<open>n \<le> LENGTH('a::len) - Suc 0 \<longleftrightarrow> n < LENGTH('a)\<close>
+ by (cases \<open>LENGTH('a)\<close>) (simp_all add: less_Suc_eq le_less)
+
+lemma decr_length_less_iff [simp]:
+ \<open>LENGTH('a::len) - Suc 0 < n \<longleftrightarrow> LENGTH('a) \<le> n\<close>
+ by (cases \<open>LENGTH('a)\<close>) auto
+
end
--- a/src/HOL/Library/code_test.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Library/code_test.ML Fri Sep 25 14:12:01 2020 +0100
@@ -9,22 +9,17 @@
val add_driver:
string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) ->
theory -> theory
- val overlord: bool Config.T
+ val debug: bool Config.T
val successN: string
val failureN: string
val start_markerN: string
val end_markerN: string
val test_terms: Proof.context -> term list -> string -> unit
- val test_targets: Proof.context -> term list -> string list -> unit
val test_code_cmd: string list -> string list -> Proof.context -> unit
val eval_term: string -> Proof.context -> term -> term
- val evaluate:
- (theory -> Path.T -> string list -> string ->
- {files: (Path.T * string) list,
- compile_cmd: string option,
- run_cmd: string,
- mk_code_file: string -> Path.T}) -> (string * string) option -> string -> theory ->
- (string * string) list * string -> Path.T -> string
+ val check_settings: string -> string -> string -> unit
+ val compile: string -> string -> unit
+ val evaluate: string -> string -> string
val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
@@ -120,7 +115,7 @@
fun parse_result target out =
(case split_first_last start_markerN end_markerN out of
- NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out)
+ NONE => error ("Evaluation failed for " ^ target ^ "!\nCompiler output:\n" ^ out)
| SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line)
@@ -136,9 +131,9 @@
(ts ~~ evals))]
fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
- Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for")
- @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
- @ pretty_eval ctxt evals eval_ts)
+ Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @
+ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @
+ pretty_eval ctxt evals eval_ts)
fun pretty_failures ctxt target failures =
Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
@@ -146,14 +141,14 @@
(* driver invocation *)
-val overlord = Attrib.setup_config_bool \<^binding>\<open>code_test_overlord\<close> (K false)
+val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)
-fun with_overlord_dir name f =
+fun with_debug_dir name f =
let
- val path =
+ val dir =
Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
- val _ = Isabelle_System.mkdirs path
- in Exn.release (Exn.capture f path) end
+ val _ = Isabelle_System.mkdirs dir
+ in Exn.release (Exn.capture f dir) end
fun dynamic_value_strict ctxt t compiler =
let
@@ -161,14 +156,13 @@
val (driver, target) =
(case get_driver thy compiler of
NONE => error ("No driver for target " ^ compiler)
- | SOME f => f)
- val debug = Config.get (Proof_Context.init_global thy) overlord
- val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
- fun evaluate result =
+ | SOME drv => drv)
+ val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir
+ fun eval result =
with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
|> parse_result compiler
fun evaluator program _ vs_ty deps =
- Exn.interruptible_capture evaluate
+ Exn.interruptible_capture eval
(Code_Target.compilation_text ctxt target program deps true vs_ty)
fun postproc f = map (apsnd (Option.map (map f)))
in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
@@ -229,17 +223,13 @@
val failed =
filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
handle ListPair.UnequalLengths =>
- error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
+ error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result))
in
- (case failed of [] =>
- ()
+ (case failed of
+ [] => ()
| _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
end
-fun test_targets ctxt = List.app o test_terms ctxt
-
-fun pretty_free ctxt = Syntax.pretty_term ctxt o Free
-
fun test_code_cmd raw_ts targets ctxt =
let
val ts = Syntax.read_terms ctxt raw_ts
@@ -248,8 +238,8 @@
if null frees then ()
else error (Pretty.string_of
(Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 ::
- Pretty.commas (map (pretty_free ctxt) frees))))
- in test_targets ctxt ts targets end
+ Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees))))
+ in List.app (test_terms ctxt ts) targets end
fun eval_term target ctxt t =
let
@@ -259,7 +249,7 @@
else
error (Pretty.string_of
(Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 ::
- Pretty.commas (map (pretty_free ctxt) frees))))
+ Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees))))
val T = fastype_of t
val _ =
@@ -275,182 +265,158 @@
in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
-(* generic driver *)
+(* check and invoke compiler *)
-fun evaluate mk_driver opt_env_var compilerN ctxt (code_files, value_name) =
- let
- val _ =
- (case opt_env_var of
- NONE => ()
- | SOME (env_var, env_var_dest) =>
- (case getenv env_var of
- "" =>
- error (Pretty.string_of (Pretty.para
- ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
- compilerN ^ ", set this variable to your " ^ env_var_dest ^
- " in the $ISABELLE_HOME_USER/etc/settings file.")))
- | _ => ()))
+fun check_settings compiler var descr =
+ if getenv var = "" then
+ error (Pretty.string_of (Pretty.para
+ ("Environment variable " ^ var ^ " is not set. To test code generation with " ^
+ compiler ^ ", set this variable to your " ^ descr ^
+ " in the $ISABELLE_HOME_USER/etc/settings file.")))
+ else ();
- fun compile NONE = ()
- | compile (SOME cmd) =
- let
- val (out, ret) = Isabelle_System.bash_output cmd
- in
- if ret = 0 then ()
- else error ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
- end
+fun compile compiler cmd =
+ let val (out, ret) = Isabelle_System.bash_output cmd in
+ if ret = 0 then ()
+ else error ("Compilation with " ^ compiler ^ " failed:\n" ^ cmd ^ "\n" ^ out)
+ end
- fun run path =
- let
- val modules = map fst code_files
- val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt path modules value_name
-
- val _ = List.app (fn (name, code) => File.write (mk_code_file name) code) code_files
- val _ = List.app (fn (name, content) => File.write name content) files
-
- val _ = compile compile_cmd
-
- val (out, res) = Isabelle_System.bash_output run_cmd
- val _ =
- if res = 0 then ()
- else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^
- Int.toString res ^ "\nBash output:\n" ^ out)
- in out end
- in run end
+fun evaluate compiler cmd =
+ let val (out, res) = Isabelle_System.bash_output cmd in
+ if res = 0 then out
+ else error ("Evaluation for " ^ compiler ^ " terminated with error code " ^
+ string_of_int res ^ "\nCompiler output:\n" ^ out)
+ end
(* driver for PolyML *)
val polymlN = "PolyML"
-fun mk_driver_polyml _ path _ value_name =
+fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir =
let
- val generatedN = "generated.sml"
- val driverN = "driver.sml"
+ val code_path = Path.append dir (Path.basic "generated.sml")
+ val driver_path = Path.append dir (Path.basic "driver.sml")
+ val out_path = Path.append dir (Path.basic "out")
- val code_path = Path.append path (Path.basic generatedN)
- val driver_path = Path.append path (Path.basic driverN)
- val driver =
- "fun main prog_name = \n" ^
- " let\n" ^
- " fun format_term NONE = \"\"\n" ^
- " | format_term (SOME t) = t ();\n" ^
- " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
- " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
- " val result = " ^ value_name ^ " ();\n" ^
- " val _ = print \"" ^ start_markerN ^ "\";\n" ^
- " val _ = map (print o format) result;\n" ^
- " val _ = print \"" ^ end_markerN ^ "\";\n" ^
- " in\n" ^
- " ()\n" ^
- " end;\n"
- val cmd =
- "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^
- " --use " ^ Bash.string (File.platform_path driver_path) ^
- " --eval " ^ Bash.string "main ()"
+ val code = #2 (the_single code_files);
+ val driver = \<^verbatim>\<open>
+fun main () =
+ let
+ fun format (true, _) = \<close> ^ ML_Syntax.print_string successN ^ \<^verbatim>\<open> ^ "\n"
+ | format (false, NONE) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ "\n"
+ | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
+ val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
+ val result_text = \<close> ^
+ ML_Syntax.print_string start_markerN ^
+ \<^verbatim>\<open> ^ String.concat (map format result) ^ \<close> ^
+ ML_Syntax.print_string end_markerN ^ \<^verbatim>\<open>
+ val out = BinIO.openOut \<close> ^ ML_Syntax.print_platform_path out_path ^ \<^verbatim>\<open>
+ val _ = BinIO.output (out, Byte.stringToBytes result_text)
+ val _ = BinIO.closeOut out
+ in () end;
+\<close>
in
- {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
+ File.write code_path code;
+ File.write driver_path driver;
+ ML_Context.eval
+ {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE,
+ writeln = writeln, warning = warning}
+ Position.none
+ (ML_Lex.read_text (code, Path.position code_path) @
+ ML_Lex.read_text (driver, Path.position driver_path) @
+ ML_Lex.read "main ()");
+ File.read out_path
end
-fun evaluate_in_polyml ctxt = evaluate mk_driver_polyml NONE polymlN ctxt
-
(* driver for mlton *)
val mltonN = "MLton"
val ISABELLE_MLTON = "ISABELLE_MLTON"
-fun mk_driver_mlton _ path _ value_name =
+fun evaluate_in_mlton (_: Proof.context) (code_files, value_name) dir =
let
+ val compiler = mltonN
val generatedN = "generated.sml"
val driverN = "driver.sml"
val projectN = "test"
- val ml_basisN = projectN ^ ".mlb"
- val code_path = Path.append path (Path.basic generatedN)
- val driver_path = Path.append path (Path.basic driverN)
- val ml_basis_path = Path.append path (Path.basic ml_basisN)
- val driver =
- "fun format_term NONE = \"\"\n" ^
- " | format_term (SOME t) = t ();\n" ^
- "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
- " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
- "val result = " ^ value_name ^ " ();\n" ^
- "val _ = print \"" ^ start_markerN ^ "\";\n" ^
- "val _ = map (print o format) result;\n" ^
- "val _ = print \"" ^ end_markerN ^ "\";\n"
- val ml_basis =
- "$(SML_LIB)/basis/basis.mlb\n" ^
- generatedN ^ "\n" ^
- driverN
-
- val compile_cmd =
- File.bash_path (Path.variable ISABELLE_MLTON) ^
- " -default-type intinf " ^ File.bash_path ml_basis_path
- val run_cmd = File.bash_path (Path.append path (Path.basic projectN))
+ val code_path = Path.append dir (Path.basic generatedN)
+ val driver_path = Path.append dir (Path.basic driverN)
+ val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb"))
+ val driver = \<^verbatim>\<open>
+fun format (true, _) = \<close> ^ ML_Syntax.print_string successN ^ \<^verbatim>\<open> ^ "\n"
+ | format (false, NONE) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ "\n"
+ | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
+val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
+val _ = print \<close> ^ ML_Syntax.print_string start_markerN ^ \<^verbatim>\<open>
+val _ = List.app (print o format) result
+val _ = print \<close> ^ ML_Syntax.print_string end_markerN ^ \<^verbatim>\<open>
+\<close>
+ val cmd = "\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path
in
- {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
- compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
+ check_settings compiler ISABELLE_MLTON "MLton executable";
+ List.app (File.write code_path o snd) code_files;
+ File.write driver_path driver;
+ File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN);
+ compile compiler cmd;
+ evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN)))
end
-fun evaluate_in_mlton ctxt =
- evaluate mk_driver_mlton (SOME (ISABELLE_MLTON, "MLton executable")) mltonN ctxt
-
(* driver for SML/NJ *)
val smlnjN = "SMLNJ"
val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
-fun mk_driver_smlnj _ path _ value_name =
+fun evaluate_in_smlnj (_: Proof.context) (code_files, value_name) dir =
let
+ val compiler = smlnjN
val generatedN = "generated.sml"
val driverN = "driver.sml"
- val code_path = Path.append path (Path.basic generatedN)
- val driver_path = Path.append path (Path.basic driverN)
- val driver =
- "structure Test = struct\n" ^
- "fun main prog_name =\n" ^
- " let\n" ^
- " fun format_term NONE = \"\"\n" ^
- " | format_term (SOME t) = t ();\n" ^
- " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
- " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
- " val result = " ^ value_name ^ " ();\n" ^
- " val _ = print \"" ^ start_markerN ^ "\";\n" ^
- " val _ = map (print o format) result;\n" ^
- " val _ = print \"" ^ end_markerN ^ "\";\n" ^
- " in\n" ^
- " 0\n" ^
- " end;\n" ^
- "end;"
+ val code_path = Path.append dir (Path.basic generatedN)
+ val driver_path = Path.append dir (Path.basic driverN)
+ val driver = \<^verbatim>\<open>
+structure Test =
+struct
+ fun main () =
+ let
+ fun format (true, _) = \<close> ^ ML_Syntax.print_string successN ^ \<^verbatim>\<open> ^ "\n"
+ | format (false, NONE) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ "\n"
+ | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failureN ^ \<^verbatim>\<open> ^ t () ^ "\n"
+ val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
+ val _ = print \<close> ^ ML_Syntax.print_string start_markerN ^ \<^verbatim>\<open>
+ val _ = List.app (print o format) result
+ val _ = print \<close> ^ ML_Syntax.print_string end_markerN ^ \<^verbatim>\<open>
+ in 0 end
+end
+\<close>
val ml_source =
"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
- "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^
- "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^
+ "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^
+ "; use " ^ ML_Syntax.print_string (File.platform_path driver_path) ^
"; Test.main ();"
- val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\""
in
- {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
+ check_settings compiler ISABELLE_SMLNJ "SMLNJ executable";
+ List.app (File.write code_path o snd) code_files;
+ File.write driver_path driver;
+ evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"")
end
-fun evaluate_in_smlnj ctxt =
- evaluate mk_driver_smlnj (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN ctxt
-
(* driver for OCaml *)
val ocamlN = "OCaml"
val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND"
-fun mk_driver_ocaml _ path _ value_name =
+fun evaluate_in_ocaml (_: Proof.context) (code_files, value_name) dir =
let
- val generatedN = "generated.ml"
- val driverN = "driver.ml"
+ val compiler = ocamlN
- val code_path = Path.append path (Path.basic generatedN)
- val driver_path = Path.append path (Path.basic driverN)
+ val code_path = Path.append dir (Path.basic "generated.ml")
+ val driver_path = Path.append dir (Path.basic "driver.ml")
val driver =
"let format_term = function\n" ^
" | None -> \"\"\n" ^
@@ -464,22 +430,19 @@
" let _ = List.map (fun x -> print_string (format x)) result in\n" ^
" print_string \"" ^ end_markerN ^ "\";;\n" ^
"main ();;"
-
- val compiled_path = Path.append path (Path.basic "test")
- val compile_cmd =
+ val compiled_path = Path.append dir (Path.basic "test")
+ val cmd =
"\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
- " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
+ " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^
File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
-
- val run_cmd = File.bash_path compiled_path
in
- {files = [(driver_path, driver)],
- compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
+ check_settings compiler ISABELLE_OCAMLFIND "ocamlfind executable";
+ List.app (File.write code_path o snd) code_files;
+ File.write driver_path driver;
+ compile compiler cmd;
+ evaluate compiler (File.bash_path compiled_path)
end
-fun evaluate_in_ocaml ctxt =
- evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN ctxt
-
(* driver for GHC *)
@@ -488,15 +451,15 @@
val ghc_options = Attrib.setup_config_string \<^binding>\<open>code_test_ghc\<close> (K "")
-fun mk_driver_ghc ctxt path modules value_name =
+fun evaluate_in_ghc ctxt (code_files, value_name) dir =
let
- val driverN = "Main.hs"
+ val compiler = ghcN
+ val modules = map fst code_files
- fun mk_code_file name = Path.append path (Path.basic name)
- val driver_path = Path.append path (Path.basic driverN)
+ val driver_path = Path.append dir (Path.basic "Main.hs")
val driver =
"module Main where {\n" ^
- String.concat (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
+ implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
"main = do {\n" ^
" let {\n" ^
" format_term Nothing = \"\";\n" ^
@@ -511,66 +474,57 @@
" }\n" ^
"}\n"
- val compiled_path = Path.append path (Path.basic "test")
- val compile_cmd =
+ val compiled_path = Path.append dir (Path.basic "test")
+ val cmd =
"\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
- Config.get ctxt ghc_options ^ " -o " ^ Bash.string (File.platform_path compiled_path) ^ " " ^
- Bash.string (File.platform_path driver_path) ^ " -i" ^ Bash.string (File.platform_path path)
-
- val run_cmd = File.bash_path compiled_path
+ Config.get ctxt ghc_options ^ " -o " ^
+ File.bash_platform_path compiled_path ^ " " ^
+ File.bash_platform_path driver_path ^ " -i" ^
+ File.bash_platform_path dir
in
- {files = [(driver_path, driver)],
- compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
+ check_settings compiler ISABELLE_GHC "GHC executable";
+ List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files;
+ File.write driver_path driver;
+ compile compiler cmd;
+ evaluate compiler (File.bash_path compiled_path)
end
-fun evaluate_in_ghc ctxt =
- evaluate mk_driver_ghc (SOME (ISABELLE_GHC, "GHC executable")) ghcN ctxt
-
(* driver for Scala *)
val scalaN = "Scala"
-fun mk_driver_scala _ path _ value_name =
+fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir =
let
val generatedN = "Generated_Code"
val driverN = "Driver.scala"
- val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
- val driver_path = Path.append path (Path.basic driverN)
- val driver =
- "import " ^ generatedN ^ "._\n" ^
- "object Test {\n" ^
- " def format_term(x : Option[Unit => String]) : String = x match {\n" ^
- " case None => \"\"\n" ^
- " case Some(x) => x(())\n" ^
- " }\n" ^
- " def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
- " case (true, _) => \"True\\n\"\n" ^
- " case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
- " }\n" ^
- " def main(args:Array[String]) = {\n" ^
- " val result = " ^ value_name ^ "(());\n" ^
- " print(\"" ^ start_markerN ^ "\");\n" ^
- " result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
- " print(\"" ^ end_markerN ^ "\");\n" ^
- " }\n" ^
- "}\n"
+ val code_path = Path.append dir (Path.basic (generatedN ^ ".scala"))
+ val driver_path = Path.append dir (Path.basic driverN)
+ val out_path = Path.append dir (Path.basic "out")
- val compile_cmd =
- "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path path) ^
- " -classpath " ^ Bash.string (File.platform_path path) ^ " " ^
- Bash.string (File.platform_path code_path) ^ " " ^
- Bash.string (File.platform_path driver_path)
-
- val run_cmd = "isabelle_scala scala -cp " ^ Bash.string (File.platform_path path) ^ " Test"
+ val code = #2 (the_single code_files);
+ val driver = \<^verbatim>\<open>
+{
+ val result = \<close> ^ value_name ^ \<^verbatim>\<open>(())
+ val result_text =
+ result.map(
+ {
+ case (true, _) => "True\n"
+ case (false, None) => "False\n"
+ case (false, Some(t)) => "False" + t(()) + "\n"
+ }).mkString
+ isabelle.File.write(
+ isabelle.Path.explode(\<close> ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>),
+ \<close> ^ quote start_markerN ^ \<^verbatim>\<open> + result_text + \<close> ^ quote end_markerN ^ \<^verbatim>\<open>)
+}\<close>
in
- {files = [(driver_path, driver)],
- compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
+ File.write code_path code;
+ File.write driver_path driver;
+ Scala_Compiler.toplevel true (code ^ driver);
+ File.read out_path
end
-fun evaluate_in_scala ctxt = evaluate mk_driver_scala NONE scalaN ctxt
-
(* command setup *)
@@ -583,7 +537,7 @@
val target_Scala = "Scala_eval"
val target_Haskell = "Haskell_eval"
-val _ = Theory.setup
+val _ = Theory.setup
(Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)])
#> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)]))
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML Fri Sep 25 14:12:01 2020 +0100
@@ -223,8 +223,7 @@
val object_file = tmp_file (module^".o")
val _ = File.write module_file source
val _ =
- Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^
- Bash.string (File.platform_path module_file))
+ Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ File.bash_platform_path module_file)
val _ =
if not (File.exists object_file) then
raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
@@ -310,8 +309,7 @@
val _ = File.write call_file call_source
val _ =
Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^
- Bash.string (File.platform_path module_file) ^ " " ^
- Bash.string (File.platform_path call_file))
+ File.bash_platform_path module_file ^ " " ^ File.bash_platform_path call_file)
val result = File.read result_file handle IO.Io _ =>
raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
val t' = parse_result arity_of result
--- a/src/HOL/Parity.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Parity.thy Fri Sep 25 14:12:01 2020 +0100
@@ -1193,6 +1193,10 @@
context semiring_bits
begin
+lemma bit_of_bool_iff:
+ \<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
+ by (simp add: bit_1_iff)
+
lemma even_of_nat_iff:
\<open>even (of_nat n) \<longleftrightarrow> even n\<close>
by (induction n rule: nat_bit_induct) simp_all
--- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Fri Sep 25 14:12:01 2020 +0100
@@ -26,7 +26,7 @@
proof -
from H8 have "nat j <= 15" by simp
with assms show ?thesis
- by (simp add: f_def bwsimps int_word_uint take_bit_int_eq_self)
+ by (simp add: f_def bwsimps take_bit_int_eq_self)
qed
spark_vc function_f_7
@@ -34,7 +34,7 @@
from H7 have "16 <= nat j" by simp
moreover from H8 have "nat j <= 31" by simp
ultimately show ?thesis using assms
- by (simp only: f_def bwsimps int_word_uint)
+ by (simp only: f_def bwsimps)
(simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
qed
@@ -43,7 +43,7 @@
from H7 have "32 <= nat j" by simp
moreover from H8 have "nat j <= 47" by simp
ultimately show ?thesis using assms
- by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
+ by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
qed
spark_vc function_f_9
@@ -51,7 +51,7 @@
from H7 have "48 <= nat j" by simp
moreover from H8 have "nat j <= 63" by simp
ultimately show ?thesis using assms
- by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
+ by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
qed
spark_vc function_f_10
@@ -59,7 +59,7 @@
from H2 have "nat j <= 79" by simp
moreover from H12 have "64 <= nat j" by simp
ultimately show ?thesis using assms
- by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
+ by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
qed
spark_end
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Fri Sep 25 14:12:01 2020 +0100
@@ -54,9 +54,7 @@
assumes "0 <= (x::int)"
assumes "x <= 4294967295"
shows"uint(word_of_int x::word32) = x"
- unfolding int_word_uint
- using assms
- by simp
+ using assms by (simp add: take_bit_int_eq_self)
lemma steps_step: "steps X cc (Suc i) = step_both X (steps X cc i) i"
unfolding steps_def
@@ -197,13 +195,13 @@
word_add_def
uint_word_of_int_id[OF \<open>0 <= a\<close> \<open>a <= ?M\<close>]
uint_word_of_int_id[OF \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>]
- int_word_uint
+ using \<open>a mod ?MM = a\<close>
+ \<open>e mod ?MM = e\<close>
+ \<open>?X mod ?MM = ?X\<close>
unfolding \<open>?MM = 2 ^ LENGTH(32)\<close>
- unfolding word_uint.Abs_norm
- by (simp add:
- \<open>a mod ?MM = a\<close>
- \<open>e mod ?MM = e\<close>
- \<open>?X mod ?MM = ?X\<close>)
+ apply (simp only: flip: take_bit_eq_mod add: uint_word_of_int_eq)
+ apply (metis (mono_tags, hide_lams) of_int_of_nat_eq ucast_id uint_word_of_int_eq unsigned_of_int)
+ done
qed
have BR:
@@ -240,14 +238,14 @@
word_add_def
uint_word_of_int_id[OF \<open>0 <= a'\<close> \<open>a' <= ?M\<close>]
uint_word_of_int_id[OF \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>]
- int_word_uint
nat_transfer
+ using \<open>a' mod ?MM = a'\<close>
+ \<open>e' mod ?MM = e'\<close>
+ \<open>?X mod ?MM = ?X\<close>
unfolding \<open>?MM = 2 ^ LENGTH(32)\<close>
- unfolding word_uint.Abs_norm
- by (simp add:
- \<open>a' mod ?MM = a'\<close>
- \<open>e' mod ?MM = e'\<close>
- \<open>?X mod ?MM = ?X\<close>)
+ apply (simp only: flip: take_bit_eq_mod add: uint_word_of_int_eq)
+ apply (metis (mono_tags, hide_lams) of_nat_nat_take_bit_eq ucast_id unsigned_of_int)
+ done
qed
show ?thesis
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Sep 25 14:12:01 2020 +0100
@@ -263,9 +263,9 @@
val cmd =
"exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
(space_implode " "
- (map (Bash.string o File.platform_path)
+ (map File.bash_platform_path
(map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
- " -o " ^ Bash.string (File.platform_path executable) ^ ";"
+ " -o " ^ File.bash_platform_path executable ^ ";"
val (_, compilation_time) =
elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
val _ = Quickcheck.add_timing compilation_time current_result
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 14:12:01 2020 +0100
@@ -50,7 +50,7 @@
fun make_command command options problem_path proof_path =
Bash.strings (command () @ options) ^ " " ^
- Bash.string (File.platform_path problem_path) ^
+ File.bash_platform_path problem_path ^
" > " ^ File.bash_path proof_path ^ " 2>&1"
fun with_trace ctxt msg f x =
--- a/src/HOL/Word/Misc_Typedef.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy Fri Sep 25 14:12:01 2020 +0100
@@ -7,10 +7,10 @@
section \<open>Type Definition Theorems\<close>
theory Misc_Typedef
- imports Main
+ imports Main Word
begin
-section "More lemmas about normal type definitions"
+subsection "More lemmas about normal type definitions"
lemma tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A"
and tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x"
@@ -197,5 +197,161 @@
lemmas td_ext_def' =
td_ext_def [unfolded type_definition_def td_ext_axioms_def]
+
+subsection \<open>Type-definition locale instantiations\<close>
+
+definition uints :: "nat \<Rightarrow> int set"
+ \<comment> \<open>the sets of integers representing the words\<close>
+ where "uints n = range (take_bit n)"
+
+definition sints :: "nat \<Rightarrow> int set"
+ where "sints n = range (signed_take_bit (n - 1))"
+
+lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
+ by (simp add: uints_def range_bintrunc)
+
+lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
+ by (simp add: sints_def range_sbintrunc)
+
+definition unats :: "nat \<Rightarrow> nat set"
+ where "unats n = {i. i < 2 ^ n}"
+
+\<comment> \<open>naturals\<close>
+lemma uints_unats: "uints n = int ` unats n"
+ apply (unfold unats_def uints_num)
+ apply safe
+ apply (rule_tac image_eqI)
+ apply (erule_tac nat_0_le [symmetric])
+ by auto
+
+lemma unats_uints: "unats n = nat ` uints n"
+ by (auto simp: uints_unats image_iff)
+
+lemma td_ext_uint:
+ "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
+ (\<lambda>w::int. w mod 2 ^ LENGTH('a))"
+ apply (unfold td_ext_def')
+ apply transfer
+ apply (simp add: uints_num take_bit_eq_mod)
+ done
+
+interpretation word_uint:
+ td_ext
+ "uint::'a::len word \<Rightarrow> int"
+ word_of_int
+ "uints (LENGTH('a::len))"
+ "\<lambda>w. w mod 2 ^ LENGTH('a::len)"
+ by (fact td_ext_uint)
+
+lemmas td_uint = word_uint.td_thm
+lemmas int_word_uint = word_uint.eq_norm
+
+lemma td_ext_ubin:
+ "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
+ (take_bit (LENGTH('a)))"
+ apply standard
+ apply transfer
+ apply simp
+ done
+
+interpretation word_ubin:
+ td_ext
+ "uint::'a::len word \<Rightarrow> int"
+ word_of_int
+ "uints (LENGTH('a::len))"
+ "take_bit (LENGTH('a::len))"
+ by (fact td_ext_ubin)
+
+lemma td_ext_unat [OF refl]:
+ "n = LENGTH('a::len) \<Longrightarrow>
+ td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
+ apply (standard; transfer)
+ apply (simp_all add: unats_def take_bit_of_nat take_bit_nat_eq_self_iff
+ flip: take_bit_eq_mod)
+ done
+
+lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
+
+interpretation word_unat:
+ td_ext
+ "unat::'a::len word \<Rightarrow> nat"
+ of_nat
+ "unats (LENGTH('a::len))"
+ "\<lambda>i. i mod 2 ^ LENGTH('a::len)"
+ by (rule td_ext_unat)
+
+lemmas td_unat = word_unat.td_thm
+
+lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
+
+lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))"
+ for z :: "'a::len word"
+ apply (unfold unats_def)
+ apply clarsimp
+ apply (rule xtrans, rule unat_lt2p, assumption)
+ done
+
+lemma td_ext_sbin:
+ "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
+ (signed_take_bit (LENGTH('a) - 1))"
+ by (standard; transfer) (auto simp add: sints_def)
+
+lemma td_ext_sint:
+ "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
+ (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) -
+ 2 ^ (LENGTH('a) - 1))"
+ using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
+
+text \<open>
+ We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version
+ and interpretations do not produce thm duplicates. I.e.
+ we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>,
+ because the latter is the same thm as the former.
+\<close>
+interpretation word_sint:
+ td_ext
+ "sint ::'a::len word \<Rightarrow> int"
+ word_of_int
+ "sints (LENGTH('a::len))"
+ "\<lambda>w. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) -
+ 2 ^ (LENGTH('a::len) - 1)"
+ by (rule td_ext_sint)
+
+interpretation word_sbin:
+ td_ext
+ "sint ::'a::len word \<Rightarrow> int"
+ word_of_int
+ "sints (LENGTH('a::len))"
+ "signed_take_bit (LENGTH('a::len) - 1)"
+ by (rule td_ext_sbin)
+
+lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]
+
+lemmas td_sint = word_sint.td
+
+lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"
+ by (fact uints_def [unfolded no_bintr_alt1])
+
+lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]
+lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]
+
+lemmas bintr_num =
+ word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
+lemmas sbintr_num =
+ word_sbin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
+
+lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
+lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
+
+interpretation test_bit:
+ td_ext
+ "(!!) :: 'a::len word \<Rightarrow> nat \<Rightarrow> bool"
+ set_bits
+ "{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len)}"
+ "(\<lambda>h i. h i \<and> i < LENGTH('a::len))"
+ by standard
+ (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq)
+
+lemmas td_nth = test_bit.td_thm
+
end
-
--- a/src/HOL/Word/More_Word.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Word/More_Word.thy Fri Sep 25 14:12:01 2020 +0100
@@ -13,6 +13,7 @@
Misc_Arithmetic
Misc_set_bit
Misc_lsb
+ Misc_Typedef
begin
declare signed_take_bit_Suc [simp]
--- a/src/HOL/Word/Reversed_Bit_Lists.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Word/Reversed_Bit_Lists.thy Fri Sep 25 14:12:01 2020 +0100
@@ -5,7 +5,7 @@
section \<open>Bit values as reversed lists of bools\<close>
theory Reversed_Bit_Lists
- imports Word
+ imports Word Misc_Typedef
begin
context comm_semiring_1
--- a/src/HOL/Word/Word.thy Fri Sep 25 14:11:48 2020 +0100
+++ b/src/HOL/Word/Word.thy Fri Sep 25 14:12:01 2020 +0100
@@ -12,7 +12,6 @@
Bits_Int
Traditional_Syntax
Bit_Comprehension
- Misc_Typedef
begin
subsection \<open>Preliminaries\<close>
@@ -75,7 +74,6 @@
transfer_rule_numeral [transfer_rule]
transfer_rule_of_nat [transfer_rule]
transfer_rule_of_int [transfer_rule]
-
begin
lemma power_transfer_word [transfer_rule]:
@@ -275,6 +273,14 @@
\<open>v = w \<longleftrightarrow> unsigned v = unsigned w\<close>
by (auto intro: unsigned_word_eqI)
+lemma inj_unsigned [simp]:
+ \<open>inj unsigned\<close>
+ by (rule injI) (simp add: unsigned_word_eqI)
+
+lemma unsigned_eq_0_iff:
+ \<open>unsigned w = 0 \<longleftrightarrow> w = 0\<close>
+ using word_eq_iff_unsigned [of w 0] by simp
+
end
context ring_1
@@ -326,6 +332,14 @@
\<open>v = w \<longleftrightarrow> signed v = signed w\<close>
by (auto intro: signed_word_eqI)
+lemma inj_signed [simp]:
+ \<open>inj signed\<close>
+ by (rule injI) (simp add: signed_word_eqI)
+
+lemma signed_eq_0_iff:
+ \<open>signed w = 0 \<longleftrightarrow> w = 0\<close>
+ using word_eq_iff_signed [of w 0] by simp
+
end
abbreviation unat :: \<open>'a::len word \<Rightarrow> nat\<close>
@@ -403,6 +417,10 @@
\<open>nat (uint w) = unat w\<close>
by transfer simp
+lemma sgn_uint_eq [simp]:
+ \<open>sgn (uint w) = of_bool (w \<noteq> 0)\<close>
+ by transfer (simp add: less_le)
+
text \<open>Aliasses only for code generation\<close>
context
@@ -561,6 +579,49 @@
by transfer rule
+
+subsection \<open>Enumeration\<close>
+
+lemma inj_on_word_of_nat:
+ \<open>inj_on (word_of_nat :: nat \<Rightarrow> 'a::len word) {0..<2 ^ LENGTH('a)}\<close>
+ by (rule inj_onI; transfer) (simp_all add: take_bit_int_eq_self)
+
+lemma UNIV_word_eq_word_of_nat:
+ \<open>(UNIV :: 'a::len word set) = word_of_nat ` {0..<2 ^ LENGTH('a)}\<close> (is \<open>_ = ?A\<close>)
+proof
+ show \<open>word_of_nat ` {0..<2 ^ LENGTH('a)} \<subseteq> UNIV\<close>
+ by simp
+ show \<open>UNIV \<subseteq> ?A\<close>
+ proof
+ fix w :: \<open>'a word\<close>
+ show \<open>w \<in> (word_of_nat ` {0..<2 ^ LENGTH('a)} :: 'a word set)\<close>
+ by (rule image_eqI [of _ _ \<open>unat w\<close>]; transfer) simp_all
+ qed
+qed
+
+instantiation word :: (len) enum
+begin
+
+definition enum_word :: \<open>'a word list\<close>
+ where \<open>enum_word = map word_of_nat [0..<2 ^ LENGTH('a)]\<close>
+
+definition enum_all_word :: \<open>('a word \<Rightarrow> bool) \<Rightarrow> bool\<close>
+ where \<open>enum_all_word = Ball UNIV\<close>
+
+definition enum_ex_word :: \<open>('a word \<Rightarrow> bool) \<Rightarrow> bool\<close>
+ where \<open>enum_ex_word = Bex UNIV\<close>
+
+lemma [code]:
+ \<open>Enum.enum_all P \<longleftrightarrow> Ball UNIV P\<close>
+ \<open>Enum.enum_ex P \<longleftrightarrow> Bex UNIV P\<close> for P :: \<open>'a word \<Rightarrow> bool\<close>
+ by (simp_all add: enum_all_word_def enum_ex_word_def)
+
+instance
+ by standard (simp_all add: UNIV_word_eq_word_of_nat inj_on_word_of_nat enum_word_def enum_all_word_def enum_ex_word_def distinct_map)
+
+end
+
+
subsection \<open>Bit-wise operations\<close>
instantiation word :: (len) semiring_modulo
@@ -1066,11 +1127,11 @@
context unique_euclidean_semiring_numeral
begin
-lemma unsigned_greater_eq:
+lemma unsigned_greater_eq [simp]:
\<open>0 \<le> unsigned w\<close> for w :: \<open>'b::len word\<close>
by (transfer fixing: less_eq) simp
-lemma unsigned_less:
+lemma unsigned_less [simp]:
\<open>unsigned w < 2 ^ LENGTH('b)\<close> for w :: \<open>'b::len word\<close>
by (transfer fixing: less) simp
@@ -1933,138 +1994,6 @@
qed
-subsection \<open>Type-definition locale instantiations\<close>
-
-definition uints :: "nat \<Rightarrow> int set"
- \<comment> \<open>the sets of integers representing the words\<close>
- where "uints n = range (take_bit n)"
-
-definition sints :: "nat \<Rightarrow> int set"
- where "sints n = range (signed_take_bit (n - 1))"
-
-lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
- by (simp add: uints_def range_bintrunc)
-
-lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
- by (simp add: sints_def range_sbintrunc)
-
-definition unats :: "nat \<Rightarrow> nat set"
- where "unats n = {i. i < 2 ^ n}"
-
-\<comment> \<open>naturals\<close>
-lemma uints_unats: "uints n = int ` unats n"
- apply (unfold unats_def uints_num)
- apply safe
- apply (rule_tac image_eqI)
- apply (erule_tac nat_0_le [symmetric])
- by auto
-
-lemma unats_uints: "unats n = nat ` uints n"
- by (auto simp: uints_unats image_iff)
-
-lemma td_ext_uint:
- "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
- (\<lambda>w::int. w mod 2 ^ LENGTH('a))"
- apply (unfold td_ext_def')
- apply transfer
- apply (simp add: uints_num take_bit_eq_mod)
- done
-
-interpretation word_uint:
- td_ext
- "uint::'a::len word \<Rightarrow> int"
- word_of_int
- "uints (LENGTH('a::len))"
- "\<lambda>w. w mod 2 ^ LENGTH('a::len)"
- by (fact td_ext_uint)
-
-lemmas td_uint = word_uint.td_thm
-lemmas int_word_uint = word_uint.eq_norm
-
-lemma td_ext_ubin:
- "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
- (take_bit (LENGTH('a)))"
- apply standard
- apply transfer
- apply simp
- done
-
-interpretation word_ubin:
- td_ext
- "uint::'a::len word \<Rightarrow> int"
- word_of_int
- "uints (LENGTH('a::len))"
- "take_bit (LENGTH('a::len))"
- by (fact td_ext_ubin)
-
-lemma td_ext_unat [OF refl]:
- "n = LENGTH('a::len) \<Longrightarrow>
- td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
- apply (standard; transfer)
- apply (simp_all add: unats_def take_bit_of_nat take_bit_nat_eq_self_iff
- flip: take_bit_eq_mod)
- done
-
-lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
-
-interpretation word_unat:
- td_ext
- "unat::'a::len word \<Rightarrow> nat"
- of_nat
- "unats (LENGTH('a::len))"
- "\<lambda>i. i mod 2 ^ LENGTH('a::len)"
- by (rule td_ext_unat)
-
-lemmas td_unat = word_unat.td_thm
-
-lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
-
-lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))"
- for z :: "'a::len word"
- apply (unfold unats_def)
- apply clarsimp
- apply (rule xtrans, rule unat_lt2p, assumption)
- done
-
-lemma td_ext_sbin:
- "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
- (signed_take_bit (LENGTH('a) - 1))"
- by (standard; transfer) (auto simp add: sints_def)
-
-lemma td_ext_sint:
- "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
- (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) -
- 2 ^ (LENGTH('a) - 1))"
- using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
-
-text \<open>
- We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version
- and interpretations do not produce thm duplicates. I.e.
- we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>,
- because the latter is the same thm as the former.
-\<close>
-interpretation word_sint:
- td_ext
- "sint ::'a::len word \<Rightarrow> int"
- word_of_int
- "sints (LENGTH('a::len))"
- "\<lambda>w. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) -
- 2 ^ (LENGTH('a::len) - 1)"
- by (rule td_ext_sint)
-
-interpretation word_sbin:
- td_ext
- "sint ::'a::len word \<Rightarrow> int"
- word_of_int
- "sints (LENGTH('a::len))"
- "signed_take_bit (LENGTH('a::len) - 1)"
- by (rule td_ext_sbin)
-
-lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]
-
-lemmas td_sint = word_sint.td
-
-
subsection \<open>More shift operations\<close>
lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
@@ -2317,29 +2246,27 @@
where "max_word \<equiv> - 1"
-subsection \<open>Theorems about typedefs\<close>
+subsection \<open>More on conversions\<close>
+
+lemma int_word_sint:
+ \<open>sint (word_of_int x :: 'a::len word) = (x + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)\<close>
+ by transfer (simp add: no_sbintr_alt2)
lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) bin"
- by (auto simp: sint_uint word_ubin.eq_norm sbintrunc_bintrunc_lt)
+ by simp
lemma uint_sint: "uint w = take_bit (LENGTH('a)) (sint w)"
for w :: "'a::len word"
- by (auto simp: sint_uint bintrunc_sbintrunc_le)
+ by transfer simp
lemma bintr_uint: "LENGTH('a) \<le> n \<Longrightarrow> take_bit n (uint w) = uint w"
for w :: "'a::len word"
- apply (subst word_ubin.norm_Rep [symmetric])
- apply (simp only: bintrunc_bintrunc_min word_size)
- apply (simp add: min.absorb2)
- done
+ by transfer (simp add: min_def)
lemma wi_bintr:
"LENGTH('a::len) \<le> n \<Longrightarrow>
word_of_int (take_bit n w) = (word_of_int w :: 'a word)"
- by (auto simp: word_ubin.norm_eq_iff [symmetric] min.absorb1)
-
-lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"
- by (fact uints_def [unfolded no_bintr_alt1])
+ by transfer simp
lemma word_numeral_alt: "numeral b = word_of_int (numeral b)"
by (induct b, simp_all only: numeral.simps word_of_int_homs)
@@ -2354,19 +2281,19 @@
lemma uint_bintrunc [simp]:
"uint (numeral bin :: 'a word) =
take_bit (LENGTH('a::len)) (numeral bin)"
- unfolding word_numeral_alt by (rule word_ubin.eq_norm)
+ by transfer rule
lemma uint_bintrunc_neg [simp]:
"uint (- numeral bin :: 'a word) = take_bit (LENGTH('a::len)) (- numeral bin)"
- by (simp only: word_neg_numeral_alt word_ubin.eq_norm)
+ by transfer rule
lemma sint_sbintrunc [simp]:
"sint (numeral bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) (numeral bin)"
- by (simp only: word_numeral_alt word_sbin.eq_norm)
+ by transfer simp
lemma sint_sbintrunc_neg [simp]:
"sint (- numeral bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) (- numeral bin)"
- by (simp only: word_neg_numeral_alt word_sbin.eq_norm)
+ by transfer simp
lemma unat_bintrunc [simp]:
"unat (numeral bin :: 'a::len word) = nat (take_bit (LENGTH('a)) (numeral bin))"
@@ -2378,29 +2305,22 @@
lemma size_0_eq: "size w = 0 \<Longrightarrow> v = w"
for v w :: "'a::len word"
- apply (unfold word_size)
- apply (rule word_uint.Rep_eqD)
- apply (rule box_equals)
- defer
- apply (rule word_ubin.norm_Rep)+
- apply simp
- done
+ by transfer simp
lemma uint_ge_0 [iff]: "0 \<le> uint x"
- for x :: "'a::len word"
- using word_uint.Rep [of x] by (simp add: uints_num)
+ by (fact unsigned_greater_eq)
lemma uint_lt2p [iff]: "uint x < 2 ^ LENGTH('a)"
for x :: "'a::len word"
- using word_uint.Rep [of x] by (simp add: uints_num)
+ by (fact unsigned_less)
lemma sint_ge: "- (2 ^ (LENGTH('a) - 1)) \<le> sint x"
for x :: "'a::len word"
- using word_sint.Rep [of x] by (simp add: sints_num)
+ using sint_greater_eq [of x] by simp
lemma sint_lt: "sint x < 2 ^ (LENGTH('a) - 1)"
for x :: "'a::len word"
- using word_sint.Rep [of x] by (simp add: sints_num)
+ using sint_less [of x] by simp
lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0"
by (simp add: sign_Pls_ge_0)
@@ -2424,36 +2344,37 @@
by transfer simp
lemma uint_numeral: "uint (numeral b :: 'a::len word) = numeral b mod 2 ^ LENGTH('a)"
- by (simp only: word_numeral_alt int_word_uint)
+ by (simp flip: take_bit_eq_mod add: of_nat_take_bit)
lemma uint_neg_numeral: "uint (- numeral b :: 'a::len word) = - numeral b mod 2 ^ LENGTH('a)"
- by (simp only: word_neg_numeral_alt int_word_uint)
+ by (simp flip: take_bit_eq_mod add: of_nat_take_bit)
lemma unat_numeral: "unat (numeral b :: 'a::len word) = numeral b mod 2 ^ LENGTH('a)"
by transfer (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
lemma sint_numeral:
"sint (numeral b :: 'a::len word) =
- (numeral b +
- 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) -
- 2 ^ (LENGTH('a) - 1)"
- unfolding word_numeral_alt by (rule int_word_sint)
+ (numeral b + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)"
+ apply (transfer fixing: b)
+ using int_word_sint [of \<open>numeral b\<close>]
+ apply simp
+ done
lemma word_of_int_0 [simp, code_post]: "word_of_int 0 = 0"
- unfolding word_0_wi ..
+ by (fact of_int_0)
lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1"
- unfolding word_1_wi ..
+ by (fact of_int_1)
lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"
by (simp add: wi_hom_syms)
lemma word_of_int_numeral [simp] : "(word_of_int (numeral bin) :: 'a::len word) = numeral bin"
- by (simp only: word_numeral_alt)
+ by (fact of_int_numeral)
lemma word_of_int_neg_numeral [simp]:
"(word_of_int (- numeral bin) :: 'a::len word) = - numeral bin"
- by (simp only: word_numeral_alt wi_hom_syms)
+ by (fact of_int_neg_numeral)
lemma word_int_case_wi:
"word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ LENGTH('b::len))"
@@ -2469,14 +2390,11 @@
(\<nexists>n. x = (word_of_int n :: 'b::len word) \<and> 0 \<le> n \<and> n < 2 ^ LENGTH('b::len) \<and> \<not> P (f n))"
by transfer (auto simp add: take_bit_eq_mod)
-lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]
-lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]
-
lemma uint_range_size: "0 \<le> uint w \<and> uint w < 2 ^ size w"
- unfolding word_size by (rule uint_range')
+ by transfer simp
lemma sint_range_size: "- (2 ^ (size w - Suc 0)) \<le> sint w \<and> sint w < 2 ^ (size w - Suc 0)"
- unfolding word_size by (rule sint_range')
+ by transfer (use sbintr_ge sbintr_lt in blast)
lemma sint_above_size: "2 ^ (size w - 1) \<le> x \<Longrightarrow> sint w < x"
for w :: "'a::len word"
@@ -2491,15 +2409,11 @@
lemma test_bit_eq_iff: "test_bit u = test_bit v \<longleftrightarrow> u = v"
for u v :: "'a::len word"
- unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
-
-lemma test_bit_size [rule_format] : "w !! n \<longrightarrow> n < size w"
+ by (simp add: bit_eq_iff test_bit_eq_bit fun_eq_iff)
+
+lemma test_bit_size: "w !! n \<Longrightarrow> n < size w"
for w :: "'a::len word"
- apply (unfold word_test_bit_def)
- apply (subst word_ubin.norm_Rep [symmetric])
- apply (simp only: nth_bintr word_size)
- apply fast
- done
+ by transfer simp
lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). x !! n = y !! n)" (is \<open>?P \<longleftrightarrow> ?Q\<close>)
for x y :: "'a::len word"
@@ -2514,49 +2428,51 @@
by simp
lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bin_nth (uint w) n"
- by (simp add: word_test_bit_def word_size nth_bintr [symmetric])
+ by transfer (simp add: bit_take_bit_iff)
lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
lemma bin_nth_uint_imp: "bin_nth (uint w) n \<Longrightarrow> n < LENGTH('a)"
for w :: "'a::len word"
- apply (rule nth_bintr [THEN iffD1, THEN conjunct1])
- apply (subst word_ubin.norm_Rep)
- apply assumption
- done
+ by transfer (simp add: bit_take_bit_iff)
lemma bin_nth_sint:
"LENGTH('a) \<le> n \<Longrightarrow>
bin_nth (sint w) n = bin_nth (sint w) (LENGTH('a) - 1)"
for w :: "'a::len word"
- apply (subst word_sbin.norm_Rep [symmetric])
- apply (auto simp add: nth_sbintr)
- done
-
-lemmas bintr_num =
- word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
-lemmas sbintr_num =
- word_sbin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
+ by (transfer fixing: n) (simp add: bit_signed_take_bit_iff le_diff_conv min_def)
lemma num_of_bintr':
"take_bit (LENGTH('a::len)) (numeral a :: int) = (numeral b) \<Longrightarrow>
numeral a = (numeral b :: 'a word)"
- unfolding bintr_num by (erule subst, simp)
+proof (transfer fixing: a b)
+ assume \<open>take_bit LENGTH('a) (numeral a :: int) = numeral b\<close>
+ then have \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (numeral a :: int)) = take_bit LENGTH('a) (numeral b)\<close>
+ by simp
+ then show \<open>take_bit LENGTH('a) (numeral a :: int) = take_bit LENGTH('a) (numeral b)\<close>
+ by simp
+qed
lemma num_of_sbintr':
"signed_take_bit (LENGTH('a::len) - 1) (numeral a :: int) = (numeral b) \<Longrightarrow>
numeral a = (numeral b :: 'a word)"
- unfolding sbintr_num by (erule subst, simp)
-
+proof (transfer fixing: a b)
+ assume \<open>signed_take_bit (LENGTH('a) - 1) (numeral a :: int) = numeral b\<close>
+ then have \<open>take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - 1) (numeral a :: int)) = take_bit LENGTH('a) (numeral b)\<close>
+ by simp
+ then show \<open>take_bit LENGTH('a) (numeral a :: int) = take_bit LENGTH('a) (numeral b)\<close>
+ by simp
+qed
+
lemma num_abs_bintr:
"(numeral x :: 'a word) =
word_of_int (take_bit (LENGTH('a::len)) (numeral x))"
- by (simp only: word_ubin.Abs_norm word_numeral_alt)
+ by transfer simp
lemma num_abs_sbintr:
"(numeral x :: 'a word) =
word_of_int (signed_take_bit (LENGTH('a::len) - 1) (numeral x))"
- by (simp only: word_sbin.Abs_norm word_numeral_alt)
+ by transfer simp
text \<open>
\<open>cast\<close> -- note, no arg for new length, as it's determined by type of result,
@@ -2785,15 +2701,18 @@
and "sint (word_pred a) = signed_take_bit (LENGTH('a) - 1) (sint a - 1)"
and "sint (0 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 0"
and "sint (1 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 1"
- apply (simp_all only: word_sbin.inverse_norm [symmetric])
- apply (simp_all add: wi_hom_syms)
- apply transfer apply simp
- apply transfer apply simp
+ prefer 8
+ apply (simp add: Suc_lessI sbintrunc_minus_simps(3))
+ prefer 7
+ apply simp
+ apply transfer apply (simp add: signed_take_bit_add)
+ apply transfer apply (simp add: signed_take_bit_diff)
+ apply transfer apply (simp add: signed_take_bit_mult)
+ apply transfer apply (simp add: signed_take_bit_minus)
+ apply (metis One_nat_def id_apply of_int_eq_id sbintrunc_sbintrunc signed.rep_eq signed_word_eqI sint_sbintrunc' wi_hom_succ)
+ apply (metis (no_types, lifting) One_nat_def signed_take_bit_decr_length_iff sint_uint uint_sint uint_word_of_int_eq wi_hom_pred word_of_int_uint)
done
-lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
-lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
-
lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"
unfolding word_pred_m1 by simp
@@ -2859,9 +2778,11 @@
then have \<open>unat v * n \<ge> 2 ^ LENGTH('a)\<close>
using \<open>unat v > 0\<close> mult_le_mono [of 1 \<open>unat v\<close> \<open>2 ^ LENGTH('a)\<close> n]
by simp
- with \<open>unat w = unat v * n\<close> unat_lt2p [of w]
- show False
+ with \<open>unat w = unat v * n\<close>
+ have \<open>unat w \<ge> 2 ^ LENGTH('a)\<close>
by simp
+ with unsigned_less [of w, where ?'a = nat] show False
+ by linarith
qed
ultimately have \<open>unat w = unat v * unat (word_of_nat n :: 'a word)\<close>
by (auto simp add: take_bit_nat_eq_self_iff intro: sym)
@@ -2884,6 +2805,31 @@
by (simp add: udvd_iff_dvd)
qed
+lemma udvd_imp_dvd:
+ \<open>v dvd w\<close> if \<open>v udvd w\<close> for v w :: \<open>'a::len word\<close>
+proof -
+ from that obtain u :: \<open>'a word\<close> where \<open>unat w = unat v * unat u\<close> ..
+ then have \<open>(word_of_nat (unat w) :: 'a word) = word_of_nat (unat v * unat u)\<close>
+ by simp
+ then have \<open>w = v * u\<close>
+ by simp
+ then show \<open>v dvd w\<close> ..
+qed
+
+lemma exp_dvd_iff_exp_udvd:
+ \<open>2 ^ n dvd w \<longleftrightarrow> 2 ^ n udvd w\<close> for v w :: \<open>'a::len word\<close>
+proof
+ assume \<open>2 ^ n udvd w\<close> then show \<open>2 ^ n dvd w\<close>
+ by (rule udvd_imp_dvd)
+next
+ assume \<open>2 ^ n dvd w\<close>
+ then obtain u :: \<open>'a word\<close> where \<open>w = 2 ^ n * u\<close> ..
+ then have \<open>w = push_bit n u\<close>
+ by (simp add: push_bit_eq_mult)
+ then show \<open>2 ^ n udvd w\<close>
+ by transfer (simp add: take_bit_push_bit dvd_eq_mod_eq_0 flip: take_bit_eq_mod)
+qed
+
lemma udvd_nat_alt:
\<open>a udvd b \<longleftrightarrow> (\<exists>n. unat b = n * unat a)\<close>
by (auto simp add: udvd_iff_dvd)
@@ -2913,7 +2859,8 @@
with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ LENGTH('a)) = nat (uint w) - 1"
by (auto simp del: nat_uint_eq)
then show ?thesis
- by (simp only: unat_eq_nat_uint int_word_uint word_arith_wis mod_diff_right_eq)
+ by (simp only: unat_eq_nat_uint word_arith_wis mod_diff_right_eq)
+ (metis of_int_1 uint_word_of_int unsigned_1)
qed
lemma measure_unat: "p \<noteq> 0 \<Longrightarrow> unat (p - 1) < unat p"
@@ -2942,7 +2889,7 @@
by (metis mod_pos_pos_trivial uint_lt2p uint_mult_ge0 uint_word_ariths(3))
lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"
- by (metis (mono_tags, hide_lams) diff_ge_0_iff_ge mod_pos_pos_trivial of_nat_0_le_iff take_bit_eq_mod uint_nat uint_sub_lt2p word_sub_wi word_ubin.eq_norm)
+ by (metis diff_ge_0_iff_ge of_nat_0_le_iff uint_nat uint_sub_lt2p uint_word_of_int unique_euclidean_semiring_numeral_class.mod_less word_sub_wi)
lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend)
@@ -2994,8 +2941,9 @@
lemma word_of_int_inverse:
"word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> uint a = r"
for a :: "'a::len word"
- apply (erule word_uint.Abs_inverse' [rotated])
- apply (simp add: uints_num)
+ apply transfer
+ apply (drule sym)
+ apply (simp add: take_bit_int_eq_self)
done
lemma uint_split:
@@ -3012,7 +2960,7 @@
lemmas uint_arith_simps =
word_le_def word_less_alt
- word_uint.Rep_inject [symmetric]
+ word_uint_eq_iff
uint_sub_if' uint_plus_if'
\<comment> \<open>use this to stop, eg. \<open>2 ^ LENGTH(32)\<close> being simplified\<close>
@@ -3021,12 +2969,13 @@
\<comment> \<open>\<open>uint_arith_tac\<close>: reduce to arithmetic on int, try to solve by arith\<close>
ML \<open>
-fun uint_arith_simpset ctxt =
- ctxt addsimps @{thms uint_arith_simps}
- delsimps @{thms word_uint.Rep_inject}
- |> fold Splitter.add_split @{thms if_split_asm}
- |> fold Simplifier.add_cong @{thms power_False_cong}
-
+val uint_arith_simpset =
+ @{context}
+ |> fold Simplifier.add_simp @{thms uint_arith_simps}
+ |> fold Splitter.add_split @{thms if_split_asm}
+ |> fold Simplifier.add_cong @{thms power_False_cong}
+ |> simpset_of;
+
fun uint_arith_tacs ctxt =
let
fun arith_tac' n t =
@@ -3034,7 +2983,7 @@
handle Cooper.COOPER _ => Seq.empty;
in
[ clarify_tac ctxt 1,
- full_simp_tac (uint_arith_simpset ctxt) 1,
+ full_simp_tac (put_simpset uint_arith_simpset ctxt) 1,
ALLGOALS (full_simp_tac
(put_simpset HOL_ss ctxt
|> fold Splitter.add_split @{thms uint_splits}
@@ -3223,8 +3172,7 @@
apply clarify
apply (simp add: uint_arith_simps split: if_split_asm)
prefer 2
- apply (insert uint_range' [of s])[1]
- apply arith
+ using uint_lt2p [of s] apply simp
apply (drule add.commute [THEN xtrans(1)])
apply (simp flip: diff_less_eq)
apply (subst (asm) mult_less_cancel_right)
@@ -3253,8 +3201,10 @@
lemma iszero_word_no [simp]:
"iszero (numeral bin :: 'a::len word) =
iszero (take_bit LENGTH('a) (numeral bin :: int))"
- using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0]
- by (simp add: iszero_def [symmetric])
+ apply (simp add: iszero_def)
+ apply transfer
+ apply simp
+ done
text \<open>Use \<open>iszero\<close> to simplify equalities between word numerals.\<close>
@@ -3266,15 +3216,14 @@
lemma word_nchotomy: "\<forall>w :: 'a::len word. \<exists>n. w = of_nat n \<and> n < 2 ^ LENGTH('a)"
apply (rule allI)
- apply (rule word_unat.Abs_cases)
- apply (unfold unats_def)
- apply auto
+ apply (rule exI [of _ \<open>unat w\<close> for w :: \<open>'a word\<close>])
+ apply simp
done
lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ LENGTH('a))"
for w :: "'a::len word"
using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric]
- by (auto simp add: word_unat.inverse_norm)
+ by (auto simp flip: take_bit_eq_mod)
lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)"
unfolding word_size by (rule of_nat_eq)
@@ -3332,7 +3281,11 @@
word_arith_nat_mod
lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
- by simp
+ by (fact arg_cong)
+
+lemma unat_of_nat:
+ \<open>unat (word_of_nat x :: 'a::len word) = x mod 2 ^ LENGTH('a)\<close>
+ by transfer (simp flip: take_bit_eq_mod add: nat_take_bit_eq)
lemmas unat_word_ariths = word_arith_nat_defs
[THEN trans [OF unat_cong unat_of_nat]]
@@ -3344,14 +3297,16 @@
"unat x + unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x + y) = unat x + unat y"
for x y :: "'a::len word"
apply (auto simp: unat_word_ariths)
- apply (metis unat_lt2p word_unat.eq_norm)
+ apply (drule sym)
+ apply (metis unat_of_nat unsigned_less)
done
lemma unat_mult_lem:
"unat x * unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
for x y :: "'a::len word"
apply (auto simp: unat_word_ariths)
- apply (metis unat_lt2p word_unat.eq_norm)
+ apply (drule sym)
+ apply (metis unat_of_nat unsigned_less)
done
lemma unat_plus_if':
@@ -3362,7 +3317,8 @@
apply (auto simp: unat_word_ariths not_less)
apply (subst (asm) le_iff_add)
apply auto
- apply (metis add_less_cancel_left add_less_cancel_right le_less_trans less_imp_le mod_less unat_lt2p)
+ apply (simp flip: take_bit_eq_mod add: take_bit_nat_eq_self_iff)
+ apply (metis add.commute add_less_cancel_right le_less_trans less_imp_le unsigned_less)
done
lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b"
@@ -3424,23 +3380,34 @@
for x :: "'a::len word"
by auto (metis take_bit_nat_eq_self_iff)
-lemmas of_nat_inverse =
- word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
+lemma of_nat_inverse:
+ \<open>word_of_nat r = a \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> unat a = r\<close>
+ for a :: \<open>'a::len word\<close>
+ apply (drule sym)
+ apply transfer
+ apply (simp add: take_bit_int_eq_self)
+ done
+
+lemma word_unat_eq_iff:
+ \<open>v = w \<longleftrightarrow> unat v = unat w\<close>
+ for v w :: \<open>'a::len word\<close>
+ by (fact word_eq_iff_unsigned)
lemmas unat_splits = unat_split unat_split_asm
lemmas unat_arith_simps =
word_le_nat_alt word_less_nat_alt
- word_unat.Rep_inject [symmetric]
+ word_unat_eq_iff
unat_sub_if' unat_plus_if' unat_div unat_mod
\<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
ML \<open>
-fun unat_arith_simpset ctxt =
- ctxt addsimps @{thms unat_arith_simps}
- delsimps @{thms word_unat.Rep_inject}
- |> fold Splitter.add_split @{thms if_split_asm}
- |> fold Simplifier.add_cong @{thms power_False_cong}
+val unat_arith_simpset =
+ @{context}
+ |> fold Simplifier.add_simp @{thms unat_arith_simps}
+ |> fold Splitter.add_split @{thms if_split_asm}
+ |> fold Simplifier.add_cong @{thms power_False_cong}
+ |> simpset_of
fun unat_arith_tacs ctxt =
let
@@ -3449,7 +3416,7 @@
handle Cooper.COOPER _ => Seq.empty;
in
[ clarify_tac ctxt 1,
- full_simp_tac (unat_arith_simpset ctxt) 1,
+ full_simp_tac (put_simpset unat_arith_simpset ctxt) 1,
ALLGOALS (full_simp_tac
(put_simpset HOL_ss ctxt
|> fold Splitter.add_split @{thms unat_splits}
@@ -3492,7 +3459,7 @@
apply clarsimp
apply (drule mult_le_mono1)
apply (erule order_le_less_trans)
- apply (metis add_lessD1 div_mult_mod_eq unat_lt2p)
+ apply (metis add_lessD1 div_mult_mod_eq unsigned_less)
done
lemmas div_lt'' = order_less_imp_le [THEN div_lt']
@@ -3540,7 +3507,10 @@
lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x
lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x
-lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
+lemma le_unat_uoi:
+ \<open>y \<le> unat z \<Longrightarrow> unat (word_of_nat y :: 'a word) = y\<close>
+ for z :: \<open>'a::len word\<close>
+ by transfer (simp add: nat_take_bit_eq take_bit_nat_eq_self_iff le_less_trans)
lemmas thd = times_div_less_eq_dividend
@@ -3578,7 +3548,7 @@
done
lemma inj_uint: \<open>inj uint\<close>
- by (rule injI) simp
+ by (fact inj_unsigned)
lemma range_uint: \<open>range (uint :: 'a word \<Rightarrow> int) = {0..<2 ^ LENGTH('a::len)}\<close>
by transfer (auto simp add: bintr_lt2p range_bintrunc)
@@ -3610,8 +3580,8 @@
\<comment> \<open>following definitions require both arithmetic and bit-wise word operations\<close>
\<comment> \<open>to get \<open>word_no_log_defs\<close> from \<open>word_log_defs\<close>, using \<open>bin_log_bintrs\<close>\<close>
-lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
- folded word_ubin.eq_norm, THEN eq_reflection]
+lemmas wils1 = bin_log_bintrs [THEN word_of_int_eq_iff [THEN iffD2],
+ folded uint_word_of_int_eq, THEN eq_reflection]
\<comment> \<open>the binary operations only\<close> (* BH: why is this needed? *)
lemmas word_log_binary_defs =
@@ -3683,15 +3653,15 @@
\<open>uint (x XOR y) = uint x XOR uint y\<close>
by transfer simp
-lemma test_bit_wi [simp]:
- "(word_of_int x :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bin_nth x n"
- by (simp add: word_test_bit_def word_ubin.eq_norm nth_bintr)
-
lemma word_test_bit_transfer [transfer_rule]:
"(rel_fun pcr_word (rel_fun (=) (=)))
(\<lambda>x n. n < LENGTH('a) \<and> bit x n) (test_bit :: 'a::len word \<Rightarrow> _)"
by (simp only: test_bit_eq_bit) transfer_prover
+lemma test_bit_wi [simp]:
+ "(word_of_int x :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bin_nth x n"
+ by transfer simp
+
lemma word_ops_nth_size:
"n < size x \<Longrightarrow>
(x OR y) !! n = (x !! n | y !! n) \<and>
@@ -3923,17 +3893,6 @@
\<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close>
by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff)
-interpretation test_bit:
- td_ext
- "(!!) :: 'a::len word \<Rightarrow> nat \<Rightarrow> bool"
- set_bits
- "{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len)}"
- "(\<lambda>h i. h i \<and> i < LENGTH('a::len))"
- by standard
- (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq)
-
-lemmas td_nth = test_bit.td_thm
-
subsection \<open>Shifting, Rotating, and Splitting Words\<close>
@@ -4118,7 +4077,7 @@
lemma sshiftr1_sbintr [simp]:
"(sshiftr1 (numeral w) :: 'a::len word) =
word_of_int (bin_rest (signed_take_bit (LENGTH('a) - 1) (numeral w)))"
- unfolding sshiftr1_eq word_numeral_alt by (simp add: word_sbin.eq_norm)
+ by transfer simp
text \<open>TODO: rules for \<^term>\<open>- (numeral n)\<close>\<close>
@@ -4243,10 +4202,9 @@
by auto (metis pos_mod_conj)+
lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
- apply (simp add: and_mask_bintr)
- apply (simp add: word_ubin.inverse_norm)
- apply (simp add: eq_mod_iff take_bit_eq_mod min_def)
- apply (fast intro!: lt2p_lem)
+ apply (auto simp flip: take_bit_eq_mask)
+ apply (metis take_bit_int_eq_self_iff uint_take_bit_eq)
+ apply (simp add: take_bit_int_eq_self unsigned_take_bit_eq word_uint_eqI)
done
lemma and_mask_dvd: "2 ^ n dvd uint w \<longleftrightarrow> w AND mask n = 0"
@@ -4529,10 +4487,18 @@
have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
(sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
(sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close>
- using sint_range' [of x] sint_range' [of y]
+ using sint_less [of x] sint_greater_eq [of x] sint_less [of y] sint_greater_eq [of y]
+ signed_take_bit_int_eq_self [of \<open>LENGTH('a) - 1\<close> \<open>sint x + sint y\<close>]
apply (auto simp add: not_less)
- apply (unfold sint_word_ariths word_sbin.set_iff_norm [symmetric] sints_num)
- apply (auto simp add: signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
+ apply (unfold sint_word_ariths)
+ apply (subst signed_take_bit_int_eq_self)
+ prefer 4
+ apply (subst signed_take_bit_int_eq_self)
+ prefer 7
+ apply (subst signed_take_bit_int_eq_self)
+ prefer 10
+ apply (subst signed_take_bit_int_eq_self)
+ apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
done
then show ?thesis
apply (simp only: One_nat_def word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
@@ -4569,12 +4535,7 @@
lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
a = take_bit (LENGTH('a) - n) a \<and> b = take_bit (LENGTH('a)) b"
for w :: "'a::len word"
- apply (frule word_ubin.norm_Rep [THEN ssubst])
- apply (drule bin_split_trunc1)
- apply (drule sym [THEN trans])
- apply assumption
- apply safe
- done
+ by transfer (simp add: drop_bit_take_bit ac_simps)
\<comment> \<open>keep quantifiers for use in simplification\<close>
lemma test_bit_split':
@@ -4584,8 +4545,13 @@
a !! m = (m < size a \<and> c !! (m + size b)))"
apply (unfold word_split_bin' test_bit_bin)
apply (clarify)
- apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
- apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_unsigned_iff ac_simps exp_eq_zero_iff dest: bit_imp_le_length)
+ apply simp
+ apply (erule conjE)
+ apply (drule sym)
+ apply (drule sym)
+ apply (simp add: bit_take_bit_iff bit_drop_bit_eq)
+ apply transfer
+ apply (simp add: bit_take_bit_iff ac_simps)
done
lemma test_bit_split:
@@ -4675,7 +4641,10 @@
and therefore of the same length, as the original word.\<close>
lemma word_rsplit_same: "word_rsplit w = [w]"
- by (simp add: word_rsplit_def bin_rsplit_all)
+ apply (simp add: word_rsplit_def bin_rsplit_all)
+ apply transfer
+ apply simp
+ done
lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0"
by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
@@ -4697,15 +4666,17 @@
defer
apply (rule map_ident [THEN fun_cong])
apply (rule refl [THEN map_cong])
- apply (simp add : word_ubin.eq_norm)
- apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
- done
+ apply simp
+ using bin_rsplit_size_sign take_bit_int_eq_self_iff by blast
lemma horner_sum_uint_exp_Cons_eq:
\<open>horner_sum uint (2 ^ LENGTH('a)) (w # ws) =
concat_bit LENGTH('a) (uint w) (horner_sum uint (2 ^ LENGTH('a)) ws)\<close>
for ws :: \<open>'a::len word list\<close>
- by (simp add: concat_bit_eq push_bit_eq_mult)
+ apply (simp add: concat_bit_eq push_bit_eq_mult)
+ apply transfer
+ apply simp
+ done
lemma bit_horner_sum_uint_exp_iff:
\<open>bit (horner_sum uint (2 ^ LENGTH('a)) ws) n \<longleftrightarrow>
@@ -4955,18 +4926,18 @@
lemma word_int_cases:
fixes x :: "'a::len word"
obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^LENGTH('a)"
- by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
+ by (rule that [of \<open>uint x\<close>]) simp_all
lemma word_nat_cases [cases type: word]:
fixes x :: "'a::len word"
obtains n where "x = of_nat n" and "n < 2^LENGTH('a)"
- by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
+ by (rule that [of \<open>unat x\<close>]) simp_all
lemma max_word_max [intro!]: "n \<le> max_word"
by (fact word_order.extremum)
lemma word_of_int_2p_len: "word_of_int (2 ^ LENGTH('a)) = (0::'a::len word)"
- by (subst word_uint.Abs_norm [symmetric]) simp
+ by simp
lemma word_pow_0: "(2::'a::len word) ^ LENGTH('a) = 0"
by (fact word_exp_length_eq_0)
@@ -5036,7 +5007,7 @@
else uint x + uint y - 2^size x)"
apply (simp only: word_arith_wis word_size uint_word_of_int_eq)
apply (auto simp add: not_less take_bit_int_eq_self_iff)
- apply (metis not_less uint_plus_if' word_add_def word_ubin.eq_norm)
+ apply (metis not_less take_bit_eq_mod uint_plus_if' uint_word_ariths(1))
done
lemma unat_plus_if_size:
@@ -5066,7 +5037,7 @@
else uint x - uint y + 2^size x)"
apply (simp only: word_arith_wis word_size uint_word_of_int_eq)
apply (auto simp add: take_bit_int_eq_self_iff not_le)
- apply (metis not_le uint_sub_if' word_sub_wi word_ubin.eq_norm)
+ apply (metis not_less uint_sub_if' uint_word_arith_bintrs(2))
done
lemma unat_sub:
@@ -5089,18 +5060,15 @@
lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
lemma word_of_int_minus: "word_of_int (2^LENGTH('a) - i) = (word_of_int (-i)::'a::len word)"
-proof -
- have *: "2^LENGTH('a) - i = -i + 2^LENGTH('a)"
- by simp
- show ?thesis
- apply (subst *)
- apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
- apply simp
- done
-qed
-
-lemmas word_of_int_inj =
- word_uint.Abs_inject [unfolded uints_num, simplified]
+ apply transfer
+ apply (subst take_bit_diff [symmetric])
+ apply (simp add: take_bit_minus)
+ done
+
+lemma word_of_int_inj:
+ \<open>(word_of_int x :: 'a::len word) = word_of_int y \<longleftrightarrow> x = y\<close>
+ if \<open>0 \<le> x \<and> x < 2 ^ LENGTH('a)\<close> \<open>0 \<le> y \<and> y < 2 ^ LENGTH('a)\<close>
+ using that by (transfer fixing: x y) (simp add: take_bit_int_eq_self)
lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y"
for x y :: "'z::len word"
@@ -5197,7 +5165,7 @@
lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
for n :: "'a::len word"
apply (auto simp add: word_rec_def unat_word_ariths)
- apply (metis (mono_tags, lifting) old.nat.simps(7) unatSuc word_unat.Rep_inverse word_unat.eq_norm word_unat.td_th)
+ apply (metis (mono_tags, lifting) Abs_fnat_hom_add add_diff_cancel_left' o_def of_nat_1 old.nat.simps(7) plus_1_eq_Suc unatSuc unat_word_ariths(1) unsigned_1 word_arith_nat_add)
done
lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
--- a/src/Pure/General/file.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/Pure/General/file.ML Fri Sep 25 14:12:01 2020 +0100
@@ -10,6 +10,7 @@
val platform_path: Path.T -> string
val bash_path: Path.T -> string
val bash_paths: Path.T list -> string
+ val bash_platform_path: Path.T -> string
val full_path: Path.T -> Path.T -> Path.T
val tmp_path: Path.T -> Path.T
val exists: Path.T -> bool
@@ -50,6 +51,8 @@
val bash_path = Bash_Syntax.string o standard_path;
val bash_paths = Bash_Syntax.strings o map standard_path;
+val bash_platform_path = Bash_Syntax.string o platform_path;
+
(* full_path *)
--- a/src/Pure/ML/ml_syntax.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/Pure/ML/ml_syntax.ML Fri Sep 25 14:12:01 2020 +0100
@@ -20,6 +20,7 @@
val print_string: string -> string
val print_strings: string list -> string
val print_path: Path.T -> string
+ val print_platform_path: Path.T -> string
val print_properties: Properties.T -> string
val print_position: Position.T -> string
val print_range: Position.range -> string
@@ -91,6 +92,8 @@
fun print_path path =
"Path.explode " ^ print_string (Path.implode path);
+val print_platform_path = print_string o File.platform_path;
+
val print_properties = print_list (print_pair print_string print_string);
fun print_position pos =
--- a/src/Pure/System/scala.scala Fri Sep 25 14:11:48 2020 +0100
+++ b/src/Pure/System/scala.scala Fri Sep 25 14:12:01 2020 +0100
@@ -10,7 +10,7 @@
import java.io.{File => JFile, StringWriter, PrintWriter}
import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
-import scala.tools.nsc.interpreter.IMain
+import scala.tools.nsc.interpreter.{IMain, Results}
object Scala
@@ -100,12 +100,15 @@
}
}
- def toplevel(source: String): List[String] =
+ def toplevel(interpret: Boolean, source: String): List[String] =
{
val out = new StringWriter
val interp = interpreter(new PrintWriter(out))
- val rep = new interp.ReadEvalPrint
- val ok = interp.withLabel("\u0001") { rep.compile(source) }
+ val ok =
+ interp.withLabel("\u0001") {
+ if (interpret) interp.interpret(source) == Results.Success
+ else (new interp.ReadEvalPrint).compile(source)
+ }
out.close
val Error = """(?s)^\S* error: (.*)$""".r
@@ -120,10 +123,16 @@
object Toplevel extends Fun("scala_toplevel")
{
- def apply(source: String): String =
+ def apply(arg: String): String =
{
+ val (interpret, source) =
+ YXML.parse_body(arg) match {
+ case Nil => (false, "")
+ case List(XML.Text(source)) => (false, source)
+ case body => import XML.Decode._; pair(bool, string)(body)
+ }
val errors =
- try { Compiler.context().toplevel(source) }
+ try { Compiler.context().toplevel(interpret, source) }
catch { case ERROR(msg) => List(msg) }
locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
}
--- a/src/Pure/System/scala_compiler.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/Pure/System/scala_compiler.ML Fri Sep 25 14:12:01 2020 +0100
@@ -6,7 +6,7 @@
signature SCALA_COMPILER =
sig
- val toplevel: string -> unit
+ val toplevel: bool -> string -> unit
val static_check: string * Position.T -> unit
end;
@@ -15,15 +15,18 @@
(* check declaration *)
-fun toplevel source =
+fun toplevel interpret source =
let val errors =
- \<^scala>\<open>scala_toplevel\<close> source
+ (interpret, source)
+ |> let open XML.Encode in pair bool string end
+ |> YXML.string_of_body
+ |> \<^scala>\<open>scala_toplevel\<close>
|> YXML.parse_body
|> let open XML.Decode in list string end
in if null errors then () else error (cat_lines errors) end;
fun static_check (source, pos) =
- toplevel ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
+ toplevel false ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
handle ERROR msg => error (msg ^ Position.here pos);
--- a/src/Pure/Tools/ghc.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/Pure/Tools/ghc.ML Fri Sep 25 14:12:01 2020 +0100
@@ -85,7 +85,7 @@
val _ = File.write template_path (project_template {depends = depends, modules = modules});
val {rc, err, ...} =
Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
- " --bare " ^ Bash.string (File.platform_path template_path));
+ " --bare " ^ File.bash_platform_path template_path);
in if rc = 0 then () else error err end;
end;
--- a/src/Tools/Code/code_scala.ML Fri Sep 25 14:11:48 2020 +0100
+++ b/src/Tools/Code/code_scala.ML Fri Sep 25 14:12:01 2020 +0100
@@ -287,7 +287,7 @@
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, vs_args), tys) =
concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
+ (str ("final case class " ^ deresolve_const co)) vs_args)
@@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
(Name.invent_names (snd reserved) "a" tys))),
str "extends",
@@ -296,7 +296,7 @@
];
in
Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
- NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
+ NOBR (str ("abstract sealed class " ^ deresolve_tyco tyco)) vs
:: map print_co cos)
end
| print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) =
@@ -334,7 +334,7 @@
(map print_classparam_val classparams))
:: map print_classparam_def classparams
@| Pretty.block_enclose
- ((concat o map str) ["object", deresolve_class class, "{"], str "}")
+ (str ("object " ^ deresolve_class class ^ "{"), str "}")
(map (print_inst class) insts)
)
end;