Theory GExp

```subsection ‹Guards Expressions›
text‹
This theory defines the guard language of EFSMs which can be translated directly to and from
contexts. Boolean values true and false respectively represent the guards which are always and never
satisfied. Guards may test for (in)equivalence of two arithmetic expressions or be connected using
\textsc{nor} logic into compound expressions. The use of \textsc{nor} logic reduces the number of
subgoals when inducting over guard expressions.

We also define syntax hacks for the relations less than, less than or equal to, greater than or
equal to, and not equal to as well as the expression of logical conjunction, disjunction, and
negation in terms of nor logic.›

theory GExp
imports AExp Trilean
begin

text_raw‹\snip{gexptype}{1}{2}{%›
datatype 'a gexp = Bc bool | Eq "'a aexp" "'a aexp" | Gt "'a aexp" "'a aexp" | In 'a "value list" |  Nor "'a gexp" "'a gexp"
text_raw‹}%endsnip›

fun gval :: "'a gexp ⇒ 'a datastate ⇒ trilean" where
"gval (Bc True) _ = true" |
"gval (Bc False) _ = false" |
"gval (Gt a1 a2) s = value_gt (aval a1 s) (aval a2 s)" |
"gval (Eq a1 a2) s = value_eq (aval a1 s) (aval a2 s)" |
"gval (In v l) s = (case s v of None ⇒ invalid | Some vv ⇒ if vv ∈ set l then true else false)" |
"gval (Nor a1 a2) s = ¬? ((gval a1 s) ∨? (gval a2 s))"

text_raw‹\snip{connectives}{1}{2}{%›
definition gNot :: "'a gexp ⇒ 'a gexp"  where
"gNot g ≡ Nor g g"

definition gOr :: "'a gexp ⇒ 'a gexp ⇒ 'a gexp" (*infix "∨" 60*) where
"gOr v va ≡ Nor (Nor v va) (Nor v va)"

definition gAnd :: "'a gexp ⇒ 'a gexp ⇒ 'a gexp" (*infix "∧" 60*) where
"gAnd v va ≡ Nor (Nor v v) (Nor va va)"

definition gImplies :: "'a gexp ⇒ 'a gexp ⇒ 'a gexp" where
"gImplies p q ≡ gOr (gNot p) q"

definition Lt :: "'a aexp ⇒ 'a aexp ⇒ 'a gexp" (*infix "<" 60*) where
"Lt a b ≡ Gt b a"

definition Le :: "'a aexp ⇒ 'a aexp ⇒ 'a gexp" (*infix "≤" 60*) where
"Le v va ≡ gNot (Gt v va)"

definition Ge :: "'a aexp ⇒ 'a aexp ⇒ 'a gexp" (*infix "≥" 60*) where
"Ge v va ≡ gNot (Lt v va)"

definition Ne :: "'a aexp ⇒ 'a aexp ⇒ 'a gexp" (*infix "≠" 60*) where
"Ne v va ≡ gNot (Eq v va)"
text_raw‹}%endsnip›

lemma gval_Lt [simp]:
"gval (Lt a1 a2) s = value_gt (aval a2 s) (aval a1 s)"

lemma gval_Le [simp]:
"gval (Le a1 a2) s = ¬? (value_gt (aval a1 s) (aval a2 s))"
by (simp add: Le_def value_gt_def gNot_def maybe_or_idempotent)

lemma gval_Ge [simp]:
"gval (Ge a1 a2) s = ¬? (value_gt (aval a2 s) (aval a1 s))"
by (simp add: Ge_def value_gt_def gNot_def maybe_or_idempotent)

lemma gval_Ne [simp]:
"gval (Ne a1 a2) s = ¬? (value_eq (aval a1 s) (aval a2 s))"
by (simp add: Ne_def value_gt_def gNot_def maybe_or_idempotent)

lemmas connectives = gAnd_def gOr_def gNot_def Lt_def Le_def Ge_def Ne_def

lemma gval_gOr [simp]: "gval (gOr x y) r = (gval x r) ∨? (gval y r)"
by (simp add: maybe_double_negation maybe_or_idempotent gOr_def)

lemma gval_gNot [simp]: "gval (gNot x) s = ¬? (gval x s)"

lemma gval_gAnd [simp]:
"gval (gAnd g1 g2) s = (gval g1 s) ∧? (gval g2 s)"
by (simp add: de_morgans_1 maybe_double_negation maybe_or_idempotent gAnd_def)

lemma gAnd_commute: "gval (gAnd a b) s = gval (gAnd b a) s"

lemma gOr_commute: "gval (gOr a b) s = gval (gOr b a) s"

lemma gval_gAnd_True:
"(gval (gAnd g1 g2) s = true) = ((gval g1 s = true) ∧ gval g2 s = true)"

lemma nor_equiv: "gval (gNot (gOr a b)) s = gval (Nor a b) s"
by simp

definition satisfiable :: "vname gexp ⇒ bool" where
"satisfiable g ≡ (∃i r. gval g (join_ir i r) = true)"

definition "satisfiable_list l = satisfiable (fold gAnd l (Bc True))"

lemma unsatisfiable_false: "¬ satisfiable (Bc False)"

lemma satisfiable_true: "satisfiable (Bc True)"

definition valid :: "vname gexp ⇒ bool" where
"valid g ≡ (∀s. gval g s = true)"

lemma valid_true: "valid (Bc True)"

fun gexp_constrains :: "'a gexp ⇒ 'a aexp ⇒ bool" where
"gexp_constrains (Bc _) _ = False" |
"gexp_constrains (Eq a1 a2) a = (aexp_constrains a1 a ∨ aexp_constrains a2 a)" |
"gexp_constrains (Gt a1 a2) a = (aexp_constrains a1 a ∨ aexp_constrains a2 a)" |
"gexp_constrains (Nor g1 g2) a = (gexp_constrains g1 a ∨ gexp_constrains g2 a)" |
"gexp_constrains (In v l) a = aexp_constrains (V v) a"

fun contains_bool :: "'a gexp ⇒ bool" where
"contains_bool (Bc _) = True" |
"contains_bool (Nor g1 g2) = (contains_bool g1 ∨ contains_bool g2)" |
"contains_bool _ = False"

fun gexp_same_structure :: "'a gexp ⇒ 'a gexp ⇒ bool" where
"gexp_same_structure (Bc b) (Bc b') = (b = b')" |
"gexp_same_structure (Eq a1 a2) (Eq a1' a2') = (aexp_same_structure a1 a1' ∧ aexp_same_structure a2 a2')" |
"gexp_same_structure (Gt a1 a2) (Gt a1' a2') = (aexp_same_structure a1 a1' ∧ aexp_same_structure a2 a2')" |
"gexp_same_structure (Nor g1 g2) (Nor g1' g2') = (gexp_same_structure g1 g1' ∧ gexp_same_structure g2 g2')" |
"gexp_same_structure (In v l) (In v' l') = (v = v' ∧ l = l')" |
"gexp_same_structure _ _ = False"

lemma gval_foldr_true:
"(gval (foldr gAnd G (Bc True)) s = true) = (∀g ∈ set G. gval g s = true)"
proof(induct G)
case (Cons a G)
then show ?case
apply (simp only: foldr.simps comp_def gval_gAnd maybe_and_true)
by simp
qed auto

fun enumerate_gexp_inputs :: "vname gexp ⇒ nat set" where
"enumerate_gexp_inputs (Bc _) = {}" |
"enumerate_gexp_inputs (Eq v va) = enumerate_aexp_inputs v ∪ enumerate_aexp_inputs va" |
"enumerate_gexp_inputs (Gt v va) = enumerate_aexp_inputs v ∪ enumerate_aexp_inputs va" |
"enumerate_gexp_inputs (In v va) = enumerate_aexp_inputs (V v)" |
"enumerate_gexp_inputs (Nor v va) = enumerate_gexp_inputs v ∪ enumerate_gexp_inputs va"

lemma enumerate_gexp_inputs_list: "∃l. enumerate_gexp_inputs g = set l"
proof(induct g)
case (Eq x1a x2)
then show ?case
by (metis enumerate_aexp_inputs_list enumerate_gexp_inputs.simps(2) set_append)
next
case (Gt x1a x2)
then show ?case
by (metis enumerate_aexp_inputs_list enumerate_gexp_inputs.simps(3) set_append)
next
case (In x1a x2)
then show ?case
next
case (Nor g1 g2)
then show ?case
by (metis enumerate_gexp_inputs.simps(5) set_append)
qed auto

definition max_input :: "vname gexp ⇒ nat option" where
"max_input g = (let inputs = enumerate_gexp_inputs g in if inputs = {} then None else Some (Max inputs))"

definition max_input_list :: "vname gexp list ⇒ nat option" where
"max_input_list g = fold max (map max_input g) None"

lemma max_input_list_cons:
"max_input_list (a # G) = max (max_input a) (max_input_list G)"
apply (cases ‹max_input a›)
apply (simp_all add: max_input_list_def flip: Max.set_eq_fold)
apply (metis (mono_tags, lifting) List.finite_set Max_insert Max_singleton bot_option_def finite_imageI max.assoc max_bot2)
done

fun enumerate_regs :: "vname gexp ⇒ nat set" where
"enumerate_regs (Bc _) = {}" |
"enumerate_regs (Eq v va) = AExp.enumerate_regs v ∪ AExp.enumerate_regs va" |
"enumerate_regs (Gt v va) = AExp.enumerate_regs v ∪ AExp.enumerate_regs va" |
"enumerate_regs (In v va) = AExp.enumerate_regs (V v)" |
"enumerate_regs (Nor v va) = enumerate_regs v ∪ enumerate_regs va"

lemma finite_enumerate_regs: "finite (enumerate_regs g)"
using AExp.finite_enumerate_regs by (induct g, auto)

definition max_reg :: "vname gexp ⇒ nat option" where
"max_reg g = (let regs = (enumerate_regs g) in if regs = {} then None else Some (Max regs))"

lemma max_reg_gNot: "max_reg (gNot x) = max_reg x"

lemma max_reg_Eq: "max_reg (Eq a b) = max (AExp.max_reg a) (AExp.max_reg b)"
apply (simp add: max_reg_def AExp.max_reg_def Let_def max_absorb2)
by (metis AExp.finite_enumerate_regs Max.union bot_option_def max_bot2 sup_Some sup_max)

lemma max_reg_Gt: "max_reg (Gt a b) = max (AExp.max_reg a) (AExp.max_reg b)"
apply (simp add: max_reg_def AExp.max_reg_def Let_def max_absorb2)
by (metis AExp.finite_enumerate_regs Max.union bot_option_def max_bot2 sup_Some sup_max)

lemma max_reg_Nor: "max_reg (Nor a b) = max (max_reg a) (max_reg b)"
apply (simp add: max_reg_def AExp.max_reg_def Let_def max_absorb2)
by (metis GExp.finite_enumerate_regs Max.union bot_option_def max_bot2 sup_Some sup_max)

lemma gval_In_cons:
"gval (In v (a # as)) s = (gval (Eq (V v) (L a)) s ∨? gval (In v as) s)"
by (cases "s v", auto)

lemma possible_to_be_in: "s ≠ [] ⟹ satisfiable (In v s)"
proof-
assume "s ≠ []"
have aux: "∃v' i r. join_ir i r v = Some v' ∧ v' ∈ set s ⟹
∃i r. (case join_ir i r v of None ⇒ false | Some v ⇒ if v ∈ set s then true else false) = true"
by (metis (mono_tags, lifting) option.simps(5))
show ?thesis
apply (cases s)
apply (simp add: ‹s ≠ []›)
apply (cases v)
apply (case_tac "∃(i::value list). length i > x1 ∧ i ! x1 = a")
apply clarsimp
subgoal for _ _ i by (rule exI[of _ i], intro exI, simp)
apply (metis gt_ex length_list_update length_repeat nth_list_update_eq)
apply (rule_tac exI)
apply (case_tac "∃r. r \$ x2 = Some a")
apply clarsimp
subgoal for _ _ _ r by (rule exI[of _ r], simp)
by (metis join_ir_R join_ir_double_exists)
qed

definition max_reg_list :: "vname gexp list ⇒ nat option" where
"max_reg_list g = fold max (map max_reg g) None"

lemma max_reg_list_cons:
"max_reg_list (a # G) = max (max_reg a) (max_reg_list G)"
apply (simp add: max_reg_list_def flip: Max.set_eq_fold)
apply (metis List.finite_set Max_insert bot_option_def empty_not_insert finite_imageI finite_insert insert_commute max.commute max_bot2)
done

lemma max_reg_list_append_singleton:
"max_reg_list (as@[bs]) = max (max_reg_list as) (max_reg_list [bs])"
by (metis max.commute sup_None_2 sup_max)

lemma max_reg_list_append:
"max_reg_list (as@bs) = max (max_reg_list as) (max_reg_list bs)"
proof(induct bs rule: rev_induct)
case Nil
then show ?case
by (metis append_Nil2 fold_simps(1) list.simps(8) max_reg_list_def sup_None_2 sup_max)
next
case (snoc x xs)
then show ?case
by (metis append_assoc max.assoc max_reg_list_append_singleton)
qed

definition apply_guards :: "vname gexp list ⇒ vname datastate ⇒ bool" where
"apply_guards G s = (∀g ∈ set (map (λg. gval g s) G). g = true)"

lemma apply_guards_singleton[simp]: "(apply_guards [g] s) = (gval g s = true)"

lemma apply_guards_empty [simp]: "apply_guards [] s"

lemma apply_guards_cons:
"apply_guards (a # G) c = (gval a c = true ∧ apply_guards G c)"

lemma apply_guards_double_cons:
"apply_guards (y # x # G) s = (gval (gAnd y x) s = true ∧ apply_guards G s)"
using apply_guards_cons gval_gAnd_True by blast

lemma apply_guards_append:
"apply_guards (a@a') s = (apply_guards a s ∧ apply_guards a' s)"
using apply_guards_def by auto

lemma apply_guards_foldr:
"apply_guards G s = (gval (foldr gAnd G (Bc True)) s = true)"
proof(induct G)
case Nil
then show ?case
next
case (Cons a G)
then show ?case
by (metis apply_guards_cons foldr.simps(2) gval_gAnd_True o_apply)
qed

lemma rev_apply_guards: "apply_guards (rev G) s = apply_guards G s"

lemma apply_guards_fold:
"apply_guards G s = (gval (fold gAnd G (Bc True)) s = true)"
using rev_apply_guards[symmetric]

lemma fold_apply_guards:
"(gval (fold gAnd G (Bc True)) s = true) = apply_guards G s"

lemma foldr_apply_guards:
"(gval (foldr gAnd G (Bc True)) s = true) = apply_guards G s"

lemma apply_guards_subset:
"set g' ⊆ set g ⟹ apply_guards g c ⟶ apply_guards g' c"
proof(induct g)
case (Cons a g)
then show ?case
using apply_guards_def by auto
qed auto

lemma apply_guards_subset_append:
"set G ⊆ set G' ⟹ apply_guards (G @ G') s = apply_guards (G') s"
using apply_guards_append apply_guards_subset by blast

lemma apply_guards_rearrange:
"x ∈ set G ⟹ apply_guards G s = apply_guards (x#G) s"
using apply_guards_def by auto

lemma apply_guards_condense: "∃g. apply_guards G s = (gval g s = true)"
using apply_guards_fold by blast

lemma apply_guards_false_condense: "∃g. (¬apply_guards G s) = (gval g s = false)"
using foldr_apply_guards gval.simps(2) not_true by blast

lemma max_input_Bc: "max_input (Bc x) = None"

lemma max_input_Eq:
"max_input (Eq a1 a2) = max (AExp.max_input a1) (AExp.max_input a2)"
apply (simp add: AExp.max_input_def max_input_def Let_def max_absorb2)
by (metis List.finite_set Max.union bot_option_def enumerate_aexp_inputs_not_empty max_bot2 sup_Some sup_max)

lemma max_input_Gt:
"max_input (Gt a1 a2) = max (AExp.max_input a1) (AExp.max_input a2)"
apply (simp add: AExp.max_input_def max_input_def Let_def max_absorb2)
by (metis List.finite_set Max.union bot_option_def enumerate_aexp_inputs_not_empty max_bot2 sup_Some sup_max)

lemma gexp_max_input_Nor:
"max_input (Nor g1 g2) = max (max_input g1) (max_input g2)"
apply (simp add: AExp.max_input_def max_input_def Let_def max_absorb2)
by (metis List.finite_set Max.union enumerate_gexp_inputs_list less_eq_option_Some_None max_def sup_Some sup_max)

lemma gexp_max_input_In: "max_input (In v l) = AExp.max_input (V v)"

lemma gval_foldr_gOr_invalid:
"(gval (fold gOr l g) s = invalid) = (∃g' ∈ (set (g#l)). gval g' s = invalid)"
proof(induct l rule: rev_induct)
case (snoc x xs)
then show ?case
by (simp, metis gval_gOr maybe_or_invalid)
qed auto

lemma gval_foldr_gOr_true:
"(gval (fold gOr l g) s = true) = ((∃g' ∈ (set (g#l)). gval g' s = true) ∧ (∀g' ∈ (set (g#l)). gval g' s ≠ invalid))"
proof(induct l rule: rev_induct)
case (snoc x xs)
then show ?case
using gval_foldr_gOr_invalid by auto
qed auto

lemma gval_foldr_gOr_false:
"(gval (fold gOr l g) s = false) = (∀g' ∈ (set (g#l)). gval g' s = false)"
proof(induct l rule: rev_induct)
case (snoc x xs)
then show ?case
qed auto

lemma gval_fold_gOr_rev: "gval (fold gOr (rev l) g) s = gval (fold gOr l g) s"
apply (cases "gval (fold gOr l g) s")

lemma gval_fold_gOr_foldr: "gval (fold gOr l g) s = gval (foldr gOr l g) s"

lemma gval_fold_gOr:
"gval (fold gOr (a # l) g) s = (gval a s ∨? gval (fold gOr l g) s)"
by (simp only: gval_fold_gOr_foldr foldr.simps comp_def gval_gOr)

lemma gval_In_fold:
"gval (In v l) s = (if s v = None then invalid else gval (fold gOr (map (λx. Eq (V v) (L x)) l) (Bc False)) s)"
proof(induct l)
case Nil
then show ?case
apply simp
apply (cases "s v")
apply simp
by auto
next
case (Cons a l)
then show ?case
apply (simp only: gval_In_cons)
apply (cases "s v")
apply simp
by (simp add: gval_fold_gOr del: fold.simps)
qed

fun fold_In :: "'a ⇒ value list ⇒ 'a gexp" where
"fold_In _ [] = Bc False" |
"fold_In v (l#t) = gOr (Eq (V v) (L l)) (fold_In v t)"

lemma gval_fold_In: "l ≠ [] ⟹ gval (In v l) s = gval (fold_In v l) s"
proof(induct l)
next
case (Cons a l)
then show ?case
apply (case_tac "s v")
apply simp
apply simp
apply safe
apply simp
apply (metis fold_In.simps(1) gval.simps(2) plus_trilean.simps(4) plus_trilean.simps(5))
apply fastforce
apply fastforce
by fastforce
qed auto

lemma fold_maybe_or_invalid_base: "fold (∨?) l invalid = invalid"
proof(induct l)
case (Cons a l)
then show ?case
by (metis fold_simps(2) maybe_or_valid)
qed auto

lemma fold_maybe_or_true_base_never_false:
"fold (∨?) l true ≠ false"
proof(induct l)
case (Cons a l)
then show ?case
by (metis fold_maybe_or_invalid_base fold_simps(2) maybe_not.cases maybe_or_valid plus_trilean.simps(4) plus_trilean.simps(6))
qed auto

lemma fold_true_fold_false_not_invalid:
"fold (∨?) l true = true ⟹
fold (∨?) (rev l) false ≠ invalid"
proof(induct l)
case (Cons a l)
then show ?case
apply simp
by (metis fold_maybe_or_invalid_base maybe_or_invalid maybe_or_true)
qed auto

lemma fold_true_invalid_fold_rev_false_invalid:
"fold (∨?) l true = invalid ⟹
fold (∨?) (rev l) false = invalid"
proof(induct l)
case (Cons a l)
then show ?case
apply simp
by (metis maybe_or_true maybe_or_valid)
qed auto

lemma fold_maybe_or_rev:
"fold (∨?) l b = fold (∨?) (rev l) b"
proof(induct l)
case (Cons a l)
then show ?case
proof(induction a b rule: plus_trilean.induct)
case (1 uu)
then show ?case
next
case "2_1"
then show ?case
next
case "2_2"
then show ?case
next
case "3_1"
then show ?case
apply simp
by (metis add.assoc fold_maybe_or_true_base_never_false maybe_not.cases maybe_or_idempotent maybe_or_true)
next
case "3_2"
then show ?case
apply simp
apply (case_tac "fold (∨?) l true")
apply (case_tac "fold (∨?) (rev l) false")
apply simp
apply simp
next
case 4
then show ?case
next
case 5
then show ?case
qed
qed auto

lemma fold_maybe_or_cons:
"fold (∨?) (a#l) b = a ∨? (fold (∨?) l b)"
by (metis fold_maybe_or_rev foldr.simps(2) foldr_conv_fold o_apply)

lemma gval_fold_gOr_map:
"gval (fold gOr l (Bc False)) s = fold (∨?) (map (λg. gval g s) l) (false)"
proof(induct l)
case (Cons a l)
then show ?case
by (metis fold_maybe_or_cons gval_fold_gOr list.simps(9))
qed auto

lemma gval_unfold_first:
"gval (fold gOr (map (λx. Eq (V v) (L x)) ls) (Eq (V v) (L l))) s =
gval (fold gOr (map (λx. Eq (V v) (L x)) (l#ls)) (Bc False)) s"
proof(induct ls)
case Nil
then show ?case
apply (cases "s v")
apply simp
next
case (Cons a ls)
then show ?case
proof -
have "gval (fold gOr (map (λva. Eq (V v) (L va)) ls) (gOr (Eq (V v) (L l)) (Bc False))) s = gval (fold gOr (map (λva. Eq (V v) (L va)) (l # ls)) (Bc False)) s"
by simp
then have "gval (fold gOr (map (λva. Eq (V v) (L va)) (a # ls)) (Eq (V v) (L l))) s = gval (fold gOr (Eq (V v) (L a) # map (λva. Eq (V v) (L va)) ls) (gOr (Eq (V v) (L l)) (Bc False))) s"
by (metis (no_types) Cons.hyps gval_fold_gOr list.simps(9))
then show ?thesis
by force
qed
qed

lemma fold_Eq_true:
"∀v. fold (∨?) (map (λx. if v = x then true else false) vs) true = true"
by(induct vs, auto)

lemma x_in_set_fold_eq:
"x ∈ set ll ⟹
fold (∨?) (map (λxa. if x = xa then true else false) ll) false = true"
proof(induct ll)
case (Cons a ll)
then show ?case
apply simp
apply standard
by auto
qed auto

lemma x_not_in_set_fold_eq:
"s v ∉ Some ` set ll ⟹
false = fold (∨?) (map (λx. if s v = Some x then true else false) ll) false"
by(induct ll, auto)

lemma gval_take: "max_input g < Some a ⟹
gval g (join_ir i r) = gval g (join_ir (take a i) r)"
proof(induct g)
case (Bc x)
then show ?case
by (metis (full_types) gval.simps(1) gval.simps(2))
next
case (Eq x1a x2)
then show ?case
by (metis aval_take gval.simps(4) max_input_Eq max_less_iff_conj)
next
case (Gt x1a x2)
then show ?case
by (metis aval_take gval.simps(3) max_input_Gt max_less_iff_conj)
next
case (Nor g1 g2)
then show ?case
next
case (In v l)
then show ?case
using aval_take by fastforce
qed

lemma gval_fold_gAnd_append_singleton:
"gval (fold gAnd (a @ [G]) (Bc True)) s = gval (fold gAnd a (Bc True)) s ∧? gval G s"
apply simp
using times_trilean_commutative by blast

lemma gval_fold_rev_true:
"gval (fold gAnd (rev G) (Bc True)) s = true ⟹
gval (fold gAnd G (Bc True)) s = true"
by (metis foldr_conv_fold gval_foldr_true rev_rev_ident set_rev)

lemma gval_fold_not_invalid_all_valid_contra:
"∃g ∈ set G. gval g s = invalid ⟹
gval (fold gAnd G (Bc True)) s = invalid"
proof(induct G rule: rev_induct)
case (snoc a G)
then show ?case
apply (simp only: gval_fold_gAnd_append_singleton)
apply simp
using maybe_and_valid by blast
qed auto

lemma gval_fold_not_invalid_all_valid:
"gval (fold gAnd G (Bc True)) s ≠ invalid ⟹
∀g ∈ set G. gval g s ≠ invalid"
using gval_fold_not_invalid_all_valid_contra by blast

lemma all_gval_not_false:
"(∀g ∈ set G. gval g s ≠ false) = (∀g ∈ set G. gval g s = true) ∨ (∃g ∈ set G. gval g s = invalid)"
using trilean.exhaust by auto

lemma must_have_one_false_contra:
"∀g ∈ set G. gval g s ≠ false ⟹
gval (fold gAnd G (Bc True)) s ≠ false"
using all_gval_not_false[of G s]
apply simp
apply (case_tac "(∀g∈set G. gval g s = true)")
apply (metis (full_types) foldr_conv_fold gval_fold_rev_true gval_foldr_true not_true)

lemma must_have_one_false:
"gval (fold gAnd G (Bc True)) s = false ⟹
∃g ∈ set G. gval g s = false"
using must_have_one_false_contra by blast

lemma all_valid_fold:
"∀g ∈ set G. gval g s ≠ invalid ⟹
gval (fold gAnd G (Bc True)) s ≠ invalid"
apply (induct G rule: rev_induct)
apply simp

lemma one_false_all_valid_false:
"∃g∈set G. gval g s = false ⟹
∀g∈set G. gval g s ≠ invalid ⟹
gval (fold gAnd G (Bc True)) s = false"
by (metis (full_types) all_valid_fold foldr_conv_fold gval_foldr_true not_true rev_rev_ident set_rev)

lemma gval_fold_rev_false:
"gval (fold gAnd (rev G) (Bc True)) s = false ⟹
gval (fold gAnd G (Bc True)) s = false"
using must_have_one_false[of "rev G" s]
gval_fold_not_invalid_all_valid[of "rev G" s]

lemma fold_invalid_means_one_invalid:
"gval (fold gAnd G (Bc True)) s = invalid ⟹
∃g ∈ set G. gval g s = invalid"
using all_valid_fold by blast

lemma gval_fold_rev_invalid:
"gval (fold gAnd (rev G) (Bc True)) s = invalid ⟹
gval (fold gAnd G (Bc True)) s = invalid"
using fold_invalid_means_one_invalid[of "rev G" s]

lemma gval_fold_rev_equiv_fold:
"gval (fold gAnd (rev G) (Bc True)) s =  gval (fold gAnd G (Bc True)) s"
apply (cases "gval (fold gAnd (rev G) (Bc True)) s")

lemma gval_fold_equiv_fold_rev:
"gval (fold gAnd G (Bc True)) s = gval (fold gAnd (rev G) (Bc True)) s"

lemma gval_fold_equiv_gval_foldr:
"gval (fold gAnd G (Bc True)) s = gval (foldr gAnd G (Bc True)) s"
proof -
have "gval (fold gAnd G (Bc True)) s = gval (fold gAnd (rev G) (Bc True)) s"
using gval_fold_equiv_fold_rev by force
then show ?thesis
qed

lemma gval_foldr_equiv_gval_fold:
"gval (foldr gAnd G (Bc True)) s = gval (fold gAnd G (Bc True)) s"

lemma gval_fold_cons:
"gval (fold gAnd (g # gs) (Bc True)) s = gval g s ∧? gval (fold gAnd gs (Bc True)) s"
apply (simp only: apply_guards_fold gval_fold_equiv_gval_foldr)
by (simp only: foldr.simps comp_def gval_gAnd)

lemma gval_fold_take: "max_input_list G < Some a ⟹
a ≤ length i ⟹
max_input_list G ≤ Some (length i) ⟹
gval (fold gAnd G (Bc True)) (join_ir i r) = gval (fold gAnd G (Bc True)) (join_ir (take a i) r)"
proof(induct G)
case (Cons g gs)
then show ?case
apply (simp only: gval_fold_cons)
using gval_take[of g a i r]
by simp
qed auto

primrec padding :: "nat ⇒ 'a list" where

definition take_or_pad :: "'a list ⇒ nat ⇒ 'a list" where
"take_or_pad a n = (if length a ≥ n then take n a else a@(padding (n-length a)))"

by (induct n, auto)

fun enumerate_gexp_strings :: "'a gexp ⇒ String.literal set" where
"enumerate_gexp_strings (Bc _) = {}" |
"enumerate_gexp_strings (Eq a1 a2) = enumerate_aexp_strings a1 ∪ enumerate_aexp_strings a2" |
"enumerate_gexp_strings (Gt a1 a2) = enumerate_aexp_strings a1 ∪ enumerate_aexp_strings a2" |
"enumerate_gexp_strings (In v l) = fold (λx acc. case x of Num n ⇒ acc | Str s ⇒ insert s acc) l {}" |
"enumerate_gexp_strings (Nor g1 g2) = enumerate_gexp_strings g1 ∪ enumerate_gexp_strings g2"

fun enumerate_gexp_ints :: "'a gexp ⇒ int set" where
"enumerate_gexp_ints (Bc _) = {}" |
"enumerate_gexp_ints (Eq a1 a2) = enumerate_aexp_ints a1 ∪ enumerate_aexp_ints a2" |
"enumerate_gexp_ints (Gt a1 a2) = enumerate_aexp_ints a1 ∪ enumerate_aexp_ints a2" |
"enumerate_gexp_ints (In v l) = fold (λx acc. case x of Str s ⇒ acc | Num n ⇒ insert n acc) l {}" |
"enumerate_gexp_ints (Nor g1 g2) = enumerate_gexp_ints g1 ∪ enumerate_gexp_ints g2"

definition restricted_once :: "'a ⇒ 'a gexp list ⇒ bool" where
"restricted_once v G = (length (filter (λg. gexp_constrains g (V v)) G) = 1)"

definition not_restricted :: "'a ⇒ 'a gexp list ⇒ bool" where
"not_restricted v G = (length (filter (λg. gexp_constrains g (V v)) G) = 0)"

lemma restricted_once_cons:
"restricted_once v (g#gs) = ((gexp_constrains g (V v) ∧ not_restricted v gs) ∨ ((¬ gexp_constrains g (V v)) ∧ restricted_once v gs))"

lemma not_restricted_cons:
"not_restricted v (g#gs) = ((¬ gexp_constrains g (V v)) ∧ not_restricted v gs)"

definition enumerate_vars :: "vname gexp ⇒ vname list" where
"enumerate_vars g = sorted_list_of_set ((image R (enumerate_regs g)) ∪ (image I (enumerate_gexp_inputs g)))"

fun rename_regs :: "(nat ⇒ nat) ⇒ vname gexp ⇒ vname gexp" where
"rename_regs _ (Bc b) = Bc b" |
"rename_regs f (Eq a1 a2) = Eq (AExp.rename_regs f a1) (AExp.rename_regs f a2)" |
"rename_regs f (Gt a1 a2) = Gt (AExp.rename_regs f a1) (AExp.rename_regs f a2)" |
"rename_regs f (In (R r) vs) = In (R (f r)) vs" |
"rename_regs f (In v vs) = In v vs" |
"rename_regs f (Nor g1 g2) = Nor (rename_regs f g1) (rename_regs f g2)"

definition eq_upto_rename :: "vname gexp ⇒ vname gexp ⇒ bool" where
"eq_upto_rename g1 g2 = (∃f. bij f ∧ rename_regs f g1 = g2)"

lemma gval_reg_some_superset:
"∀a. (r \$ a  ≠ None) ⟶ r \$ a = r' \$ a ⟹
x ≠ invalid ⟹
gval a (join_ir i r) = x ⟹
gval a (join_ir i r') = x"
proof(induct a arbitrary: x)
case (Bc b)
then show ?case by (cases b, auto)
next
case (Eq x1a x2)
then show ?case
apply (cases x)
apply simp
using value_eq_true[of "aval x1a (join_ir i r)" "aval x2 (join_ir i r)"]
apply clarsimp
apply simp
using value_eq_false[of "aval x1a (join_ir i r)" "aval x2 (join_ir i r)"]
apply clarsimp
by simp
next
case (Gt x1a x2)
then show ?case
apply (cases x)
apply simp
using value_gt_true_Some[of "aval x1a (join_ir i r)" "aval x2 (join_ir i r)"]
apply clarsimp
apply simp
using value_gt_false_Some[of "aval x1a (join_ir i r)" "aval x2 (join_ir i r)"]
apply clarsimp
by simp
next
case (In x1a x2)
then show ?case
apply simp
apply (case_tac "join_ir i r x1a")
apply simp
apply (case_tac "join_ir i r' x1a")
apply simp
apply (metis aval_reg_some_superset In.prems(1) aval.simps(2) option.distinct(1))
apply simp
by (metis (full_types) aval_reg_some_superset In.prems(1) aval.simps(2) option.inject)
next
case (Nor a1 a2)
then show ?case
apply simp
apply (cases x)
apply presburger
by simp
qed

lemma apply_guards_reg_some_superset:
"∀a. (r \$ a  ≠ None) ⟶ r \$ a = r' \$ a ⟹
apply_guards G (join_ir i r) ⟹
apply_guards G (join_ir i r')"
apply (induct G)
apply simp