theory SubMonadLib

lemma corres_submonad:
  "\<lbrakk> submonad f r g fn; submonad f' r' g' fn';
     \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr;
     \<forall>s s' ss ss'. ((s, s') \<in> sr \<and> (ss, ss') \<in> ssr) \<longrightarrow> (r ss s, r' ss' s') \<in> sr;
     corres_underlying ssr False nf' rvr \<top> \<top> x x'\<rbrakk>
   \<Longrightarrow> corres_underlying sr False nf' rvr g g' (fn x) (fn' x')" apply (subst submonad.fn_is_sm, assumption)+ apply (clarsimp simp: submonad_fn_def) apply (rule corres_underlying_split [OF _ _ stateAssert_sp stateAssert_sp]) apply (fastforce simp: corres_underlying_def stateAssert_def get_def
                         assert_def return_def bind_def) apply (rule corres_underlying_split [where r'="\<lambda>x y. (x, y) \<in> ssr",
                             OF _ _ hoare_post_taut hoare_post_taut]) apply clarsimp apply (rule corres_underlying_split [where r'="\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr",
                             OF _ _ hoare_post_taut hoare_post_taut]) defer apply clarsimp apply (rule corres_underlying_split [where r'=dc, OF _ _ hoare_post_taut hoare_post_taut]) apply (simp add: corres_modify') apply clarsimp apply (rule corres_select_f_stronger) apply (clarsimp simp: corres_underlying_def) apply (drule (1) bspec, clarsimp) apply (drule (1) bspec, simp) apply blast apply (clarsimp simp: corres_underlying_def) apply (drule (1) bspec, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr g g' (fn x) (fn' x') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr g g' (submonad_fn f r g x) (submonad_fn f' r' g' x') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr g g' (do y <- stateAssert g [];
substate <- gets f;
(rv, substate') <- select_f (x substate);
y <- modify (r substate');
return rv
od) (do y <- stateAssert g' [];
substate <- gets f';
(rv, substate') <- select_f (x' substate);
y <- modify (r' substate');
return rv
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' ?r'2 g g' (stateAssert g []) (stateAssert g' [])
 2. \<And>y ya. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; ?r'2 y ya\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (g and g) (g' and g') (do substate <- gets f;
(rv, substate') <- select_f (x substate);
y <- modify (r substate');
return rv
od) (do substate <- gets f';
(rv, substate') <- select_f (x' substate);
y <- modify (r' substate');
return rv
od) proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (g and g) (g' and g') (do substate <- gets f;
(rv, substate') <- select_f (x substate);
y <- modify (r substate');
return rv
od) (do substate <- gets f';
(rv, substate') <- select_f (x' substate);
y <- modify (r' substate');
return rv
od) proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' (\<lambda>x y. (x, y) \<in> ssr) (g and g) (g' and g') (gets f) (gets f')
 2. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) (do (rv, substate') <- select_f (x substate);
y <- modify (r substate');
return rv
od) (do (rv, substate') <- select_f (x' substatea);
y <- modify (r' substate');
return rv
od) proof (prove)
goal (1 subgoal):
 1. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) (do (rv, substate') <- select_f (x substate);
y <- modify (r substate');
return rv
od) (do (rv, substate') <- select_f (x' substatea);
y <- modify (r' substate');
return rv
od) proof (prove)
goal (2 subgoals):
 1. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (\<lambda>_. True) (\<lambda>_. True) (select_f (x substate)) (select_f (x' substatea))
 2. \<And>y ya substate substatea rv rv'. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr; (case rv of (x, x') \<Rightarrow> \<lambda>(y, y'). rvr x y \<and> (x', y') \<in> ssr) rv'\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) (case rv of (rv, substate') \<Rightarrow> do y <- modify (r substate');
return rv
od) (case rv' of (rv, substate') \<Rightarrow> do y <- modify (r' substate');
return rv
od) proof (prove)
goal (2 subgoals):
 1. \<And>y ya substate substatea rv rv'. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr; (case rv of (x, x') \<Rightarrow> \<lambda>(y, y'). rvr x y \<and> (x', y') \<in> ssr) rv'\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) (case rv of (rv, substate') \<Rightarrow> do y <- modify (r substate');
return rv
od) (case rv' of (rv, substate') \<Rightarrow> do y <- modify (r' substate');
return rv
od)
 2. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (\<lambda>_. True) (\<lambda>_. True) (select_f (x substate)) (select_f (x' substatea)) proof (prove)
goal (2 subgoals):
 1. \<And>substate substatea a b aa ba. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; (substate, substatea) \<in> ssr; rvr a aa; (b, ba) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) (do y <- modify (r b);
return a
od) (do y <- modify (r' ba);
return aa
od)
 2. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (\<lambda>_. True) (\<lambda>_. True) (select_f (x substate)) (select_f (x' substatea)) proof (prove)
goal (3 subgoals):
 1. \<And>substate substatea a b aa ba. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; (substate, substatea) \<in> ssr; rvr a aa; (b, ba) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' dc (\<lambda>_. True) (\<lambda>_. True) (modify (r b)) (modify (r' ba))
 2. \<And>substate substatea a b aa ba y ya. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; (substate, substatea) \<in> ssr; rvr a aa; (b, ba) \<in> ssr; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) (return a) (return aa)
 3. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (\<lambda>_. True) (\<lambda>_. True) (select_f (x substate)) (select_f (x' substatea)) proof (prove)
goal (2 subgoals):
 1. \<And>substate substatea a b aa ba y ya. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; (substate, substatea) \<in> ssr; rvr a aa; (b, ba) \<in> ssr; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) (return a) (return aa)
 2. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (\<lambda>_. True) (\<lambda>_. True) (select_f (x substate)) (select_f (x' substatea)) proof (prove)
goal (1 subgoal):
 1. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr False nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (\<lambda>_. True) (\<lambda>_. True) (select_f (x substate)) (select_f (x' substatea)) proof (prove)
goal (2 subgoals):
 1. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> \<forall>s'\<in>fst (x' substatea). \<exists>s\<in>fst (x substate). (case s of (x, x') \<Rightarrow> \<lambda>(y, y'). rvr x y \<and> (x', y') \<in> ssr) s'
 2. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr; nf'\<rbrakk> \<Longrightarrow> \<not> snd (x' substatea) proof (prove)
goal (2 subgoals):
 1. \<And>substate substatea a b. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; \<forall>xa\<in>ssr. case xa of (s, s') \<Rightarrow> (\<forall>xa\<in>fst (x' s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x s). case x of (r, t) \<Rightarrow> (t, t') \<in> ssr \<and> rvr r r') \<and> (nf' \<longrightarrow> \<not> snd (x' s')); (substate, substatea) \<in> ssr; (a, b) \<in> fst (x' substatea)\<rbrakk> \<Longrightarrow> \<exists>s\<in>fst (x substate). (case s of (x, x') \<Rightarrow> \<lambda>(y, y'). rvr x y \<and> (x', y') \<in> ssr) (a, b)
 2. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr; nf'\<rbrakk> \<Longrightarrow> \<not> snd (x' substatea) proof (prove)
goal (2 subgoals):
 1. \<And>substate substatea a b. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; (substate, substatea) \<in> ssr; (a, b) \<in> fst (x' substatea); \<forall>xa\<in>fst (x' substatea). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x substate). case x of (r, t) \<Rightarrow> (t, t') \<in> ssr \<and> rvr r r'; nf' \<longrightarrow> \<not> snd (x' substatea)\<rbrakk> \<Longrightarrow> \<exists>s\<in>fst (x substate). (case s of (x, x') \<Rightarrow> \<lambda>(y, y'). rvr x y \<and> (x', y') \<in> ssr) (a, b)
 2. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr; nf'\<rbrakk> \<Longrightarrow> \<not> snd (x' substatea) proof (prove)
goal (2 subgoals):
 1. \<And>substate substatea a b. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; (substate, substatea) \<in> ssr; (a, b) \<in> fst (x' substatea); nf' \<longrightarrow> \<not> snd (x' substatea); \<exists>x\<in>fst (x substate). case x of (r, t) \<Rightarrow> (t, b) \<in> ssr \<and> rvr r a\<rbrakk> \<Longrightarrow> \<exists>s\<in>fst (x substate). (case s of (x, x') \<Rightarrow> \<lambda>(y, y'). rvr x y \<and> (x', y') \<in> ssr) (a, b)
 2. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr; nf'\<rbrakk> \<Longrightarrow> \<not> snd (x' substatea) proof (prove)
goal (1 subgoal):
 1. \<And>y ya substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; corres_underlying ssr False nf' rvr (\<lambda>_. True) (\<lambda>_. True) x x'; True; (substate, substatea) \<in> ssr; nf'\<rbrakk> \<Longrightarrow> \<not> snd (x' substatea) proof (prove)
goal (1 subgoal):
 1. \<And>substate substatea. \<lbrakk>submonad f r g fn; submonad f' r' g' fn'; \<forall>s s'. (s, s') \<in> sr \<and> g s \<and> g' s' \<longrightarrow> (f s, f' s') \<in> ssr; \<forall>s s' ss ss'. (s, s') \<in> sr \<and> (ss, ss') \<in> ssr \<longrightarrow> (r ss s, r' ss' s') \<in> sr; \<forall>xa\<in>ssr. case xa of (s, s') \<Rightarrow> (\<forall>xa\<in>fst (x' s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x s). case x of (r, t) \<Rightarrow> (t, t') \<in> ssr \<and> rvr r r') \<and> \<not> snd (x' s'); (substate, substatea) \<in> ssr; nf'; snd (x' substatea)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!