Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Com.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      ZF/IMP/Com.thy
    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
*)

section \<open>Arithmetic expressions, boolean expressions, commands\<close>

theory Com imports ZF begin

subsection \<open>Arithmetic expressions\<close>

consts
  loc :: i
  aexp :: i

datatype \<subseteq> "univ(loc \<union> (nat -> nat) \<union> ((nat \<times> nat) -> nat))"
  aexp = N ("n \ nat")
       | X ("x \ loc")
       | Op1 ("f \ nat -> nat", "a \ aexp")
       | Op2 ("f \ (nat \ nat) -> nat", "a0 \ aexp", "a1 \ aexp")

consts evala :: i

abbreviation
  evala_syntax :: "[i, i] => o"    (infixl \<open>-a->\<close> 50)
  where "p -a-> n == \ evala"

inductive
  domains "evala" \<subseteq> "(aexp \<times> (loc -> nat)) \<times> nat"
  intros
    N:   "[| n \ nat; sigma \ loc->nat |] ==> -a-> n"
    X:   "[| x \ loc; sigma \ loc->nat |] ==> -a-> sigma`x"
    Op1: "[| -a-> n; f \ nat -> nat |] ==> -a-> f`n"
    Op2: "[| -a-> n0; -a-> n1; f \ (nat\nat) -> nat |]
          ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
  type_intros aexp.intros apply_funtype

subsection \<open>Boolean expressions\<close>

consts bexp :: i

datatype \<subseteq> "univ(aexp \<union> ((nat \<times> nat)->bool))"
  bexp = true
       | false
       | ROp  ("f \ (nat \ nat)->bool", "a0 \ aexp", "a1 \ aexp")
       | noti ("b \ bexp")
       | andi ("b0 \ bexp", "b1 \ bexp") (infixl \andi\ 60)
       | ori  ("b0 \ bexp", "b1 \ bexp") (infixl \ori\ 60)

consts evalb :: i

abbreviation
  evalb_syntax :: "[i,i] => o"    (infixl \<open>-b->\<close> 50)
  where "p -b-> b == \ evalb"

inductive
  domains "evalb" \<subseteq> "(bexp \<times> (loc -> nat)) \<times> bool"
  intros
    true:  "[| sigma \ loc -> nat |] ==> -b-> 1"
    false: "[| sigma \ loc -> nat |] ==> -b-> 0"
    ROp:   "[| -a-> n0; -a-> n1; f \ (nat*nat)->bool |]
           ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
    noti:  "[| -b-> w |] ==> -b-> not(w)"
    andi:  "[| -b-> w0; -b-> w1 |]
          ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
    ori:   "[| -b-> w0; -b-> w1 |]
            ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
  type_intros  bexp.intros
               apply_funtype and_type or_type bool_1I bool_0I not_type
  type_elims   evala.dom_subset [THEN subsetD, elim_format]

subsection \<open>Commands\<close>

consts com :: i
datatype com =
    skip                                  (\<open>\<SKIP>\<close> [])
  | assignment ("x \ loc", "a \ aexp") (infixl \\\ 60)
  | semicolon ("c0 \ com", "c1 \ com") (\_\ _\ [60, 60] 10)
  | while ("b \ bexp", "c \ com") (\\ _ \ _\ 60)
  | "if" ("b \ bexp", "c0 \ com", "c1 \ com") (\\ _ \ _ \ _\ 60)

consts evalc :: i

abbreviation
  evalc_syntax :: "[i, i] => o"    (infixl \<open>-c->\<close> 50)
  where "p -c-> s == \ evalc"

inductive
  domains "evalc" \<subseteq> "(com \<times> (loc -> nat)) \<times> (loc -> nat)"
  intros
    skip:    "[| sigma \ loc -> nat |] ==> <\,sigma> -c-> sigma"

    assign:  "[| m \ nat; x \ loc; -a-> m |]
              ==> <x \<ASSN> a,sigma> -c-> sigma(x:=m)"

    semi:    "[| -c-> sigma2; -c-> sigma1 |]
              ==> <c0\<SEQ> c1, sigma> -c-> sigma1"

    if1:     "[| b \ bexp; c1 \ com; sigma \ loc->nat;
                 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |]
              ==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1"

    if0:     "[| b \ bexp; c0 \ com; sigma \ loc->nat;
                 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |]
               ==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1"

    while0:   "[| c \ com; -b-> 0 |]
               ==> <\<WHILE> b \<DO> c,sigma> -c-> sigma"

    while1:   "[| c \ com; -b-> 1; -c-> sigma2;
                  <\<WHILE> b \<DO> c, sigma2> -c-> sigma1 |]
               ==> <\<WHILE> b \<DO> c, sigma> -c-> sigma1"

  type_intros  com.intros update_type
  type_elims   evala.dom_subset [THEN subsetD, elim_format]
               evalb.dom_subset [THEN subsetD, elim_format]

subsection \<open>Misc lemmas\<close>

lemmas evala_1 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
  and evala_2 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
  and evala_3 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD2]

lemmas evalb_1 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
  and evalb_2 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
  and evalb_3 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD2]

lemmas evalc_1 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
  and evalc_2 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
  and evalc_3 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD2]

inductive_cases
    evala_N_E [elim!]: " -a-> i"
  and evala_X_E [elim!]: " -a-> i"
  and evala_Op1_E [elim!]: " -a-> i"
  and evala_Op2_E [elim!]: " -a-> i"

end

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.