theory Detype_AI

lemma corres_submonad3:
  "\<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>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s');
    corres_underlying ssr nf nf' rvr P P' x x'\<rbrakk>
   \<Longrightarrow> corres_underlying sr nf 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 _ _ gets_sp gets_sp]) 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 (simp add: corres_underlying_def select_f_def) apply fastforce 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; ?r'2 y ya\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' rvr (G and g and (\<lambda>s. f s = substate)) (G' and g' and (\<lambda>s. f' s = substatea)) (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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' rvr (G and g and (\<lambda>s. f s = substate)) (G' and g' and (\<lambda>s. f' s = substatea)) (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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (G and g and (\<lambda>s. f s = substate)) (G' and g' and (\<lambda>s. f' s = substatea)) (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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' 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 nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' 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 nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (G and g and (\<lambda>s. f s = substate)) (G' and g' and (\<lambda>s. f' s = substatea)) (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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; (substate, substatea) \<in> ssr; rvr a aa; (b, ba) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (G and g and (\<lambda>s. f s = substate)) (G' and g' and (\<lambda>s. f' s = substatea)) (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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; (substate, substatea) \<in> ssr; rvr a aa; (b, ba) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; (substate, substatea) \<in> ssr; rvr a aa; (b, ba) \<in> ssr; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (G and g and (\<lambda>s. f s = substate)) (G' and g' and (\<lambda>s. f' s = substatea)) (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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; (substate, substatea) \<in> ssr; rvr a aa; (b, ba) \<in> ssr; dc y ya\<rbrakk> \<Longrightarrow> corres_underlying sr nf 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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (G and g and (\<lambda>s. f s = substate)) (G' and g' and (\<lambda>s. f' s = substatea)) (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; \<forall>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); corres_underlying ssr nf nf' rvr P P' x x'; True; (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr) (G and g and (\<lambda>s. f s = substate)) (G' and g' and (\<lambda>s. f' s = substatea)) (select_f (x substate)) (select_f (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>s. G s \<longrightarrow> g s \<and> P (f s); \<forall>s'. G' s' \<longrightarrow> g' s' \<and> P' (f' s'); \<forall>(s, s')\<in>ssr. P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (x' s'). \<exists>(r, t)\<in>fst (x s). (t, t') \<in> ssr \<and> rvr r r') \<and> (nf' \<longrightarrow> \<not> snd (x' s')); (substate, substatea) \<in> ssr\<rbrakk> \<Longrightarrow> \<forall>(s, s')\<in>sr. G s \<and> g s \<and> f s = substate \<and> G' s' \<and> g' s' \<and> f' s' = substatea \<longrightarrow> (nf \<longrightarrow> \<not> snd (x substate)) \<longrightarrow> (\<forall>xa\<in>fst (x' substatea). (s, s') \<in> sr \<and> (\<exists>x\<in>fst (x substate). (case x of (x, x') \<Rightarrow> \<lambda>(y, y'). rvr x y \<and> (x', y') \<in> ssr) xa)) \<and> (nf' \<longrightarrow> \<not> snd (x' substatea)) proof (prove)
goal:
No subgoals!