theory Examples_CAMKES

lemma "\<not>wellformed_assembly broken_assembly" apply (unfold wellformed_assembly_def) apply (case_tac "wellformed_composition (composition broken_assembly)") apply (unfold broken_assembly_def) apply (frule wellformed_composition_is_nonempty) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> wellformed_assembly broken_assembly proof (prove)
goal (1 subgoal):
 1. \<not> (wellformed_composition (composition broken_assembly) \<and> (case configuration broken_assembly of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_configuration x)) proof (prove)
goal (2 subgoals):
 1. wellformed_composition (composition broken_assembly) \<Longrightarrow> \<not> (wellformed_composition (composition broken_assembly) \<and> (case configuration broken_assembly of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_configuration x))
 2. \<not> wellformed_composition (composition broken_assembly) \<Longrightarrow> \<not> (wellformed_composition (composition broken_assembly) \<and> (case configuration broken_assembly of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_configuration x)) proof (prove)
goal (2 subgoals):
 1. wellformed_composition (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>) \<Longrightarrow> \<not> (wellformed_composition (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>) \<and> (case configuration \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr> of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_configuration x))
 2. \<not> wellformed_composition (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>) \<Longrightarrow> \<not> (wellformed_composition (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>) \<and> (case configuration \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr> of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_configuration x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wellformed_composition (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>); components (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>) \<noteq> []\<rbrakk> \<Longrightarrow> \<not> (wellformed_composition (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>) \<and> (case configuration \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr> of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_configuration x))
 2. \<not> wellformed_composition (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>) \<Longrightarrow> \<not> (wellformed_composition (composition \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>) \<and> (case configuration \<lparr>composition = \<lparr>components = [], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr> of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_configuration x)) proof (prove)
goal:
No subgoals!