theory Examples_CAMKES

lemma "\<not> wellformed_assembly broken_assembly" apply (unfold wellformed_assembly_def) apply (subst de_Morgan_conj) apply (rule disjI1) apply (unfold wellformed_composition_def broken_assembly_def, simp) apply (unfold refs_valid_composition_def
                refs_valid_components_def
                refs_valid_procedures_def
                x_def ex_one_def) apply fastforce 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 (1 subgoal):
 1. \<not> wellformed_composition (composition broken_assembly) \<or> \<not> (case configuration broken_assembly of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_configuration x) proof (prove)
goal (1 subgoal):
 1. \<not> wellformed_composition (composition broken_assembly) proof (prove)
goal (1 subgoal):
 1. refs_valid_composition \<lparr>components = [(undefined, x)], connections = [], group_labels = undefined\<rparr> \<longrightarrow> control x \<longrightarrow> (\<exists>x\<in>set undefined. \<not> (case x of (comp, group) \<Rightarrow> comp = undefined)) \<or> \<not> wellformed_component x proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set (components \<lparr>components = [(undefined, \<lparr>control = undefined, hardware = undefined, requires = [(undefined, InterfaceRequired, [undefined])], provides = undefined, dataports = undefined, emits = undefined, consumes = undefined, attributes = undefined\<rparr>)], connections = [], group_labels = undefined\<rparr>). \<forall>(name, req, proc)\<in>set (requires (snd x)). req = InterfaceRequired \<longrightarrow> proc \<noteq> [] \<longrightarrow> length (filter (\<lambda>z. z = (fst x, name)) (concat (map (\<lambda>y. conn_from (snd y)) (connections \<lparr>components = [(undefined, \<lparr>control = undefined, hardware = undefined, requires = [(undefined, InterfaceRequired, [undefined])], provides = undefined, dataports = undefined, emits = undefined, consumes = undefined, attributes = undefined\<rparr>)], connections = [], group_labels = undefined\<rparr>)))) = 1) \<and> refs_valid_connections (connections \<lparr>components = [(undefined, \<lparr>control = undefined, hardware = undefined, requires = [(undefined, InterfaceRequired, [undefined])], provides = undefined, dataports = undefined, emits = undefined, consumes = undefined, attributes = undefined\<rparr>)], connections = [], group_labels = undefined\<rparr>) (components \<lparr>components = [(undefined, \<lparr>control = undefined, hardware = undefined, requires = [(undefined, InterfaceRequired, [undefined])], provides = undefined, dataports = undefined, emits = undefined, consumes = undefined, attributes = undefined\<rparr>)], connections = [], group_labels = undefined\<rparr>) \<longrightarrow> control \<lparr>control = undefined, hardware = undefined, requires = [(undefined, InterfaceRequired, [undefined])], provides = undefined, dataports = undefined, emits = undefined, consumes = undefined, attributes = undefined\<rparr> \<longrightarrow> (\<exists>x\<in>set undefined. \<not> (case x of (comp, group) \<Rightarrow> comp = undefined)) \<or> \<not> wellformed_component \<lparr>control = undefined, hardware = undefined, requires = [(undefined, InterfaceRequired, [undefined])], provides = undefined, dataports = undefined, emits = undefined, consumes = undefined, attributes = undefined\<rparr> proof (prove)
goal:
No subgoals!