theory ToyLang_demo
  imports Main
begin

\<comment> \<open> This otherwise useless toy programming language is sufficient for us to get stuck
     in interesting ways when doing inductive proofs. \<close>
datatype toy_language =
    Skip \<comment> \<open> do nothing \<close>
    | Seq toy_language toy_language \<comment> \<open> Seq p q = first do p then do q (p; q) \<close>
    | Do toy_language \<comment> \<open> Keep doing p forever     while(1) { p }  \<close>

\<comment> \<open> semantics = "small-step transitions"
     Intuitively, if semantics p q holds, then p can reduce to q in a single step
\<close>
inductive semantics :: "toy_language \<Rightarrow> toy_language \<Rightarrow> bool" where
  semantics_seq1: "\<lbrakk>semantics p p'\<rbrakk>  \<Longrightarrow> semantics (Seq p q) (Seq p' q)"
| semantics_seq2: "\<lbrakk>p = Skip\<rbrakk>  \<Longrightarrow> semantics (Seq p q) q"
| semantics_do: "semantics (Do p) (Seq p (Do p))"

\<comment> \<open> Note: this is very similar to rtranclp!
     Intuitively, if big_semantics p q, then
     p reduces to q with a (possibly empty) sequence of semantics steps \<close>
inductive big_semantics :: "toy_language \<Rightarrow> toy_language \<Rightarrow> bool" where
  big_semantics1: "big_semantics p p"
| big_semantics2: "\<lbrakk>semantics p q; big_semantics q r\<rbrakk> \<Longrightarrow> big_semantics p r"

\<comment> \<open> A program is stuck if it can't take any further small steps \<close>
definition stuck where "stuck p = (\<forall>q. semantics p q \<longrightarrow> False)"

\<comment> \<open> A program terminates if it can reach a state where it is stuck.
     Our programming language is so basic that the only interesting observation
     we can make about programs is whether they terminate or not.
   \<close>
definition terminates where
  "terminates p = (\<exists>q. big_semantics p q \<and> stuck q)"


\<comment> \<open> As a warm-up exercise, let's prove that Skip terminates \<close>
lemma "terminates Skip"
  unfolding terminates_def stuck_def
  apply(rule exI[where x=Skip])
  \<comment> \<open> rule_tac x=Skip in exI would also work. \<close>
  apply(rule conjI)
   apply(rule big_semantics1)
  apply(rule allI)
  apply(rule impI)
  apply(erule semantics.cases)
    apply simp+
  done
  \<comment> \<open> Btw, this can all be automated:
        apply(auto intro: big_semantics.intros elim: semantics.cases)
     \<close>

text \<open> Now, let's prove that Do p doesn't terminate.
       The first step is to figure out what lemmas we'll need.
       If you're not in a thinking mood, one option is to start
       stepping through the proof to see what kind of goal we
       get stuck on.
     \<close>

lemma "\<not>terminates(Do p)"
  unfolding terminates_def stuck_def
  apply auto \<comment> \<open>This goal state looks like a suitable lemma, let's prove it!\<close>
  oops

text \<open> Since big_semantics is inductive, it's likely that we'll need to prove
       this lemma by induction. But how should we set the induction?

       There are many ways to do it, and many ways to go wrong.

       We'll try the simplest possible induction first, see where we get stuck,
       and try more advanced things as the need arises.

       Here are some things to consider to determine if your induction proof is
       on the right track:

       1. Do the subgoals look true?
       2. Are the subgoals simpler than the original statement?
       3. Do the induction hypotheses look applicable?
     \<close>

text \<open> First try: structural induction \<close>

lemma terminates_do_lemma:
  "big_semantics (Do p) q \<Longrightarrow> Ex (semantics q)"
  apply(induct p)
\<comment> \<open> Is this a good place to be? Let's apply the tests above!
     1. The first subgoal looks true enough: the "reduction orbit" of Do Skip is
           Do Skip -> Seq Skip (Do Skip) -> Do Skip -> ...
        so clearly another step is always possible.
        The other subgoals also look true for similar reasons.
     2. The new subgoals don't look simpler in any way: yes we have more structure on p,
        but it's not at all obvious how that will help us reason about semantics and
        big_semantics, since the semantics_do rule doesn't care what's in the loop body.
     3. The induction hypotheses of the second and third subgoal are useless.
        For example, neither Do p1 nor Do p2 are in the "reduction orbit" of
        Do (Seq p1 p2), so starting from Do (Seq p1 p2) we'll never end up with a
        program that looks like the one in the induction hypothesis.
   \<close>
  oops

text \<open> Second try: rule induction \<close>

lemma terminates_do_lemma:
  "big_semantics (Do p) q \<Longrightarrow> Ex (semantics q)"
  apply(induct rule: big_semantics.induct)
  \<comment> \<open> The second subgoal is easy.
       Unfortunately, the first subgoal is clearly false: we need to prove
       that every process reduces to something, but Skip doesn't.

       It seems that induct ate the (important!) information that the first
       argument to big_semantics is a Do.
   \<close>
  oops

text \<open> Third try: rule induction but remember that we're starting from Do. \<close>

lemma terminates_do_lemma:
  "big_semantics (Do p) q \<Longrightarrow> Ex (semantics q)"
  apply(induct "Do p" q rule: big_semantics.induct)
  \<comment> \<open> The first subgoal is easy. \<close>
   apply(force intro: semantics.intros)
  \<comment> \<open> For the second, subgoal, the induction hypothesis is inapplicable:
       because we are inducting over things with the shape "Do p", the induction
       hypothesis is only applicable if q = Do p. However, that will not be
       the case, as we can see from stepping through the proofs a bit: \<close>
  apply(erule semantics.cases;clarsimp)
  \<comment> \<open> Maybe we can prove the remaining subgoal as yet another lemma though? \<close>
  oops

text \<open> Fourth try: similar induction, different hypothesis \<close>

lemma terminates_do_lemma_lemma:
  "big_semantics (Seq q (Do p)) r \<Longrightarrow> Ex (semantics r)"
  apply(induct "Seq q (Do p)" r rule: big_semantics.induct)
  \<comment> \<open> The first case requires us to prove that a sequential composition can
       always reduce, which is true.

       However, two things go wrong here:
       However, the induction hypothesis in the second case is inapplicable:
       clearly, it will not be the case that qa is exactly Seq q (Do p), but
       rather Seq q' (Do p) for some other q'.
     \<close>
  oops

text \<open> Fifth try: preverse syntactic structure but with arbitrary contents. \<close>

lemma terminates_do_lemma_lemma:
  "big_semantics (Seq q (Do p)) r \<Longrightarrow> Ex (semantics r)"
  apply(induct "Seq q (Do p)" r arbitrary: q rule: big_semantics.induct)
  \<comment> \<open> The first case still looks good. (Let's sorry it anyway) \<close>
  subgoal sorry  
  apply(erule semantics.cases;clarsimp) \<comment> \<open> As for the second case... \<close>
  \<comment> \<open> We solved the problem from the fourth try, but we've gone in
       circles: we now require the original lemma after all!

       Since these lemmas clearly depend on each other, maybe we can prove them
       simultaneously?
     \<close>
  oops

text \<open> Sixth try: third try \<or> fifth try \<close>

\<comment> \<open> This lemma seems useful for the first case we've had for the past few tries \<close>
lemma nonskip_reduces:
  "p \<noteq> Skip \<Longrightarrow> Ex (semantics p)"
  apply(induct p)
    apply simp
   apply clarsimp
   apply(case_tac "p1=Skip")
    apply(force intro: semantics_seq2)
   apply clarsimp
   apply(force intro: semantics_seq1)
  apply(force intro: semantics_do)
  done

lemma terminates_do_lemma:
  "big_semantics p s \<Longrightarrow> p = Seq q (Do r) \<or> p = Do r \<Longrightarrow> Ex (semantics s)"
  \<comment> \<open> This one actually goes through! \<close>
  apply(induct arbitrary: q r rule: big_semantics.induct)
   apply(force intro: nonskip_reduces)
  apply(erule disjE;clarsimp)
   apply(erule semantics.cases;clarsimp)
  apply(erule semantics.cases;clarsimp)
  done

lemma "\<not>terminates(Do p)"
  unfolding terminates_def stuck_def
  by(auto intro: terminates_do_lemma)

text \<open> Bonus content: "induction on q" path we pursued in the lecture \<close>

lemma terminates_do_lemma_lemma:
  "big_semantics (Do p) Skip \<Longrightarrow> False"
  apply(cases rule: big_semantics.cases,assumption)
   apply simp
  apply(erule semantics.cases;clarsimp)
  \<comment> \<open> Here we'd really want an induction hypothesis. \<close>
  oops

\<comment> \<open> My (Johannes') alternative from the lecture to the disjunction we ended up with above.
     This was originally based on a confusion of mine: I was thinking that Do would reduce like this:

       Seq (Do p) (Do q) --> Seq p (Seq (Do p) (Do q))

     whereas in reality it works like this:

       Seq (Do p) (Do q) --> Seq (Seq p Do p) (Do q))

     hence the infinite descending chain of auxiliary lemmas I worried about in the lecture
     does not in fact happen: the proof above shows that it stabilises after just one.

     However, I still find this proof slightly more elegant, even though it turned out to
     be overkill to introduce an auxiliary inductive relation:
 \<close>
primrec whiley
  where "whiley Skip = False"
  | "whiley(Do p) = True"
  | "whiley(Seq p q) = whiley q"

lemma terminates_do_lemma_lemma:
  "big_semantics p Skip \<Longrightarrow> whiley p \<Longrightarrow> False"
  apply(induct p Skip rule: big_semantics.induct)
   apply simp
  apply(erule semantics.cases;clarsimp)
  done

lemma semantics_whiley_pres:
  "semantics p q \<Longrightarrow> whiley p \<Longrightarrow> whiley q"
  apply(erule semantics.cases;clarsimp)
  \<comment> \<open> meth1;meth2 roughly:
       first apply meth1, then apply meth2 to all new subgoals\<close>
  done

lemma terminates_do_lemma':
  "big_semantics (Do p) q \<Longrightarrow> Ex (semantics q)"
  apply(cases q;clarsimp)
    apply(drule terminates_do_lemma_lemma)
     apply simp
    apply simp
   apply(case_tac "x21=Skip")
    apply clarify
    apply(rule exI)
    apply(rule semantics_seq2)
    apply simp
   apply(force dest: nonskip_reduces intro: semantics_seq1)
  apply(force intro: semantics_do)
  done

text \<open> Instead of cases on q, rule induction works well: \<close>

lemma terminates_do_lemma'':
  "big_semantics p q \<Longrightarrow> whiley p \<Longrightarrow> Ex (semantics q)"
  apply(induct rule: big_semantics.induct)
   apply(rule nonskip_reduces)
   apply(rule ccontr)
   apply simp
  apply(drule semantics_whiley_pres,assumption)
  \<comment> \<open> meth1,meth2 roughly:
       first apply meth1, then apply meth2 to the first subgoal\<close>
  apply simp
  done

lemma "\<not>terminates(Do p)"
  unfolding terminates_def stuck_def
  by(auto intro: terminates_do_lemma')

text \<open> Bonus content: proofs based on questions from the lectures. \<close>

lemma big_semantics_is_rtranclp:
  "big_semantics p q = semantics\<^sup>*\<^sup>* p q"
proof(rule iffI)
  assume "big_semantics p q"
  thus "semantics\<^sup>*\<^sup>* p q"
    by(induct rule:big_semantics.induct) auto
next
  assume "semantics\<^sup>*\<^sup>* p q"
  thus "big_semantics p q"
    \<comment> \<open> The default induction principle (rtranclp.induct) would be supremely annoying to use here:
         unlike big_semantics it has the "big step" to the left instead of to the right. \<close>
    by(induct rule: converse_rtranclp_induct) (auto intro: big_semantics.intros)
qed

lemma semantics_deterministic:
  assumes "semantics p q"
   and "semantics p r"
 shows "r = q"
  using assms
  apply(induct arbitrary: r rule: semantics.induct)
    apply(erule semantics.cases[where ?a1.0="Seq p q" for p q])
    \<comment> \<open> This highly specific instantiation prevents semantics.cases from being
         applied to the first subgoal. \<close>
      apply clarsimp
     apply(drule_tac x=p' in meta_spec)
     apply clarsimp
     apply(erule semantics.cases;clarsimp)
     apply(drule_tac x=p' in meta_spec)
     apply clarsimp
    apply(erule semantics.cases;clarsimp)
   apply(erule semantics.cases;clarsimp)
  apply(erule semantics.cases;clarsimp)
  done

text \<open> Bonus content: exercise \<close>

lemma "terminates (Seq p q) = (terminates p \<and> terminates q)"
  \<comment> \<open> This will require a fair bit of work. \<close>
  oops

end