# Theory Least_Upper_Bound

section‹Least Upper Bound›
text‹The simplest way to merge a pair of transitions with identical outputs and updates is to
simply take the least upper bound of their \emph{guards}. This theory presents several variants on
this theme.›

theory Least_Upper_Bound
imports "../Inference"
begin

fun literal_args :: "'a gexp ⇒ bool" where
"literal_args (Bc v) = False" |
"literal_args (Eq (V _) (L _)) = True" |
"literal_args (In _ _) = True" |
"literal_args (Eq _ _) = False" |
"literal_args (Gt va v) = False" |
"literal_args (Nor v va) = (literal_args v ∧ literal_args va)"

lemma literal_args_eq:
"literal_args (Eq a b) ⟹ ∃v l. a = (V v) ∧ b = (L l)"
apply (cases a)
apply simp
apply (cases b)
by auto

definition "all_literal_args t = (∀g ∈ set (Guards t). literal_args g)"

fun merge_in_eq :: "vname ⇒ value ⇒ vname gexp list ⇒ vname gexp list" where
"merge_in_eq v l [] = [Eq (V v) (L l)]" |
"merge_in_eq v l ((Eq (V v') (L l'))#t) = (if v = v' ∧ l ≠ l' then (In v [l, l'])#t else (Eq (V v') (L l'))#(merge_in_eq v l t))" |
"merge_in_eq v l ((In v' l')#t) = (if v = v' then (In v (remdups (l#l')))#t else (In v' l')#(merge_in_eq v l t))" |
"merge_in_eq v l (h#t) = h#(merge_in_eq v l t)"

fun merge_in_in :: "vname ⇒ value list ⇒ vname gexp list ⇒ vname gexp list" where
"merge_in_in v l [] = [In v l]" |
"merge_in_in v l ((Eq (V v') (L l'))#t) = (if v = v' then (In v (List.insert l' l))#t else (Eq (V v') (L l'))#(merge_in_in v l t))" |
"merge_in_in v l ((In v' l')#t) = (if v = v' then (In v (List.union l l'))#t else (In v' l')#(merge_in_in v l t))" |
"merge_in_in v l (h#t) = h#(merge_in_in v l t)"

fun merge_guards :: "vname gexp list ⇒ vname gexp list ⇒ vname gexp list" where
"merge_guards [] g2 = g2" |
"merge_guards ((Eq (V v) (L l))#t) g2 =  merge_guards t (merge_in_eq v l g2)" |
"merge_guards ((In v l)#t) g2 = merge_guards t (merge_in_in v l g2)" |
"merge_guards (h#t) g2 = h#(merge_guards t g2)"

text‹The least upper bound'' (lob) heuristic simply disjoins the guards of two transitions with
definition lob_aux :: "transition ⇒ transition ⇒ transition option" where
"lob_aux t1 t2 = (if Outputs t1 = Outputs t2 ∧ Updates t1 = Updates t2 ∧ all_literal_args t1 ∧ all_literal_args t2 then
Some ⦇Label = Label t1, Arity = Arity t1, Guards = remdups (merge_guards (Guards t1) (Guards t2)), Outputs = Outputs t1, Updates = Updates t1⦈
else None)"

fun lob :: update_modifier where
"lob t1ID t2ID s new _ old _ = (let
t1 = (get_by_ids new t1ID);
t2 = (get_by_ids new t2ID) in
case lob_aux t1 t2 of
None ⇒ None |
Some lob_t ⇒
Some (replace_transitions new [(t1ID, lob_t), (t2ID, lob_t)])
)"

lemma lob_aux_some: "Outputs t1 = Outputs t2 ⟹
all_literal_args t1 ⟹
all_literal_args t2 ⟹
Label t = Label t1 ⟹
Arity t = Arity t1 ⟹
Guards t = remdups (merge_guards (Guards t1) (Guards t2)) ⟹
Outputs t = Outputs t1 ⟹
lob_aux t1 t2 = Some t"

fun has_corresponding :: "vname gexp ⇒ vname gexp list ⇒ bool" where
"has_corresponding g [] = False" |
"has_corresponding (Eq (V v) (L l)) ((Eq (V v') (L l'))#t) = (if v = v' ∧ l = l' then True else has_corresponding (Eq (V v) (L l)) t)" |
"has_corresponding (In v' l') ((Eq (V v) (L l))#t) = (if v = v' ∧ l ∈ set l' then True else has_corresponding (In v' l') t)" |
"has_corresponding (In v l) ((In v' l')#t) = (if v = v' ∧ set l' ⊆ set l then True else has_corresponding (In v l) t)" |
"has_corresponding g (h#t) = has_corresponding g t"

lemma no_corresponding_bc: "¬has_corresponding (Bc x1) G1"
apply (induct G1)
by auto

lemma no_corresponding_gt: "¬has_corresponding (Gt x1 y1) G1"
apply (induct G1)
by auto

lemma no_corresponding_nor: "¬has_corresponding (Nor x1 y1) G1"
apply (induct G1)
by auto

lemma has_corresponding_eq: "has_corresponding (Eq x21 x22) G1 ⟹ (Eq x21 x22) ∈ set G1"
proof(induct G1)
case (Cons a G1)
then show ?case
apply (cases a)
apply simp
subgoal for x21a x22a
apply (case_tac "x21a")
apply simp
apply (case_tac "x22a")
apply clarify
apply simp
apply (case_tac "x21")
apply simp
apply (case_tac "x22")
apply (metis has_corresponding.simps(2))
by auto
by auto
qed auto

lemma has_corresponding_In: "has_corresponding (In v l) G1 ⟹ (∃l'. (In v l') ∈ set G1 ∧ set l' ⊆ set l) ∨ (∃l' ∈ set l. (Eq (V v) (L l')) ∈ set G1)"
proof(induct G1)
case (Cons a G1)
then show ?case
apply (cases a)
apply simp
defer
apply simp
apply simp
defer
apply simp
apply simp
subgoal for x21 x22 apply (case_tac x21)
apply simp
apply (case_tac x22)
apply fastforce
apply simp+
done
by metis
qed auto

lemma gval_each_one: "g ∈ set G ⟹ apply_guards G s ⟹ gval g s = true"
using apply_guards_cons apply_guards_rearrange by blast

lemma has_corresponding_apply_guards:
"∀g∈set G2. has_corresponding g G1 ⟹
apply_guards G1 s ⟹
apply_guards G2 s"
proof(induct G2)
case (Cons a G2)
then show ?case
apply (cases a)
apply simp
apply (metis (full_types) has_corresponding_eq append_Cons append_self_conv2 apply_guards_append apply_guards_rearrange)
apply simp
subgoal for v l
apply (insert has_corresponding_In[of v l G1])
apply simp
apply (erule disjE)
apply clarsimp
subgoal for l'
apply (insert apply_guards_rearrange[of "In v l'" G1 s])
apply simp
apply (simp only: apply_guards_cons[of "In v l" G2])
apply (simp only: apply_guards_cons[of "In v l'" G1])
apply simp
apply (cases "s v")
apply simp
by force
apply clarsimp
subgoal for l'
apply (insert apply_guards_rearrange[of "Eq (V v) (L l')" G1 s])
apply simp
apply (simp only: apply_guards_cons[of "In v l" G2])
apply (simp only: apply_guards_cons[of "Eq (V v) (L l')" G1])
apply (cases "s v")
apply simp
apply simp
using trilean.distinct(1) by presburger
done
qed auto

lemma correspondence_subsumption:
"Label t1 = Label t2 ⟹
Arity t1 = Arity t2 ⟹
Outputs t1 = Outputs t2 ⟹
∀g ∈ set (Guards t2). has_corresponding g (Guards t1) ⟹
subsumes t2 c t1"
by (simp add: can_take_def can_take_transition_def has_corresponding_apply_guards subsumption)

definition "is_lob t1 t2 = (
Label t1 = Label t2 ∧
Arity t1 = Arity t2 ∧
Outputs t1 = Outputs t2 ∧
(∀g ∈ set (Guards t2). has_corresponding g (Guards t1)))"

lemma is_lob_direct_subsumption:
"is_lob t1 t2 ⟹ directly_subsumes e1 e2 s s' t2 t1"
apply (rule subsumes_in_all_contexts_directly_subsumes)

fun has_distinguishing :: "vname gexp ⇒ vname gexp list ⇒ bool" where
"has_distinguishing g [] = False" |
"has_distinguishing (Eq (V v) (L l)) ((Eq (V v') (L l'))#t) = (if v = v' ∧ l ≠ l' then True else has_distinguishing (Eq (V v) (L l)) t)" |
"has_distinguishing (In (I v') l') ((Eq (V (I v)) (L l))#t) = (if v = v' ∧ l ∉ set l' then True else has_distinguishing (In (I v') l') t)" |
"has_distinguishing (In (I v) l) ((In (I v') l')#t) = (if v = v' ∧ set l' ⊃ set l then True else has_distinguishing (In (I v) l) t)" |
"has_distinguishing g (h#t) = has_distinguishing g t"

lemma has_distinguishing: "has_distinguishing g G ⟹ (∃v l. g = (Eq (V v) (L l))) ∨ (∃v l. g = In v l)"
proof(induct G)
case (Cons a G)
then show ?case
apply (cases g)
apply simp
apply (case_tac x21)
apply simp
apply (case_tac x22)
by auto
qed auto

lemma has_distinguishing_Eq: "has_distinguishing (Eq (V v) (L l)) G ⟹ ∃l'. (Eq (V v) (L l')) ∈ set G ∧ l ≠ l'"
proof (induct G)
case (Cons a G)
then show ?case
apply (cases a)
apply simp
apply (case_tac x21)
apply simp
apply (case_tac x22)
apply (metis has_distinguishing.simps(2) list.set_intros(1) list.set_intros(2))
by auto
qed auto

lemma ex_mutex: "Eq (V v) (L l) ∈ set G1 ⟹
Eq (V v) (L l') ∈ set G2 ⟹
l ≠ l' ⟹
apply_guards G1 s ⟹
¬ apply_guards G2 s"
apply (rule_tac x="Eq (V v) (L l')" in exI)
apply simp
apply (case_tac "s v")
by auto

lemma has_distinguishing_In:
"has_distinguishing (In v l) G ⟹
(∃l' i. v = I i ∧ Eq (V v) (L l') ∈ set G ∧ l' ∉ set l) ∨ (∃l' i. v = I i ∧ In v l' ∈ set G ∧ set l' ⊃ set l)"
proof(induct G)
case (Cons a G)
then show ?case
apply (case_tac v)
subgoal for x
apply simp
apply (cases a)
apply simp
subgoal for x21 x22
apply (case_tac x21)
apply simp
apply (case_tac x22)
apply (case_tac x2)
apply fastforce
apply simp+
done
subgoal by simp
subgoal for x41
apply (case_tac x41)
apply (simp, metis)
by auto
by auto
by auto
qed auto

lemma Eq_apply_guards:
"Eq (V v) (L l) ∈ set G1 ⟹
apply_guards G1 s ⟹
s v = Some l"
apply (cases "s v")
apply simp
apply simp
using trilean.distinct(1) by presburger

lemma In_neq_apply_guards:
"In v l ∈ set G2 ⟹
Eq (V v) (L l') ∈ set G1 ⟹
l' ∉ set l ⟹
apply_guards G1 s ⟹
¬apply_guards G2 s"
proof(induct G1)
case (Cons a G1)
then show ?case
apply (rule_tac x="In v l" in exI)
using Eq_apply_guards[of v l' "a#G1" s]
qed auto

lemma In_apply_guards: "In v l ∈ set G1 ⟹ apply_guards G1 s ⟹ ∃v' ∈ set l. s v = Some v'"
apply (cases "s v")
apply simp
apply simp
by (meson image_iff trilean.simps(2))

lemma input_not_constrained_aval_swap_inputs:
"¬ aexp_constrains a (V (I v)) ⟹
aval a (join_ir i c) = aval a (join_ir (list_update i v x) c)"
apply(induct a rule: aexp_induct_separate_V_cases)
apply simp
apply (metis aexp_constrains.simps(2) aval.simps(2) input2state_nth input2state_out_of_bounds join_ir_def length_list_update not_le nth_list_update_neq vname.simps(5))
using join_ir_def by auto

lemma input_not_constrained_gval_swap_inputs:
"¬ gexp_constrains a (V (I v)) ⟹
gval a (join_ir i c) = gval a (join_ir (i[v := x]) c)"
proof(induct a)
case (Bc x)
then show ?case
by (metis (full_types) gval.simps(1) gval.simps(2))
next
case (Eq x1a x2)
then show ?case
using input_not_constrained_aval_swap_inputs by auto
next
case (Gt x1a x2)
then show ?case
using input_not_constrained_aval_swap_inputs by auto
next
case (In x1a x2)
then show ?case
apply simp
apply (case_tac "join_ir i c x1a")
apply (case_tac "join_ir (i[v := x]) c x1a")
apply simp
apply (metis In.prems aval.simps(2) gexp_constrains.simps(5) input_not_constrained_aval_swap_inputs option.discI)
apply (case_tac "join_ir (i[v := x]) c x1a")
apply (metis In.prems aval.simps(2) gexp_constrains.simps(5) input_not_constrained_aval_swap_inputs option.discI)
by (metis In.prems aval.simps(2) gexp_constrains.simps(5) input_not_constrained_aval_swap_inputs)
qed auto

lemma test_aux: "∀g∈set (removeAll (In (I v) l) G1). ¬ gexp_constrains g (V (I v)) ⟹
apply_guards G1 (join_ir i c) ⟹
x ∈ set l ⟹
apply_guards G1 (join_ir (i[v := x]) c)"
proof(induct G1)
case (Cons a G1)
then show ?case
apply (simp only: apply_guards_cons)
apply (case_tac "a = In (I v) l")
apply simp
apply (case_tac "join_ir i c (I v)")
apply simp
apply (case_tac "join_ir (i[v := x]) c (I v)")
apply (metis join_ir_nth le_less_linear length_list_update list_update_beyond option.discI)
apply simp
apply (metis join_ir_nth le_less_linear length_list_update list_update_beyond nth_list_update_eq option.inject trilean.distinct(1))
apply (case_tac "join_ir (i[v := x]) c (I v)")
apply (metis join_ir_nth le_less_linear length_list_update list_update_beyond option.discI)
apply simp
using input_not_constrained_gval_swap_inputs by auto
qed auto

lemma test:
assumes
p1: "In (I v) l ∈ set G2" and
p2: "In (I v) l' ∈ set G1" and
p3: "x ∈ set l'" and
p4: "x ∉ set l" and
p5: "apply_guards G1 (join_ir i c)" and
p6: "length i = a" and
p7: "∀g ∈ set (removeAll (In (I v) l') G1). ¬ gexp_constrains g (V (I v))"
shows "∃i. length i = a ∧ apply_guards G1 (join_ir i c) ∧ (length i = a ⟶ ¬ apply_guards G2 (join_ir i c))"
apply (rule_tac x="list_update i v x" in exI)
apply standard
apply standard
using p3 p5 p7 test_aux apply blast
using p1 p4
apply (case_tac "input2state (i[v := x]) $v") apply simp apply simp by (metis input2state_nth input2state_within_bounds length_list_update nth_list_update_eq option.inject) definition get_Ins :: "vname gexp list ⇒ (nat × value list) list" where "get_Ins G = map (λg. case g of (In (I v) l) ⇒ (v, l)) (filter (λg. case g of (In (I _) _ ) ⇒ True | _ ⇒ False) G)" lemma get_Ins_Cons_equiv: "∄v l. a = In (I v) l ⟹ get_Ins (a # G) = get_Ins G" apply (simp add: get_Ins_def) apply (cases a) apply simp+ apply (metis (full_types) vname.exhaust vname.simps(6)) by simp lemma Ball_Cons: "(∀x ∈ set (a#l). P x) = (P a ∧ (∀x ∈ set l. P x))" by simp lemma In_in_get_Ins: "(In (I v) l ∈ set G) = ((v, l) ∈ set (get_Ins G))" proof(induct G) case Nil then show ?case by (simp add: get_Ins_def) next case (Cons a G) then show ?case apply (simp add: get_Ins_def) apply (cases a) apply simp+ subgoal for x by (case_tac x, auto) apply auto done qed definition "check_get_Ins G = (∀(v, l') ∈ set (get_Ins G). ∀g ∈ set (removeAll (In (I v) l') G). ¬ gexp_constrains g (V (I v)))" lemma no_Ins: "[] = get_Ins G ⟹ set G - {In (I i) l} = set G" proof(induct G) case (Cons a G) then show ?case apply (cases a) apply (simp add: get_Ins_Cons_equiv insert_Diff_if)+ subgoal for x41 x42 apply (case_tac x41) apply simp apply (metis In_in_get_Ins equals0D list.set(1) list.set_intros(1)) apply (simp add: get_Ins_Cons_equiv) done by (simp add: get_Ins_Cons_equiv insert_Diff_if) qed auto lemma test2: "In (I i) l ∈ set (Guards t2) ⟹ In (I i) l' ∈ set (Guards t1) ⟹ length ia = Arity t1 ⟹ apply_guards (Guards t1) (join_ir ia c) ⟹ x ∈ set l' ⟹ x ∉ set l ⟹ ∀(v, l')∈insert (0, []) (set (get_Ins (Guards t1))). ∀g∈set (removeAll (In (I v) l') (Guards t1)). ¬ gexp_constrains g (V (I v)) ⟹ Arity t1 = Arity t2 ⟹ ∃i. length i = Arity t2 ∧ apply_guards (Guards t1) (join_ir i c) ∧ (length i = Arity t2 ⟶ ¬ apply_guards (Guards t2) (join_ir i c))" using test[of i l "Guards t2" l' "Guards t1" x ia c "Arity t2"] apply simp apply (case_tac "∀g∈set (Guards t1) - {In (I i) l'}. ¬ gexp_constrains g (V (I i))") apply simp apply simp using In_in_get_Ins by blast lemma distinguishing_subsumption: assumes p1: "∃g ∈ set (Guards t2). has_distinguishing g (Guards t1)" and p2: "Arity t1 = Arity t2" and p3: "∃i. can_take_transition t1 i c" and p4: "(∀(v, l') ∈ insert (0, []) (set (get_Ins (Guards t1))). ∀g ∈ set (removeAll (In (I v) l') (Guards t1)). ¬ gexp_constrains g (V (I v)))" shows "¬ subsumes t2 c t1" proof- show ?thesis apply (rule bad_guards) apply (simp add: can_take_transition_def can_take_def p2) apply (insert p1, simp add: Bex_def) apply (erule exE) apply (case_tac "∃v l. x = (Eq (V v) (L l))") apply (metis can_take_def can_take_transition_def ex_mutex p2 p3 has_distinguishing_Eq) apply (case_tac "∃v l. x = In v l") defer using has_distinguishing apply blast apply clarify apply (case_tac "∃l' i. v = I i ∧ Eq (V v) (L l') ∈ set (Guards t1) ∧ l' ∉ set l") apply (metis In_neq_apply_guards can_take_def can_take_transition_def p2 p3) apply (case_tac "(∃l' i. v = I i ∧ In v l' ∈ set (Guards t1) ∧ set l' ⊃ set l)") defer using has_distinguishing_In apply blast apply simp apply (erule conjE) apply (erule exE)+ apply (erule conjE) apply (insert p3, simp only: can_take_transition_def can_take_def) apply (case_tac "∃x. x ∈ set l' ∧ x ∉ set l") apply (erule exE)+ apply (erule conjE)+ apply (insert p4 p2) using test2 apply blast by auto qed definition "lob_distinguished t1 t2 = ( (∃g ∈ set (Guards t2). has_distinguishing g (Guards t1)) ∧ Arity t1 = Arity t2 ∧ (∀(v, l') ∈ insert (0, []) (set (get_Ins (Guards t1))). ∀g ∈ set (removeAll (In (I v) l') (Guards t1)). ¬ gexp_constrains g (V (I v))))" lemma must_be_another: "1 < size (fset_of_list b) ⟹ x ∈ set b ⟹ ∃x' ∈ set b. x ≠ x'" proof(induct b) case (Cons a b) then show ?case apply (simp add: Bex_def) by (metis List.finite_set One_nat_def card.insert card_gt_0_iff card_mono fset_of_list.rep_eq insert_absorb le_0_eq less_nat_zero_code less_numeral_extra(4) not_less_iff_gr_or_eq set_empty2 subsetI) qed auto lemma another_swap_inputs: "apply_guards G (join_ir i c) ⟹ filter (λg. gexp_constrains g (V (I a))) G = [In (I a) b] ⟹ xa ∈ set b ⟹ apply_guards G (join_ir (i[a := xa]) c)" proof(induct G) case (Cons g G) then show ?case apply (simp add: apply_guards_cons) apply (case_tac "gexp_constrains g (V (I a))") defer using input_not_constrained_gval_swap_inputs apply auto[1] apply simp apply (case_tac "join_ir i c (I a) ∈ Some  set b") defer apply simp apply clarify apply standard using apply_guards_def input_not_constrained_gval_swap_inputs apply (simp add: filter_empty_conv) apply (case_tac "join_ir i c (I a)") apply simp apply (case_tac "join_ir (i[a := xa]) c (I a)") apply simp apply (metis image_eqI trilean.distinct(1)) apply simp apply (metis image_eqI trilean.distinct(1)) apply (case_tac "join_ir i c (I a)") apply simp apply simp apply (metis image_eqI trilean.distinct(1)) apply (case_tac "join_ir i c (I a)") apply simp apply (case_tac "join_ir (i[a := xa]) c (I a)") apply simp apply (metis join_ir_nth le_less_linear length_list_update list_update_beyond option.discI) apply simp apply standard apply (metis (no_types, lifting) Cons.hyps Cons.prems(2) filter_empty_conv removeAll_id set_ConsD test_aux) by (metis in_these_eq join_ir_nth le_less_linear length_list_update list_update_beyond nth_list_update_eq these_image_Some_eq) qed auto lemma lob_distinguished_2_not_subsumes: "∃(i, l) ∈ set (get_Ins (Guards t2)). filter (λg. gexp_constrains g (V (I i))) (Guards t2) = [(In (I i) l)] ∧ (∃l' ∈ set l. i < Arity t1 ∧ Eq (V (I i)) (L l') ∈ set (Guards t1) ∧ size (fset_of_list l) > 1) ⟹ Arity t1 = Arity t2 ⟹ ∃i. can_take_transition t2 i c ⟹ ¬ subsumes t1 c t2" apply (rule bad_guards) apply simp apply (simp add: can_take_def can_take_transition_def Bex_def) apply clarify apply (case_tac "∃x' ∈ set b. x ≠ x'") defer apply (simp add: must_be_another) apply (simp add: Bex_def) apply (erule exE) apply (rule_tac x="list_update i a xa" in exI) apply simp apply standard apply (simp add: another_swap_inputs) by (metis Eq_apply_guards input2state_nth join_ir_def length_list_update nth_list_update_eq option.inject vname.simps(5)) definition "lob_distinguished_2 t1 t2 = (∃(i, l) ∈ set (get_Ins (Guards t2)). filter (λg. gexp_constrains g (V (I i))) (Guards t2) = [(In (I i) l)] ∧ (∃l' ∈ set l. i < Arity t1 ∧ Eq (V (I i)) (L l') ∈ set (Guards t1) ∧ size (fset_of_list l) > 1) ∧ Arity t1 = Arity t2)" lemma lob_distinguished_3_not_subsumes: "∃(i, l) ∈ set (get_Ins (Guards t2)). filter (λg. gexp_constrains g (V (I i))) (Guards t2) = [(In (I i) l)] ∧ (∃(i', l') ∈ set (get_Ins (Guards t1)). i = i' ∧ set l' ⊂ set l) ⟹ Arity t1 = Arity t2 ⟹ ∃i. can_take_transition t2 i c ⟹ ¬ subsumes t1 c t2" apply (rule bad_guards) apply simp apply (simp add: can_take_def can_take_transition_def Bex_def) apply (erule exE)+ apply (erule conjE)+ apply (erule exE)+ apply (erule conjE)+ apply (case_tac "∃x. x ∈ set b ∧ x ∉ set ba") defer apply auto[1] apply (erule exE)+ apply (erule conjE)+ apply (rule_tac x="list_update i a x" in exI) apply simp apply standard using another_swap_inputs apply blast by (metis In_apply_guards In_in_get_Ins input2state_not_None input2state_nth join_ir_def nth_list_update_eq option.distinct(1) option.inject vname.simps(5)) definition "lob_distinguished_3 t1 t2 = (∃(i, l) ∈ set (get_Ins (Guards t2)). filter (λg. gexp_constrains g (V (I i))) (Guards t2) = [(In (I i) l)] ∧ (∃(i', l') ∈ set (get_Ins (Guards t1)). i = i' ∧ set l' ⊂ set l) ∧ Arity t1 = Arity t2)" fun is_In :: "'a gexp ⇒ bool" where "is_In (In _ _) = True" | "is_In _ = False" text‹The greatest upper bound'' (gob) heuristic is similar to \texttt{lob} but applies a more intellegent approach to guard merging.› definition gob_aux :: "transition ⇒ transition ⇒ transition option" where "gob_aux t1 t2 = (if Outputs t1 = Outputs t2 ∧ Updates t1 = Updates t2 ∧ all_literal_args t1 ∧ all_literal_args t2 then Some ⦇Label = Label t1, Arity = Arity t1, Guards = remdups (filter (Not ∘ is_In) (merge_guards (Guards t1) (Guards t2))), Outputs = Outputs t1, Updates = Updates t1⦈ else None)" fun gob :: update_modifier where "gob t1ID t2ID s new _ old _ = (let t1 = (get_by_ids new t1ID); t2 = (get_by_ids new t2ID) in case gob_aux t1 t2 of None ⇒ None | Some gob_t ⇒ Some (replace_transitions new [(t1ID, gob_t), (t2ID, gob_t)]) )" text‹The Gung Ho'' heuristic simply drops the guards of both transitions, making them identical.› definition gung_ho_aux :: "transition ⇒ transition ⇒ transition option" where "gung_ho_aux t1 t2 = (if Outputs t1 = Outputs t2 ∧ Updates t1 = Updates t2 ∧ all_literal_args t1 ∧ all_literal_args t2 then Some ⦇Label = Label t1, Arity = Arity t1, Guards = [], Outputs = Outputs t1, Updates = Updates t1⦈ else None)" fun gung_ho :: update_modifier where "gung_ho t1ID t2ID s new _ old _ = (let t1 = (get_by_ids new t1ID); t2 = (get_by_ids new t2ID) in case gung_ho_aux t1 t2 of None ⇒ None | Some gob_t ⇒ Some (replace_transitions new [(t1ID, gob_t), (t2ID, gob_t)]) )" lemma guard_subset_eq_outputs_updates_subsumption: "Label t1 = Label t2 ⟹ Arity t1 = Arity t2 ⟹ Outputs t1 = Outputs t2 ⟹ Updates t1 = Updates t2 ⟹ set (Guards t2) ⊆ set (Guards t1) ⟹ subsumes t2 c t1" apply (simp add: subsumes_def) by (meson can_take_def can_take_subset can_take_transition_def) lemma guard_subset_eq_outputs_updates_direct_subsumption: "Label t1 = Label t2 ⟹ Arity t1 = Arity t2 ⟹ Outputs t1 = Outputs t2 ⟹ Updates t1 = Updates t2 ⟹ set (Guards t2) ⊆ set (Guards t1) ⟹ directly_subsumes m1 m2 s1 s2 t2 t1" apply (rule subsumes_in_all_contexts_directly_subsumes) by (simp add: guard_subset_eq_outputs_updates_subsumption) lemma unconstrained_input: "∀g∈set G. ¬ gexp_constrains g (V (I i)) ⟹ apply_guards G (join_ir ia c) ⟹ apply_guards G (join_ir (ia[i := x']) c)" proof(induct G) case (Cons a G) then show ?case apply (simp add: apply_guards_cons) using input_not_constrained_gval_swap_inputs[of a i ia c x'] by simp qed auto lemma each_input_guarded_once_cons: "∀i∈⋃ (enumerate_gexp_inputs  set (a # G)). length (filter (λg. gexp_constrains g (V (I i))) (a # G)) ≤ 1 ⟹ ∀i∈⋃ (enumerate_gexp_inputs  set G). length (filter (λg. gexp_constrains g (V (I i))) G) ≤ 1" apply (simp add: Ball_def) apply clarify proof - fix x :: nat and xa :: "vname gexp" assume a1: "∀x. (x ∈ enumerate_gexp_inputs a ⟶ length (if gexp_constrains a (V (I x)) then a # filter (λg. gexp_constrains g (V (I x))) G else filter (λg. gexp_constrains g (V (I x))) G) ≤ 1) ∧ ((∃xa∈set G. x ∈ enumerate_gexp_inputs xa) ⟶ length (if gexp_constrains a (V (I x)) then a # filter (λg. gexp_constrains g (V (I x))) G else filter (λg. gexp_constrains g (V (I x))) G) ≤ 1)" assume a2: "xa ∈ set G" assume "x ∈ enumerate_gexp_inputs xa" then have "if gexp_constrains a (V (I x)) then length (a # filter (λg. gexp_constrains g (V (I x))) G) ≤ 1 else length (filter (λg. gexp_constrains g (V (I x))) G) ≤ 1" using a2 a1 by fastforce then show "length (filter (λg. gexp_constrains g (V (I x))) G) ≤ 1" by (metis (no_types) impossible_Cons le_cases order.trans) qed lemma literal_args_can_take: "∀g∈set G. ∃i v s. g = Eq (V (I i)) (L v) ∨ g = In (I i) s ∧ s ≠ [] ⟹ ∀i∈⋃ (enumerate_gexp_inputs  set G). i < a ⟹ ∀i∈⋃ (enumerate_gexp_inputs  set G). length (filter (λg. gexp_constrains g (V (I i))) G) ≤ 1 ⟹ ∃i. length i = a ∧ apply_guards G (join_ir i c)" proof(induct G) case Nil then show ?case using Ex_list_of_length by auto next case (Cons a G) then show ?case apply simp apply (case_tac "∀y∈set G. ∀i∈enumerate_gexp_inputs y. length (filter (λg. gexp_constrains g (V (I i))) G) ≤ 1") defer using each_input_guarded_once_cons apply auto[1] apply (simp add: ball_Un) apply clarsimp apply (induct a) apply simp apply simp subgoal for x2 i ia apply (case_tac x2) apply (rule_tac x="list_update i ia x1" in exI) apply (simp add: apply_guards_cons unconstrained_input filter_empty_conv) apply simp+ done apply simp subgoal for _ x2 i ia apply (case_tac x2) apply simp subgoal for aa apply (rule_tac x="list_update i ia aa" in exI) apply (simp add: apply_guards_cons unconstrained_input filter_empty_conv) done done by simp qed lemma "(SOME x'. x' ≠ (v::value)) ≠ v" proof(induct v) case (Num x) then show ?case by (metis (full_types) someI_ex value.simps(4)) next case (Str x) then show ?case by (metis (full_types) someI_ex value.simps(4)) qed lemma opposite_gob_subsumption: "∀g ∈ set (Guards t1). ∃i v s. g = Eq (V (I i)) (L v) ∨ (g = In (I i) s ∧ s ≠ []) ⟹ ∀g ∈ set (Guards t2). ∃i v s. g = Eq (V (I i)) (L v) ∨ (g = In (I i) s ∧ s ≠ []) ⟹ ∃ i. ∃v. Eq (V (I i)) (L v) ∈ set (Guards t1) ∧ (∀g ∈ set (Guards t2). ¬ gexp_constrains g (V (I i))) ⟹ Arity t1 = Arity t2 ⟹ ∀i ∈ enumerate_inputs t2. i < Arity t2 ⟹ ∀i ∈ enumerate_inputs t2. length (filter (λg. gexp_constrains g (V (I i))) (Guards t2)) ≤ 1 ⟹ ¬ subsumes t1 c t2" apply (rule bad_guards) apply (simp add: enumerate_inputs_def can_take_transition_def can_take_def Bex_def) using literal_args_can_take[of "Guards t2" "Arity t2" c] apply simp apply clarify subgoal for i ia v apply (rule_tac x="list_update ia i (Eps (λx'. x' ≠ v))" in exI) apply simp apply standard apply (simp add: apply_guards_def) using input_not_constrained_gval_swap_inputs apply simp apply (simp add: apply_guards_def Bex_def) apply (rule_tac x="Eq (V (I i)) (L v)" in exI) apply (simp add: join_ir_def) apply (case_tac "input2state (ia[i := SOME x'. x' ≠ v])$ i")
apply simp
apply simp
apply (case_tac "i < length ia")
apply (case_tac v)
apply (metis (mono_tags) someI_ex value.simps(4))
apply (metis (mono_tags) someI_ex value.simps(4))
by (metis input2state_within_bounds length_list_update)
done

fun is_lit_eq :: "vname gexp ⇒ nat ⇒ bool" where
"is_lit_eq (Eq (V (I i)) (L v)) i' = (i = i')" |
"is_lit_eq _ _ = False"

lemma "(∃v. Eq (V (I i)) (L v) ∈ set G) = (∃g ∈ set G. is_lit_eq g i)"
by (metis is_lit_eq.elims(2) is_lit_eq.simps(1))

fun is_lit_eq_general :: "vname gexp ⇒ bool" where
"is_lit_eq_general (Eq (V (I _)) (L _)) = True" |
"is_lit_eq_general _ = False"

fun is_input_in :: "vname gexp ⇒ bool" where
"is_input_in (In (I i) s) = (s ≠ [])" |
"is_input_in _ = False"

definition "opposite_gob t1 t2 = (
(∀g ∈ set (Guards t1). is_lit_eq_general g ∨ is_input_in g) ∧
(∀g ∈ set (Guards t2). is_lit_eq_general g ∨ is_input_in g) ∧
(∃ i ∈ (enumerate_inputs t1 ∪ enumerate_inputs t2). (∃g ∈ set (Guards t1). is_lit_eq g i) ∧
(∀g ∈ set (Guards t2). ¬ gexp_constrains g (V (I i)))) ∧
Arity t1 = Arity t2 ∧
(∀i ∈ enumerate_inputs t2. i < Arity t2) ∧
(∀i ∈ enumerate_inputs t2. length (filter (λg. gexp_constrains g (V (I i))) (Guards t2)) ≤ 1))"

lemma "is_lit_eq_general g ∨ is_input_in g ⟹
∃i v s. g = Eq (V (I i)) (L v) ∨ g = In (I i) s ∧ s ≠ []"
by (meson is_input_in.elims(2) is_lit_eq_general.elims(2))

lemma opposite_gob_directly_subsumption:
"opposite_gob t1 t2 ⟹ ¬ subsumes t1 c t2"
apply (rule opposite_gob_subsumption)
unfolding opposite_gob_def
apply (meson is_input_in.elims(2) is_lit_eq_general.elims(2))+
apply (metis is_lit_eq.elims(2))
by auto

fun get_in :: "'a gexp ⇒ ('a × value list) option" where
"get_in (In v s) = Some (v, s)" |
"get_in _ = None"

lemma not_subset_not_in: "(¬ s1 ⊆ s2) = (∃i. i ∈ s1 ∧ i ∉ s2)"
by auto

lemma get_in_is: "(get_in x = Some (v, s1)) = (x = In v s1)"
by (induct x, auto)

lemma gval_rearrange:
"g ∈ set G ⟹
gval g s = true ⟹
apply_guards (removeAll g G) s ⟹
apply_guards G s"
proof(induct G)
case (Cons a G)
then show ?case
apply (simp only: apply_guards_cons)
apply standard
apply (metis apply_guards_cons removeAll.simps(2))
by (metis apply_guards_cons removeAll.simps(2) removeAll_id)
qed auto

lemma singleton_list: "(length l = 1) = (∃e. l = [e])"
by (induct l, auto)

lemma remove_restricted:
"g ∈ set G ⟹
gexp_constrains g (V v) ⟹
restricted_once v G ⟹
not_restricted v (removeAll g G)"
apply (simp add: restricted_once_def not_restricted_def singleton_list)
apply clarify
subgoal for e
apply (case_tac "e = g")
defer
apply (metis (no_types, lifting) DiffE Diff_insert_absorb Set.set_insert empty_set filter.simps(2) filter_append in_set_conv_decomp insert_iff list.set(2))
proof -
fix e :: "'a gexp"
assume "filter (λg. gexp_constrains g (V v)) G = [g]"
then have "{g ∈ set G. gexp_constrains g (V v)} = {g}"
by (metis (no_types) empty_set list.simps(15) set_filter)
then show "∀g∈set G - {g}. ¬ gexp_constrains g (V v)"
by blast
qed
done

lemma unrestricted_input_swap:
"not_restricted (I i) G ⟹
apply_guards G (join_ir iaa c) ⟹
apply_guards (removeAll g G) (join_ir (iaa[i := ia]) c)"
proof(induct G)
case (Cons a G)
then show ?case
apply safe
apply (meson neq_Nil_conv)
apply (metis input_not_constrained_gval_swap_inputs list.distinct(1))
by (metis list.distinct(1))
qed auto

lemma apply_guards_remove_restricted:
"g ∈ set G ⟹
gexp_constrains g (V (I i)) ⟹
restricted_once (I i) G ⟹
apply_guards G (join_ir iaa c) ⟹
apply_guards (removeAll g G) (join_ir (iaa[i := ia]) c)"
proof(induct G)
case (Cons a G)
then show ?case
apply simp
apply safe
apply (rule unrestricted_input_swap)
apply (meson apply_guards_subset set_subset_Cons)
apply (simp add: apply_guards_rearrange not_restricted_def restricted_once_def unrestricted_input_swap)
by (metis apply_guards_cons filter.simps(2) filter_empty_conv input_not_constrained_gval_swap_inputs list.inject restricted_once_def singleton_list)
qed auto

lemma In_swap_inputs:
"In (I i) s2 ∈ set G ⟹
restricted_once (I i) G ⟹
ia ∈ set s2 ⟹
apply_guards G (join_ir iaa c) ⟹
apply_guards G (join_ir (iaa[i := ia]) c)"
using apply_guards_remove_restricted[of "In (I i) s2" G i iaa c ia]
apply simp
apply (rule gval_rearrange[of "In (I i) s2"])
apply simp
apply (metis filter_empty_conv gval_each_one input_not_constrained_gval_swap_inputs length_0_conv not_restricted_def remove_restricted test_aux)
by blast

definition these :: "'a option list ⇒ 'a list" where
"these as = map (λx. case x of Some y ⇒ y) (filter (λx. x ≠ None) as)"

lemma these_cons: "these (a#as) = (case a of None ⇒ these as | Some x ⇒ x#(these as))"
apply (cases a)

definition get_ins :: "vname gexp list ⇒ (nat × value list) list" where
"get_ins g = map (λ(v, s). case v of I i ⇒ (i, s)) (filter (λ(v, _). case v of I _ ⇒ True | R _ ⇒ False) (these (map get_in g)))"

lemma in_get_ins:
"(I x1a, b) ∈ set (these (map get_in G)) ⟹
In (I x1a) b ∈ set G"
proof(induct G)
case Nil
then show ?case
next
case (Cons a G)
then show ?case
apply simp
apply (cases a)
by auto
qed

lemma restricted_head: "∀v. restricted_once v (Eq (V x2) (L x1) # G) ∨ not_restricted v (Eq (V x2) (L x1) # G) ⟹
not_restricted x2 G"
apply (erule_tac x=x2 in allE)

fun atomic :: "'a gexp ⇒ bool" where
"atomic (Eq (V _) (L _)) = True" |
"atomic (In _ _) = True" |
"atomic _ = False"

lemma restricted_max_once_cons: "∀v. restricted_once v (g#gs) ∨ not_restricted v (g#gs) ⟹
∀v. restricted_once v gs ∨ not_restricted v gs"
apply safe
subgoal for v
by (erule_tac x=v in allE)
(metis (mono_tags, lifting) list.distinct(1) list.inject singleton_list)
done

lemma not_restricted_swap_inputs:
"not_restricted (I x1a) G ⟹
apply_guards G (join_ir i r) ⟹
apply_guards G (join_ir (i[x1a := x1]) r)"
proof(induct G)
case (Cons a G)
then show ?case
`