417 lines
16 KiB
Plaintext
417 lines
16 KiB
Plaintext
theory StarForth_Arithmetic_Words
|
|
imports StarForth_Base
|
|
begin
|
|
|
|
(* =========================================================================
|
|
POST-02: Arithmetic Words
|
|
Mirrors: src/word_source/arithmetic_words.c
|
|
src/test_runner/modules/arithmetic_words_test.c
|
|
|
|
All operations use HOL int (arbitrary precision). Proofs hold in C
|
|
provided no intermediate value overflows 64-bit signed range.
|
|
======================================================================== *)
|
|
|
|
(* ── Helper: binary op lifting ─────────────────────────────────────────── *)
|
|
(* Most binary arithmetic words: pop two, push result. *)
|
|
|
|
definition binop :: "(cell \<Rightarrow> cell \<Rightarrow> cell) \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
|
"binop f vm =
|
|
(case data_stack vm of
|
|
n2 # n1 # rest \<Rightarrow> vm\<lparr>data_stack := f n1 n2 # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma binop_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
shows "data_stack (binop f vm) = f n1 n2 # rest"
|
|
by (simp add: binop_def assms)
|
|
|
|
lemma binop_depth:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
shows "length (data_stack (binop f vm)) = length (data_stack vm) - 1"
|
|
by (simp add: binop_def assms)
|
|
|
|
lemma binop_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (binop f vm)"
|
|
by (simp add: binop_def set_error_def assms)
|
|
|
|
lemma binop_underflow_one:
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (binop f vm)"
|
|
by (simp add: binop_def set_error_def assms)
|
|
|
|
(* ── Helper: unary op lifting ───────────────────────────────────────────── *)
|
|
|
|
definition unop :: "(cell \<Rightarrow> cell) \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
|
"unop f vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| x # xs \<Rightarrow> vm\<lparr>data_stack := f x # xs\<rparr>)"
|
|
|
|
lemma unop_normal:
|
|
assumes "data_stack vm = x # xs"
|
|
shows "data_stack (unop f vm) = f x # xs"
|
|
by (simp add: unop_def assms)
|
|
|
|
lemma unop_depth_preserved:
|
|
assumes "data_stack vm = x # xs"
|
|
shows "length (data_stack (unop f vm)) = length (data_stack vm)"
|
|
by (simp add: unop_def assms)
|
|
|
|
lemma unop_underflow:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (unop f vm)"
|
|
by (simp add: unop_def set_error_def assms)
|
|
|
|
(* ── + ( n1 n2 -- n3 ) ─────────────────────────────────────────────────── *)
|
|
|
|
definition forth_add :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_add = binop (+)"
|
|
|
|
lemma add_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
shows "data_stack (forth_add vm) = (n1 + n2) # rest"
|
|
by (simp add: forth_add_def binop_def assms)
|
|
|
|
lemma add_commutative:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "data_stack vm' = n1 # n2 # rest"
|
|
shows "data_stack (forth_add vm) = data_stack (forth_add vm')"
|
|
by (simp add: forth_add_def binop_def assms add.commute)
|
|
|
|
lemma add_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_add vm)"
|
|
by (simp add: forth_add_def binop_def set_error_def assms)
|
|
|
|
lemma add_underflow_one:
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (forth_add vm)"
|
|
by (simp add: forth_add_def binop_def set_error_def assms)
|
|
|
|
(* ── - ( n1 n2 -- n3 ) ─────────────────────────────────────────────────── *)
|
|
(* Stack effect: n3 = n1 - n2 (n2 = TOS subtracted from n1 = second) *)
|
|
|
|
definition forth_sub :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_sub = binop (-)"
|
|
|
|
lemma sub_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
shows "data_stack (forth_sub vm) = (n1 - n2) # rest"
|
|
by (simp add: forth_sub_def binop_def assms)
|
|
|
|
lemma sub_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_sub vm)"
|
|
by (simp add: forth_sub_def binop_def set_error_def assms)
|
|
|
|
lemma sub_underflow_one:
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (forth_sub vm)"
|
|
by (simp add: forth_sub_def binop_def set_error_def assms)
|
|
|
|
(* ── * ( n1 n2 -- n3 ) ─────────────────────────────────────────────────── *)
|
|
|
|
definition forth_mul :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_mul = binop (*)"
|
|
|
|
lemma mul_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
shows "data_stack (forth_mul vm) = (n1 * n2) # rest"
|
|
by (simp add: forth_mul_def binop_def assms)
|
|
|
|
lemma mul_commutative:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "data_stack vm' = n1 # n2 # rest"
|
|
shows "data_stack (forth_mul vm) = data_stack (forth_mul vm')"
|
|
by (simp add: forth_mul_def binop_def assms mult.commute)
|
|
|
|
lemma mul_by_zero_tos:
|
|
assumes "data_stack vm = 0 # n1 # rest"
|
|
shows "data_stack (forth_mul vm) = 0 # rest"
|
|
by (simp add: forth_mul_def binop_def assms)
|
|
|
|
lemma mul_by_zero_second:
|
|
assumes "data_stack vm = n2 # 0 # rest"
|
|
shows "data_stack (forth_mul vm) = 0 # rest"
|
|
by (simp add: forth_mul_def binop_def assms)
|
|
|
|
lemma mul_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_mul vm)"
|
|
by (simp add: forth_mul_def binop_def set_error_def assms)
|
|
|
|
(* ── / ( n1 n2 -- n3 ) ─────────────────────────────────────────────────── *)
|
|
(* Division by zero sets vm_error (matching C behaviour). *)
|
|
|
|
definition forth_div :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_div vm =
|
|
(case data_stack vm of
|
|
n2 # n1 # rest \<Rightarrow>
|
|
if n2 = 0
|
|
then set_error vm
|
|
else vm\<lparr>data_stack := (n1 div n2) # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma div_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "n2 \<noteq> 0"
|
|
shows "data_stack (forth_div vm) = (n1 div n2) # rest"
|
|
by (simp add: forth_div_def assms)
|
|
|
|
lemma div_by_zero:
|
|
assumes "data_stack vm = 0 # n1 # rest"
|
|
shows "vm_error (forth_div vm)"
|
|
by (simp add: forth_div_def set_error_def assms)
|
|
|
|
lemma div_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_div vm)"
|
|
by (simp add: forth_div_def set_error_def assms)
|
|
|
|
lemma div_underflow_one:
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (forth_div vm)"
|
|
by (simp add: forth_div_def set_error_def assms)
|
|
|
|
(* ── MOD ( n1 n2 -- n3 ) ───────────────────────────────────────────────── *)
|
|
|
|
definition forth_mod :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_mod vm =
|
|
(case data_stack vm of
|
|
n2 # n1 # rest \<Rightarrow>
|
|
if n2 = 0
|
|
then set_error vm
|
|
else vm\<lparr>data_stack := (n1 mod n2) # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma mod_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "n2 \<noteq> 0"
|
|
shows "data_stack (forth_mod vm) = (n1 mod n2) # rest"
|
|
by (simp add: forth_mod_def assms)
|
|
|
|
lemma mod_by_zero:
|
|
assumes "data_stack vm = 0 # n1 # rest"
|
|
shows "vm_error (forth_mod vm)"
|
|
by (simp add: forth_mod_def set_error_def assms)
|
|
|
|
lemma mod_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_mod vm)"
|
|
by (simp add: forth_mod_def set_error_def assms)
|
|
|
|
(* ── /MOD ( n1 n2 -- n3 n4 ) ───────────────────────────────────────────── *)
|
|
(* Pushes remainder (n3) then quotient (n4); quotient is TOS. *)
|
|
|
|
definition forth_divmod :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_divmod vm =
|
|
(case data_stack vm of
|
|
n2 # n1 # rest \<Rightarrow>
|
|
if n2 = 0
|
|
then set_error vm
|
|
else if ds_full vm
|
|
then set_error vm
|
|
else vm\<lparr>data_stack := (n1 div n2) # (n1 mod n2) # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma divmod_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "n2 \<noteq> 0"
|
|
assumes "\<not> ds_full vm"
|
|
shows "data_stack (forth_divmod vm) = (n1 div n2) # (n1 mod n2) # rest"
|
|
by (simp add: forth_divmod_def assms)
|
|
|
|
lemma divmod_quotient:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "n2 \<noteq> 0"
|
|
assumes "\<not> ds_full vm"
|
|
shows "hd (data_stack (forth_divmod vm)) = n1 div n2"
|
|
by (simp add: forth_divmod_def assms)
|
|
|
|
lemma divmod_remainder:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "n2 \<noteq> 0"
|
|
assumes "\<not> ds_full vm"
|
|
shows "hd (tl (data_stack (forth_divmod vm))) = n1 mod n2"
|
|
by (simp add: forth_divmod_def assms)
|
|
|
|
(* ── 1+ ( n -- n+1 ) ───────────────────────────────────────────────────── *)
|
|
|
|
definition forth_one_plus :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_one_plus = unop (\<lambda>n. n + 1)"
|
|
|
|
lemma one_plus_normal:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "data_stack (forth_one_plus vm) = (n + 1) # xs"
|
|
by (simp add: forth_one_plus_def unop_def assms)
|
|
|
|
lemma one_plus_underflow:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_one_plus vm)"
|
|
by (simp add: forth_one_plus_def unop_def set_error_def assms)
|
|
|
|
(* ── 1- ( n -- n-1 ) ───────────────────────────────────────────────────── *)
|
|
|
|
definition forth_one_minus :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_one_minus = unop (\<lambda>n. n - 1)"
|
|
|
|
lemma one_minus_normal:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "data_stack (forth_one_minus vm) = (n - 1) # xs"
|
|
by (simp add: forth_one_minus_def unop_def assms)
|
|
|
|
lemma one_minus_underflow:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_one_minus vm)"
|
|
by (simp add: forth_one_minus_def unop_def set_error_def assms)
|
|
|
|
(* ── 2+ ( n -- n+2 ) ───────────────────────────────────────────────────── *)
|
|
|
|
definition forth_two_plus :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_two_plus = unop (\<lambda>n. n + 2)"
|
|
|
|
lemma two_plus_normal:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "data_stack (forth_two_plus vm) = (n + 2) # xs"
|
|
by (simp add: forth_two_plus_def unop_def assms)
|
|
|
|
(* ── 2- ( n -- n-2 ) ───────────────────────────────────────────────────── *)
|
|
|
|
definition forth_two_minus :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_two_minus = unop (\<lambda>n. n - 2)"
|
|
|
|
lemma two_minus_normal:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "data_stack (forth_two_minus vm) = (n - 2) # xs"
|
|
by (simp add: forth_two_minus_def unop_def assms)
|
|
|
|
(* ── 2* ( n -- n*2 ) ───────────────────────────────────────────────────── *)
|
|
(* Left shift by 1 in C; multiplication by 2 in HOL. *)
|
|
|
|
definition forth_two_mul :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_two_mul = unop (\<lambda>n. n * 2)"
|
|
|
|
lemma two_mul_normal:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "data_stack (forth_two_mul vm) = (n * 2) # xs"
|
|
by (simp add: forth_two_mul_def unop_def assms)
|
|
|
|
(* ── 2/ ( n -- n/2 ) ───────────────────────────────────────────────────── *)
|
|
(* Arithmetic right shift by 1 in C. In HOL, div 2 on int is floor div. *)
|
|
|
|
definition forth_two_div :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_two_div = unop (\<lambda>n. n div 2)"
|
|
|
|
lemma two_div_normal:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "data_stack (forth_two_div vm) = (n div 2) # xs"
|
|
by (simp add: forth_two_div_def unop_def assms)
|
|
|
|
(* ── ABS ( n -- |n| ) ──────────────────────────────────────────────────── *)
|
|
|
|
definition forth_abs :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_abs = unop abs"
|
|
|
|
lemma abs_normal:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "data_stack (forth_abs vm) = \<bar>n\<bar> # xs"
|
|
by (simp add: forth_abs_def unop_def assms)
|
|
|
|
lemma abs_nonneg:
|
|
assumes "data_stack vm = n # xs"
|
|
assumes "\<not> vm_error vm"
|
|
shows "hd (data_stack (forth_abs vm)) \<ge> 0"
|
|
by (simp add: forth_abs_def unop_def assms)
|
|
|
|
lemma abs_idempotent:
|
|
assumes "data_stack vm = n # xs"
|
|
assumes "\<not> vm_error vm"
|
|
shows "hd (data_stack (forth_abs (forth_abs vm))) = hd (data_stack (forth_abs vm))"
|
|
by (simp add: forth_abs_def unop_def assms)
|
|
|
|
lemma abs_underflow:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_abs vm)"
|
|
by (simp add: forth_abs_def unop_def set_error_def assms)
|
|
|
|
(* ── NEGATE ( n -- -n ) ─────────────────────────────────────────────────── *)
|
|
|
|
definition forth_negate :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_negate = unop uminus"
|
|
|
|
lemma negate_normal:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "data_stack (forth_negate vm) = (-n) # xs"
|
|
by (simp add: forth_negate_def unop_def assms)
|
|
|
|
lemma negate_involutive:
|
|
assumes "data_stack vm = n # xs"
|
|
shows "hd (data_stack (forth_negate (forth_negate vm))) = n"
|
|
by (simp add: forth_negate_def unop_def assms)
|
|
|
|
lemma negate_underflow:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_negate vm)"
|
|
by (simp add: forth_negate_def unop_def set_error_def assms)
|
|
|
|
(* ── MIN ( n1 n2 -- n3 ) ───────────────────────────────────────────────── *)
|
|
|
|
definition forth_min :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_min = binop min"
|
|
|
|
lemma min_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
shows "data_stack (forth_min vm) = min n1 n2 # rest"
|
|
by (simp add: forth_min_def binop_def assms)
|
|
|
|
lemma min_commutative:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "data_stack vm' = n1 # n2 # rest"
|
|
shows "data_stack (forth_min vm) = data_stack (forth_min vm')"
|
|
by (simp add: forth_min_def binop_def assms min.commute)
|
|
|
|
lemma min_idempotent:
|
|
assumes "data_stack vm = n # n # rest"
|
|
shows "data_stack (forth_min vm) = n # rest"
|
|
by (simp add: forth_min_def binop_def assms)
|
|
|
|
lemma min_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_min vm)"
|
|
by (simp add: forth_min_def binop_def set_error_def assms)
|
|
|
|
(* ── MAX ( n1 n2 -- n3 ) ───────────────────────────────────────────────── *)
|
|
|
|
definition forth_max :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_max = binop max"
|
|
|
|
lemma max_normal:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
shows "data_stack (forth_max vm) = max n1 n2 # rest"
|
|
by (simp add: forth_max_def binop_def assms)
|
|
|
|
lemma max_commutative:
|
|
assumes "data_stack vm = n2 # n1 # rest"
|
|
assumes "data_stack vm' = n1 # n2 # rest"
|
|
shows "data_stack (forth_max vm) = data_stack (forth_max vm')"
|
|
by (simp add: forth_max_def binop_def assms max.commute)
|
|
|
|
lemma max_idempotent:
|
|
assumes "data_stack vm = n # n # rest"
|
|
shows "data_stack (forth_max vm) = n # rest"
|
|
by (simp add: forth_max_def binop_def assms)
|
|
|
|
lemma max_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_max vm)"
|
|
by (simp add: forth_max_def binop_def set_error_def assms)
|
|
|
|
(* ── min/max algebraic relationship ────────────────────────────────────── *)
|
|
|
|
lemma min_le_max:
|
|
"min (a::int) b \<le> max a b"
|
|
by (simp add: min_def max_def)
|
|
|
|
end
|