Theory PsLang

(*  Title:       Mutually recursive procedures
    Author:      Tobias Nipkow, 2001/2006
    Maintainer:  Tobias Nipkow
*)

section "Hoare Logics for Mutually Recursive Procedure"

theory PsLang imports Main begin

subsection‹The language›

typedecl state
typedecl pname

type_synonym bexp = "state ⇒ bool"

datatype
  com = Do "state ⇒ state set"
      | Semi  com com          ("_; _"  [60, 60] 10)
      | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
      | While bexp com         ("WHILE _ DO _"  60)
      | CALL pname
      | Local "(state ⇒ state)" com "(state ⇒ state ⇒ state)"
               ("LOCAL _; _; _" [0,0,60] 60)

consts body :: "pname ⇒ com"

text‹We generalize from a single procedure to a whole set of
procedures following the ideas of von Oheimb~\<^cite>‹"Oheimb-FSTTCS99"›.
The basic setup is modified only in a few places:
\begin{itemize}
\item We introduce a new basic type @{typ pname} of procedure names.
\item Constant @{term body} is now of type @{typ"pname ⇒ com"}.
\item The @{term CALL} command now has an argument of type @{typ pname},
the name of the procedure that is to be called.
\end{itemize}
›

inductive
  exec :: "state ⇒ com ⇒ state ⇒ bool"   ("_/ -_→/ _" [50,0,50] 50)
where
    Do:     "t ∈ f s ⟹ s -Do f→ t"

  | Semi:   "⟦ s0 -c1→ s1; s1 -c2→ s2 ⟧ ⟹ s0 -c1;c2→ s2"

  | IfTrue:  "⟦ b s;  s -c1→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"
  | IfFalse: "⟦ ¬b s; s -c2→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"

  | WhileFalse: "¬b s ⟹ s -WHILE b DO c→ s"
  | WhileTrue:  "⟦ b s; s -c→ t; t -WHILE b DO c→ u ⟧
                ⟹ s -WHILE b DO c→ u"

  | Call: "s -body p→ t ⟹ s -CALL p→ t"

  | Local: "f s -c→ t ⟹ s -LOCAL f; c; g→ g s t"

lemma [iff]: "(s -Do f→ t) = (t ∈ f s)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -c;d→ u) = (∃t. s -c→ t ∧ t -d→ u)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -IF b THEN c ELSE d→ t) =
              (s -if b s then c else d→ t)"
apply(rule iffI)
 apply(auto elim: exec.cases intro:exec.intros)
apply(auto intro:exec.intros split:if_split_asm)
done

lemma [iff]: "(s -CALL p→ t) = (s -body p→ t)"
by(blast elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -LOCAL f; c; g→ u) = (∃t. f s -c→ t ∧ u = g s t)"
by(fastforce elim: exec.cases intro:exec.intros)

inductive
  execn :: "state ⇒ com ⇒ nat ⇒ state ⇒ bool"   ("_/ -_-_→/ _" [50,0,0,50] 50)
where
    Do:     "t ∈ f s ⟹ s -Do f-n→ t"

  | Semi:   "⟦ s0 -c0-n→ s1; s1 -c1-n→ s2 ⟧ ⟹ s0 -c0;c1-n→ s2"

  | IfTrue: "⟦ b s; s -c0-n→ t ⟧ ⟹ s -IF b THEN c0 ELSE c1-n→ t"

  | IfFalse: "⟦ ¬b s; s -c1-n→ t ⟧ ⟹ s -IF b THEN c0 ELSE c1-n→ t"

  | WhileFalse: "¬b s ⟹ s -WHILE b DO c-n→ s"

  | WhileTrue:  "⟦ b s; s -c-n→ t; t -WHILE b DO c-n→ u ⟧
                ⟹ s -WHILE b DO c-n→ u"

  | Call:  "s -body p-n→ t ⟹ s -CALL p-Suc n→ t"

  | Local: "f s -c-n→ t ⟹ s -LOCAL f; c; g-n→ g s t"

lemma [iff]: "(s -Do f-n→ t) = (t ∈ f s)"
by(auto elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -c1;c2-n→ u) = (∃t. s -c1-n→ t ∧ t -c2-n→ u)"
by(best elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -IF b THEN c ELSE d-n→ t) =
              (s -if b s then c else d-n→ t)"
apply auto
apply(blast elim: execn.cases intro:execn.intros)+
done

lemma [iff]: "(s -CALL p- 0→ t) = False"
by(blast elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -CALL p-Suc n→ t) = (s -body p-n→ t)"
by(blast elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -LOCAL f; c; g-n→ u) = (∃t. f s -c-n→ t ∧ u = g s t)"
by(auto elim: execn.cases intro:execn.intros)


lemma exec_mono[rule_format]: "s -c-m→ t ⟹ ∀n. m ≤ n ⟶ s -c-n→ t"
apply(erule execn.induct)
       apply(blast)
      apply(blast)
     apply(simp)
    apply(simp)
   apply(simp add:execn.intros)
  apply(blast intro:execn.intros)
 apply(clarify)
 apply(rename_tac m)
 apply(case_tac m)
  apply simp
 apply simp
apply blast
done

lemma exec_iff_execn: "(s -c→ t) = (∃n. s -c-n→ t)"
apply(rule iffI)
 apply(erule exec.induct)
        apply blast
       apply clarify
       apply(rename_tac m n)
       apply(rule_tac x = "max m n" in exI)
       apply(fastforce intro:exec.intros exec_mono simp add:max_def)
      apply fastforce
     apply fastforce
    apply(blast intro:execn.intros)
   apply clarify
   apply(rename_tac m n)
   apply(rule_tac x = "max m n" in exI)
   apply(fastforce elim:execn.WhileTrue exec_mono simp add:max_def)
  apply blast
 apply blast
apply(erule exE, erule execn.induct)
       apply blast
      apply blast
     apply fastforce
    apply fastforce
   apply(erule exec.WhileFalse)
  apply(blast intro: exec.intros)
 apply blast
apply blast
done

lemma while_lemma[rule_format]:
"s -w-n→ t ⟹ ∀b c. w = WHILE b DO c ∧ P s ∧
                    (∀s s'. P s ∧ b s ∧ s -c-n→ s' ⟶ P s') ⟶ P t ∧ ¬b t"
apply(erule execn.induct)
apply clarify+
defer
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast
done

lemma while_rule:
 "⟦s -WHILE b DO c-n→ t; P s; ⋀s s'. ⟦P s; b s; s -c-n→ s' ⟧ ⟹ P s'⟧
  ⟹ P t ∧ ¬b t"
apply(drule while_lemma)
prefer 2 apply assumption
apply blast
done

end