theory Bisim_UL

lemma bisim_noop_det_on:
  assumes a: "\<And>s. \<lbrace>Pa and (=) s\<rbrace> a \<lbrace>\<lambda>_. (=) s\<rbrace>"
  and     b: "\<And>s. \<lbrace>Pb and (=) s\<rbrace> b \<lbrace>\<lambda>_. (=) s\<rbrace>"
  and    da: "det_on P a"
  and    db: "det_on P' b"
  shows   "bisim_underlying sr dc (Pa and P) (Pb and P') a b" using da db apply - apply (rule bisim_underlyingI) apply clarsimp apply (erule (1) det_onE)+ apply (frule use_valid [OF _ a], fastforce) apply (frule use_valid [OF _ b], fastforce) apply fastforce apply clarsimp apply (erule (1) det_onE)+ apply (frule use_valid [OF _ a], fastforce) apply (frule use_valid [OF _ b], fastforce) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying sr dc (Pa and P) (Pb and P') a b proof (prove)
using this:
det_on P a
det_on P' b

goal (1 subgoal):
 1. bisim_underlying sr dc (Pa and P) (Pb and P') a b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det_on P a; det_on P' b\<rbrakk> \<Longrightarrow> bisim_underlying sr dc (Pa and P) (Pb and P') a b proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>det_on P a; det_on P' b; sr s s'; (Pa and P) s; (Pb and P') s'; (r, t) \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<in>fst (b s'). dc r r' \<and> sr t t'
 2. \<And>s s' r' t'. \<lbrakk>det_on P a; det_on P' b; sr s s'; (Pa and P) s; (Pb and P') s'; (r', t') \<in> fst (b s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). dc r r' \<and> sr t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>det_on P a; det_on P' b; sr s s'; (r, t) \<in> fst (a s); Pa s; P s; Pb s'; P' s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (b s'). case x of (r', t') \<Rightarrow> sr t t'
 2. \<And>s s' r' t'. \<lbrakk>det_on P a; det_on P' b; sr s s'; (Pa and P) s; (Pb and P') s'; (r', t') \<in> fst (b s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). dc r r' \<and> sr t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t ra s'a rb s'b. \<lbrakk>sr s s'; (r, t) \<in> fst (a s); Pa s; P s; Pb s'; P' s'; (ra, s'a) \<in> fst (a s); \<not> snd (a s); (rb, s'b) \<in> fst (b s'); \<not> snd (b s')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (b s'). case x of (r', t') \<Rightarrow> sr t t'
 2. \<And>s s' r' t'. \<lbrakk>det_on P a; det_on P' b; sr s s'; (Pa and P) s; (Pb and P') s'; (r', t') \<in> fst (b s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). dc r r' \<and> sr t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t ra s'a rb s'b. \<lbrakk>sr s s'; (r, t) \<in> fst (a s); Pa s; P s; Pb s'; P' s'; (ra, s'a) \<in> fst (a s); \<not> snd (a s); (rb, s'b) \<in> fst (b s'); \<not> snd (b s'); s = t\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (b s'). case x of (r', t') \<Rightarrow> sr t t'
 2. \<And>s s' r' t'. \<lbrakk>det_on P a; det_on P' b; sr s s'; (Pa and P) s; (Pb and P') s'; (r', t') \<in> fst (b s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). dc r r' \<and> sr t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t ra s'a rb s'b. \<lbrakk>sr s s'; (r, t) \<in> fst (a s); Pa s; P s; Pb s'; P' s'; (ra, s'a) \<in> fst (a s); \<not> snd (a s); (rb, s'b) \<in> fst (b s'); \<not> snd (b s'); s = t; s' = s'b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (b s'). case x of (r', t') \<Rightarrow> sr t t'
 2. \<And>s s' r' t'. \<lbrakk>det_on P a; det_on P' b; sr s s'; (Pa and P) s; (Pb and P') s'; (r', t') \<in> fst (b s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). dc r r' \<and> sr t t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>det_on P a; det_on P' b; sr s s'; (Pa and P) s; (Pb and P') s'; (r', t') \<in> fst (b s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). dc r r' \<and> sr t t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>det_on P a; det_on P' b; sr s s'; (r', t') \<in> fst (b s'); Pa s; P s; Pb s'; P' s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> sr t t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' r s'a ra s'b. \<lbrakk>sr s s'; (r', t') \<in> fst (b s'); Pa s; P s; Pb s'; P' s'; (r, s'a) \<in> fst (a s); \<not> snd (a s); (ra, s'b) \<in> fst (b s'); \<not> snd (b s')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> sr t t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' r s'a ra s'b. \<lbrakk>sr s s'; (r', t') \<in> fst (b s'); Pa s; P s; Pb s'; P' s'; (r, s'a) \<in> fst (a s); \<not> snd (a s); (ra, s'b) \<in> fst (b s'); \<not> snd (b s'); s = s'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> sr t t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' r s'a ra s'b. \<lbrakk>sr s s'; (r', t') \<in> fst (b s'); Pa s; P s; Pb s'; P' s'; (r, s'a) \<in> fst (a s); \<not> snd (a s); (ra, s'b) \<in> fst (b s'); \<not> snd (b s'); s = s'a; s' = t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> sr t t' proof (prove)
goal:
No subgoals!