theory Wellformed_CAMKES

lemma refs_valid_connection_ann:
  "refs_valid_connection conn component_list =
      (wellformed_connector (conn_type conn) \<and>
       (\<comment> \<open>Every to- and from-end of the component must exist.\<close>
        \<forall>(from_name, from_interface) \<in> set (conn_from conn).
          \<exists>1from \<in> component_list.
            fst from = from_name \<and>
            (\<forall>(to_name, to_interface) \<in> set (conn_to conn).
               \<exists>1to \<in> component_list.
                 fst to = to_name \<and>
                 \<comment> \<open>The following checks that the component interfaces have the correct type.\<close>
                 check_wellformed ((refs_valid_connection, ''interface''), (from_name, to_name))
                   (case connector_interface (conn_type conn) of
                       RPCInterface \<Rightarrow>      from_interface \<in> fst ` set (requires (snd from)) \<and>
                                            to_interface \<in> fst ` set (provides (snd to))
                     | EventInterface \<Rightarrow>    from_interface \<in> fst ` set (emits (snd from)) \<and>
                                            to_interface \<in> fst ` set (consumes (snd to))
                     \<comment> \<open>TODO: the check for memory connectors could be optimised; we don't need to
                               check all pairs of from- and to- for dataports with many subscribers.\<close>
                     | DataportInterface \<Rightarrow> from_interface \<in> fst ` set (dataports (snd from)) \<and>
                                            to_interface \<in> fst ` set (dataports (snd to))
                   )
                 \<and>
                 \<comment> \<open>Next, we check that the kind of components being connected are appropriate.\<close>
                 check_wellformed ((refs_valid_connection, ''component''), (from_name, to_name))
                   (case connector_type (conn_type conn) of
                       \<comment> \<open>Both endpoints must be regular components.\<close>
                       NativeConnector \<Rightarrow>  \<not> hardware (snd from) \<and> \<not> hardware (snd to)
                       \<comment> \<open>At least one endpoint must be a hardware component.
                           FIXME: might not be quite what we want.\<close>
                     | HardwareConnector \<Rightarrow> hardware (snd from) \<or> hardware (snd to)
                     | ExportConnector \<Rightarrow> undefined ''compound components not supported yet''
                   )
            )
     ))" by (simp only: refs_valid_connection_def remove_generic_tag simp_thms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. refs_valid_connection conn component_list = (wellformed_connector (conn_type conn) \<and> (\<forall>(from_name, from_interface)\<in>set (conn_from conn). \<exists>1 from\<in>component_list. fst from = from_name \<and> (\<forall>(to_name, to_interface)\<in>set (conn_to conn). \<exists>1 to\<in>component_list. fst to = to_name \<and> check_wellformed ((refs_valid_connection, ''interface''), from_name, to_name) (case connector_interface (conn_type conn) of RPCInterface \<Rightarrow> from_interface \<in> fst ` set (requires (snd from)) \<and> to_interface \<in> fst ` set (provides (snd to)) | EventInterface \<Rightarrow> from_interface \<in> fst ` set (emits (snd from)) \<and> to_interface \<in> fst ` set (consumes (snd to)) | DataportInterface \<Rightarrow> from_interface \<in> fst ` set (dataports (snd from)) \<and> to_interface \<in> fst ` set (dataports (snd to))) \<and> check_wellformed ((refs_valid_connection, ''component''), from_name, to_name) (case connector_type (conn_type conn) of NativeConnector \<Rightarrow> \<not> hardware (snd from) \<and> \<not> hardware (snd to) | HardwareConnector \<Rightarrow> hardware (snd from) \<or> hardware (snd to) | ExportConnector \<Rightarrow> undefined ''compound components not supported yet''))))