Theory PsLang

Up to index of Isabelle/HOL/Abstract-Hoare-Logics

theory PsLang
imports Main
(*  Title:       Mutually recursive procedures    Author:      Tobias Nipkow, 2001/2006    Maintainer:  Tobias Nipkow*)header "Hoare Logics for Mutually Recursive Procedure"theory PsLang imports Main beginsubsection{* The language *}typedecl statetypedecl pnametype_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 ofprocedures 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:split_if_asm)donelemma [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 autoapply(blast elim: execn.cases intro:execn.intros)+donelemma [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 simpapply blastdonelemma 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 blastapply(erule exE, erule execn.induct)       apply blast      apply blast     apply fastforce    apply fastforce   apply(erule exec.WhileFalse)  apply(blast intro: exec.intros) apply blastapply blastdonelemma 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+deferapply clarify+apply(subgoal_tac "P t")apply blastapply blastdonelemma 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 assumptionapply blastdoneend