theory Ipc_DR

lemma corres_guard_from_wp_r:
  assumes ac: "corres_underlying sr False False r G G' a c"
  and     rl: "\<lbrace>\<lambda>s. \<not> P s\<rbrace> c \<lbrace>\<lambda>_ _. False\<rbrace>"
  shows "corres_underlying sr False False r G (\<lambda>s. P s \<longrightarrow> G' s) a c" apply (rule corres_name_pre) apply (case_tac "P s'") apply simp apply (rule corres_guard_imp) apply (rule ac) apply simp apply simp apply (rule corres_underlyingI) apply (frule use_valid [OF _ rl]) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr False False r G (\<lambda>s. P s \<longrightarrow> G' s) a c proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c
 2. \<And>s s'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> sr; P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c
 2. \<And>s s'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> sr; P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r (?Q3 s s') (?Q'3 s s') a c
 2. \<And>s s' sa. \<lbrakk>G s; G' s'; (s, s') \<in> sr; P s'; s = sa\<rbrakk> \<Longrightarrow> ?Q3 s s' sa
 3. \<And>s s' sa. \<lbrakk>G s; G' s'; (s, s') \<in> sr; P s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'3 s s' sa
 4. \<And>s s'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa. \<lbrakk>G s; G' s'; (s, s') \<in> sr; P s'; s = sa\<rbrakk> \<Longrightarrow> G sa
 2. \<And>s s' sa. \<lbrakk>G s; G' s'; (s, s') \<in> sr; P s'; s' = sa\<rbrakk> \<Longrightarrow> G' sa
 3. \<And>s s'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>G s; G' s'; (s, s') \<in> sr; P s'; s' = sa\<rbrakk> \<Longrightarrow> G' sa
 2. \<And>s s'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'\<rbrakk> \<Longrightarrow> corres_underlying sr False False r ((=) s) ((=) s') a c proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa t rv' t'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'; (sa, t) \<in> sr; s = sa; s' = t; (rv', t') \<in> fst (c t)\<rbrakk> \<Longrightarrow> \<exists>(rv, s')\<in>fst (a sa). (s', t') \<in> sr \<and> r rv rv'
 2. \<And>s s' sa t. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'; (sa, t) \<in> sr; s = sa; s' = t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa t rv' t'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'; (sa, t) \<in> sr; s = sa; s' = t; (rv', t') \<in> fst (c t)\<rbrakk> \<Longrightarrow> \<not> P t
 2. \<And>s s' sa t rv' t'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'; (sa, t) \<in> sr; s = sa; s' = t; (rv', t') \<in> fst (c t); False\<rbrakk> \<Longrightarrow> \<exists>(rv, s')\<in>fst (a sa). (s', t') \<in> sr \<and> r rv rv'
 3. \<And>s s' sa t. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'; (sa, t) \<in> sr; s = sa; s' = t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa t rv' t'. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'; (sa, t) \<in> sr; s = sa; s' = t; (rv', t') \<in> fst (c t); False\<rbrakk> \<Longrightarrow> \<exists>(rv, s')\<in>fst (a sa). (s', t') \<in> sr \<and> r rv rv'
 2. \<And>s s' sa t. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'; (sa, t) \<in> sr; s = sa; s' = t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa t. \<lbrakk>G s; P s' \<longrightarrow> G' s'; (s, s') \<in> sr; \<not> P s'; (sa, t) \<in> sr; s = sa; s' = t; False\<rbrakk> \<Longrightarrow> \<not> snd (c t) proof (prove)
goal:
No subgoals!