Theory PsTermi

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

subsection{*Termination*}

inductive
  termi :: "com => state => bool" (infixl "\<down>" 50)
where
    Do[iff]: "f s ≠ {} ==> Do f \<down> s"
  | Semi[intro!]:   "[| c1 \<down> s0; !!s1. s0 -c1-> s1 ==> c2 \<down> s1 |]
            ==> (c1;c2) \<down> s0"

  | IfTrue[intro,simp]: "[| b s; c1 \<down> s |] ==> IF b THEN c1 ELSE c2 \<down> s"
  | IfFalse[intro,simp]: "[| ¬b s; c2 \<down> s |] ==> IF b THEN c1 ELSE c2 \<down> s"

  | WhileFalse: "¬b s ==> WHILE b DO c \<down> s"

  | WhileTrue:  "[| b s; c \<down> s; !!t. s -c-> t ==> WHILE b DO c \<down> t |]
                ==> WHILE b DO c \<down> s"

  | "body p \<down> s ==> CALL p \<down> s"

  | Local: "c \<down> f s ==> LOCAL f;c;g \<down> s"

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

lemma [iff]: "((c1;c2) \<down> s0) = (c1 \<down> s0 ∧ (∀s1. s0 -c1-> s1 --> c2 \<down> 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 \<down> s) =
              ((if b s then c1 else c2) \<down> 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 p \<down> s) = (body p \<down> s)"
by(fast elim: termi.cases intro:termi.intros)

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

lemma termi_while_lemma[rule_format]:
 "w\<down>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) \<down> 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 \<down> 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