theory Nondet_While_Loop_Rules_Completeness

lemma shortest_path_gets_shorter:
  "\<lbrakk> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>;
       C r s \<rbrakk>
     \<Longrightarrow> \<exists>(r', s') \<in> fst (B r s).
                shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q
                 \<and> \<lbrace> \<lambda>s. s = s' \<rbrace> whileLoop C B r' \<exists>\<lbrace> Q \<rbrace>" apply (drule shortest_path_exists) apply clarsimp apply (rename_tac l) apply (case_tac l rule: remdups_adj.cases) apply clarsimp apply clarsimp apply (rule bexI[rotated]) apply clarsimp apply assumption apply clarify apply (simp only: valid_path.simps, clarify) apply (frule shortest_path_is_shortest [where Q=Q]) apply simp apply clarsimp apply (drule valid_path_implies_exs_valid_whileLoop) apply (clarsimp simp: exs_valid_def) apply (erule bexI [rotated]) apply (clarsimp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; C r s\<rbrakk> \<Longrightarrow> \<exists>(r', s')\<in>fst (B r s). shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C r s; \<exists>l. valid_path C B l \<and> shortest_path_length C B (r, s) Q = length l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> \<exists>(r', s')\<in>fst (B r s). shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = []\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace>
 2. \<And>l x. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = [x]\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace>
 3. \<And>l x y xs. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = x # y # xs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>l x. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = [x]\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace>
 2. \<And>l x y xs. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = x # y # xs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l x y xs. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = x # y # xs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>l x y xs. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = x # y # xs\<rbrakk> \<Longrightarrow> ?x13 l x y xs \<in> fst (B r s)
 2. \<And>l x y xs. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = x # y # xs\<rbrakk> \<Longrightarrow> case ?x13 l x y xs of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = Suc (Suc (length xs)); Q (fst (if xs = [] then (aa, ba) else last xs)) (snd (if xs = [] then (aa, ba) else last xs)); (aa, ba) \<in> fst (B r s); valid_path C B ((aa, ba) # xs)\<rbrakk> \<Longrightarrow> ?x13 ((r, s) # (aa, ba) # xs) (r, s) (aa, ba) xs \<in> fst (B r s)
 2. \<And>l x y xs. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = x # y # xs\<rbrakk> \<Longrightarrow> case ?x13 l x y xs of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l x y xs. \<lbrakk>C r s; valid_path C B l; shortest_path_length C B (r, s) Q = length l; hd l = (r, s); Q (fst (last l)) (snd (last l)); l = x # y # xs\<rbrakk> \<Longrightarrow> case y of (r', s') \<Rightarrow> shortest_path_length C B (r', s') Q < length l \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l a b aa ba xs. \<lbrakk>C r s; valid_path C B ((a, b) # (aa, ba) # xs); shortest_path_length C B (r, s) Q = length ((a, b) # (aa, ba) # xs); hd ((a, b) # (aa, ba) # xs) = (r, s); Q (fst (last ((a, b) # (aa, ba) # xs))) (snd (last ((a, b) # (aa, ba) # xs)))\<rbrakk> \<Longrightarrow> shortest_path_length C B (aa, ba) Q < length ((a, b) # (aa, ba) # xs) \<and> \<lbrace>\<lambda>s. s = ba\<rbrace> whileLoop C
  B aa \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l a b aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = length ((a, b) # (aa, ba) # xs); hd ((a, b) # (aa, ba) # xs) = (r, s); Q (fst (last ((a, b) # (aa, ba) # xs))) (snd (last ((a, b) # (aa, ba) # xs))); C (fst (a, b)) (snd (a, b)); (aa, ba) \<in> fst (B (fst (a, b)) (snd (a, b))); valid_path C B ((aa, ba) # xs)\<rbrakk> \<Longrightarrow> shortest_path_length C B (aa, ba) Q < length ((a, b) # (aa, ba) # xs) \<and> \<lbrace>\<lambda>s. s = ba\<rbrace> whileLoop C
  B aa \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>l a b aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = length ((a, b) # (aa, ba) # xs); hd ((a, b) # (aa, ba) # xs) = (r, s); Q (fst (last ((a, b) # (aa, ba) # xs))) (snd (last ((a, b) # (aa, ba) # xs))); C (fst (a, b)) (snd (a, b)); (aa, ba) \<in> fst (B (fst (a, b)) (snd (a, b))); valid_path C B ((aa, ba) # xs)\<rbrakk> \<Longrightarrow> Q (fst (last ((aa, ba) # xs))) (snd (last ((aa, ba) # xs)))
 2. \<And>l a b aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = length ((a, b) # (aa, ba) # xs); hd ((a, b) # (aa, ba) # xs) = (r, s); Q (fst (last ((a, b) # (aa, ba) # xs))) (snd (last ((a, b) # (aa, ba) # xs))); C (fst (a, b)) (snd (a, b)); (aa, ba) \<in> fst (B (fst (a, b)) (snd (a, b))); valid_path C B ((aa, ba) # xs); shortest_path_length C B (hd ((aa, ba) # xs)) Q \<le> length ((aa, ba) # xs)\<rbrakk> \<Longrightarrow> shortest_path_length C B (aa, ba) Q < length ((a, b) # (aa, ba) # xs) \<and> \<lbrace>\<lambda>s. s = ba\<rbrace> whileLoop C
  B aa \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l a b aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = length ((a, b) # (aa, ba) # xs); hd ((a, b) # (aa, ba) # xs) = (r, s); Q (fst (last ((a, b) # (aa, ba) # xs))) (snd (last ((a, b) # (aa, ba) # xs))); C (fst (a, b)) (snd (a, b)); (aa, ba) \<in> fst (B (fst (a, b)) (snd (a, b))); valid_path C B ((aa, ba) # xs); shortest_path_length C B (hd ((aa, ba) # xs)) Q \<le> length ((aa, ba) # xs)\<rbrakk> \<Longrightarrow> shortest_path_length C B (aa, ba) Q < length ((a, b) # (aa, ba) # xs) \<and> \<lbrace>\<lambda>s. s = ba\<rbrace> whileLoop C
  B aa \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = Suc (Suc (length xs)); Q (fst (if xs = [] then (aa, ba) else last xs)) (snd (if xs = [] then (aa, ba) else last xs)); (aa, ba) \<in> fst (B r s); valid_path C B ((aa, ba) # xs); shortest_path_length C B (aa, ba) Q \<le> Suc (length xs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = ba\<rbrace> whileLoop C
  B aa \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = Suc (Suc (length xs)); Q (fst (if xs = [] then (aa, ba) else last xs)) (snd (if xs = [] then (aa, ba) else last xs)); (aa, ba) \<in> fst (B r s); shortest_path_length C B (aa, ba) Q \<le> Suc (length xs); \<lbrace>\<lambda>s. s = snd (hd ((aa, ba) # xs))\<rbrace> whileLoop C
  B (fst (hd ((aa, ba) # xs))) \<exists>\<lbrace>\<lambda>r s. (r, s) = last ((aa, ba) # xs)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = ba\<rbrace> whileLoop C
  B aa \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = Suc (Suc (length xs)); Q (fst (if xs = [] then (aa, ba) else last xs)) (snd (if xs = [] then (aa, ba) else last xs)); (aa, ba) \<in> fst (B r s); shortest_path_length C B (aa, ba) Q \<le> Suc (length xs); (if xs = [] then (aa, ba) else last xs) \<in> fst (whileLoop C
  B aa ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (whileLoop C
  B aa ba). case x of (x, xa) \<Rightarrow> Q x xa proof (prove)
goal (1 subgoal):
 1. \<And>aa ba xs. \<lbrakk>C r s; shortest_path_length C B (r, s) Q = Suc (Suc (length xs)); Q (fst (if xs = [] then (aa, ba) else last xs)) (snd (if xs = [] then (aa, ba) else last xs)); (aa, ba) \<in> fst (B r s); shortest_path_length C B (aa, ba) Q \<le> Suc (length xs)\<rbrakk> \<Longrightarrow> case if xs = [] then (aa, ba) else last xs of (x, xa) \<Rightarrow> Q x xa proof (prove)
goal:
No subgoals!