Theory Termi

(*  Title:       Inductive definition of termination
    Author:      Tobias Nipkow, 2001/2006
    Maintainer:  Tobias Nipkow
*)

theory Termi imports Lang begin

subsection‹Termination›

text‹Although partial correctness appeals because of its simplicity,
in many cases one would like the additional assurance that the command
is guaranteed to termiate if started in a state that satisfies the
precondition. Even to express this we need to define when a command is
guaranteed to terminate. We can do this without modifying our existing
semantics by merely adding a second inductively defined judgement
‹c↓s› that expresses guaranteed termination of @{term c}
started in state @{term s}:›

inductive
  termi :: "com ⇒ state ⇒ bool" (infixl "↓" 50)
where
  (*<*)Do[iff]:(*>*) "f s ≠ {} ⟹ Do f ↓ s"

| (*<*)Semi[intro!]:(*>*) "⟦ c⇩1 ↓ s⇩0; ∀s⇩1. s⇩0 -c⇩1→ s⇩1 ⟶ c⇩2 ↓ s⇩1 ⟧ ⟹ (c⇩1;c⇩2) ↓ s⇩0"

| (*<*)IfT[intro,simp]:(*>*) "⟦  b s; c⇩1 ↓ s ⟧ ⟹ IF b THEN c⇩1 ELSE c⇩2 ↓ s"
| (*<*)IfF[intro,simp]:(*>*) "⟦ ¬b s; c⇩2 ↓ s ⟧ ⟹ IF b THEN c⇩1 ELSE c⇩2 ↓ s"

| (*<*)WhileFalse:(*>*) "¬b s ⟹ WHILE b DO c ↓ s"
| (*<*)WhileTrue:(*>*) "⟦ b s; c ↓ s; ∀t. s -c→ t ⟶ WHILE b DO c ↓ t ⟧ ⟹ WHILE b DO c ↓ s"

| (*<*)Local:(*>*) "c ↓ f s ⟹ LOCAL f;c;g ↓ s"


lemma [iff]: "Do f ↓ s = (f s ≠ {})"
apply(rule iffI)
 prefer 2
 apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "((c⇩1;c⇩2) ↓ s⇩0) = (c⇩1 ↓ s⇩0 ∧ (∀s⇩1. s⇩0 -c⇩1→ s⇩1 ⟶ c⇩2 ↓ s⇩1))"
apply(rule iffI)
 prefer 2
 apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done            

lemma [iff]: "(IF b THEN c⇩1 ELSE c⇩2 ↓ s) =
              ((if b s then c⇩1 else c⇩2) ↓ s)"
apply simp
apply(rule conjI)
apply(rule impI)
apply(rule iffI)
prefer 2
apply(blast intro:termi.intros)
apply(erule termi.cases)
apply blast+
apply(rule impI)
apply(rule iffI)
prefer 2
apply(blast intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "(LOCAL f;c;g ↓ s) = (c ↓ f s)"
by(fast elim: termi.cases intro:termi.intros)

lemma termi_while_lemma[rule_format]:
 "w↓fk ⟹
 (∀k b c. fk = f k ∧ w = WHILE b DO c ∧ (∀i. f i -c→ f(Suc i))
          ⟶ (∃i. ¬b(f i)))"
apply(erule termi.induct)
apply simp_all
apply blast
apply blast
done

lemma termi_while:
 "⟦ (WHILE b DO c) ↓ f k;  ∀i. f i -c→ f(Suc i) ⟧ ⟹ ∃i. ¬b(f i)"
by(blast intro:termi_while_lemma)

lemma wf_termi: "wf {(t,s). WHILE b DO c ↓ s ∧ b s ∧ s -c→ t}"
apply(subst wf_iff_no_infinite_down_chain)
apply(rule notI)
apply clarsimp
apply(insert termi_while)
apply blast
done

end