Quelle Example.thy Sprache: Isabelle

(*  Title:      HOL/NanoJava/Example.thy
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

section "Example"

theory Example
imports Equivalence
begin

text \<open>

\begin{verbatim}
class Nat {

  Nat pred;

  Nat suc()
    { Nat n = new Nat(); n.pred = this; return n; }

  Nat eq(Nat n)
    { if (this.pred != null) if (n.pred != null) return this.pred.eq(n.pred);
                             else return n.pred; // false
      else if (n.pred != null) return this.pred; // false
           else return this.suc(); // true
    }

  Nat add(Nat n)
    { if (this.pred != null) return this.pred.add(n.suc()); else return n; }

  public static void main(String[] args) // test x+1=1+x
    {
        Nat one = new Nat().suc();
        Nat x   = new Nat().suc().suc().suc().suc();
        Nat ok = x.suc().eq(x.add(one));
        System.out.println(ok != null);
    }
}
\end{verbatim}

\<close>

axiomatization where
  This_neq_Par [simp]: "This \ Par" and
  Res_neq_This [simp]: "Res \ This"

subsection "Program representation"

axiomatization
  N    :: cname (\<open>Nat\<close>) (* with mixfix because of clash with NatDef.Nat *)
  and pred :: fname
  and suc add :: mname
  and any  :: vname

abbreviation
  dummy :: expr (\<open><>\<close>)
  where "<> == LAcc any"

abbreviation
  one :: expr
  where "one == {Nat}new Nat..suc(<>)"

text \<open>The following properties could be derived from a more complete
        program model, which we leave out for laziness.\<close>

axiomatization where Nat_no_subclasses [simp]: "D \C Nat = (D=Nat)"

axiomatization where method_Nat_add [simp]: "method Nat add = Some
  \<lparr> par=Class Nat, res=Class Nat, lcl=[],
   bdy= If((LAcc This..pred))
          (Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>)))
        Else Res :== LAcc Par \<rparr>"

axiomatization where method_Nat_suc [simp]: "method Nat suc = Some
  \<lparr> par=NT, res=Class Nat, lcl=[],
   bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>"

axiomatization where field_Nat [simp]: "field Nat = Map.empty(pred\Class Nat)"

lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s"
by (simp add: init_locs_def init_vars_def)

lemma init_locs_Nat_suc [simp]: "init_locs Nat suc s = s"
by (simp add: init_locs_def init_vars_def)

lemma upd_obj_new_obj_Nat [simp]:
  "upd_obj a pred v (new_obj a Nat s) = hupd(a\(Nat, Map.empty(pred\v))) s"
by (simp add: new_obj_def init_vars_def upd_obj_def Let_def)

subsection "``atleast'' relation for interpretation of Nat ``values''"

primrec Nat_atleast :: "state \ val \ nat \ bool" (\_:_ \ _\ [51, 51, 51] 50) where
  "s:x\0 = (x\Null)"
| "s:x\Suc n = (\a. x=Addr a \ heap s a \ None \ s:get_field s a pred\n)"

lemma Nat_atleast_lupd [rule_format, simp]:
"\s v::val. lupd(x\y) s:v \ n = (s:v \ n)"
apply (induct n)
by  auto

lemma Nat_atleast_set_locs [rule_format, simp]:
"\s v::val. set_locs l s:v \ n = (s:v \ n)"
apply (induct n)
by auto

lemma Nat_atleast_del_locs [rule_format, simp]:
"\s v::val. del_locs s:v \ n = (s:v \ n)"
apply (induct n)
by auto

lemma Nat_atleast_NullD [rule_format]: "s:Null \ n \ False"
apply (induct n)
by auto

lemma Nat_atleast_pred_NullD [rule_format]:
"Null = get_field s a pred \ s:Addr a \ n \ n = 0"
apply (induct n)
by (auto dest: Nat_atleast_NullD)

lemma Nat_atleast_mono [rule_format]:
"\a. s:get_field s a pred \ n \ heap s a \ None \ s:Addr a \ n"
apply (induct n)
by auto

lemma Nat_atleast_newC [rule_format]:
  "heap s aa = None \ \v::val. s:v \ n \ hupd(aa\obj) s:v \ n"
apply (induct n)
apply  auto
apply  (case_tac "aa=a")
apply   auto
apply (tactic "smp_tac \<^context> 1 1")
apply (case_tac "aa=a")
apply  auto
done

subsection "Proof(s) using the Hoare logic"

theorem add_homomorph_lb:
  "{} \ {\s. s:s \ X \ s:s \ Y} Meth(Nat,add) {\s. s:s \ X+Y}"
apply (rule hoare_ehoare.Meth) (* 1 *)
apply clarsimp
apply (rule_tac P'= "\Z s. (s:s \ fst Z \ s:s \ snd Z) \ D=Nat" and
        Q'= "\Z s. s:s \ fst Z+snd Z" in AxSem.Conseq)
prefer 2
apply  (clarsimp simp add: init_locs_def init_vars_def)
apply rule
apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
apply (rule_tac P = "\Z Cm s. s:s \ fst Z \ s:s \ snd Z" in AxSem.Impl1)
apply (clarsimp simp add: body_def)  (* 4 *)
apply (rename_tac n m)
apply (rule_tac Q = "\v s. (s:s \ n \ s:s \ m) \
        (\<exists>a. s<This> = Addr a \<and> v = get_field s a pred)" in hoare_ehoare.Cond)
apply  (rule hoare_ehoare.FAcc)
apply  (rule eConseq1)
apply   (rule hoare_ehoare.LAcc)
apply  fast
apply auto
prefer 2
apply  (rule hoare_ehoare.LAss)
apply  (rule eConseq1)
apply   (rule hoare_ehoare.LAcc)
apply  (auto dest: Nat_atleast_pred_NullD)
apply (rule hoare_ehoare.LAss)
apply (rule_tac
    Q = "\v s. (\m. n = Suc m \ s:v \ m) \ s:s \ m" and
    R = "\T P s. (\m. n = Suc m \ s:T \ m) \ s:P \ Suc m"
    in hoare_ehoare.Call) (* 13 *)
apply   (rule hoare_ehoare.FAcc)
apply   (rule eConseq1)
apply    (rule hoare_ehoare.LAcc)
apply   clarify
apply   (drule sym, rotate_tac -1, frule (1) trans)
apply   simp
prefer 2
apply  clarsimp
apply  (rule hoare_ehoare.Meth) (* 17 *)
apply  clarsimp
apply  (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
apply  (rule AxSem.Conseq)
apply   rule
apply   (rule hoare_ehoare.Asm) (* 20 *)
apply   (rule_tac a = "((case n of 0 \ 0 | Suc m \ m),m+1)" in UN_I, rule+)
apply  (clarsimp split: nat.split_asm dest!: Nat_atleast_mono)
apply rule
apply (rule hoare_ehoare.Call) (* 21 *)
apply   (rule hoare_ehoare.LAcc)
apply  rule
apply  (rule hoare_ehoare.LAcc)
apply clarify
apply (rule hoare_ehoare.Meth) (* 24 *)
apply clarsimp
apply  (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
apply (rule AxSem.Impl1)
apply (clarsimp simp add: body_def)
apply (rule hoare_ehoare.Comp) (* 26 *)
prefer 2
apply  (rule hoare_ehoare.FAss)
prefer 2
apply   rule
apply   (rule hoare_ehoare.LAcc)
apply  (rule hoare_ehoare.LAcc)
apply (rule hoare_ehoare.LAss)
apply (rule eConseq1)
apply  (rule hoare_ehoare.NewC) (* 32 *)
apply (auto dest!: new_AddrD elim: Nat_atleast_newC)
done

end

quality98%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.