Extended_Finite_State_Machines/Extended_Finite_State_Machines/Value_Lexorder.thy

42 lines
1.5 KiB
Plaintext

subsection\<open>Value Lexorder\<close>
text\<open>This theory defines a lexicographical ordering on values such that we can build orderings for
arithmetic expressions and guards. Here, numbers are defined as less than strings, else the natural
ordering on the respective datatypes is used.\<close>
theory Value_Lexorder
imports Value
begin
instantiation "value" :: linorder begin
text_raw\<open>\snip{valueorder}{1}{2}{%\<close>
fun less_value :: "value \<Rightarrow> value \<Rightarrow> bool" where
"(Num n) < (Str s) = True" |
"(Str s) < (Num n) = False" |
"(Str s1) < (Str s2) = (s1 < s2)" |
"(Num n1) < (Num n2) = (n1 < n2)"
text_raw\<open>}%endsnip\<close>
definition less_eq_value :: "value \<Rightarrow> value \<Rightarrow> bool" where
"less_eq_value v1 v2 = (v1 < v2 \<or> v1 = v2)"
declare less_eq_value_def [simp]
instance
apply standard
apply (simp, metis less_imp_not_less less_value.elims(2) less_value.simps(3) less_value.simps(4))
apply simp
subgoal for x y z
apply (induct x y rule: less_value.induct)
apply (metis less_eq_value_def less_value.elims(3) less_value.simps(2) value.simps(4))
apply simp
apply (metis dual_order.strict_trans less_eq_value_def less_value.elims(2) less_value.simps(3) value.distinct(1))
by (cases z, auto)
apply (metis less_eq_value_def less_imp_not_less less_value.elims(2) less_value.simps(3) less_value.simps(4))
subgoal for x y
by (induct x y rule: less_value.induct, auto)
done
end
end