src/HOL/ex/MT.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 24326 3e9d3ba894b8
child 41460 ea56b98aee83
permissions -rw-r--r--
added lemmas
wenzelm@24326
     1
(*  Title:      HOL/ex/MT.thy
clasohm@969
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
clasohm@969
     4
    Copyright   1993  University of Cambridge
clasohm@969
     5
clasohm@969
     6
Based upon the article
clasohm@969
     7
    Robin Milner and Mads Tofte,
clasohm@969
     8
    Co-induction in Relational Semantics,
clasohm@969
     9
    Theoretical Computer Science 87 (1991), pages 209-220.
clasohm@969
    10
clasohm@969
    11
Written up as
clasohm@969
    12
    Jacob Frost, A Case Study of Co_induction in Isabelle/HOL
clasohm@969
    13
    Report 308, Computer Lab, University of Cambridge (1993).
clasohm@969
    14
*)
clasohm@969
    15
wenzelm@24326
    16
header {* Milner-Tofte: Co-induction in Relational Semantics *}
wenzelm@24326
    17
wenzelm@17289
    18
theory MT
wenzelm@17289
    19
imports Main
wenzelm@17289
    20
begin
clasohm@969
    21
wenzelm@17289
    22
typedecl Const
clasohm@969
    23
wenzelm@17289
    24
typedecl ExVar
wenzelm@17289
    25
typedecl Ex
clasohm@969
    26
wenzelm@17289
    27
typedecl TyConst
wenzelm@17289
    28
typedecl Ty
clasohm@969
    29
wenzelm@17289
    30
typedecl Clos
wenzelm@17289
    31
typedecl Val
clasohm@969
    32
wenzelm@17289
    33
typedecl ValEnv
wenzelm@17289
    34
typedecl TyEnv
clasohm@969
    35
clasohm@969
    36
consts
paulson@15450
    37
  c_app :: "[Const, Const] => Const"
clasohm@969
    38
paulson@15450
    39
  e_const :: "Const => Ex"
paulson@15450
    40
  e_var :: "ExVar => Ex"
paulson@15450
    41
  e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
paulson@15450
    42
  e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
wenzelm@17289
    43
  e_app :: "[Ex, Ex] => Ex" ("_ @@ _" [51,51] 1000)
paulson@15450
    44
  e_const_fst :: "Ex => Const"
clasohm@969
    45
paulson@15450
    46
  t_const :: "TyConst => Ty"
paulson@15450
    47
  t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
clasohm@969
    48
paulson@15450
    49
  v_const :: "Const => Val"
paulson@15450
    50
  v_clos :: "Clos => Val"
wenzelm@17289
    51
clasohm@1376
    52
  ve_emp :: ValEnv
paulson@15450
    53
  ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
paulson@15450
    54
  ve_dom :: "ValEnv => ExVar set"
paulson@15450
    55
  ve_app :: "[ValEnv, ExVar] => Val"
clasohm@969
    56
paulson@15450
    57
  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
clasohm@969
    58
clasohm@1376
    59
  te_emp :: TyEnv
paulson@15450
    60
  te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
paulson@15450
    61
  te_app :: "[TyEnv, ExVar] => Ty"
paulson@15450
    62
  te_dom :: "TyEnv => ExVar set"
clasohm@969
    63
clasohm@969
    64
  eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
clasohm@969
    65
  eval_rel :: "((ValEnv * Ex) * Val) set"
paulson@15450
    66
  eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
clasohm@969
    67
clasohm@969
    68
  elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
clasohm@969
    69
  elab_rel :: "((TyEnv * Ex) * Ty) set"
paulson@15450
    70
  elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
wenzelm@17289
    71
paulson@15450
    72
  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
paulson@15450
    73
  isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
clasohm@969
    74
clasohm@969
    75
  hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
clasohm@969
    76
  hasty_rel :: "(Val * Ty) set"
paulson@15450
    77
  hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
paulson@15450
    78
  hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
clasohm@969
    79
wenzelm@17289
    80
axioms
clasohm@969
    81
wenzelm@17289
    82
(*
clasohm@969
    83
  Expression constructors must be injective, distinct and it must be possible
clasohm@969
    84
  to do induction over expressions.
clasohm@969
    85
*)
clasohm@969
    86
clasohm@969
    87
(* All the constructors are injective *)
clasohm@969
    88
wenzelm@17289
    89
  e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2"
wenzelm@17289
    90
  e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
wenzelm@17289
    91
  e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
wenzelm@17289
    92
  e_fix_inj:
wenzelm@17289
    93
    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
wenzelm@17289
    94
     ev11 = ev21 & ev12 = ev22 & e1 = e2
clasohm@1151
    95
   "
wenzelm@17289
    96
  e_app_inj: "e11 @@ e12 = e21 @@ e22 ==> e11 = e21 & e12 = e22"
clasohm@969
    97
clasohm@969
    98
(* All constructors are distinct *)
clasohm@969
    99
wenzelm@17289
   100
  e_disj_const_var: "~e_const(c) = e_var(ev)"
wenzelm@17289
   101
  e_disj_const_fn: "~e_const(c) = fn ev => e"
wenzelm@17289
   102
  e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e"
wenzelm@17289
   103
  e_disj_const_app: "~e_const(c) = e1 @@ e2"
wenzelm@17289
   104
  e_disj_var_fn: "~e_var(ev1) = fn ev2 => e"
wenzelm@17289
   105
  e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e"
wenzelm@17289
   106
  e_disj_var_app: "~e_var(ev) = e1 @@ e2"
wenzelm@17289
   107
  e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2"
wenzelm@17289
   108
  e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22"
wenzelm@17289
   109
  e_disj_fix_app: "~fix ev11(ev12) = e1 = e21 @@ e22"
clasohm@969
   110
clasohm@969
   111
(* Strong elimination, induction on expressions  *)
clasohm@969
   112
wenzelm@17289
   113
  e_ind:
wenzelm@17289
   114
    " [|  !!ev. P(e_var(ev));
wenzelm@17289
   115
         !!c. P(e_const(c));
wenzelm@17289
   116
         !!ev e. P(e) ==> P(fn ev => e);
wenzelm@17289
   117
         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e);
wenzelm@17289
   118
         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @@ e2)
wenzelm@17289
   119
     |] ==>
wenzelm@17289
   120
   P(e)
clasohm@1151
   121
   "
clasohm@969
   122
clasohm@969
   123
(* Types - same scheme as for expressions *)
clasohm@969
   124
wenzelm@17289
   125
(* All constructors are injective *)
clasohm@969
   126
wenzelm@17289
   127
  t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2"
wenzelm@17289
   128
  t_fun_inj: "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22"
clasohm@969
   129
clasohm@969
   130
(* All constructors are distinct, not needed so far ... *)
clasohm@969
   131
clasohm@969
   132
(* Strong elimination, induction on types *)
clasohm@969
   133
wenzelm@17289
   134
 t_ind:
wenzelm@17289
   135
    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |]
clasohm@1151
   136
    ==> P(t)"
clasohm@969
   137
clasohm@969
   138
clasohm@969
   139
(* Values - same scheme again *)
clasohm@969
   140
wenzelm@17289
   141
(* All constructors are injective *)
clasohm@969
   142
wenzelm@17289
   143
  v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2"
wenzelm@17289
   144
  v_clos_inj:
wenzelm@17289
   145
    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
clasohm@1151
   146
     ev1 = ev2 & e1 = e2 & ve1 = ve2"
wenzelm@17289
   147
clasohm@969
   148
(* All constructors are distinct *)
clasohm@969
   149
wenzelm@17289
   150
  v_disj_const_clos: "~v_const(c) = v_clos(cl)"
clasohm@969
   151
paulson@15450
   152
(* No induction on values: they are a codatatype! ... *)
clasohm@969
   153
clasohm@969
   154
wenzelm@17289
   155
(*
clasohm@969
   156
  Value environments bind variables to values. Only the following trivial
clasohm@969
   157
  properties are needed.
clasohm@969
   158
*)
clasohm@969
   159
wenzelm@17289
   160
  ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}"
wenzelm@17289
   161
wenzelm@17289
   162
  ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v"
wenzelm@17289
   163
  ve_app_owr2: "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2"
clasohm@969
   164
clasohm@969
   165
clasohm@969
   166
(* Type Environments bind variables to types. The following trivial
clasohm@969
   167
properties are needed.  *)
clasohm@969
   168
wenzelm@17289
   169
  te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}"
wenzelm@17289
   170
wenzelm@17289
   171
  te_app_owr1: "te_app (te + {ev |=> t}) ev=t"
wenzelm@17289
   172
  te_app_owr2: "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2"
clasohm@969
   173
clasohm@969
   174
clasohm@969
   175
(* The dynamic semantics is defined inductively by a set of inference
clasohm@969
   176
rules.  These inference rules allows one to draw conclusions of the form ve
clasohm@969
   177
|- e ---> v, read the expression e evaluates to the value v in the value
clasohm@969
   178
environment ve.  Therefore the relation _ |- _ ---> _ is defined in Isabelle
clasohm@969
   179
as the least fixpoint of the functor eval_fun below.  From this definition
clasohm@969
   180
introduction rules and a strong elimination (induction) rule can be
wenzelm@17289
   181
derived.
clasohm@969
   182
*)
clasohm@969
   183
wenzelm@17289
   184
defs
wenzelm@17289
   185
  eval_fun_def:
wenzelm@17289
   186
    " eval_fun(s) ==
wenzelm@17289
   187
     { pp.
wenzelm@17289
   188
       (? ve c. pp=((ve,e_const(c)),v_const(c))) |
clasohm@1151
   189
       (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
wenzelm@17289
   190
       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))|
wenzelm@17289
   191
       ( ? ve e x f cl.
wenzelm@17289
   192
           pp=((ve,fix f(x) = e),v_clos(cl)) &
wenzelm@17289
   193
           cl=<|x, e, ve+{f |-> v_clos(cl)} |>
wenzelm@17289
   194
       ) |
wenzelm@17289
   195
       ( ? ve e1 e2 c1 c2.
wenzelm@17289
   196
           pp=((ve,e1 @@ e2),v_const(c_app c1 c2)) &
wenzelm@17289
   197
           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s
wenzelm@17289
   198
       ) |
wenzelm@17289
   199
       ( ? ve vem e1 e2 em xm v v2.
wenzelm@17289
   200
           pp=((ve,e1 @@ e2),v) &
wenzelm@17289
   201
           ((ve,e1),v_clos(<|xm,em,vem|>)):s &
wenzelm@17289
   202
           ((ve,e2),v2):s &
wenzelm@17289
   203
           ((vem+{xm |-> v2},em),v):s
wenzelm@17289
   204
       )
clasohm@1151
   205
     }"
clasohm@969
   206
wenzelm@17289
   207
  eval_rel_def: "eval_rel == lfp(eval_fun)"
wenzelm@17289
   208
  eval_def: "ve |- e ---> v == ((ve,e),v):eval_rel"
clasohm@969
   209
clasohm@969
   210
(* The static semantics is defined in the same way as the dynamic
clasohm@969
   211
semantics.  The relation te |- e ===> t express the expression e has the
clasohm@969
   212
type t in the type environment te.
clasohm@969
   213
*)
clasohm@969
   214
wenzelm@17289
   215
  elab_fun_def:
wenzelm@17289
   216
  "elab_fun(s) ==
wenzelm@17289
   217
  { pp.
wenzelm@17289
   218
    (? te c t. pp=((te,e_const(c)),t) & c isof t) |
wenzelm@17289
   219
    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
wenzelm@17289
   220
    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
wenzelm@17289
   221
    (? te f x e t1 t2.
wenzelm@17289
   222
       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
wenzelm@17289
   223
    ) |
wenzelm@17289
   224
    (? te e1 e2 t1 t2.
wenzelm@17289
   225
       pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
wenzelm@17289
   226
    )
clasohm@1151
   227
  }"
clasohm@969
   228
wenzelm@17289
   229
  elab_rel_def: "elab_rel == lfp(elab_fun)"
wenzelm@17289
   230
  elab_def: "te |- e ===> t == ((te,e),t):elab_rel"
clasohm@969
   231
clasohm@969
   232
(* The original correspondence relation *)
clasohm@969
   233
wenzelm@17289
   234
  isof_env_def:
wenzelm@17289
   235
    " ve isofenv te ==
wenzelm@17289
   236
     ve_dom(ve) = te_dom(te) &
wenzelm@17289
   237
     ( ! x.
wenzelm@17289
   238
         x:ve_dom(ve) -->
wenzelm@17289
   239
         (? c. ve_app ve x = v_const(c) & c isof te_app te x)
wenzelm@17289
   240
     )
clasohm@1151
   241
   "
clasohm@969
   242
wenzelm@17289
   243
axioms
wenzelm@17289
   244
  isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
clasohm@969
   245
wenzelm@17289
   246
defs
clasohm@969
   247
(* The extented correspondence relation *)
clasohm@969
   248
wenzelm@17289
   249
  hasty_fun_def:
wenzelm@17289
   250
    " hasty_fun(r) ==
wenzelm@17289
   251
     { p.
wenzelm@17289
   252
       ( ? c t. p = (v_const(c),t) & c isof t) |
wenzelm@17289
   253
       ( ? ev e ve t te.
wenzelm@17289
   254
           p = (v_clos(<|ev,e,ve|>),t) &
wenzelm@17289
   255
           te |- fn ev => e ===> t &
wenzelm@17289
   256
           ve_dom(ve) = te_dom(te) &
wenzelm@17289
   257
           (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
wenzelm@17289
   258
       )
wenzelm@17289
   259
     }
clasohm@1151
   260
   "
clasohm@969
   261
wenzelm@17289
   262
  hasty_rel_def: "hasty_rel == gfp(hasty_fun)"
wenzelm@17289
   263
  hasty_def: "v hasty t == (v,t) : hasty_rel"
wenzelm@17289
   264
  hasty_env_def:
wenzelm@17289
   265
    " ve hastyenv te ==
wenzelm@17289
   266
     ve_dom(ve) = te_dom(te) &
clasohm@1151
   267
     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
clasohm@969
   268
wenzelm@24326
   269
wenzelm@24326
   270
(* ############################################################ *)
wenzelm@24326
   271
(* Inference systems                                            *)
wenzelm@24326
   272
(* ############################################################ *)
wenzelm@24326
   273
wenzelm@24326
   274
ML {*
wenzelm@24326
   275
val infsys_mono_tac = REPEAT (ares_tac (@{thms basic_monos} @ [allI, impI]) 1)
wenzelm@24326
   276
*}
wenzelm@24326
   277
wenzelm@24326
   278
lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))"
wenzelm@24326
   279
  by simp
wenzelm@24326
   280
wenzelm@24326
   281
lemma infsys_p2: "P (fst (a,b)) (snd (a,b)) ==> P a b"
wenzelm@24326
   282
  by simp
wenzelm@24326
   283
wenzelm@24326
   284
lemma infsys_pp1: "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))"
wenzelm@24326
   285
  by simp
wenzelm@24326
   286
wenzelm@24326
   287
lemma infsys_pp2: "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c"
wenzelm@24326
   288
  by simp
wenzelm@24326
   289
wenzelm@24326
   290
wenzelm@24326
   291
(* ############################################################ *)
wenzelm@24326
   292
(* Fixpoints                                                    *)
wenzelm@24326
   293
(* ############################################################ *)
wenzelm@24326
   294
wenzelm@24326
   295
(* Least fixpoints *)
wenzelm@24326
   296
wenzelm@24326
   297
lemma lfp_intro2: "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)"
wenzelm@24326
   298
apply (rule subsetD)
wenzelm@24326
   299
apply (rule lfp_lemma2)
wenzelm@24326
   300
apply assumption+
wenzelm@24326
   301
done
wenzelm@24326
   302
wenzelm@24326
   303
lemma lfp_elim2:
wenzelm@24326
   304
  assumes lfp: "x:lfp(f)"
wenzelm@24326
   305
    and mono: "mono(f)"
wenzelm@24326
   306
    and r: "!!y. y:f(lfp(f)) ==> P(y)"
wenzelm@24326
   307
  shows "P(x)"
wenzelm@24326
   308
apply (rule r)
wenzelm@24326
   309
apply (rule subsetD)
wenzelm@24326
   310
apply (rule lfp_lemma3)
wenzelm@24326
   311
apply (rule mono)
wenzelm@24326
   312
apply (rule lfp)
wenzelm@24326
   313
done
wenzelm@24326
   314
wenzelm@24326
   315
lemma lfp_ind2:
wenzelm@24326
   316
  assumes lfp: "x:lfp(f)"
wenzelm@24326
   317
    and mono: "mono(f)"
wenzelm@24326
   318
    and r: "!!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y)"
wenzelm@24326
   319
  shows "P(x)"
wenzelm@24326
   320
apply (rule lfp_induct_set [OF lfp mono])
wenzelm@24326
   321
apply (erule r)
wenzelm@24326
   322
done
wenzelm@24326
   323
wenzelm@24326
   324
(* Greatest fixpoints *)
wenzelm@24326
   325
wenzelm@24326
   326
(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
wenzelm@24326
   327
wenzelm@24326
   328
lemma gfp_coind2:
wenzelm@24326
   329
  assumes cih: "x:f({x} Un gfp(f))"
wenzelm@24326
   330
    and monoh: "mono(f)"
wenzelm@24326
   331
  shows "x:gfp(f)"
wenzelm@24326
   332
apply (rule cih [THEN [2] gfp_upperbound [THEN subsetD]])
wenzelm@24326
   333
apply (rule monoh [THEN monoD])
wenzelm@24326
   334
apply (rule UnE [THEN subsetI])
wenzelm@24326
   335
apply assumption
wenzelm@24326
   336
apply (blast intro!: cih)
wenzelm@24326
   337
apply (rule monoh [THEN monoD [THEN subsetD]])
wenzelm@24326
   338
apply (rule Un_upper2)
wenzelm@24326
   339
apply (erule monoh [THEN gfp_lemma2, THEN subsetD])
wenzelm@24326
   340
done
wenzelm@24326
   341
wenzelm@24326
   342
lemma gfp_elim2:
wenzelm@24326
   343
  assumes gfph: "x:gfp(f)"
wenzelm@24326
   344
    and monoh: "mono(f)"
wenzelm@24326
   345
    and caseh: "!!y. y:f(gfp(f)) ==> P(y)"
wenzelm@24326
   346
  shows "P(x)"
wenzelm@24326
   347
apply (rule caseh)
wenzelm@24326
   348
apply (rule subsetD)
wenzelm@24326
   349
apply (rule gfp_lemma2)
wenzelm@24326
   350
apply (rule monoh)
wenzelm@24326
   351
apply (rule gfph)
wenzelm@24326
   352
done
wenzelm@24326
   353
wenzelm@24326
   354
(* ############################################################ *)
wenzelm@24326
   355
(* Expressions                                                  *)
wenzelm@24326
   356
(* ############################################################ *)
wenzelm@24326
   357
wenzelm@24326
   358
lemmas e_injs = e_const_inj e_var_inj e_fn_inj e_fix_inj e_app_inj
wenzelm@24326
   359
wenzelm@24326
   360
lemmas e_disjs =
wenzelm@24326
   361
  e_disj_const_var
wenzelm@24326
   362
  e_disj_const_fn
wenzelm@24326
   363
  e_disj_const_fix
wenzelm@24326
   364
  e_disj_const_app
wenzelm@24326
   365
  e_disj_var_fn
wenzelm@24326
   366
  e_disj_var_fix
wenzelm@24326
   367
  e_disj_var_app
wenzelm@24326
   368
  e_disj_fn_fix
wenzelm@24326
   369
  e_disj_fn_app
wenzelm@24326
   370
  e_disj_fix_app
wenzelm@24326
   371
wenzelm@24326
   372
lemmas e_disj_si = e_disjs  e_disjs [symmetric]
wenzelm@24326
   373
wenzelm@24326
   374
lemmas e_disj_se = e_disj_si [THEN notE]
wenzelm@24326
   375
wenzelm@24326
   376
(* ############################################################ *)
wenzelm@24326
   377
(* Values                                                      *)
wenzelm@24326
   378
(* ############################################################ *)
wenzelm@24326
   379
wenzelm@24326
   380
lemmas v_disjs = v_disj_const_clos
wenzelm@24326
   381
lemmas v_disj_si = v_disjs  v_disjs [symmetric]
wenzelm@24326
   382
lemmas v_disj_se = v_disj_si [THEN notE]
wenzelm@24326
   383
wenzelm@24326
   384
lemmas v_injs = v_const_inj v_clos_inj
wenzelm@24326
   385
wenzelm@24326
   386
(* ############################################################ *)
wenzelm@24326
   387
(* Evaluations                                                  *)
wenzelm@24326
   388
(* ############################################################ *)
wenzelm@24326
   389
wenzelm@24326
   390
(* Monotonicity of eval_fun *)
wenzelm@24326
   391
wenzelm@24326
   392
lemma eval_fun_mono: "mono(eval_fun)"
wenzelm@24326
   393
unfolding mono_def eval_fun_def
wenzelm@24326
   394
apply (tactic infsys_mono_tac)
wenzelm@24326
   395
done
wenzelm@24326
   396
wenzelm@24326
   397
(* Introduction rules *)
wenzelm@24326
   398
wenzelm@24326
   399
lemma eval_const: "ve |- e_const(c) ---> v_const(c)"
wenzelm@24326
   400
unfolding eval_def eval_rel_def
wenzelm@24326
   401
apply (rule lfp_intro2)
wenzelm@24326
   402
apply (rule eval_fun_mono)
wenzelm@24326
   403
apply (unfold eval_fun_def)
wenzelm@24326
   404
        (*Naughty!  But the quantifiers are nested VERY deeply...*)
wenzelm@24326
   405
apply (blast intro!: exI)
wenzelm@24326
   406
done
wenzelm@24326
   407
wenzelm@24326
   408
lemma eval_var2:
wenzelm@24326
   409
  "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev"
wenzelm@24326
   410
apply (unfold eval_def eval_rel_def)
wenzelm@24326
   411
apply (rule lfp_intro2)
wenzelm@24326
   412
apply (rule eval_fun_mono)
wenzelm@24326
   413
apply (unfold eval_fun_def)
wenzelm@24326
   414
apply (blast intro!: exI)
wenzelm@24326
   415
done
wenzelm@24326
   416
wenzelm@24326
   417
lemma eval_fn:
wenzelm@24326
   418
  "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)"
wenzelm@24326
   419
apply (unfold eval_def eval_rel_def)
wenzelm@24326
   420
apply (rule lfp_intro2)
wenzelm@24326
   421
apply (rule eval_fun_mono)
wenzelm@24326
   422
apply (unfold eval_fun_def)
wenzelm@24326
   423
apply (blast intro!: exI)
wenzelm@24326
   424
done
wenzelm@24326
   425
wenzelm@24326
   426
lemma eval_fix:
wenzelm@24326
   427
  " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
wenzelm@24326
   428
    ve |- fix ev2(ev1) = e ---> v_clos(cl)"
wenzelm@24326
   429
apply (unfold eval_def eval_rel_def)
wenzelm@24326
   430
apply (rule lfp_intro2)
wenzelm@24326
   431
apply (rule eval_fun_mono)
wenzelm@24326
   432
apply (unfold eval_fun_def)
wenzelm@24326
   433
apply (blast intro!: exI)
wenzelm@24326
   434
done
wenzelm@24326
   435
wenzelm@24326
   436
lemma eval_app1:
wenzelm@24326
   437
  " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==>
wenzelm@24326
   438
    ve |- e1 @@ e2 ---> v_const(c_app c1 c2)"
wenzelm@24326
   439
apply (unfold eval_def eval_rel_def)
wenzelm@24326
   440
apply (rule lfp_intro2)
wenzelm@24326
   441
apply (rule eval_fun_mono)
wenzelm@24326
   442
apply (unfold eval_fun_def)
wenzelm@24326
   443
apply (blast intro!: exI)
wenzelm@24326
   444
done
wenzelm@24326
   445
wenzelm@24326
   446
lemma eval_app2:
wenzelm@24326
   447
  " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>);
wenzelm@24326
   448
        ve |- e2 ---> v2;
wenzelm@24326
   449
        vem + {xm |-> v2} |- em ---> v
wenzelm@24326
   450
    |] ==>
wenzelm@24326
   451
    ve |- e1 @@ e2 ---> v"
wenzelm@24326
   452
apply (unfold eval_def eval_rel_def)
wenzelm@24326
   453
apply (rule lfp_intro2)
wenzelm@24326
   454
apply (rule eval_fun_mono)
wenzelm@24326
   455
apply (unfold eval_fun_def)
wenzelm@24326
   456
apply (blast intro!: disjI2)
wenzelm@24326
   457
done
wenzelm@24326
   458
wenzelm@24326
   459
(* Strong elimination, induction on evaluations *)
wenzelm@24326
   460
wenzelm@24326
   461
lemma eval_ind0:
wenzelm@24326
   462
  " [| ve |- e ---> v;
wenzelm@24326
   463
       !!ve c. P(((ve,e_const(c)),v_const(c)));
wenzelm@24326
   464
       !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev));
wenzelm@24326
   465
       !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>)));
wenzelm@24326
   466
       !!ev1 ev2 ve cl e.
wenzelm@24326
   467
         cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
wenzelm@24326
   468
         P(((ve,fix ev2(ev1) = e),v_clos(cl)));
wenzelm@24326
   469
       !!ve c1 c2 e1 e2.
wenzelm@24326
   470
         [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==>
wenzelm@24326
   471
         P(((ve,e1 @@ e2),v_const(c_app c1 c2)));
wenzelm@24326
   472
       !!ve vem xm e1 e2 em v v2.
wenzelm@24326
   473
         [|  P(((ve,e1),v_clos(<|xm,em,vem|>)));
wenzelm@24326
   474
             P(((ve,e2),v2));
wenzelm@24326
   475
             P(((vem + {xm |-> v2},em),v))
wenzelm@24326
   476
         |] ==>
wenzelm@24326
   477
         P(((ve,e1 @@ e2),v))
wenzelm@24326
   478
    |] ==>
wenzelm@24326
   479
    P(((ve,e),v))"
wenzelm@24326
   480
unfolding eval_def eval_rel_def
wenzelm@24326
   481
apply (erule lfp_ind2)
wenzelm@24326
   482
apply (rule eval_fun_mono)
wenzelm@24326
   483
apply (unfold eval_fun_def)
wenzelm@24326
   484
apply (drule CollectD)
wenzelm@24326
   485
apply safe
wenzelm@24326
   486
apply auto
wenzelm@24326
   487
done
wenzelm@24326
   488
wenzelm@24326
   489
lemma eval_ind:
wenzelm@24326
   490
  " [| ve |- e ---> v;
wenzelm@24326
   491
       !!ve c. P ve (e_const c) (v_const c);
wenzelm@24326
   492
       !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev);
wenzelm@24326
   493
       !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>);
wenzelm@24326
   494
       !!ev1 ev2 ve cl e.
wenzelm@24326
   495
         cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
wenzelm@24326
   496
         P ve (fix ev2(ev1) = e) (v_clos cl);
wenzelm@24326
   497
       !!ve c1 c2 e1 e2.
wenzelm@24326
   498
         [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==>
wenzelm@24326
   499
         P ve (e1 @@ e2) (v_const(c_app c1 c2));
wenzelm@24326
   500
       !!ve vem evm e1 e2 em v v2.
wenzelm@24326
   501
         [|  P ve e1 (v_clos <|evm,em,vem|>);
wenzelm@24326
   502
             P ve e2 v2;
wenzelm@24326
   503
             P (vem + {evm |-> v2}) em v
wenzelm@24326
   504
         |] ==> P ve (e1 @@ e2) v
wenzelm@24326
   505
    |] ==> P ve e v"
wenzelm@24326
   506
apply (rule_tac P = "P" in infsys_pp2)
wenzelm@24326
   507
apply (rule eval_ind0)
wenzelm@24326
   508
apply (rule infsys_pp1)
wenzelm@24326
   509
apply auto
wenzelm@24326
   510
done
wenzelm@24326
   511
wenzelm@24326
   512
(* ############################################################ *)
wenzelm@24326
   513
(* Elaborations                                                 *)
wenzelm@24326
   514
(* ############################################################ *)
wenzelm@24326
   515
wenzelm@24326
   516
lemma elab_fun_mono: "mono(elab_fun)"
wenzelm@24326
   517
unfolding mono_def elab_fun_def
wenzelm@24326
   518
apply (tactic infsys_mono_tac)
wenzelm@24326
   519
done
wenzelm@24326
   520
wenzelm@24326
   521
(* Introduction rules *)
wenzelm@24326
   522
wenzelm@24326
   523
lemma elab_const:
wenzelm@24326
   524
  "c isof ty ==> te |- e_const(c) ===> ty"
wenzelm@24326
   525
apply (unfold elab_def elab_rel_def)
wenzelm@24326
   526
apply (rule lfp_intro2)
wenzelm@24326
   527
apply (rule elab_fun_mono)
wenzelm@24326
   528
apply (unfold elab_fun_def)
wenzelm@24326
   529
apply (blast intro!: exI)
wenzelm@24326
   530
done
wenzelm@24326
   531
wenzelm@24326
   532
lemma elab_var:
wenzelm@24326
   533
  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x"
wenzelm@24326
   534
apply (unfold elab_def elab_rel_def)
wenzelm@24326
   535
apply (rule lfp_intro2)
wenzelm@24326
   536
apply (rule elab_fun_mono)
wenzelm@24326
   537
apply (unfold elab_fun_def)
wenzelm@24326
   538
apply (blast intro!: exI)
wenzelm@24326
   539
done
wenzelm@24326
   540
wenzelm@24326
   541
lemma elab_fn:
wenzelm@24326
   542
  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2"
wenzelm@24326
   543
apply (unfold elab_def elab_rel_def)
wenzelm@24326
   544
apply (rule lfp_intro2)
wenzelm@24326
   545
apply (rule elab_fun_mono)
wenzelm@24326
   546
apply (unfold elab_fun_def)
wenzelm@24326
   547
apply (blast intro!: exI)
wenzelm@24326
   548
done
wenzelm@24326
   549
wenzelm@24326
   550
lemma elab_fix:
wenzelm@24326
   551
  "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==>
wenzelm@24326
   552
         te |- fix f(x) = e ===> ty1->ty2"
wenzelm@24326
   553
apply (unfold elab_def elab_rel_def)
wenzelm@24326
   554
apply (rule lfp_intro2)
wenzelm@24326
   555
apply (rule elab_fun_mono)
wenzelm@24326
   556
apply (unfold elab_fun_def)
wenzelm@24326
   557
apply (blast intro!: exI)
wenzelm@24326
   558
done
wenzelm@24326
   559
wenzelm@24326
   560
lemma elab_app:
wenzelm@24326
   561
  "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==>
wenzelm@24326
   562
         te |- e1 @@ e2 ===> ty2"
wenzelm@24326
   563
apply (unfold elab_def elab_rel_def)
wenzelm@24326
   564
apply (rule lfp_intro2)
wenzelm@24326
   565
apply (rule elab_fun_mono)
wenzelm@24326
   566
apply (unfold elab_fun_def)
wenzelm@24326
   567
apply (blast intro!: disjI2)
wenzelm@24326
   568
done
wenzelm@24326
   569
wenzelm@24326
   570
(* Strong elimination, induction on elaborations *)
wenzelm@24326
   571
wenzelm@24326
   572
lemma elab_ind0:
wenzelm@24326
   573
  assumes 1: "te |- e ===> t"
wenzelm@24326
   574
    and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))"
wenzelm@24326
   575
    and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))"
wenzelm@24326
   576
    and 4: "!!te x e t1 t2.
wenzelm@24326
   577
       [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==>
wenzelm@24326
   578
       P(((te,fn x => e),t1->t2))"
wenzelm@24326
   579
    and 5: "!!te f x e t1 t2.
wenzelm@24326
   580
       [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2;
wenzelm@24326
   581
          P(((te + {f |=> t1->t2} + {x |=> t1},e),t2))
wenzelm@24326
   582
       |] ==>
wenzelm@24326
   583
       P(((te,fix f(x) = e),t1->t2))"
wenzelm@24326
   584
    and 6: "!!te e1 e2 t1 t2.
wenzelm@24326
   585
       [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2));
wenzelm@24326
   586
          te |- e2 ===> t1; P(((te,e2),t1))
wenzelm@24326
   587
       |] ==>
wenzelm@24326
   588
       P(((te,e1 @@ e2),t2))"
wenzelm@24326
   589
  shows "P(((te,e),t))"
wenzelm@24326
   590
apply (rule lfp_ind2 [OF 1 [unfolded elab_def elab_rel_def]])
wenzelm@24326
   591
apply (rule elab_fun_mono)
wenzelm@24326
   592
apply (unfold elab_fun_def)
wenzelm@24326
   593
apply (drule CollectD)
wenzelm@24326
   594
apply safe
wenzelm@24326
   595
apply (erule 2)
wenzelm@24326
   596
apply (erule 3)
wenzelm@24326
   597
apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+
wenzelm@24326
   598
apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+
wenzelm@24326
   599
apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+
wenzelm@24326
   600
done
wenzelm@24326
   601
wenzelm@24326
   602
lemma elab_ind:
wenzelm@24326
   603
  " [| te |- e ===> t;
wenzelm@24326
   604
        !!te c t. c isof t ==> P te (e_const c) t;
wenzelm@24326
   605
       !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x);
wenzelm@24326
   606
       !!te x e t1 t2.
wenzelm@24326
   607
         [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==>
wenzelm@24326
   608
         P te (fn x => e) (t1->t2);
wenzelm@24326
   609
       !!te f x e t1 t2.
wenzelm@24326
   610
         [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2;
wenzelm@24326
   611
            P (te + {f |=> t1->t2} + {x |=> t1}) e t2
wenzelm@24326
   612
         |] ==>
wenzelm@24326
   613
         P te (fix f(x) = e) (t1->t2);
wenzelm@24326
   614
       !!te e1 e2 t1 t2.
wenzelm@24326
   615
         [| te |- e1 ===> t1->t2; P te e1 (t1->t2);
wenzelm@24326
   616
            te |- e2 ===> t1; P te e2 t1
wenzelm@24326
   617
         |] ==>
wenzelm@24326
   618
         P te (e1 @@ e2) t2
wenzelm@24326
   619
    |] ==>
wenzelm@24326
   620
    P te e t"
wenzelm@24326
   621
apply (rule_tac P = "P" in infsys_pp2)
wenzelm@24326
   622
apply (erule elab_ind0)
wenzelm@24326
   623
apply (rule_tac [!] infsys_pp1)
wenzelm@24326
   624
apply auto
wenzelm@24326
   625
done
wenzelm@24326
   626
wenzelm@24326
   627
(* Weak elimination, case analysis on elaborations *)
wenzelm@24326
   628
wenzelm@24326
   629
lemma elab_elim0:
wenzelm@24326
   630
  assumes 1: "te |- e ===> t"
wenzelm@24326
   631
    and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))"
wenzelm@24326
   632
    and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))"
wenzelm@24326
   633
    and 4: "!!te x e t1 t2.
wenzelm@24326
   634
         te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2))"
wenzelm@24326
   635
    and 5: "!!te f x e t1 t2.
wenzelm@24326
   636
         te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==>
wenzelm@24326
   637
         P(((te,fix f(x) = e),t1->t2))"
wenzelm@24326
   638
    and 6: "!!te e1 e2 t1 t2.
wenzelm@24326
   639
         [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==>
wenzelm@24326
   640
         P(((te,e1 @@ e2),t2))"
wenzelm@24326
   641
  shows "P(((te,e),t))"
wenzelm@24326
   642
apply (rule lfp_elim2 [OF 1 [unfolded elab_def elab_rel_def]])
wenzelm@24326
   643
apply (rule elab_fun_mono)
wenzelm@24326
   644
apply (unfold elab_fun_def)
wenzelm@24326
   645
apply (drule CollectD)
wenzelm@24326
   646
apply safe
wenzelm@24326
   647
apply (erule 2)
wenzelm@24326
   648
apply (erule 3)
wenzelm@24326
   649
apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+
wenzelm@24326
   650
apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+
wenzelm@24326
   651
apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+
wenzelm@24326
   652
done
wenzelm@24326
   653
wenzelm@24326
   654
lemma elab_elim:
wenzelm@24326
   655
  " [| te |- e ===> t;
wenzelm@24326
   656
        !!te c t. c isof t ==> P te (e_const c) t;
wenzelm@24326
   657
       !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x);
wenzelm@24326
   658
       !!te x e t1 t2.
wenzelm@24326
   659
         te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2);
wenzelm@24326
   660
       !!te f x e t1 t2.
wenzelm@24326
   661
         te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==>
wenzelm@24326
   662
         P te (fix f(x) = e) (t1->t2);
wenzelm@24326
   663
       !!te e1 e2 t1 t2.
wenzelm@24326
   664
         [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==>
wenzelm@24326
   665
         P te (e1 @@ e2) t2
wenzelm@24326
   666
    |] ==>
wenzelm@24326
   667
    P te e t"
wenzelm@24326
   668
apply (rule_tac P = "P" in infsys_pp2)
wenzelm@24326
   669
apply (rule elab_elim0)
wenzelm@24326
   670
apply auto
wenzelm@24326
   671
done
wenzelm@24326
   672
wenzelm@24326
   673
(* Elimination rules for each expression *)
wenzelm@24326
   674
wenzelm@24326
   675
lemma elab_const_elim_lem:
wenzelm@24326
   676
    "te |- e ===> t ==> (e = e_const(c) --> c isof t)"
wenzelm@24326
   677
apply (erule elab_elim)
wenzelm@24326
   678
apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
wenzelm@24326
   679
done
wenzelm@24326
   680
wenzelm@24326
   681
lemma elab_const_elim: "te |- e_const(c) ===> t ==> c isof t"
wenzelm@24326
   682
apply (drule elab_const_elim_lem)
wenzelm@24326
   683
apply blast
wenzelm@24326
   684
done
wenzelm@24326
   685
wenzelm@24326
   686
lemma elab_var_elim_lem:
wenzelm@24326
   687
  "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))"
wenzelm@24326
   688
apply (erule elab_elim)
wenzelm@24326
   689
apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
wenzelm@24326
   690
done
wenzelm@24326
   691
wenzelm@24326
   692
lemma elab_var_elim: "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)"
wenzelm@24326
   693
apply (drule elab_var_elim_lem)
wenzelm@24326
   694
apply blast
wenzelm@24326
   695
done
wenzelm@24326
   696
wenzelm@24326
   697
lemma elab_fn_elim_lem:
wenzelm@24326
   698
  " te |- e ===> t ==>
wenzelm@24326
   699
    ( e = fn x1 => e1 -->
wenzelm@24326
   700
      (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2)
wenzelm@24326
   701
    )"
wenzelm@24326
   702
apply (erule elab_elim)
wenzelm@24326
   703
apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
wenzelm@24326
   704
done
wenzelm@24326
   705
wenzelm@24326
   706
lemma elab_fn_elim: " te |- fn x1 => e1 ===> t ==>
wenzelm@24326
   707
    (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)"
wenzelm@24326
   708
apply (drule elab_fn_elim_lem)
wenzelm@24326
   709
apply blast
wenzelm@24326
   710
done
wenzelm@24326
   711
wenzelm@24326
   712
lemma elab_fix_elim_lem:
wenzelm@24326
   713
  " te |- e ===> t ==>
wenzelm@24326
   714
    (e = fix f(x) = e1 -->
wenzelm@24326
   715
    (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"
wenzelm@24326
   716
apply (erule elab_elim)
wenzelm@24326
   717
apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
wenzelm@24326
   718
done
wenzelm@24326
   719
wenzelm@24326
   720
lemma elab_fix_elim: " te |- fix ev1(ev2) = e1 ===> t ==>
wenzelm@24326
   721
    (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)"
wenzelm@24326
   722
apply (drule elab_fix_elim_lem)
wenzelm@24326
   723
apply blast
wenzelm@24326
   724
done
wenzelm@24326
   725
wenzelm@24326
   726
lemma elab_app_elim_lem:
wenzelm@24326
   727
  " te |- e ===> t2 ==>
wenzelm@24326
   728
    (e = e1 @@ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"
wenzelm@24326
   729
apply (erule elab_elim)
wenzelm@24326
   730
apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
wenzelm@24326
   731
done
wenzelm@24326
   732
wenzelm@24326
   733
lemma elab_app_elim: "te |- e1 @@ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"
wenzelm@24326
   734
apply (drule elab_app_elim_lem)
wenzelm@24326
   735
apply blast
wenzelm@24326
   736
done
wenzelm@24326
   737
wenzelm@24326
   738
(* ############################################################ *)
wenzelm@24326
   739
(* The extended correspondence relation                       *)
wenzelm@24326
   740
(* ############################################################ *)
wenzelm@24326
   741
wenzelm@24326
   742
(* Monotonicity of hasty_fun *)
wenzelm@24326
   743
wenzelm@24326
   744
lemma mono_hasty_fun: "mono(hasty_fun)"
wenzelm@24326
   745
unfolding mono_def hasty_fun_def
wenzelm@24326
   746
apply (tactic infsys_mono_tac)
wenzelm@24326
   747
apply blast
wenzelm@24326
   748
done
wenzelm@24326
   749
wenzelm@24326
   750
(*
wenzelm@24326
   751
  Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
wenzelm@24326
   752
  enjoys two strong indtroduction (co-induction) rules and an elimination rule.
wenzelm@24326
   753
*)
wenzelm@24326
   754
wenzelm@24326
   755
(* First strong indtroduction (co-induction) rule for hasty_rel *)
wenzelm@24326
   756
wenzelm@24326
   757
lemma hasty_rel_const_coind: "c isof t ==> (v_const(c),t) : hasty_rel"
wenzelm@24326
   758
apply (unfold hasty_rel_def)
wenzelm@24326
   759
apply (rule gfp_coind2)
wenzelm@24326
   760
apply (unfold hasty_fun_def)
wenzelm@24326
   761
apply (rule CollectI)
wenzelm@24326
   762
apply (rule disjI1)
wenzelm@24326
   763
apply blast
wenzelm@24326
   764
apply (rule mono_hasty_fun)
wenzelm@24326
   765
done
wenzelm@24326
   766
wenzelm@24326
   767
(* Second strong introduction (co-induction) rule for hasty_rel *)
wenzelm@24326
   768
wenzelm@24326
   769
lemma hasty_rel_clos_coind:
wenzelm@24326
   770
  " [|  te |- fn ev => e ===> t;
wenzelm@24326
   771
        ve_dom(ve) = te_dom(te);
wenzelm@24326
   772
        ! ev1.
wenzelm@24326
   773
          ev1:ve_dom(ve) -->
wenzelm@24326
   774
          (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel
wenzelm@24326
   775
    |] ==>
wenzelm@24326
   776
    (v_clos(<|ev,e,ve|>),t) : hasty_rel"
wenzelm@24326
   777
apply (unfold hasty_rel_def)
wenzelm@24326
   778
apply (rule gfp_coind2)
wenzelm@24326
   779
apply (unfold hasty_fun_def)
wenzelm@24326
   780
apply (rule CollectI)
wenzelm@24326
   781
apply (rule disjI2)
wenzelm@24326
   782
apply blast
wenzelm@24326
   783
apply (rule mono_hasty_fun)
wenzelm@24326
   784
done
wenzelm@24326
   785
wenzelm@24326
   786
(* Elimination rule for hasty_rel *)
wenzelm@24326
   787
wenzelm@24326
   788
lemma hasty_rel_elim0:
wenzelm@24326
   789
  " [| !! c t. c isof t ==> P((v_const(c),t));
wenzelm@24326
   790
       !! te ev e t ve.
wenzelm@24326
   791
         [| te |- fn ev => e ===> t;
wenzelm@24326
   792
            ve_dom(ve) = te_dom(te);
wenzelm@24326
   793
            !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel
wenzelm@24326
   794
         |] ==> P((v_clos(<|ev,e,ve|>),t));
wenzelm@24326
   795
       (v,t) : hasty_rel
wenzelm@24326
   796
    |] ==> P(v,t)"
wenzelm@24326
   797
unfolding hasty_rel_def
wenzelm@24326
   798
apply (erule gfp_elim2)
wenzelm@24326
   799
apply (rule mono_hasty_fun)
wenzelm@24326
   800
apply (unfold hasty_fun_def)
wenzelm@24326
   801
apply (drule CollectD)
wenzelm@24326
   802
apply (fold hasty_fun_def)
wenzelm@24326
   803
apply auto
wenzelm@24326
   804
done
wenzelm@24326
   805
wenzelm@24326
   806
lemma hasty_rel_elim:
wenzelm@24326
   807
  " [| (v,t) : hasty_rel;
wenzelm@24326
   808
       !! c t. c isof t ==> P (v_const c) t;
wenzelm@24326
   809
       !! te ev e t ve.
wenzelm@24326
   810
         [| te |- fn ev => e ===> t;
wenzelm@24326
   811
            ve_dom(ve) = te_dom(te);
wenzelm@24326
   812
            !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel
wenzelm@24326
   813
         |] ==> P (v_clos <|ev,e,ve|>) t
wenzelm@24326
   814
    |] ==> P v t"
wenzelm@24326
   815
apply (rule_tac P = "P" in infsys_p2)
wenzelm@24326
   816
apply (rule hasty_rel_elim0)
wenzelm@24326
   817
apply auto
wenzelm@24326
   818
done
wenzelm@24326
   819
wenzelm@24326
   820
(* Introduction rules for hasty *)
wenzelm@24326
   821
wenzelm@24326
   822
lemma hasty_const: "c isof t ==> v_const(c) hasty t"
wenzelm@24326
   823
apply (unfold hasty_def)
wenzelm@24326
   824
apply (erule hasty_rel_const_coind)
wenzelm@24326
   825
done
wenzelm@24326
   826
wenzelm@24326
   827
lemma hasty_clos:
wenzelm@24326
   828
 "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t"
wenzelm@24326
   829
apply (unfold hasty_def hasty_env_def)
wenzelm@24326
   830
apply (rule hasty_rel_clos_coind)
wenzelm@24326
   831
apply (blast del: equalityI)+
wenzelm@24326
   832
done
wenzelm@24326
   833
wenzelm@24326
   834
(* Elimination on constants for hasty *)
wenzelm@24326
   835
wenzelm@24326
   836
lemma hasty_elim_const_lem:
wenzelm@24326
   837
  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))"
wenzelm@24326
   838
apply (unfold hasty_def)
wenzelm@24326
   839
apply (rule hasty_rel_elim)
wenzelm@24326
   840
apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+
wenzelm@24326
   841
done
wenzelm@24326
   842
wenzelm@24326
   843
lemma hasty_elim_const: "v_const(c) hasty t ==> c isof t"
wenzelm@24326
   844
apply (drule hasty_elim_const_lem)
wenzelm@24326
   845
apply blast
wenzelm@24326
   846
done
wenzelm@24326
   847
wenzelm@24326
   848
(* Elimination on closures for hasty *)
wenzelm@24326
   849
wenzelm@24326
   850
lemma hasty_elim_clos_lem:
wenzelm@24326
   851
  " v hasty t ==>
wenzelm@24326
   852
    ! x e ve.
wenzelm@24326
   853
      v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)"
wenzelm@24326
   854
apply (unfold hasty_env_def hasty_def)
wenzelm@24326
   855
apply (rule hasty_rel_elim)
wenzelm@24326
   856
apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+
wenzelm@24326
   857
done
wenzelm@24326
   858
wenzelm@24326
   859
lemma hasty_elim_clos: "v_clos(<|ev,e,ve|>) hasty t ==>
wenzelm@24326
   860
        ? te. te |- fn ev => e ===> t & ve hastyenv te "
wenzelm@24326
   861
apply (drule hasty_elim_clos_lem)
wenzelm@24326
   862
apply blast
wenzelm@24326
   863
done
wenzelm@24326
   864
wenzelm@24326
   865
(* ############################################################ *)
wenzelm@24326
   866
(* The pointwise extension of hasty to environments             *)
wenzelm@24326
   867
(* ############################################################ *)
wenzelm@24326
   868
wenzelm@24326
   869
lemma hasty_env1: "[| ve hastyenv te; v hasty t |] ==>
wenzelm@24326
   870
         ve + {ev |-> v} hastyenv te + {ev |=> t}"
wenzelm@24326
   871
apply (unfold hasty_env_def)
wenzelm@24326
   872
apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
wenzelm@24326
   873
apply (tactic {* safe_tac HOL_cs *})
wenzelm@24326
   874
apply (case_tac "ev=x")
wenzelm@24326
   875
apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
wenzelm@24326
   876
apply (simp add: ve_app_owr2 te_app_owr2)
wenzelm@24326
   877
done
wenzelm@24326
   878
wenzelm@24326
   879
(* ############################################################ *)
wenzelm@24326
   880
(* The Consistency theorem                                      *)
wenzelm@24326
   881
(* ############################################################ *)
wenzelm@24326
   882
wenzelm@24326
   883
lemma consistency_const: "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t"
wenzelm@24326
   884
apply (drule elab_const_elim)
wenzelm@24326
   885
apply (erule hasty_const)
wenzelm@24326
   886
done
wenzelm@24326
   887
wenzelm@24326
   888
lemma consistency_var:
wenzelm@24326
   889
  "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==>
wenzelm@24326
   890
        ve_app ve ev hasty t"
wenzelm@24326
   891
apply (unfold hasty_env_def)
wenzelm@24326
   892
apply (drule elab_var_elim)
wenzelm@24326
   893
apply blast
wenzelm@24326
   894
done
wenzelm@24326
   895
wenzelm@24326
   896
lemma consistency_fn: "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==>
wenzelm@24326
   897
        v_clos(<| ev, e, ve |>) hasty t"
wenzelm@24326
   898
apply (rule hasty_clos)
wenzelm@24326
   899
apply blast
wenzelm@24326
   900
done
wenzelm@24326
   901
wenzelm@24326
   902
lemma consistency_fix:
wenzelm@24326
   903
  "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>;
wenzelm@24326
   904
       ve hastyenv te ;
wenzelm@24326
   905
       te |- fix ev2  ev1  = e ===> t
wenzelm@24326
   906
    |] ==>
wenzelm@24326
   907
    v_clos(cl) hasty t"
wenzelm@24326
   908
apply (unfold hasty_env_def hasty_def)
wenzelm@24326
   909
apply (drule elab_fix_elim)
wenzelm@24326
   910
apply (tactic {* safe_tac HOL_cs *})
wenzelm@24326
   911
(*Do a single unfolding of cl*)
wenzelm@24326
   912
apply (frule ssubst) prefer 2 apply assumption
wenzelm@24326
   913
apply (rule hasty_rel_clos_coind)
wenzelm@24326
   914
apply (erule elab_fn)
wenzelm@24326
   915
apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
wenzelm@24326
   916
wenzelm@24326
   917
apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
wenzelm@24326
   918
apply (tactic {* safe_tac HOL_cs *})
wenzelm@24326
   919
apply (case_tac "ev2=ev1a")
wenzelm@24326
   920
apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
wenzelm@24326
   921
apply blast
wenzelm@24326
   922
apply (simp add: ve_app_owr2 te_app_owr2)
wenzelm@24326
   923
done
wenzelm@24326
   924
wenzelm@24326
   925
lemma consistency_app1: "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;
wenzelm@24326
   926
       ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t;
wenzelm@24326
   927
       ve hastyenv te ; te |- e1 @@ e2 ===> t
wenzelm@24326
   928
    |] ==>
wenzelm@24326
   929
    v_const(c_app c1 c2) hasty t"
wenzelm@24326
   930
apply (drule elab_app_elim)
wenzelm@24326
   931
apply safe
wenzelm@24326
   932
apply (rule hasty_const)
wenzelm@24326
   933
apply (rule isof_app)
wenzelm@24326
   934
apply (rule hasty_elim_const)
wenzelm@24326
   935
apply blast
wenzelm@24326
   936
apply (rule hasty_elim_const)
wenzelm@24326
   937
apply blast
wenzelm@24326
   938
done
wenzelm@24326
   939
wenzelm@24326
   940
lemma consistency_app2: "[| ! t te.
wenzelm@24326
   941
         ve hastyenv te  -->
wenzelm@24326
   942
         te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t;
wenzelm@24326
   943
       ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t;
wenzelm@24326
   944
       ! t te.
wenzelm@24326
   945
         vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t;
wenzelm@24326
   946
       ve hastyenv te ;
wenzelm@24326
   947
       te |- e1 @@ e2 ===> t
wenzelm@24326
   948
    |] ==>
wenzelm@24326
   949
    v hasty t"
wenzelm@24326
   950
apply (drule elab_app_elim)
wenzelm@24326
   951
apply safe
wenzelm@24326
   952
apply (erule allE, erule allE, erule impE)
wenzelm@24326
   953
apply assumption
wenzelm@24326
   954
apply (erule impE)
wenzelm@24326
   955
apply assumption
wenzelm@24326
   956
apply (erule allE, erule allE, erule impE)
wenzelm@24326
   957
apply assumption
wenzelm@24326
   958
apply (erule impE)
wenzelm@24326
   959
apply assumption
wenzelm@24326
   960
apply (drule hasty_elim_clos)
wenzelm@24326
   961
apply safe
wenzelm@24326
   962
apply (drule elab_fn_elim)
wenzelm@24326
   963
apply (blast intro: hasty_env1 dest!: t_fun_inj)
wenzelm@24326
   964
done
wenzelm@24326
   965
wenzelm@24326
   966
lemma consistency: "ve |- e ---> v ==>
wenzelm@24326
   967
   (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)"
wenzelm@24326
   968
wenzelm@24326
   969
(* Proof by induction on the structure of evaluations *)
wenzelm@24326
   970
wenzelm@24326
   971
apply (erule eval_ind)
wenzelm@24326
   972
apply safe
wenzelm@24326
   973
apply (blast intro: consistency_const consistency_var consistency_fn consistency_fix consistency_app1 consistency_app2)+
wenzelm@24326
   974
done
wenzelm@24326
   975
wenzelm@24326
   976
(* ############################################################ *)
wenzelm@24326
   977
(* The Basic Consistency theorem                                *)
wenzelm@24326
   978
(* ############################################################ *)
wenzelm@24326
   979
wenzelm@24326
   980
lemma basic_consistency_lem:
wenzelm@24326
   981
  "ve isofenv te ==> ve hastyenv te"
wenzelm@24326
   982
apply (unfold isof_env_def hasty_env_def)
wenzelm@24326
   983
apply safe
wenzelm@24326
   984
apply (erule allE)
wenzelm@24326
   985
apply (erule impE)
wenzelm@24326
   986
apply assumption
wenzelm@24326
   987
apply (erule exE)
wenzelm@24326
   988
apply (erule conjE)
wenzelm@24326
   989
apply (drule hasty_const)
wenzelm@24326
   990
apply (simp (no_asm_simp))
wenzelm@24326
   991
done
wenzelm@24326
   992
wenzelm@24326
   993
lemma basic_consistency:
wenzelm@24326
   994
  "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t"
wenzelm@24326
   995
apply (rule hasty_elim_const)
wenzelm@24326
   996
apply (drule consistency)
wenzelm@24326
   997
apply (blast intro!: basic_consistency_lem)
wenzelm@24326
   998
done
wenzelm@17289
   999
clasohm@969
  1000
end