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