theory week10B_demo
imports Main "autocorres-2015/lib/wp/NonDetMonadVCG" "~~/src/HOL/Eisbach/Eisbach_Tools"
begin

lemmas dup = thin_rl[of "PROP W" "PROP W" for W]

section \<open>; combinator\<close>

lemma 
  assumes B: "C"
  shows "(A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<and> C"
  apply (intro conjI ; (rule impI, rule B | rule B))
  done
  


section Eisbach_Demo


lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
  apply (rule impI)
  apply (erule conjE)+
  apply (erule disjE)
    apply (erule impE)
   apply assumption
  apply assumption
  apply (erule impE,assumption)
  apply assumption
  done



lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
  apply (assumption | rule conjI impI | erule conjE impCE disjE | (erule notE,assumption))+
  done


method my_awesome_method = 
  (assumption | rule conjI impI | erule conjE impCE disjE | (erule notE,assumption))+


lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
  by my_awesome_method


subsection \<open>Fact Abstraction\<close>

text \<open>The uses keyword is a fact parameter that must always be provided at run-time\<close>

method my_awesome_method2 uses intros elims = 
  (assumption | rule intros | erule elims | (erule notE,assumption))+

lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
  by (my_awesome_method2 intros: conjI impI elims: conjE impCE disjE)

text \<open>Named theorems are facts that can grow and shrink using attributes\<close>

named_theorems intros and elims

lemmas [intros] = conjI impI
lemmas [elims] = conjE impCE disjE

thm intros
thm elims

declare FalseE[intros]

thm intros

text \<open>Not a safe rule. Lets get rid of it.\<close>

declare FalseE[intros del]

method my_awesome_method3 declares intros elims =
  (assumption | rule intros | erule elims | (erule notE,assumption))+


lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
  by my_awesome_method3

lemma "B \<longrightarrow> (B \<longleftrightarrow> C) \<longrightarrow> C"
  by (my_awesome_method3 elims: iffE)

method prop_solver' declares intros elims =
      ((assumption 
       | rule intros
       | erule elims 
       | (erule notE, (prop_solver' ; fail)))+)[1]

lemmas [intros] = conjI impI disjCI iffI notI
lemmas [elims] = impCE conjE disjE


lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C" 
  apply prop_solver'
  done


text \<open>The "; fail" suffix is necessary to ensure we don't terminate in an unsolvable state.
      This is the same as using the "solves" combinator (i.e. solves \<open>prop_solver'\<close>)\<close>


lemma "\<not> A \<Longrightarrow> \<not>(A \<longrightarrow> B) \<Longrightarrow> False" 
  apply prop_solver'
  done


subsection \<open>Term Abstraction\<close>

text \<open>Methods are implicitly polymorphic over term parameters\<close>

method elim_all for Q :: "'a \<Rightarrow> bool" and y :: 'a = 
  (erule allE[where P = Q and x = y ])
      
lemma "\<forall>x. P x \<Longrightarrow> P y"
  apply (elim_all P y)
  apply assumption
done

text \<open>Term parameters are type-checked\<close>

method induct_auto for l :: "'a list" =
  (induct l; auto)

lemma "distinct l \<Longrightarrow> card (set l) = length l"
  by (induct_auto l)

lemma "length (l @ l') = length l' + length l"
  (*by (induct_auto "length l")*)
  sorry


subsection \<open>Method abstraction\<close>

text \<open>Method expressions can be given as parameters, to create higher-order methods\<close>

method induct_then for x :: 'a methods m = (induct x; m)

lemma "distinct l \<Longrightarrow> card (set l) = length l"
  by (induct_then l \<open>simp\<close>)

subsection \<open>Interlude: Helper methods\<close>

text \<open>Eisbach provides a few helper methods to aid in run-time debugging.\<close>

lemma "True"
  apply (print_fact conjE)
  apply (print_term "True \<and> False")
  by (rule TrueI)

text \<open>These get run every time a method backtracks, which is useful to gain insight into
      its behaviour\<close>

lemma "\<forall>x :: 'a. Q x \<Longrightarrow> \<forall>x :: 'a. P x \<Longrightarrow> P y"
  by (erule allE[where x=y], print_term P, assumption)

text \<open>Here we see that the first call to "assumption" fails, so backtracking forces "erule allE"
      to specialize a different quantifier. The method "print_term" is then called again.\<close>


subsection \<open>The match method\<close>


text \<open>The match method is a proof method specifically written for use in Eisbach. It performs
structured decomposition of the goal known as "subgoal focusing". This allows subgoal
elements to be named, based on patterns.\<close>



text \<open>When given exactly the right assumptions, the "simplified" method works.
      However, the additional assumption "ceqb" will cause it to loop.\<close>

lemma
  assumes Pb: "P b" and beqa: "b = a" and aeqc: "a = c" and ceqb: "c = a"
  shows "P c"
  by (rule Pb[simplified beqa aeqc])


text \<open>Additionally, if we add all of the assumptions to the subgoal, the simplifier
      will simply loop. Proof methods "metis" and "blast" will still solve the goal, however.\<close>

lemma
  assumes Pb : "P b"
  shows "\<And>a c. b = a \<Longrightarrow> a = c \<Longrightarrow> c = a \<Longrightarrow> P c"
  (*apply (simp add: Pb)?*)
  (*apply (rule subst)
  apply assumption*)
  by (rule subst, assumption, rule subst, assumption, rule Pb)

lemma
  assumes Pb : "P b"
  shows "\<And>a c. b = a \<Longrightarrow> a = c \<Longrightarrow> c = a \<Longrightarrow> P c"
  apply (match premises in H:_ \<Rightarrow> \<open>print_fact H\<close>)
  back
  back

  apply (match premises in H:_ (multi) \<Rightarrow> \<open>print_fact H\<close>)
  apply (match premises in H:"b = x" for x \<Rightarrow> \<open>print_fact H, print_term x\<close>)
  apply (match premises in H:"x = y" for x y \<Rightarrow> \<open>print_fact H, print_term x, print_term y\<close>)
  back

  (* apply (match premises in H:_ (multi) \<Rightarrow> \<open>rule Pb[simplified H]\<close>) *)

  apply (rule dup)
  
  apply (match conclusion in "P y" for y \<Rightarrow> 
          \<open>match premises in H: "x = y" and H': "b = x" for x \<Rightarrow>
            \<open>rule Pb[simplified H H']\<close>\<close>)

  apply (rule dup)

   apply (match premises in H: "_ = x" and H': "x = _" for x \<Rightarrow>
           \<open>rule Pb[simplified H H']\<close>)

  apply (rule dup)

   apply (match premises in H[simp]: "_ = x" and H'[simp]: "x = _" for x \<Rightarrow>
           \<open>rule Pb[simplified]\<close>)

  apply (match conclusion in "P y" for y \<Rightarrow> 
          \<open>match premises in H[thin]: "y = _" \<Rightarrow> \<open>succeed\<close>\<close>)

  apply (match premises in H:_ (multi) \<Rightarrow> \<open>rule Pb[simplified H]\<close>)
  done

text \<open>Multiple match patterns can be given at once and they will
      be interpreted top-down. However, once a pattern is matched
      backtracking will not occur past it.\<close>
thm conjE
lemma "Q \<and> Q' \<Longrightarrow> Q"
  
  apply (match premises in 
         (* H:"Q \<and> _" \<Rightarrow> \<open>rule H\<close>
        \<bar>*) H:"_ \<and> _" \<Rightarrow> \<open>rule conjE[OF H]\<close>)
  by simp+
  


subsection \<open>Putting it all together\<close>


text \<open>This method picks a universally quantified assumption and attempts to guess an instantiation
      for it, backtracking over possible other instantiations and eventually discarding
      it. Both the conclusion and the premises are used to try to find candidate (type-correct)
      instantiations.\<close>

method guess_all_elim =
        (match premises in U[thin]: "\<forall>x. P (x :: 'a)" for P  \<Rightarrow>
           \<open>(match premises in "?H (y :: 'a)" for y \<Rightarrow>
              \<open>rule allE[where P=P and x=y, OF U]\<close>)?,
            (match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
              \<open>rule allE[where P=P and x=y, OF U]\<close>)?\<close>)


lemma "\<forall>x :: 'a. P x \<Longrightarrow> \<forall>x :: 'a. Q x \<Longrightarrow> Q y"
  apply (guess_all_elim)
  back
  apply assumption
  done

text \<open>This method is similar to above, but instead searches for witnesses for an existential
      conclusion.\<close>

method guess_ex_intro =
      (match conclusion in "\<exists>x. P (x :: 'a)" for P \<Rightarrow>
        \<open>(match premises in "?H (x :: 'a)" for x \<Rightarrow>
           \<open>rule exI [where x = x and P = P]\<close>)?,
         (match conclusion in "?H (x :: 'a)" for x \<Rightarrow>
           \<open>rule exI [where x = x and P = P]\<close>)?\<close>)

lemma "P y \<Longrightarrow> Q x \<Longrightarrow> P x \<Longrightarrow> \<exists>x. Q x \<and> P x"
  apply (guess_ex_intro)
  back
  apply simp
  done

lemma "\<exists>x. x = y"
  apply (guess_ex_intro)
  apply (rule refl)
  done
      
named_theorems subst and dests

method prop_solver declares intros elims subst dests =
      (assumption 
       | rule intros
       | erule elims
       | drule dests
       | subst subst
       | subst (asm) subst
       | (erule notE; solves \<open>prop_solver\<close>))+

method fol_solver =
      ((prop_solver | guess_ex_intro | guess_all_elim ) ; solves \<open>fol_solver\<close>)
      
declare allI[intros]
        Meson.not_exD[dests] 
        Meson.not_allD[dests]
        exE[elims]
        ex_simps[subst]
        all_simps[subst]


lemma "(\<forall>x. P x) \<and> (\<forall>x. Q x) \<Longrightarrow> (\<forall>x. Q x \<and> P x)"
      and  "\<exists>x. (P x \<longrightarrow> (\<forall>x. P x))"
      and "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
      by fol_solver+

section \<open>Advanced Methods\<close>

text \<open>In this section we'll walk through creating a practical method for simplifying
      postconditions in hoare logic.\<close>

text \<open>Here is some toy monadic specification that maintains a distinct list in its
      state, while keeping its length pre-calculated. Abstract flags
      "initialized" and "finalized" are included to represent state that this
      function might have to deal with if it were part of a large program.\<close>



record state = 
  list_state :: "nat list" 
  length_state :: nat

  initialized_state :: bool
  finalized_state :: bool

definition "length_valid s == 
  length (list_state s) = length_state s"

definition "list_distinct s == distinct (list_state s)"


definition "valid_state s \<equiv> 
  length_valid s \<and> list_distinct s \<and> finalized_state s"

definition
  "incr_length ==
  modify (\<lambda>s. s\<lparr>length_state := (length_state s) + 1\<rparr>)"

definition
  finalize :: "(state,unit) nondet_monad" where
  "finalize \<equiv> 
    modify (\<lambda>s. s\<lparr>finalized_state := length_valid s \<and> list_distinct s \<and> initialized_state s\<rparr>)"

definition  
  initialize :: "(state,unit) nondet_monad" where
  "initialize \<equiv> 
    modify (\<lambda>s. s\<lparr>initialized_state := valid_state s\<rparr>)"

text \<open>cons_list performs some abstract initialization,
      updates the list if the element is not already present,
      and then does some finalization.\<close>

definition 
  "cons_list x ==
  do
     initialize;
     l <- gets list_state;
     unless (x \<in> set l)
     (do
      modify (\<lambda>s. s\<lparr>list_state := x # l\<rparr>);
      incr_length
      od);
     finalize
  od"


lemma
  initialize_initial[wp]:
  "\<lbrace>valid_state\<rbrace> initialize \<lbrace>\<lambda>_. initialized_state\<rbrace>"
  unfolding initialize_def
  apply wp
  by (simp add: valid_state_def)


lemma
  initialize_valid_state[wp]:
  "\<lbrace>valid_state\<rbrace> initialize \<lbrace>\<lambda>_. valid_state\<rbrace>"
  unfolding initialize_def
  apply wp
  by (simp add: valid_state_def length_valid_def list_distinct_def)

lemma 
  finalize_valid_state[wp]:
  "\<lbrace>\<lambda>s. initialized_state s \<and> length_valid s \<and> list_distinct s\<rbrace>
  finalize
  \<lbrace>\<lambda>_. valid_state\<rbrace>"
  unfolding finalize_def
  apply wp
  by (simp add: valid_state_def length_valid_def list_distinct_def)


lemma incr_length_length_valid[wp]:
  "\<lbrace>\<lambda>s. length (list_state s) = Suc (length_state s)\<rbrace>
   incr_length
   \<lbrace>\<lambda>_. length_valid\<rbrace>"
  unfolding incr_length_def
  apply wp
  by (simp add: length_valid_def)

lemma incr_length_distinct[wp]:
  "\<lbrace>list_distinct\<rbrace> incr_length \<lbrace>\<lambda>_. list_distinct\<rbrace>"
  unfolding incr_length_def
  apply wp
  by (simp add: list_distinct_def)

lemma incr_length_finalzed[wp]:
  "\<lbrace>initialized_state\<rbrace> incr_length \<lbrace>\<lambda>_. initialized_state\<rbrace>"
  unfolding incr_length_def
  apply wp
  by simp
  

text \<open>In the final proof we encounter a small wrinkle. The generated
      postcondition is a bit of a jumble and wp gets stuck.
      After thinking for a bit, it's clear that this is just
      valid_state and initialized_state. The standard
      way to do this is to provide this explicitly with a rule_tac.
      \<close>

lemma
  "\<lbrace>valid_state\<rbrace> cons_list x \<lbrace>\<lambda>_. valid_state\<rbrace>"
  unfolding cons_list_def unless_def
  apply wp
  apply simp
  apply (rule_tac Q="\<lambda>r s. valid_state s \<and> initialized_state s" in hoare_strengthen_post)
  apply wp
  apply simp
  by (auto simp: valid_state_def length_valid_def list_distinct_def)


text \<open>In a large proof with potentially dozens of invariants,
      it becomes impractical to put them into the proof
      script implicitly like this.

      Instead of strengthening, we can add implications to
      the postcondition. The simplifier then implicitly picks
      this up and solves those postconditions.
      \<close>


lemma
  "\<lbrace>valid_state\<rbrace> cons_list x \<lbrace>\<lambda>_. valid_state\<rbrace>"
  unfolding cons_list_def unless_def
  apply (rule hoare_pre)
   apply wp
   apply simp
   apply (rule hoare_add_post[OF initialize_initial,rotated])
    apply simp
    apply (rule hoare_strengthen_post[OF initialize_valid_state])
    by (auto simp: valid_state_def length_valid_def list_distinct_def)

text \<open>Unfortunately we can't directly match out of the wp set,
      so we make a new named theorem to capture hoare triples
      that we might want to use to strengthen.\<close>

named_theorems hoare_strengthen

text \<open>One possible implementation is to write a method that
      recursively decomposes the postcondition, trying
      to find a match from our database. Once found, we
      add it to the postcondition, simplify, then strip it
      off again.\<close>

method use_hoare 
  for f :: "('b,'a) nondet_monad" and Q :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
  declares hoare_strengthen =
  (match hoare_strengthen in U: "\<lbrace>_\<rbrace> f \<lbrace>Q\<rbrace>" \<Rightarrow> 
     \<open>rule hoare_add_post[OF U,rotated],
      simp,
      (rule hoare_drop_imp[where R=Q])?\<close>
 |(match (Q) in 
    "\<lambda>(r :: 'a) (s :: 'b). Q' r s \<and> Q'' r s" for Q' Q'' \<Rightarrow>
      \<open>(use_hoare f Q')?, (use_hoare f Q'')?\<close>
  \<bar> "\<lambda>(r :: 'a) (s :: 'b). Q' r s \<longrightarrow> Q'' r s" for Q' Q'' \<Rightarrow>
      \<open>(use_hoare f Q')?, (use_hoare f Q'')?\<close>))

declare initialize_initial[hoare_strengthen]

thm hoare_strengthen

method auto_strengthen_post
  declares hoare_strengthen =
  (match conclusion in "\<lbrace>_\<rbrace> f \<lbrace>Q\<rbrace>" for f Q \<Rightarrow> 
    \<open>use_hoare f Q\<close>)

text \<open>Like magic, initialized_state disappears!\<close>

lemma
  "\<lbrace>valid_state\<rbrace> cons_list x \<lbrace>\<lambda>_. valid_state\<rbrace>"
  unfolding cons_list_def unless_def
  apply (rule hoare_pre)
   apply wp
   apply simp
   apply auto_strengthen_post
    apply (rule hoare_strengthen_post[OF initialize_valid_state])
    by (auto simp: valid_state_def length_valid_def list_distinct_def)

text \<open>Alternatively we can turn the implementation inside out.
      We retrieve strengthening rules that match our function,
      and then see if our postcondition contains it. Much cleaner,
      but potentially slower.\<close>

method auto_strengthen_post'
  declares hoare_strengthen =
  (match conclusion in "\<lbrace>_\<rbrace> f \<lbrace>Q\<rbrace>" for f Q \<Rightarrow>
    \<open>match hoare_strengthen in U: "\<lbrace>_\<rbrace> f \<lbrace>Q'\<rbrace>" for Q' \<Rightarrow>
      \<open>match (Q) in "?H Q'" \<Rightarrow> 
        \<open>rule hoare_add_post[OF U,rotated],
         simp,
         (rule hoare_drop_imp[where R=Q'])?\<close>\<close>\<close>)

lemma
  "\<lbrace>valid_state\<rbrace> cons_list x \<lbrace>\<lambda>_. valid_state\<rbrace>"
  unfolding cons_list_def unless_def
  apply (rule hoare_pre)
   apply wp
   apply simp
   apply auto_strengthen_post'
    apply (rule hoare_strengthen_post[OF initialize_valid_state])
    by (auto simp: valid_state_def length_valid_def list_distinct_def)


end