[STATEMENT]
lemma cdl_heap_add_assoc:
  "\<lbrakk>sep_state_disj x y; sep_state_disj y z; sep_state_disj x z\<rbrakk>
  \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z =
      cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_state_disj x y; sep_state_disj y z; sep_state_disj x z\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))
[PROOF STEP]
apply (clarsimp simp: sep_state_disj_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>All (not_conflicting_objects x y); All (not_conflicting_objects y z); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))
[PROOF STEP]
apply (cut_tac cdl_heap_add_assoc')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>All (not_conflicting_objects x y); All (not_conflicting_objects y z); All (not_conflicting_objects x z); cdl_heap_add (SepState (cdl_heap_add ?x1 ?y1) (cdl_ghost_state_add ?x1 ?y1)) ?z1 = cdl_heap_add ?x1 (SepState (cdl_heap_add ?y1 ?z1) (cdl_ghost_state_add ?y1 ?z1))\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))
 2. \<lbrakk>All (not_conflicting_objects x y); All (not_conflicting_objects y z); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> \<forall>obj_id. not_conflicting_objects ?x1 ?z1 obj_id \<and> not_conflicting_objects ?y1 ?z1 obj_id \<and> not_conflicting_objects ?x1 ?z1 obj_id
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>All (not_conflicting_objects x y); All (not_conflicting_objects y z); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> \<forall>obj_id. not_conflicting_objects x z obj_id \<and> not_conflicting_objects y z obj_id \<and> not_conflicting_objects x z obj_id
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cdl_ghost_state_add_assoc:
  "cdl_ghost_state_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z =
   cdl_ghost_state_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cdl_ghost_state_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_ghost_state_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. cdl_ghost_state_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z xa = cdl_ghost_state_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) xa
[PROOF STEP]
apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def Let_unfold)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clean_slots_map_add_comm:
  "cmps_a \<inter> cmps_b = {}
  \<Longrightarrow> clean_slots slots_a cmps_a ++ clean_slots slots_b cmps_b =
      clean_slots slots_b cmps_b ++ clean_slots slots_a cmps_a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmps_a \<inter> cmps_b = {} \<Longrightarrow> clean_slots slots_a cmps_a ++ clean_slots slots_b cmps_b = clean_slots slots_b cmps_b ++ clean_slots slots_a cmps_a
[PROOF STEP]
apply (clarsimp simp: clean_slots_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmps_a \<inter> cmps_b = {} \<Longrightarrow> slots_a |` the_set cmps_a ++ slots_b |` the_set cmps_b = slots_b |` the_set cmps_b ++ slots_a |` the_set cmps_a
[PROOF STEP]
apply (drule the_set_inter_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_set cmps_a \<inter> the_set cmps_b = {} \<Longrightarrow> slots_a |` the_set cmps_a ++ slots_b |` the_set cmps_b = slots_b |` the_set cmps_b ++ slots_a |` the_set cmps_a
[PROOF STEP]
apply (erule map_add_restrict_comm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma object_clean_all:
  "object_type obj_a = object_type obj_b \<Longrightarrow> object_clean obj_b {} = object_clean obj_a {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type obj_a = object_type obj_b \<Longrightarrow> object_clean obj_b {} = object_clean obj_a {}
[PROOF STEP]
apply (clarsimp simp: object_clean_def object_clean_slots_def clean_slots_def the_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type obj_a = object_type obj_b \<Longrightarrow> update_slots Map.empty (object_clean_fields obj_b {}) = update_slots Map.empty (object_clean_fields obj_a {})
[PROOF STEP]
apply (rule_tac cmps'1="{}" and obj'1="obj_a" in trans [OF update_slots_object_clean_fields], fastforce+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma object_add_comm:
  "\<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk>
  \<Longrightarrow> object_add obj_a obj_b cmps_a cmps_b = object_add obj_b obj_a cmps_b cmps_a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> object_add obj_a obj_b cmps_a cmps_b = object_add obj_b obj_a cmps_b cmps_a
[PROOF STEP]
apply (clarsimp simp: object_add_def Let_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> (None \<in> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)))) \<and> (None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))))
[PROOF STEP]
apply (rule conjI | clarsimp)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<in> cmps_b; None \<in> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<in> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))
 3. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<in> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)))
[PROOF STEP]
apply (rule conjI | clarsimp)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<in> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)))
[PROOF STEP]
apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; None \<in> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}; clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b = clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)))
[PROOF STEP]
apply (rule conjI | clarsimp)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<in> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))
[PROOF STEP]
apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; None \<notin> cmps_b; None \<in> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}; clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b = clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))
[PROOF STEP]
apply (rule conjI | clarsimp)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a = {}; cmps_b = {}\<rbrakk> \<Longrightarrow> object_clean obj_b {} = object_clean obj_a {}
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<notin> cmps_a\<rbrakk> \<Longrightarrow> cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
[PROOF STEP]
apply (erule object_clean_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<notin> cmps_a\<rbrakk> \<Longrightarrow> cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
[PROOF STEP]
apply (rule_tac cmps'1=cmps_b and obj'1=obj_b in trans [OF update_slots_object_clean], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
[PROOF STEP]
apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; None \<notin> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}; clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b = clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sep_state_add_comm:
  "sep_state_disj x y \<Longrightarrow> sep_state_add x y = sep_state_add y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sep_state_disj x y \<Longrightarrow> sep_state_add x y = sep_state_add y x
[PROOF STEP]
apply (clarsimp simp: sep_state_add_def sep_state_disj_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. All (not_conflicting_objects x y) \<Longrightarrow> cdl_heap_add x y = cdl_heap_add y x \<and> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. All (not_conflicting_objects x y) \<Longrightarrow> cdl_heap_add x y = cdl_heap_add y x
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (case_tac x, case_tac y, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>All (not_conflicting_objects (SepState x1 x2) (SepState x1a x2a)); x = SepState x1 x2; y = SepState x1a x2a\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState x1 x2) (SepState x1a x2a) = cdl_heap_add (SepState x1a x2a) (SepState x1 x2)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (rename_tac heap_a gs_a heap_b gs_b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState heap_a gs_a) (SepState heap_b gs_b) = cdl_heap_add (SepState heap_b gs_b) (SepState heap_a gs_a)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (clarsimp simp: cdl_heap_add_def Let_unfold)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b\<rbrakk> \<Longrightarrow> (\<lambda>obj_id. case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id))) = (\<lambda>obj_id. case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_b \<Rightarrow> case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_b obj_id) (gs_a obj_id)))
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b\<rbrakk> \<Longrightarrow> (case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id))) = (case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_b \<Rightarrow> case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_b obj_id) (gs_a obj_id)))
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (case_tac "heap_a obj_id")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = None\<rbrakk> \<Longrightarrow> (case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id))) = (case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_b \<Rightarrow> case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_b obj_id) (gs_a obj_id)))
 2. \<And>heap_a gs_a heap_b gs_b obj_id a. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some a\<rbrakk> \<Longrightarrow> (case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id))) = (case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_b \<Rightarrow> case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_b obj_id) (gs_a obj_id)))
 3. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (case_tac "heap_b obj_id", simp_all add: slots_of_heap_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id a. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some a\<rbrakk> \<Longrightarrow> (case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_b \<Rightarrow> case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id))) = (case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a a (gs_b obj_id) (gs_a obj_id)))
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (case_tac "heap_b obj_id", simp_all add: slots_of_heap_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id a aa. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some a; heap_b obj_id = Some aa\<rbrakk> \<Longrightarrow> object_add a aa (gs_a obj_id) (gs_b obj_id) = object_add aa a (gs_b obj_id) (gs_a obj_id)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (rename_tac obj_a obj_b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b\<rbrakk> \<Longrightarrow> object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id) = object_add obj_b obj_a (gs_b obj_id) (gs_a obj_id)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (erule_tac x=obj_id in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b; not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b) obj_id\<rbrakk> \<Longrightarrow> object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id) = object_add obj_b obj_a (gs_b obj_id) (gs_a obj_id)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (rule object_add_comm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b; not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b) obj_id\<rbrakk> \<Longrightarrow> object_type obj_a = object_type obj_b
 2. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b; not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b) obj_id\<rbrakk> \<Longrightarrow> gs_a obj_id \<inter> gs_b obj_id = {}
 3. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (clarsimp simp: not_conflicting_objects_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b; not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b) obj_id\<rbrakk> \<Longrightarrow> gs_a obj_id \<inter> gs_b obj_id = {}
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (clarsimp simp: not_conflicting_objects_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x
[PROOF STEP]
apply (rule ext, fastforce simp: cdl_ghost_state_add_def Let_unfold Un_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma add_to_slots_comm:
  "\<lbrakk>object_slots y_obj \<bottom> object_slots z_obj; update_slots Map.empty y_obj = update_slots Map.empty z_obj \<rbrakk>
  \<Longrightarrow> add_to_slots (object_slots z_obj) y_obj = add_to_slots (object_slots y_obj) z_obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_slots y_obj \<bottom> object_slots z_obj; update_slots Map.empty y_obj = update_slots Map.empty z_obj\<rbrakk> \<Longrightarrow> Abstract_Separation_D.add_to_slots (object_slots z_obj) y_obj = Abstract_Separation_D.add_to_slots (object_slots y_obj) z_obj
[PROOF STEP]
by (fastforce simp: add_to_slots_def update_slots_def object_slots_def
                     cdl_tcb.splits cdl_cnode.splits
              dest!: map_add_com
              split: cdl_object.splits)


[STATEMENT]
lemma cdl_heap_add_none1:
  "cdl_heap_add x y obj_id = None \<Longrightarrow> (sep_heap x) obj_id = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cdl_heap_add x y obj_id = None \<Longrightarrow> sep_heap x obj_id = None
[PROOF STEP]
by (clarsimp simp: cdl_heap_add_def Let_unfold split:option.splits if_split_asm)


[STATEMENT]
lemma cdl_heap_add_none2:
  "cdl_heap_add x y obj_id = None \<Longrightarrow> (sep_heap y) obj_id = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cdl_heap_add x y obj_id = None \<Longrightarrow> sep_heap y obj_id = None
[PROOF STEP]
by (clarsimp simp: cdl_heap_add_def Let_unfold split:option.splits if_split_asm)


[STATEMENT]
lemma object_type_object_addL:
  "object_type obj = object_type obj'
  \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type obj = object_type obj' \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj
[PROOF STEP]
by (clarsimp simp: object_add_def Let_unfold)


[STATEMENT]
lemma object_type_object_addR:
  "object_type obj = object_type obj'
  \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type obj = object_type obj' \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj'
[PROOF STEP]
by (clarsimp simp: object_add_def Let_unfold)


[STATEMENT]
lemma sep_state_add_disjL:
  "\<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x y
[PROOF STEP]
apply (clarsimp simp: sep_state_disj_def sep_state_add_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)))\<rbrakk> \<Longrightarrow> not_conflicting_objects x y xa
[PROOF STEP]
apply (rename_tac obj_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)))\<rbrakk> \<Longrightarrow> not_conflicting_objects x y obj_id
[PROOF STEP]
apply (clarsimp simp: not_conflicting_objects_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>\<forall>obj_id. case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<forall>obj_id. case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap y obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state y obj_id = {}
[PROOF STEP]
apply (erule_tac x=obj_id in allE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap y obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state y obj_id = {}
[PROOF STEP]
apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR
                 split: option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sep_state_add_disjR:
  "\<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x z
[PROOF STEP]
apply (clarsimp simp: sep_state_disj_def sep_state_add_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)))\<rbrakk> \<Longrightarrow> not_conflicting_objects x z xa
[PROOF STEP]
apply (rename_tac obj_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)))\<rbrakk> \<Longrightarrow> not_conflicting_objects x z obj_id
[PROOF STEP]
apply (clarsimp simp: not_conflicting_objects_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>\<forall>obj_id. case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<forall>obj_id. case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}
[PROOF STEP]
apply (erule_tac x=obj_id in allE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}
[PROOF STEP]
apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR
                 split: option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sep_state_add_disj:
  "\<lbrakk>sep_state_disj y z; sep_state_disj x y; sep_state_disj x z\<rbrakk> \<Longrightarrow> sep_state_disj x (sep_state_add y z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_state_disj y z; sep_state_disj x y; sep_state_disj x z\<rbrakk> \<Longrightarrow> sep_state_disj x (sep_state_add y z)
[PROOF STEP]
apply (clarsimp simp: sep_state_disj_def sep_state_add_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x y); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) xa
[PROOF STEP]
apply (rename_tac obj_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x y); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) obj_id
[PROOF STEP]
apply (clarsimp simp: not_conflicting_objects_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>\<forall>obj_id. case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<forall>obj_id. case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap y obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state y obj_id = {}; \<forall>obj_id. case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}
[PROOF STEP]
apply (erule_tac x=obj_id in allE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap y obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state y obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {}
[PROOF STEP]
apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR
                 split: option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cancel_left_a: "b l\<rightarrow> (a * b) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b l\<rightarrow> a * b = a
[PROOF STEP]
apply (rule_tac a = b in mult_cancel_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b l\<rightarrow> a * b) * b = a * b
[PROOF STEP]
apply (subst inf_l_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> (a * b) = a * b
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> (a * b) \<le> a * b
 2. a * b \<le> b \<sqinter> (a * b)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma cancel_right_a: "b r\<rightarrow> (b * a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b r\<rightarrow> b * a = a
[PROOF STEP]
apply (rule_tac a = b in mult_cancel_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * (b r\<rightarrow> b * a) = b * a
[PROOF STEP]
apply (subst inf_r_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> (b * a) = b * a
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> (b * a) \<le> b * a
 2. b * a \<le> b \<sqinter> (b * a)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma lemma_4_2_i: "a l\<rightarrow> b = (a * c) l\<rightarrow> (b * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> b = a * c l\<rightarrow> b * c
[PROOF STEP]
apply (subgoal_tac "a l\<rightarrow> b = a l\<rightarrow> (c l\<rightarrow> (b * c)) \<and> a l\<rightarrow> (c l\<rightarrow> (b * c)) = (a * c) l\<rightarrow> (b * c)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a l\<rightarrow> b = a l\<rightarrow> c l\<rightarrow> b * c \<and> a l\<rightarrow> c l\<rightarrow> b * c = a * c l\<rightarrow> b * c \<Longrightarrow> a l\<rightarrow> b = a * c l\<rightarrow> b * c
 2. a l\<rightarrow> b = a l\<rightarrow> c l\<rightarrow> b * c \<and> a l\<rightarrow> c l\<rightarrow> b * c = a * c l\<rightarrow> b * c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> b = a l\<rightarrow> c l\<rightarrow> b * c \<and> a l\<rightarrow> c l\<rightarrow> b * c = a * c l\<rightarrow> b * c
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a l\<rightarrow> b = a l\<rightarrow> c l\<rightarrow> b * c
 2. a l\<rightarrow> c l\<rightarrow> b * c = a * c l\<rightarrow> b * c
[PROOF STEP]
apply (simp add: cancel_left_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> c l\<rightarrow> b * c = a * c l\<rightarrow> b * c
[PROOF STEP]
by (simp add: left_impl_ded)


[STATEMENT]
lemma lemma_4_2_ii: "a r\<rightarrow> b = (c * a) r\<rightarrow> (c * b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a r\<rightarrow> b = c * a r\<rightarrow> c * b
[PROOF STEP]
apply (subgoal_tac "a r\<rightarrow> b = a r\<rightarrow> (c r\<rightarrow> (c * b)) \<and> a r\<rightarrow> (c r\<rightarrow> (c * b)) = (c * a) r\<rightarrow> (c * b)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a r\<rightarrow> b = a r\<rightarrow> c r\<rightarrow> c * b \<and> a r\<rightarrow> c r\<rightarrow> c * b = c * a r\<rightarrow> c * b \<Longrightarrow> a r\<rightarrow> b = c * a r\<rightarrow> c * b
 2. a r\<rightarrow> b = a r\<rightarrow> c r\<rightarrow> c * b \<and> a r\<rightarrow> c r\<rightarrow> c * b = c * a r\<rightarrow> c * b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a r\<rightarrow> b = a r\<rightarrow> c r\<rightarrow> c * b \<and> a r\<rightarrow> c r\<rightarrow> c * b = c * a r\<rightarrow> c * b
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a r\<rightarrow> b = a r\<rightarrow> c r\<rightarrow> c * b
 2. a r\<rightarrow> c r\<rightarrow> c * b = c * a r\<rightarrow> c * b
[PROOF STEP]
apply (simp add: cancel_right_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a r\<rightarrow> c r\<rightarrow> c * b = c * a r\<rightarrow> c * b
[PROOF STEP]
by (simp add: right_impl_ded)


[STATEMENT]
lemma lemma_4_2_iii: "(a * c \<le> b * c) = (a \<le> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * c \<le> b * c) = (a \<le> b)
[PROOF STEP]
by (simp add: left_lesseq lemma_4_2_i [THEN sym])


[STATEMENT]
lemma lemma_4_2_iv: "(c * a \<le> c * b) = (a \<le> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c * a \<le> c * b) = (a \<le> b)
[PROOF STEP]
by (simp add: right_lesseq lemma_4_2_ii [THEN sym])


[STATEMENT]
lemma lemma_4_3_i_a: "a \<squnion>1 b = (a l\<rightarrow> b) r\<rightarrow> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>1 b = (a l\<rightarrow> b) r\<rightarrow> b
[PROOF STEP]
by (simp add: sup1_def wajsberg1)


[STATEMENT]
lemma lemma_4_3_ii_a: "a \<squnion>2 b = (a r\<rightarrow> b) l\<rightarrow> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>2 b = (a r\<rightarrow> b) l\<rightarrow> b
[PROOF STEP]
by (simp add: sup2_def wajsberg2)


[STATEMENT]
lemma lemma_4_3_ii_b: "a \<squnion>2 b = (b r\<rightarrow> a) l\<rightarrow> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>2 b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
by (simp add: sup2_def wajsberg2)


[STATEMENT]
lemma (in wajsberg_pseudo_hoop_algebra) sup1_eq_sup2: "(\<squnion>1) = (\<squnion>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<squnion>1) = (\<squnion>2)
[PROOF STEP]
apply (simp add: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. x \<squnion>1 xa = x \<squnion>2 xa
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. x \<squnion>1 xa = x \<squnion>2 xa
[PROOF STEP]
apply (cut_tac a = x and b = xa in lattice1.supremum_pair)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. supremum {x, xa} = {x \<squnion>1 xa} \<Longrightarrow> x \<squnion>1 xa = x \<squnion>2 xa
[PROOF STEP]
apply (cut_tac a = x and b = xa in lattice2.supremum_pair)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>supremum {x, xa} = {x \<squnion>1 xa}; supremum {x, xa} = {x \<squnion>2 xa}\<rbrakk> \<Longrightarrow> x \<squnion>1 xa = x \<squnion>2 xa
[PROOF STEP]
by blast


[STATEMENT]
lemma [simp]: "0 l\<rightarrow> a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) l\<rightarrow> a = (1::'a)
[PROOF STEP]
by (simp add: order [THEN sym])


[STATEMENT]
lemma [simp]: "0 r\<rightarrow> a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) r\<rightarrow> a = (1::'a)
[PROOF STEP]
by (simp add: order_r [THEN sym])


[STATEMENT]
lemma "class.bounded_wajsberg_pseudo_hoop_algebra mult inf_a (l\<rightarrow>) (\<le>) (<) 1 (r\<rightarrow>) (0::'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.bounded_wajsberg_pseudo_hoop_algebra mult inf_a (l\<rightarrow>) (\<le>) (<) (1::'a) (r\<rightarrow>) (0::'a)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>a b. inf_a a b = mult (a l\<rightarrow> b) a
 2. \<And>a b. (a < b) = (a \<le> b \<and> \<not> b \<le> a)
 3. \<And>a. mult (1::'a) a = a
 4. \<And>a. mult a (1::'a) = a
 5. \<And>a. a l\<rightarrow> a = (1::'a)
 6. \<And>a b. mult (a l\<rightarrow> b) a = mult (b l\<rightarrow> a) b
 7. \<And>a b c. mult a b l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
 8. \<And>a b. (a \<le> b) = (a l\<rightarrow> b = (1::'a))
 9. \<And>a b. inf_a a b = mult a (a r\<rightarrow> b)
 10. \<And>a. a r\<rightarrow> a = (1::'a)
A total of 16 subgoals...
[PROOF STEP]
apply (simp add: inf_a_def mult_def W6)
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>a b. (a < b) = (a \<le> b \<and> \<not> b \<le> a)
 2. \<And>a. mult (1::'a) a = a
 3. \<And>a. mult a (1::'a) = a
 4. \<And>a. a l\<rightarrow> a = (1::'a)
 5. \<And>a b. mult (a l\<rightarrow> b) a = mult (b l\<rightarrow> a) b
 6. \<And>a b c. mult a b l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
 7. \<And>a b. (a \<le> b) = (a l\<rightarrow> b = (1::'a))
 8. \<And>a b. inf_a a b = mult a (a r\<rightarrow> b)
 9. \<And>a. a r\<rightarrow> a = (1::'a)
 10. \<And>a b. mult a (a r\<rightarrow> b) = mult b (b r\<rightarrow> a)
A total of 15 subgoals...
[PROOF STEP]
apply (simp add: strict)
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>a. mult (1::'a) a = a
 2. \<And>a. mult a (1::'a) = a
 3. \<And>a. a l\<rightarrow> a = (1::'a)
 4. \<And>a b. mult (a l\<rightarrow> b) a = mult (b l\<rightarrow> a) b
 5. \<And>a b c. mult a b l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
 6. \<And>a b. (a \<le> b) = (a l\<rightarrow> b = (1::'a))
 7. \<And>a b. inf_a a b = mult a (a r\<rightarrow> b)
 8. \<And>a. a r\<rightarrow> a = (1::'a)
 9. \<And>a b. mult a (a r\<rightarrow> b) = mult b (b r\<rightarrow> a)
 10. \<And>a b c. mult a b r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
A total of 14 subgoals...
[PROOF STEP]
apply (simp_all add: mult_def order_l strict)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a. -r (a l\<rightarrow> -l (1::'a)) = a
 2. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r ((b l\<rightarrow> a) l\<rightarrow> -l b)
 3. \<And>a b c. -r (a l\<rightarrow> -l b) l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
 4. \<And>a b. inf_a a b = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 5. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 6. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 7. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 8. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 9. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: zero_def [THEN sym] C3_a)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r ((b l\<rightarrow> a) l\<rightarrow> -l b)
 2. \<And>a b c. -r (a l\<rightarrow> -l b) l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
 3. \<And>a b. inf_a a b = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 4. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 5. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 6. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 7. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 8. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: W6 inf_a_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a b. inf_a a b = inf_a b a
 2. \<And>a b c. -r (a l\<rightarrow> -l b) l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
 3. \<And>a b. inf_a a b = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 4. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 5. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 6. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 7. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 8. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a b. inf_a a b \<le> inf_a b a
 2. \<And>a b. inf_a b a \<le> inf_a a b
 3. \<And>a b c. -r (a l\<rightarrow> -l b) l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
 4. \<And>a b. inf_a a b = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 5. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 6. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 7. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 8. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 9. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a b c. -r (a l\<rightarrow> -l b) l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
 2. \<And>a b. inf_a a b = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 3. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 4. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 5. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 6. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 7. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: C6 P9 [THEN sym] C5_b)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. inf_a a b = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 2. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 3. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 4. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 5. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 6. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: inf_b_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. inf_a a b = inf_b b a
 2. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 3. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 4. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 5. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 6. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a b. inf_a a b \<le> inf_b b a
 2. \<And>a b. inf_b b a \<le> inf_a a b
 3. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 4. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 5. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 6. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 7. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. -r (a l\<rightarrow> -l (a r\<rightarrow> b)) = -r (b l\<rightarrow> -l (b r\<rightarrow> a))
 2. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 3. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 4. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 5. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: inf_b_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. inf_b b a = inf_b a b
 2. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 3. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 4. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 5. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. inf_b b a \<le> inf_b a b
 2. \<And>a b. inf_b a b \<le> inf_b b a
 3. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 4. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 5. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 6. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. -r (a l\<rightarrow> -l b) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 2. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 3. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 4. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: W6)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. -l (b r\<rightarrow> -r a) r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
 2. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 3. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 4. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: C6 [THEN sym])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. -r c l\<rightarrow> b r\<rightarrow> -r a = b r\<rightarrow> a r\<rightarrow> c
 2. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 3. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 4. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: P9 C5_a)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = -r (a l\<rightarrow> -l (a r\<rightarrow> b))
 2. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 3. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: inf_b_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. -r ((a l\<rightarrow> b) l\<rightarrow> -l a) = inf_b b a
 2. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 3. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: W6 inf_a_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. inf_a a b = inf_b b a
 2. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 3. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. inf_a a b \<le> inf_b b a
 2. \<And>a b. inf_b b a \<le> inf_a a b
 3. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 4. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a l\<rightarrow> b) r\<rightarrow> b = (b l\<rightarrow> a) r\<rightarrow> a
 2. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: W2a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a r\<rightarrow> b) l\<rightarrow> b = (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
by (simp add: W2c)


[STATEMENT]
lemma lemma_4_5_i: "(a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (cut_tac a = a and b = b and c = "(a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)" in B1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (subgoal_tac "(a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = 1 \<and> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) = 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a); (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a) \<and> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a) \<and> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a); (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a); (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a) \<and> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (1::'a) \<le> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a) \<and> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (1::'a) \<le> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> (1::'a)
 2. (1::'a) \<le> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (1::'a) \<le> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)
 3. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a) \<and> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (1::'a) \<le> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (1::'a) \<le> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a) \<and> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a) \<and> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (subst left_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> a l\<rightarrow> b \<le> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (subst left_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)) l\<rightarrow> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) \<Longrightarrow> b l\<rightarrow> a \<le> (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a)
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_5_ii: "(a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (cut_tac a = a and b = b and c = "(a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)" in B2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (subgoal_tac "(a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = 1 \<and> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) = 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a); (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a) \<and> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a) \<and> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a); (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a); (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a) \<and> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (1::'a) \<le> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a) \<and> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (1::'a) \<le> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> (1::'a)
 2. (1::'a) \<le> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (1::'a) \<le> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)
 3. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a) \<and> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (1::'a) \<le> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (1::'a) \<le> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a) \<and> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a) \<and> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (subst right_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> a r\<rightarrow> b \<le> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a)
[PROOF STEP]
apply (subst right_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)) r\<rightarrow> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) \<Longrightarrow> b r\<rightarrow> a \<le> (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a)
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_5_iii: "a l\<rightarrow> b = (a \<squnion>1 b) l\<rightarrow> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> b = a \<squnion>1 b l\<rightarrow> b
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a l\<rightarrow> b \<le> a \<squnion>1 b l\<rightarrow> b
 2. a \<squnion>1 b l\<rightarrow> b \<le> a l\<rightarrow> b
[PROOF STEP]
apply (rule_tac y = "((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> b" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a l\<rightarrow> b \<le> ((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> b
 2. ((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> b \<le> a \<squnion>1 b l\<rightarrow> b
 3. a \<squnion>1 b l\<rightarrow> b \<le> a l\<rightarrow> b
[PROOF STEP]
apply (rule lemma_2_10_26)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> b \<le> a \<squnion>1 b l\<rightarrow> b
 2. a \<squnion>1 b l\<rightarrow> b \<le> a l\<rightarrow> b
[PROOF STEP]
apply (rule lemma_2_5_13_a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>1 b \<le> (a l\<rightarrow> b) r\<rightarrow> b
 2. a \<squnion>1 b l\<rightarrow> b \<le> a l\<rightarrow> b
[PROOF STEP]
apply (simp add: sup1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>1 b l\<rightarrow> b \<le> a l\<rightarrow> b
[PROOF STEP]
apply (rule lemma_2_5_13_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> a \<squnion>1 b
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_5_iv: "a r\<rightarrow> b = (a \<squnion>2 b) r\<rightarrow> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a r\<rightarrow> b = a \<squnion>2 b r\<rightarrow> b
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a r\<rightarrow> b \<le> a \<squnion>2 b r\<rightarrow> b
 2. a \<squnion>2 b r\<rightarrow> b \<le> a r\<rightarrow> b
[PROOF STEP]
apply (rule_tac y = "((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> b" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a r\<rightarrow> b \<le> ((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> b
 2. ((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> b \<le> a \<squnion>2 b r\<rightarrow> b
 3. a \<squnion>2 b r\<rightarrow> b \<le> a r\<rightarrow> b
[PROOF STEP]
apply (rule lemma_2_10_24)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> b \<le> a \<squnion>2 b r\<rightarrow> b
 2. a \<squnion>2 b r\<rightarrow> b \<le> a r\<rightarrow> b
[PROOF STEP]
apply (rule lemma_2_5_13_b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b \<le> (a r\<rightarrow> b) l\<rightarrow> b
 2. a \<squnion>2 b r\<rightarrow> b \<le> a r\<rightarrow> b
[PROOF STEP]
apply (simp add: sup2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>2 b r\<rightarrow> b \<le> a r\<rightarrow> b
[PROOF STEP]
apply (rule lemma_2_5_13_b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> a \<squnion>2 b
[PROOF STEP]
by simp