Theory PTermi

(*  Title:      Inductive definition of termination
    Author:      Tobias Nipkow, 2001/2006
    Maintainer:  Tobias Nipkow
*)
theory PTermi imports PLang begin

subsection‹Termination›

inductive
  termi :: "com ⇒ state ⇒ bool" (infixl ‹↓› 50)
where
  Do[iff]: "f s ≠ {} ⟹ Do f ↓ s"
| Semi[intro!]:   "⟦ c1 ↓ s0; ⋀s1. s0 -c1→ s1 ⟹ c2 ↓ s1 ⟧
            ⟹ (c1;c2) ↓ s0"

| IfTrue[intro,simp]: "⟦ b s; c1 ↓ s ⟧ ⟹ IF b THEN c1 ELSE c2 ↓ s"
| IfFalse[intro,simp]: "⟦ ¬b s; c2 ↓ s ⟧ ⟹ IF b THEN c1 ELSE c2 ↓ 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"
| "body ↓ s ⟹ CALL ↓ 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]: "((c1;c2) ↓ s0) = (c1 ↓ s0 ∧ (∀s1. s0 -c1→ s1 ⟶ c2 ↓ s1))"
apply(rule iffI)
 prefer 2
 apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "(IF b THEN c1 ELSE c2 ↓ s) =
              ((if b s then c1 else c2) ↓ 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]: "(CALL ↓ s) = (body ↓ s)"
by(fast elim: termi.cases intro:termi.intros)

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