theory Schedule_AI

lemma findM_inv'':
  assumes p: "suffix xs xs'"
  assumes x: "\<And>x xs. suffix (x # xs) xs' \<Longrightarrow> \<lbrace>P (x # xs)\<rbrace> m x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q s) \<and> (\<not> rv \<longrightarrow> P xs s)\<rbrace>"
  assumes y: "\<And>s. P [] s \<Longrightarrow> Q s"
  shows      "\<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>" using p apply (induct xs) apply simp apply wp apply (erule y) apply (frule suffix_ConsD) apply simp apply wp apply (erule x) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
using this:
suffix xs xs'

goal (1 subgoal):
 1. \<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. suffix [] xs' \<Longrightarrow> \<lbrace>P []\<rbrace> findM m [] \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> \<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>P (a # xs)\<rbrace> findM m (a # xs) \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P []\<rbrace> return None \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> \<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>P (a # xs)\<rbrace> findM m (a # xs) \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. P [] s \<Longrightarrow> Q s
 2. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> \<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>P (a # xs)\<rbrace> findM m (a # xs) \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> \<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>P (a # xs)\<rbrace> findM m (a # xs) \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> \<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'; suffix xs xs'\<rbrakk> \<Longrightarrow> \<lbrace>P (a # xs)\<rbrace> findM m (a # xs) \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'; suffix xs xs'\<rbrakk> \<Longrightarrow> \<lbrace>P (a # xs)\<rbrace> do r <- m a;
if r then return (Some a) else findM m xs
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'; suffix xs xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 a xs\<rbrace> m a \<lbrace>\<lambda>r s. (r \<longrightarrow> Q s) \<and> (\<not> r \<longrightarrow> P xs s)\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'; suffix xs xs'; P (a # xs) s\<rbrakk> \<Longrightarrow> ?Q9 a xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<lbrace>P xs\<rbrace> findM m xs \<lbrace>\<lambda>rv. Q\<rbrace>; suffix (a # xs) xs'; suffix xs xs'; P (a # xs) s\<rbrakk> \<Longrightarrow> P (a # xs) s proof (prove)
goal:
No subgoals!