src/HOL/IMP/Poly_Types.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 52046 bc01725d7918
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 theory Poly_Types imports Types begin
     2 
     3 subsection "Type Variables"
     4 
     5 datatype ty = Ity | Rty | TV nat
     6 
     7 text{* Everything else remains the same. *}
     8 
     9 type_synonym tyenv = "vname \<Rightarrow> ty"
    10 
    11 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
    12   ("(1_/ \<turnstile>p/ (_ :/ _))" [50,0,50] 50)
    13 where
    14 "\<Gamma> \<turnstile>p Ic i : Ity" |
    15 "\<Gamma> \<turnstile>p Rc r : Rty" |
    16 "\<Gamma> \<turnstile>p V x : \<Gamma> x" |
    17 "\<Gamma> \<turnstile>p a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p Plus a1 a2 : \<tau>"
    18 
    19 inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>p" 50)
    20 where
    21 "\<Gamma> \<turnstile>p Bc v" |
    22 "\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p Not b" |
    23 "\<Gamma> \<turnstile>p b1 \<Longrightarrow> \<Gamma> \<turnstile>p b2 \<Longrightarrow> \<Gamma> \<turnstile>p And b1 b2" |
    24 "\<Gamma> \<turnstile>p a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p Less a1 a2"
    25 
    26 inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>p" 50) where
    27 "\<Gamma> \<turnstile>p SKIP" |
    28 "\<Gamma> \<turnstile>p a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile>p x ::= a" |
    29 "\<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p c1;c2" |
    30 "\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p IF b THEN c1 ELSE c2" |
    31 "\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c \<Longrightarrow> \<Gamma> \<turnstile>p WHILE b DO c"
    32 
    33 fun type :: "val \<Rightarrow> ty" where
    34 "type (Iv i) = Ity" |
    35 "type (Rv r) = Rty"
    36 
    37 definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>p" 50)
    38 where "\<Gamma> \<turnstile>p s  \<longleftrightarrow>  (\<forall>x. type (s x) = \<Gamma> x)"
    39 
    40 fun tsubst :: "(nat \<Rightarrow> ty) \<Rightarrow> ty \<Rightarrow> ty" where
    41 "tsubst S (TV n) = S n" |
    42 "tsubst S t = t"
    43 
    44 
    45 subsection{* Typing is Preserved by Substitution *}
    46 
    47 lemma subst_atyping: "E \<turnstile>p a : t \<Longrightarrow> tsubst S \<circ> E \<turnstile>p a : tsubst S t"
    48 apply(induction rule: atyping.induct)
    49 apply(auto intro: atyping.intros)
    50 done
    51 
    52 lemma subst_btyping: "E \<turnstile>p (b::bexp) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p b"
    53 apply(induction rule: btyping.induct)
    54 apply(auto intro: btyping.intros)
    55 apply(drule subst_atyping[where S=S])
    56 apply(drule subst_atyping[where S=S])
    57 apply(simp add: o_def btyping.intros)
    58 done
    59 
    60 lemma subst_ctyping: "E \<turnstile>p (c::com) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p c"
    61 apply(induction rule: ctyping.induct)
    62 apply(auto intro: ctyping.intros)
    63 apply(drule subst_atyping[where S=S])
    64 apply(simp add: o_def ctyping.intros)
    65 apply(drule subst_btyping[where S=S])
    66 apply(simp add: o_def ctyping.intros)
    67 apply(drule subst_btyping[where S=S])
    68 apply(simp add: o_def ctyping.intros)
    69 done
    70 
    71 end