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
@{text"c\<down>s"} that expresses guaranteed termination of @{term c}
started in state @{term s}: *}
inductive
termi :: "com => state => bool" (infixl "\<down>" 50)
where
Do[iff]: "f s ≠ {} ==> Do f \<down> s"
| Semi[intro!]: "[| c⇣1 \<down> s⇣0; ∀s⇣1. s⇣0 -c⇣1-> s⇣1 --> c⇣2 \<down> s⇣1 |] ==> (c⇣1;c⇣2) \<down> s⇣0"
| IfT[intro,simp]: "[| b s; c⇣1 \<down> s |] ==> IF b THEN c⇣1 ELSE c⇣2 \<down> s"
| IfF[intro,simp]: "[| ¬b s; c⇣2 \<down> s |] ==> IF b THEN c⇣1 ELSE c⇣2 \<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"
| 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]: "((c⇣1;c⇣2) \<down> s⇣0) = (c⇣1 \<down> s⇣0 ∧ (∀s⇣1. s⇣0 -c⇣1-> s⇣1 --> c⇣2 \<down> 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 \<down> s) =
((if b s then c⇣1 else c⇣2) \<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]: "(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