src/HOL/IMP/Types.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 47818 151d137f1095
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 header "A Typed Language"
     2 
     3 theory Types imports Star Complex_Main begin
     4 
     5 subsection "Arithmetic Expressions"
     6 
     7 datatype val = Iv int | Rv real
     8 
     9 type_synonym vname = string
    10 type_synonym state = "vname \<Rightarrow> val"
    11 
    12 datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
    13 
    14 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
    15 "taval (Ic i) s (Iv i)" |
    16 "taval (Rc r) s (Rv r)" |
    17 "taval (V x) s (s x)" |
    18 "taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2)
    19  \<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
    20 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
    21  \<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
    22 
    23 inductive_cases [elim!]:
    24   "taval (Ic i) s v"  "taval (Rc i) s v"
    25   "taval (V x) s v"
    26   "taval (Plus a1 a2) s v"
    27 
    28 subsection "Boolean Expressions"
    29 
    30 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
    31 
    32 inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
    33 "tbval (Bc v) s v" |
    34 "tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
    35 "tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
    36 "taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
    37 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
    38 
    39 subsection "Syntax of Commands"
    40 (* a copy of Com.thy - keep in sync! *)
    41 
    42 datatype
    43   com = SKIP 
    44       | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
    45       | Semi   com  com          ("_; _"  [60, 61] 60)
    46       | If     bexp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
    47       | While  bexp com         ("WHILE _ DO _"  [0, 61] 61)
    48 
    49 
    50 subsection "Small-Step Semantics of Commands"
    51 
    52 inductive
    53   small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
    54 where
    55 Assign:  "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
    56 
    57 Semi1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
    58 Semi2:   "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" |
    59 
    60 IfTrue:  "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
    61 IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
    62 
    63 While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
    64 
    65 lemmas small_step_induct = small_step.induct[split_format(complete)]
    66 
    67 subsection "The Type System"
    68 
    69 datatype ty = Ity | Rty
    70 
    71 type_synonym tyenv = "vname \<Rightarrow> ty"
    72 
    73 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
    74   ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
    75 where
    76 Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity" |
    77 Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
    78 V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
    79 Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
    80 
    81 text{* Warning: the ``:'' notation leads to syntactic ambiguities,
    82 i.e. multiple parse trees, because ``:'' also stands for set membership.
    83 In most situations Isabelle's type system will reject all but one parse tree,
    84 but will still inform you of the potential ambiguity. *}
    85 
    86 inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
    87 where
    88 B_ty: "\<Gamma> \<turnstile> Bc v" |
    89 Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
    90 And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
    91 Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
    92 
    93 inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
    94 Skip_ty: "\<Gamma> \<turnstile> SKIP" |
    95 Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
    96 Semi_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
    97 If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
    98 While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
    99 
   100 inductive_cases [elim!]:
   101   "\<Gamma> \<turnstile> x ::= a"  "\<Gamma> \<turnstile> c1;c2"
   102   "\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
   103   "\<Gamma> \<turnstile> WHILE b DO c"
   104 
   105 subsection "Well-typed Programs Do Not Get Stuck"
   106 
   107 fun type :: "val \<Rightarrow> ty" where
   108 "type (Iv i) = Ity" |
   109 "type (Rv r) = Rty"
   110 
   111 lemma [simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
   112 by (cases v) simp_all
   113 
   114 lemma [simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
   115 by (cases v) simp_all
   116 
   117 definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50)
   118 where "\<Gamma> \<turnstile> s  \<longleftrightarrow>  (\<forall>x. type (s x) = \<Gamma> x)"
   119 
   120 lemma apreservation:
   121   "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
   122 apply(induction arbitrary: v rule: atyping.induct)
   123 apply (fastforce simp: styping_def)+
   124 done
   125 
   126 lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
   127 proof(induction rule: atyping.induct)
   128   case (Plus_ty \<Gamma> a1 t a2)
   129   then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
   130   show ?case
   131   proof (cases v1)
   132     case Iv
   133     with Plus_ty v show ?thesis
   134       by(fastforce intro: taval.intros(4) dest!: apreservation)
   135   next
   136     case Rv
   137     with Plus_ty v show ?thesis
   138       by(fastforce intro: taval.intros(5) dest!: apreservation)
   139   qed
   140 qed (auto intro: taval.intros)
   141 
   142 lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
   143 proof(induction rule: btyping.induct)
   144   case (Less_ty \<Gamma> a1 t a2)
   145   then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
   146     by (metis aprogress)
   147   show ?case
   148   proof (cases v1)
   149     case Iv
   150     with Less_ty v show ?thesis
   151       by (fastforce intro!: tbval.intros(4) dest!:apreservation)
   152   next
   153     case Rv
   154     with Less_ty v show ?thesis
   155       by (fastforce intro!: tbval.intros(5) dest!:apreservation)
   156   qed
   157 qed (auto intro: tbval.intros)
   158 
   159 theorem progress:
   160   "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
   161 proof(induction rule: ctyping.induct)
   162   case Skip_ty thus ?case by simp
   163 next
   164   case Assign_ty 
   165   thus ?case by (metis Assign aprogress)
   166 next
   167   case Semi_ty thus ?case by simp (metis Semi1 Semi2)
   168 next
   169   case (If_ty \<Gamma> b c1 c2)
   170   then obtain bv where "tbval b s bv" by (metis bprogress)
   171   show ?case
   172   proof(cases bv)
   173     assume "bv"
   174     with `tbval b s bv` show ?case by simp (metis IfTrue)
   175   next
   176     assume "\<not>bv"
   177     with `tbval b s bv` show ?case by simp (metis IfFalse)
   178   qed
   179 next
   180   case While_ty show ?case by (metis While)
   181 qed
   182 
   183 theorem styping_preservation:
   184   "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
   185 proof(induction rule: small_step_induct)
   186   case Assign thus ?case
   187     by (auto simp: styping_def) (metis Assign(1,3) apreservation)
   188 qed auto
   189 
   190 theorem ctyping_preservation:
   191   "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> c'"
   192 by (induct rule: small_step_induct) (auto simp: ctyping.intros)
   193 
   194 abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
   195 where "x \<rightarrow>* y == star small_step x y"
   196 
   197 theorem type_sound:
   198   "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
   199    \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
   200 apply(induction rule:star_induct)
   201 apply (metis progress)
   202 by (metis styping_preservation ctyping_preservation)
   203 
   204 end