# Theory Value

```section‹Values›

text‹Our EFSM implementation can currently handle integers and strings. Here we define a sum type
which combines these. We also define an arithmetic in terms of values such that EFSMs do not need
to be strongly typed.›

theory Value
imports Trilean
begin

text_raw‹\snip{valuetype}{1}{2}{%›
datatype "value" = Num int | Str String.literal
text_raw‹}%endsnip›

fun is_Num :: "value ⇒ bool" where
"is_Num (Num _) = True" |
"is_Num (Str _) = False"

text_raw‹\snip{maybeIntArith}{1}{2}{%›
fun maybe_arith_int :: "(int ⇒ int ⇒ int) ⇒ value option ⇒ value option ⇒ value option" where
"maybe_arith_int f (Some (Num x)) (Some (Num y)) = Some (Num (f x y))" |
"maybe_arith_int _ _ _ = None"
text_raw‹}%endsnip›

lemma maybe_arith_int_not_None:
"maybe_arith_int f a b ≠ None = (∃n n'. a = Some (Num n) ∧ b = Some (Num n'))"
using maybe_arith_int.elims maybe_arith_int.simps(1) by blast

lemma maybe_arith_int_Some:
"maybe_arith_int f a b = Some (Num x) = (∃n n'. a = Some (Num n) ∧ b = Some (Num n') ∧ f n n' = x)"
using maybe_arith_int.elims maybe_arith_int.simps(1) by blast

lemma maybe_arith_int_None:
"(maybe_arith_int f a1 a2 = None) = (∄n n'. a1 = Some (Num n) ∧ a2 = Some (Num n'))"
using maybe_arith_int_not_None by blast

lemma maybe_arith_int_Not_Num:
"(∀n. maybe_arith_int f a1 a2 ≠ Some (Num n)) = (maybe_arith_int f a1 a2 = None)"
by (metis maybe_arith_int.elims option.distinct(1))

lemma maybe_arith_int_never_string: "maybe_arith_int f a b ≠ Some (Str x)"
using maybe_arith_int.elims by blast

definition "value_plus = maybe_arith_int (+)"

lemma value_plus_never_string: "value_plus a b ≠ Some (Str x)"

lemma value_plus_symmetry: "value_plus x y = value_plus y x"
apply (induct x y rule: maybe_arith_int.induct)

definition "value_minus = maybe_arith_int (-)"

lemma value_minus_never_string: "value_minus a b ≠ Some (Str x)"

definition "value_times = maybe_arith_int (*)"

lemma value_times_never_string: "value_times a b ≠ Some (Str x)"

fun MaybeBoolInt :: "(int ⇒ int ⇒ bool) ⇒ value option ⇒ value option ⇒ trilean" where
"MaybeBoolInt f (Some (Num a)) (Some (Num b)) = (if f a b then true else false)" |
"MaybeBoolInt _ _ _ = invalid"

lemma MaybeBoolInt_not_num_1:
"∀n. r ≠ Some (Num n) ⟹ MaybeBoolInt f n r = invalid"
using MaybeBoolInt.elims by blast

definition value_gt :: "value option ⇒ value option ⇒ trilean"  where
"value_gt a b ≡ MaybeBoolInt (>) a b"

fun value_eq :: "value option ⇒ value option ⇒ trilean" where
"value_eq None _ = invalid" |
"value_eq _ None = invalid" |
"value_eq (Some a) (Some b) = (if a = b then true else false)"

lemma value_eq_true: "(value_eq a b = true) = (∃x y. a = Some x ∧ b = Some y ∧ x = y)"
by (cases a; cases b, auto)

lemma value_eq_false: "(value_eq a b = false) = (∃x y. a = Some x ∧ b = Some y ∧ x ≠ y)"
by (cases a; cases b, auto)

lemma value_gt_true_Some: "value_gt a b = true ⟹ (∃x. a = Some x) ∧ (∃y. b = Some y)"
by (cases a; cases b, auto simp: value_gt_def)

lemma value_gt_true: "(value_gt a b = true) = (∃x y. a = Some (Num x) ∧ b = Some (Num y) ∧ x > y)"
apply (cases a)
using value_gt_true_Some apply blast
apply (cases b)
using value_gt_true_Some apply blast
subgoal for aa bb by (cases aa; cases bb, auto simp: value_gt_def)
done

lemma value_gt_false_Some: "value_gt a b = false ⟹ (∃x. a = Some x) ∧ (∃y. b = Some y)"
by (cases a; cases b, auto simp: value_gt_def)

end
```