theory MonadicRewrite

lemma monadic_rewrite_symb_exec_r':
  "\<lbrakk> \<And>rv. monadic_rewrite F E (Q rv) x (y rv);
     \<And>P. m \<lbrace>P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m;
     \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= (\<lambda>rv. y rv))" apply (cases E) subgoal  (* E *)
      apply (clarsimp simp: monadic_rewrite_def bind_def prod_eq_iff) apply (drule (1) no_failD) apply clarsimp apply (simp add: empty_fail_def, drule_tac x=s in spec) apply (prop_tac "\<forall>(rv, s') \<in> fst (m s). y rv s' = x s") apply clarsimp apply (drule (1) in_inv_by_hoareD) apply (drule (2) use_valid) apply (clarsimp simp: Ball_def prod_eq_iff) apply (auto elim!: nonemptyE elim: rev_bexI simp add: Bex_def Ball_def cong: conj_cong) done subgoal  (* \<not> E *)
     apply (clarsimp simp: monadic_rewrite_def bind_def) apply (drule(1) no_failD) apply (subgoal_tac "\<forall>v \<in> fst (m s). Q (fst v) (snd v) \<and> snd v = s") apply fastforce apply clarsimp apply (frule(2) use_valid) apply (frule use_valid, assumption, rule refl) apply simp done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= y)
 2. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= y) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s)\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = ((\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = ((\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) \<or> snd (m s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s)\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s)\<rbrakk> \<Longrightarrow> \<forall>(rv, s')\<in>fst (m s). y rv s' = x s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). y rv s' = x s\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) \<noteq> {}; (a, b) \<in> fst (m s)\<rbrakk> \<Longrightarrow> y a b = x s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). y rv s' = x s\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) \<noteq> {}; (a, b) \<in> fst (m s); b = s\<rbrakk> \<Longrightarrow> y a b = x s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). y rv s' = x s\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) \<noteq> {}; b = s; Q a b\<rbrakk> \<Longrightarrow> y a b = x s
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). y rv s' = x s\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (x s) = fst (y rv s) \<and> snd (x s) = snd (y rv s); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); fst (m s) = {} \<longrightarrow> snd (m s); \<forall>(rv, s')\<in>fst (m s). y rv s' = x s\<rbrakk> \<Longrightarrow> fst (x s) = (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<and> snd (x s) = (\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite F E (Q rv) x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; E \<longrightarrow> empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P') x (m >>= y) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (y rv s) \<subseteq> fst (x s) \<and> (snd (y rv s) \<longrightarrow> snd (x s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> \<not> snd (x s)\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<subseteq> fst (x s) \<and> ((\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) \<longrightarrow> snd (x s)) \<and> (snd (m s) \<longrightarrow> snd (x s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (y rv s) \<subseteq> fst (x s) \<and> (snd (y rv s) \<longrightarrow> snd (x s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<subseteq> fst (x s) \<and> ((\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) \<longrightarrow> snd (x s)) \<and> (snd (m s) \<longrightarrow> snd (x s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (y rv s) \<subseteq> fst (x s) \<and> (snd (y rv s) \<longrightarrow> snd (x s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (m s). fst (case a of (x, xa) \<Rightarrow> y x xa)) \<subseteq> fst (x s) \<and> ((\<exists>x\<in>fst (m s). snd (case x of (x, xa) \<Rightarrow> y x xa)) \<longrightarrow> snd (x s)) \<and> (snd (m s) \<longrightarrow> snd (x s))
 2. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (y rv s) \<subseteq> fst (x s) \<and> (snd (y rv s) \<longrightarrow> snd (x s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (y rv s) \<subseteq> fst (x s) \<and> (snd (y rv s) \<longrightarrow> snd (x s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>fst (m s). Q (fst v) (snd v) \<and> snd v = s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (y rv s) \<subseteq> fst (x s) \<and> (snd (y rv s) \<longrightarrow> snd (x s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); (a, b) \<in> fst (m s)\<rbrakk> \<Longrightarrow> Q a b \<and> b = s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (y rv s) \<subseteq> fst (x s) \<and> (snd (y rv s) \<longrightarrow> snd (x s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); (a, b) \<in> fst (m s); Q a b\<rbrakk> \<Longrightarrow> Q a b \<and> b = s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>rv. \<forall>s. Q rv s \<and> (F \<longrightarrow> \<not> snd (x s)) \<longrightarrow> fst (y rv s) \<subseteq> fst (x s) \<and> (snd (y rv s) \<longrightarrow> snd (x s)); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>; \<not> E; P s; P' s; F \<longrightarrow> \<not> snd (x s); \<not> snd (m s); (a, b) \<in> fst (m s); Q a b; ?t102 s b a b = ?t101 s b a b\<rbrakk> \<Longrightarrow> Q a b \<and> b = s
flex-flex pairs:
\<lambda>s. ?t101 s s \<equiv>\<^sup>? \<lambda>s. ?t102 s s proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!