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