Make equivalence work with new_channel

[jeltsch]

Currently, equivalence is not configured to perform rewriting under new_channel. The reason is that new_channel is not compatible with bisimilarity, but only create_channel is. For rewriting under new_channel, we use the method process_family_equivalence.

However, the next-generation equivalence reasoner permits the use of arbitrary equivalences as compatibility rules. This allows us to define compatibility rules that include the expression of new_channel in terms of create_channel alongside the actual compatibility of create_channel. With such rules in place, new_channel will be turned into create_channel on the fly during application of compatibility rules.

We shall perform the following activities:

• Add compatibility rules for new_channel, using the following in their proofs:
  • The expression of new_channel in terms of create_channel
  • The create_channel compatibility lemmas
• Add compatibility rules for tagged_new_channel and prove them using the compatibility rules for new_channel
• Add necessary assignments of the compatibility_simplification attribute to existing lemmas
• Turn all invocations of process_family_equivalence into invocations of equivalence
• Start using equivalence for the goal in Core_Bisimilarities for which we currently don’t use process_family_equivalence, since process_family_equivalence apparently broke as part of the switch to the next-generation equivalence reasoner

  thorn-calculus/src/Thorn_Calculus-Core_Bisimilarities.thy

  Lines 1073 to 1079 in d6daf3a

  	also have "\<dots> \<sim>\<^sub>s \<star>\<^bsup>n\<^esup> (Q \<guillemotleft> suffix n \<parallel> \<nu> a. \<Delta> T a)"
  	by
  	(blast intro:
  	parallel_right_scope_extension
  	synchronous.bisimilarity_symmetry_rule
  	create_channel_power_is_compatible_with_synchronous_bisimilarity
  	)

• Remove the definition of process_family_equivalence, including the definition of all auxiliary gadgets
  • deep_uncurry_after_parallel
  • deep_uncurry_after_create_channel
  • de_bruijn
  • process_family_uncurry_relation
  • process_family_uncurry_relation_bi_uniqueness
  • process_family_uncurry_relation_bi_totality
  • process_family_uncurry_relation_right_uniqueness
  • process_family_uncurry_relation_right_totality
  • process_family_uncurry_transfer
  • process_family_uncurry_elimination
  • wrapped_remove_adapted
  • process_family_equivalence
• Get rid of deep_uncurry_after_new_channel to avoid having it as a lone trivial lemma
  • Remove the definition of deep_uncurry_after_new_channel
  • Make the proof of new_channel_scope_extension cope without deep_uncurry_after_new_channel
• Remove everything related to wrapped_remove_adapted
  • The definition of wrapped_remove_adapted
  • wrapped_remove_adapted_is_compatible_with_synchronous_bisimilarity
  • The rule of compatibility of wrapped_remove_adapted with synchronous.bisimilarity
  • wrapped_remove_adapted_is_compatible_with_synchronous_weak_bisimilarity
  • The rule of compatibility of wrapped_remove_adapted with synchronous.weak.bisimilarity
  • The comment regarding compatibility lemmas of adapted

    thorn-calculus/src/Thorn_Calculus-Semantics-Synchronous.thy

    Lines 1794 to 1802 in d6daf3a

    	(*FIXME:
    	Make the following changes above and below:
    	\<^item> Add compatibility lemmas for \<open>\<guillemotleft> remove _\<close> and \<open>\<guillemotleft> move\<close>
    	\<^item> Remove the compatibility lemmas for \<open>wrapped_remove_adapted\<close> and instead use the compatibility
    	lemmas for \<open>\<guillemotleft> remove _\<close> and unfolding with \<open>wrapped_remove_adapted\<close> directly in the
    	\<^theory_text>\<open>lift_definition\<close> proofs
    	*)

• Remove the create_channel compatibility rules
• Remove everything related to tagged_create_channel
  • The definition of tagged_create_channel
  • The tagged_create_channel compatibility lemmas
  • The tagged_create_channel compatibility rules