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