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