src/HOL/IMP/Poly_Types.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45212 e87feee00a4c
child 52046 bc01725d7918
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43150
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
     1
theory Poly_Types imports Types begin
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
     2
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
     3
subsection "Type Variables"
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
     4
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
     5
datatype ty = Ity | Rty | TV nat
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
     6
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
     7
text{* Everything else remains the same. *}
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
     8
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45200
diff changeset
     9
type_synonym tyenv = "vname \<Rightarrow> ty"
43150
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    10
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    11
inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    12
  ("(1_/ \<turnstile>p/ (_ :/ _))" [50,0,50] 50)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    13
where
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    14
"\<Gamma> \<turnstile>p Ic i : Ity" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    15
"\<Gamma> \<turnstile>p Rc r : Rty" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    16
"\<Gamma> \<turnstile>p V x : \<Gamma> x" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    17
"\<Gamma> \<turnstile>p a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p Plus a1 a2 : \<tau>"
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    18
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    19
inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>p" 50)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    20
where
45200
1f1897ac7877 renamed B to Bc
nipkow
parents: 45015
diff changeset
    21
"\<Gamma> \<turnstile>p Bc v" |
43150
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    22
"\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p Not b" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    23
"\<Gamma> \<turnstile>p b1 \<Longrightarrow> \<Gamma> \<turnstile>p b2 \<Longrightarrow> \<Gamma> \<turnstile>p And b1 b2" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    24
"\<Gamma> \<turnstile>p a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p Less a1 a2"
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    25
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    26
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>p" 50) where
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    27
"\<Gamma> \<turnstile>p SKIP" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    28
"\<Gamma> \<turnstile>p a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile>p x ::= a" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    29
"\<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p c1;c2" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    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" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    31
"\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c \<Longrightarrow> \<Gamma> \<turnstile>p WHILE b DO c"
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    32
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    33
fun type :: "val \<Rightarrow> ty" where
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    34
"type (Iv i) = Ity" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    35
"type (Rv r) = Rty"
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    36
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    37
definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>p" 50)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    38
where "\<Gamma> \<turnstile>p s  \<longleftrightarrow>  (\<forall>x. type (s x) = \<Gamma> x)"
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    39
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    40
fun tsubst :: "(nat \<Rightarrow> ty) \<Rightarrow> ty \<Rightarrow> ty" where
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    41
"tsubst S (TV n) = S n" |
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    42
"tsubst S t = t"
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    43
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    44
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    45
subsection{* Typing is Preserved by Substitution *}
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    46
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    47
lemma subst_atyping: "E \<turnstile>p a : t \<Longrightarrow> tsubst S \<circ> E \<turnstile>p a : tsubst S t"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43150
diff changeset
    48
apply(induction rule: atyping.induct)
43150
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    49
apply(auto intro: atyping.intros)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    50
done
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    51
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    52
lemma subst_btyping: "E \<turnstile>p (b::bexp) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p b"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43150
diff changeset
    53
apply(induction rule: btyping.induct)
43150
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    54
apply(auto intro: btyping.intros)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    55
apply(drule subst_atyping[where S=S])
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    56
apply(drule subst_atyping[where S=S])
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    57
apply(simp add: o_def btyping.intros)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    58
done
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    59
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    60
lemma subst_ctyping: "E \<turnstile>p (c::com) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p c"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43150
diff changeset
    61
apply(induction rule: ctyping.induct)
43150
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    62
apply(auto intro: ctyping.intros)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    63
apply(drule subst_atyping[where S=S])
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    64
apply(simp add: o_def ctyping.intros)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    65
apply(drule subst_btyping[where S=S])
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    66
apply(simp add: o_def ctyping.intros)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    67
apply(drule subst_btyping[where S=S])
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    68
apply(simp add: o_def ctyping.intros)
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    69
done
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    70
69bc4dafcc53 Added typed IMP
nipkow
parents:
diff changeset
    71
end