src/HOL/ex/MT.ML
author clasohm
Wed Mar 22 12:42:34 1995 +0100 (1995-03-22)
changeset 969 b051e2fc2e34
child 972 e61b058d58d2
permissions -rw-r--r--
converted ex with curried function application
clasohm@969
     1
(*  Title: 	HOL/ex/mt.ML
clasohm@969
     2
    ID:         $Id$
clasohm@969
     3
    Author: 	Jacob Frost, Cambridge University Computer Laboratory
clasohm@969
     4
    Copyright   1993  University of Cambridge
clasohm@969
     5
clasohm@969
     6
Based upon the article
clasohm@969
     7
    Robin Milner and Mads Tofte,
clasohm@969
     8
    Co-induction in Relational Semantics,
clasohm@969
     9
    Theoretical Computer Science 87 (1991), pages 209-220.
clasohm@969
    10
clasohm@969
    11
Written up as
clasohm@969
    12
    Jacob Frost, A Case Study of Co-induction in Isabelle/HOL
clasohm@969
    13
    Report 308, Computer Lab, University of Cambridge (1993).
clasohm@969
    14
*)
clasohm@969
    15
clasohm@969
    16
open MT;
clasohm@969
    17
clasohm@969
    18
val prems = goal MT.thy "~a:{b} ==> ~a=b";
clasohm@969
    19
by (cut_facts_tac prems 1);
clasohm@969
    20
by (rtac notI 1);
clasohm@969
    21
by (dtac notE 1);
clasohm@969
    22
by (hyp_subst_tac 1);
clasohm@969
    23
by (rtac singletonI 1);
clasohm@969
    24
by (assume_tac 1);
clasohm@969
    25
qed "notsingletonI";
clasohm@969
    26
clasohm@969
    27
val prems = goalw MT.thy [Un_def]
clasohm@969
    28
  "[| c : A Un B; c : A & ~c : B ==> P; c : B ==> P |] ==> P";
clasohm@969
    29
by (cut_facts_tac prems 1);bd CollectD 1;be disjE 1;
clasohm@969
    30
by (cut_facts_tac [excluded_middle] 1);be disjE 1;
clasohm@969
    31
by (resolve_tac prems 1);br conjI 1;ba 1;ba 1;
clasohm@969
    32
by (eresolve_tac prems 1);
clasohm@969
    33
by (eresolve_tac prems 1);
clasohm@969
    34
qed "UnSE";
clasohm@969
    35
clasohm@969
    36
(* ############################################################ *)
clasohm@969
    37
(* Inference systems                                            *)
clasohm@969
    38
(* ############################################################ *)
clasohm@969
    39
clasohm@969
    40
val infsys_mono_tac =
clasohm@969
    41
  (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN
clasohm@969
    42
  (rtac CollectI 1) THEN (dtac CollectD 1) THEN
clasohm@969
    43
  REPEAT 
clasohm@969
    44
    ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
clasohm@969
    45
      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
clasohm@969
    46
    );
clasohm@969
    47
clasohm@969
    48
val prems = goal MT.thy "P a b ==> P (fst <a,b>) (snd <a,b>)";
clasohm@969
    49
by (rtac (fst_conv RS ssubst) 1);
clasohm@969
    50
by (rtac (snd_conv RS ssubst) 1);
clasohm@969
    51
by (resolve_tac prems 1);
clasohm@969
    52
qed "infsys_p1";
clasohm@969
    53
clasohm@969
    54
val prems = goal MT.thy "P (fst <a,b>) (snd <a,b>) ==> P a b";
clasohm@969
    55
by (cut_facts_tac prems 1);
clasohm@969
    56
by (dtac (fst_conv RS subst) 1);
clasohm@969
    57
by (dtac (snd_conv RS subst) 1);
clasohm@969
    58
by (assume_tac 1);
clasohm@969
    59
qed "infsys_p2";
clasohm@969
    60
clasohm@969
    61
val prems = goal MT.thy 
clasohm@969
    62
  "P a b c ==> P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>)";
clasohm@969
    63
by (rtac (fst_conv RS ssubst) 1);
clasohm@969
    64
by (rtac (fst_conv RS ssubst) 1);
clasohm@969
    65
by (rtac (snd_conv RS ssubst) 1);
clasohm@969
    66
by (rtac (snd_conv RS ssubst) 1);
clasohm@969
    67
by (resolve_tac prems 1);
clasohm@969
    68
qed "infsys_pp1";
clasohm@969
    69
clasohm@969
    70
val prems = goal MT.thy 
clasohm@969
    71
  "P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>) ==> P a b c";
clasohm@969
    72
by (cut_facts_tac prems 1);
clasohm@969
    73
by (dtac (fst_conv RS subst) 1);
clasohm@969
    74
by (dtac (fst_conv RS subst) 1);
clasohm@969
    75
by (dtac (snd_conv RS subst) 1);
clasohm@969
    76
by (dtac (snd_conv RS subst) 1);
clasohm@969
    77
by (assume_tac 1);
clasohm@969
    78
qed "infsys_pp2";
clasohm@969
    79
clasohm@969
    80
(* ############################################################ *)
clasohm@969
    81
(* Fixpoints                                                    *)
clasohm@969
    82
(* ############################################################ *)
clasohm@969
    83
clasohm@969
    84
(* Least fixpoints *)
clasohm@969
    85
clasohm@969
    86
val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
clasohm@969
    87
by (rtac subsetD 1);
clasohm@969
    88
by (rtac lfp_lemma2 1);
clasohm@969
    89
by (resolve_tac prems 1);brs prems 1;
clasohm@969
    90
qed "lfp_intro2";
clasohm@969
    91
clasohm@969
    92
val prems = goal MT.thy
clasohm@969
    93
  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
clasohm@969
    94
\   P(x)";
clasohm@969
    95
by (cut_facts_tac prems 1);
clasohm@969
    96
by (resolve_tac prems 1);br subsetD 1;
clasohm@969
    97
by (rtac lfp_lemma3 1);ba 1;ba 1;
clasohm@969
    98
qed "lfp_elim2";
clasohm@969
    99
clasohm@969
   100
val prems = goal MT.thy
clasohm@969
   101
  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
clasohm@969
   102
\   P(x)";
clasohm@969
   103
by (cut_facts_tac prems 1);
clasohm@969
   104
by (etac induct 1);ba 1;
clasohm@969
   105
by (eresolve_tac prems 1);
clasohm@969
   106
qed "lfp_ind2";
clasohm@969
   107
clasohm@969
   108
(* Greatest fixpoints *)
clasohm@969
   109
clasohm@969
   110
(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
clasohm@969
   111
clasohm@969
   112
val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
clasohm@969
   113
by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
clasohm@969
   114
by (rtac (monoh RS monoD) 1);
clasohm@969
   115
by (rtac (UnE RS subsetI) 1);ba 1;
clasohm@969
   116
by (fast_tac (set_cs addSIs [cih]) 1);
clasohm@969
   117
by (rtac (monoh RS monoD RS subsetD) 1);
clasohm@969
   118
by (rtac Un_upper2 1);
clasohm@969
   119
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
clasohm@969
   120
qed "gfp_coind2";
clasohm@969
   121
clasohm@969
   122
val [gfph,monoh,caseh] = goal MT.thy 
clasohm@969
   123
  "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
clasohm@969
   124
by (rtac caseh 1);br subsetD 1;br gfp_lemma2 1;br monoh 1;br gfph 1;
clasohm@969
   125
qed "gfp_elim2";
clasohm@969
   126
clasohm@969
   127
(* ############################################################ *)
clasohm@969
   128
(* Expressions                                                  *)
clasohm@969
   129
(* ############################################################ *)
clasohm@969
   130
clasohm@969
   131
val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
clasohm@969
   132
clasohm@969
   133
val e_disjs = 
clasohm@969
   134
  [ e_disj_const_var, 
clasohm@969
   135
    e_disj_const_fn, 
clasohm@969
   136
    e_disj_const_fix, 
clasohm@969
   137
    e_disj_const_app,
clasohm@969
   138
    e_disj_var_fn, 
clasohm@969
   139
    e_disj_var_fix, 
clasohm@969
   140
    e_disj_var_app, 
clasohm@969
   141
    e_disj_fn_fix, 
clasohm@969
   142
    e_disj_fn_app, 
clasohm@969
   143
    e_disj_fix_app
clasohm@969
   144
  ];
clasohm@969
   145
clasohm@969
   146
val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
clasohm@969
   147
val e_disj_se = (e_disj_si RL [notE]);
clasohm@969
   148
clasohm@969
   149
fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
clasohm@969
   150
clasohm@969
   151
(* ############################################################ *)
clasohm@969
   152
(* Values                                                      *)
clasohm@969
   153
(* ############################################################ *)
clasohm@969
   154
clasohm@969
   155
val v_disjs = [v_disj_const_clos];
clasohm@969
   156
val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
clasohm@969
   157
val v_disj_se = (v_disj_si RL [notE]);
clasohm@969
   158
clasohm@969
   159
val v_injs = [v_const_inj, v_clos_inj];
clasohm@969
   160
clasohm@969
   161
fun v_ext_cs cs  = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
clasohm@969
   162
clasohm@969
   163
(* ############################################################ *)
clasohm@969
   164
(* Evaluations                                                  *)
clasohm@969
   165
(* ############################################################ *)
clasohm@969
   166
clasohm@969
   167
(* Monotonicity of eval_fun *)
clasohm@969
   168
clasohm@969
   169
goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)";
clasohm@969
   170
by infsys_mono_tac;
clasohm@969
   171
qed "eval_fun_mono";
clasohm@969
   172
clasohm@969
   173
(* Introduction rules *)
clasohm@969
   174
clasohm@969
   175
goalw MT.thy [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
clasohm@969
   176
by (rtac lfp_intro2 1);
clasohm@969
   177
by (rtac eval_fun_mono 1);
clasohm@969
   178
by (rewtac eval_fun_def);
clasohm@969
   179
by (rtac CollectI 1);br disjI1 1;
clasohm@969
   180
by (fast_tac HOL_cs 1);
clasohm@969
   181
qed "eval_const";
clasohm@969
   182
clasohm@969
   183
val prems = goalw MT.thy [eval_def, eval_rel_def] 
clasohm@969
   184
  "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
clasohm@969
   185
by (cut_facts_tac prems 1);
clasohm@969
   186
by (rtac lfp_intro2 1);
clasohm@969
   187
by (rtac eval_fun_mono 1);
clasohm@969
   188
by (rewtac eval_fun_def);
clasohm@969
   189
by (rtac CollectI 1);br disjI2 1;br disjI1 1;
clasohm@969
   190
by (fast_tac HOL_cs 1);
clasohm@969
   191
qed "eval_var";
clasohm@969
   192
clasohm@969
   193
val prems = goalw MT.thy [eval_def, eval_rel_def] 
clasohm@969
   194
  "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
clasohm@969
   195
by (cut_facts_tac prems 1);
clasohm@969
   196
by (rtac lfp_intro2 1);
clasohm@969
   197
by (rtac eval_fun_mono 1);
clasohm@969
   198
by (rewtac eval_fun_def);
clasohm@969
   199
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;
clasohm@969
   200
by (fast_tac HOL_cs 1);
clasohm@969
   201
qed "eval_fn";
clasohm@969
   202
clasohm@969
   203
val prems = goalw MT.thy [eval_def, eval_rel_def] 
clasohm@969
   204
  " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@969
   205
\   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
clasohm@969
   206
by (cut_facts_tac prems 1);
clasohm@969
   207
by (rtac lfp_intro2 1);
clasohm@969
   208
by (rtac eval_fun_mono 1);
clasohm@969
   209
by (rewtac eval_fun_def);
clasohm@969
   210
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
clasohm@969
   211
by (fast_tac HOL_cs 1);
clasohm@969
   212
qed "eval_fix";
clasohm@969
   213
clasohm@969
   214
val prems = goalw MT.thy [eval_def, eval_rel_def]
clasohm@969
   215
  " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
clasohm@969
   216
\   ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
clasohm@969
   217
by (cut_facts_tac prems 1);
clasohm@969
   218
by (rtac lfp_intro2 1);
clasohm@969
   219
by (rtac eval_fun_mono 1);
clasohm@969
   220
by (rewtac eval_fun_def);
clasohm@969
   221
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
clasohm@969
   222
by (fast_tac HOL_cs 1);
clasohm@969
   223
qed "eval_app1";
clasohm@969
   224
clasohm@969
   225
val prems = goalw MT.thy [eval_def, eval_rel_def] 
clasohm@969
   226
  " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
clasohm@969
   227
\       ve |- e2 ---> v2; \
clasohm@969
   228
\       vem + {xm |-> v2} |- em ---> v \
clasohm@969
   229
\   |] ==> \
clasohm@969
   230
\   ve |- e1 @ e2 ---> v";
clasohm@969
   231
by (cut_facts_tac prems 1);
clasohm@969
   232
by (rtac lfp_intro2 1);
clasohm@969
   233
by (rtac eval_fun_mono 1);
clasohm@969
   234
by (rewtac eval_fun_def);
clasohm@969
   235
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;
clasohm@969
   236
by (fast_tac HOL_cs 1);
clasohm@969
   237
qed "eval_app2";
clasohm@969
   238
clasohm@969
   239
(* Strong elimination, induction on evaluations *)
clasohm@969
   240
clasohm@969
   241
val prems = goalw MT.thy [eval_def, eval_rel_def]
clasohm@969
   242
  " [| ve |- e ---> v; \
clasohm@969
   243
\      !!ve c. P(<<ve,e_const(c)>,v_const(c)>); \
clasohm@969
   244
\      !!ev ve. ev:ve_dom(ve) ==> P(<<ve,e_var(ev)>,ve_app ve ev>); \
clasohm@969
   245
\      !!ev ve e. P(<<ve,fn ev => e>,v_clos(<|ev,e,ve|>)>); \
clasohm@969
   246
\      !!ev1 ev2 ve cl e. \
clasohm@969
   247
\        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@969
   248
\        P(<<ve,fix ev2(ev1) = e>,v_clos(cl)>); \
clasohm@969
   249
\      !!ve c1 c2 e1 e2. \
clasohm@969
   250
\        [| P(<<ve,e1>,v_const(c1)>); P(<<ve,e2>,v_const(c2)>) |] ==> \
clasohm@969
   251
\        P(<<ve,e1 @ e2>,v_const(c_app c1 c2)>); \
clasohm@969
   252
\      !!ve vem xm e1 e2 em v v2. \
clasohm@969
   253
\        [|  P(<<ve,e1>,v_clos(<|xm,em,vem|>)>); \
clasohm@969
   254
\            P(<<ve,e2>,v2>); \
clasohm@969
   255
\            P(<<vem + {xm |-> v2},em>,v>) \
clasohm@969
   256
\        |] ==> \
clasohm@969
   257
\        P(<<ve,e1 @ e2>,v>) \
clasohm@969
   258
\   |] ==> \
clasohm@969
   259
\   P(<<ve,e>,v>)";
clasohm@969
   260
by (resolve_tac (prems RL [lfp_ind2]) 1);
clasohm@969
   261
by (rtac eval_fun_mono 1);
clasohm@969
   262
by (rewtac eval_fun_def);
clasohm@969
   263
by (dtac CollectD 1);
clasohm@969
   264
by (safe_tac HOL_cs);
clasohm@969
   265
by (ALLGOALS (resolve_tac prems));
clasohm@969
   266
by (ALLGOALS (fast_tac set_cs));
clasohm@969
   267
qed "eval_ind0";
clasohm@969
   268
clasohm@969
   269
val prems = goal MT.thy 
clasohm@969
   270
  " [| ve |- e ---> v; \
clasohm@969
   271
\      !!ve c. P ve (e_const c) (v_const c); \
clasohm@969
   272
\      !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \
clasohm@969
   273
\      !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); \
clasohm@969
   274
\      !!ev1 ev2 ve cl e. \
clasohm@969
   275
\        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@969
   276
\        P ve (fix ev2(ev1) = e) (v_clos cl); \
clasohm@969
   277
\      !!ve c1 c2 e1 e2. \
clasohm@969
   278
\        [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \
clasohm@969
   279
\        P ve (e1 @ e2) (v_const(c_app c1 c2)); \
clasohm@969
   280
\      !!ve vem evm e1 e2 em v v2. \
clasohm@969
   281
\        [|  P ve e1 (v_clos <|evm,em,vem|>); \
clasohm@969
   282
\            P ve e2 v2; \
clasohm@969
   283
\            P (vem + {evm |-> v2}) em v \
clasohm@969
   284
\        |] ==> P ve (e1 @ e2) v \
clasohm@969
   285
\   |] ==> P ve e v";
clasohm@969
   286
by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969
   287
by (rtac eval_ind0 1);
clasohm@969
   288
by (ALLGOALS (rtac infsys_pp1));
clasohm@969
   289
by (ALLGOALS (resolve_tac prems));
clasohm@969
   290
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969
   291
qed "eval_ind";
clasohm@969
   292
clasohm@969
   293
(* ############################################################ *)
clasohm@969
   294
(* Elaborations                                                 *)
clasohm@969
   295
(* ############################################################ *)
clasohm@969
   296
clasohm@969
   297
goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)";
clasohm@969
   298
by infsys_mono_tac;
clasohm@969
   299
qed "elab_fun_mono";
clasohm@969
   300
clasohm@969
   301
(* Introduction rules *)
clasohm@969
   302
clasohm@969
   303
val prems = goalw MT.thy [elab_def, elab_rel_def] 
clasohm@969
   304
  "c isof ty ==> te |- e_const(c) ===> ty";
clasohm@969
   305
by (cut_facts_tac prems 1);
clasohm@969
   306
by (rtac lfp_intro2 1);
clasohm@969
   307
by (rtac elab_fun_mono 1);
clasohm@969
   308
by (rewtac elab_fun_def);
clasohm@969
   309
by (rtac CollectI 1);br disjI1 1;
clasohm@969
   310
by (fast_tac HOL_cs 1);
clasohm@969
   311
qed "elab_const";
clasohm@969
   312
clasohm@969
   313
val prems = goalw MT.thy [elab_def, elab_rel_def] 
clasohm@969
   314
  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
clasohm@969
   315
by (cut_facts_tac prems 1);
clasohm@969
   316
by (rtac lfp_intro2 1);
clasohm@969
   317
by (rtac elab_fun_mono 1);
clasohm@969
   318
by (rewtac elab_fun_def);
clasohm@969
   319
by (rtac CollectI 1);br disjI2 1;br disjI1 1;
clasohm@969
   320
by (fast_tac HOL_cs 1);
clasohm@969
   321
qed "elab_var";
clasohm@969
   322
clasohm@969
   323
val prems = goalw MT.thy [elab_def, elab_rel_def] 
clasohm@969
   324
  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
clasohm@969
   325
by (cut_facts_tac prems 1);
clasohm@969
   326
by (rtac lfp_intro2 1);
clasohm@969
   327
by (rtac elab_fun_mono 1);
clasohm@969
   328
by (rewtac elab_fun_def);
clasohm@969
   329
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;
clasohm@969
   330
by (fast_tac HOL_cs 1);
clasohm@969
   331
qed "elab_fn";
clasohm@969
   332
clasohm@969
   333
val prems = goalw MT.thy [elab_def, elab_rel_def]
clasohm@969
   334
  " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
clasohm@969
   335
\   te |- fix f(x) = e ===> ty1->ty2";
clasohm@969
   336
by (cut_facts_tac prems 1);
clasohm@969
   337
by (rtac lfp_intro2 1);
clasohm@969
   338
by (rtac elab_fun_mono 1);
clasohm@969
   339
by (rewtac elab_fun_def);
clasohm@969
   340
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
clasohm@969
   341
by (fast_tac HOL_cs 1);
clasohm@969
   342
qed "elab_fix";
clasohm@969
   343
clasohm@969
   344
val prems = goalw MT.thy [elab_def, elab_rel_def] 
clasohm@969
   345
  " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
clasohm@969
   346
\   te |- e1 @ e2 ===> ty2";
clasohm@969
   347
by (cut_facts_tac prems 1);
clasohm@969
   348
by (rtac lfp_intro2 1);
clasohm@969
   349
by (rtac elab_fun_mono 1);
clasohm@969
   350
by (rewtac elab_fun_def);
clasohm@969
   351
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;
clasohm@969
   352
by (fast_tac HOL_cs 1);
clasohm@969
   353
qed "elab_app";
clasohm@969
   354
clasohm@969
   355
(* Strong elimination, induction on elaborations *)
clasohm@969
   356
clasohm@969
   357
val prems = goalw MT.thy [elab_def, elab_rel_def]
clasohm@969
   358
  " [| te |- e ===> t; \
clasohm@969
   359
\      !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
clasohm@969
   360
\      !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \
clasohm@969
   361
\      !!te x e t1 t2. \
clasohm@969
   362
\        [| te + {x |=> t1} |- e ===> t2; P(<<te + {x |=> t1},e>,t2>) |] ==> \
clasohm@969
   363
\        P(<<te,fn x => e>,t1->t2>); \
clasohm@969
   364
\      !!te f x e t1 t2. \
clasohm@969
   365
\        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
clasohm@969
   366
\           P(<<te + {f |=> t1->t2} + {x |=> t1},e>,t2>) \
clasohm@969
   367
\        |] ==> \
clasohm@969
   368
\        P(<<te,fix f(x) = e>,t1->t2>); \
clasohm@969
   369
\      !!te e1 e2 t1 t2. \
clasohm@969
   370
\        [| te |- e1 ===> t1->t2; P(<<te,e1>,t1->t2>); \
clasohm@969
   371
\           te |- e2 ===> t1; P(<<te,e2>,t1>) \
clasohm@969
   372
\        |] ==> \
clasohm@969
   373
\        P(<<te,e1 @ e2>,t2>) \
clasohm@969
   374
\   |] ==> \
clasohm@969
   375
\   P(<<te,e>,t>)";
clasohm@969
   376
by (resolve_tac (prems RL [lfp_ind2]) 1);
clasohm@969
   377
by (rtac elab_fun_mono 1);
clasohm@969
   378
by (rewtac elab_fun_def);
clasohm@969
   379
by (dtac CollectD 1);
clasohm@969
   380
by (safe_tac HOL_cs);
clasohm@969
   381
by (ALLGOALS (resolve_tac prems));
clasohm@969
   382
by (ALLGOALS (fast_tac set_cs));
clasohm@969
   383
qed "elab_ind0";
clasohm@969
   384
clasohm@969
   385
val prems = goal MT.thy
clasohm@969
   386
  " [| te |- e ===> t; \
clasohm@969
   387
\       !!te c t. c isof t ==> P te (e_const c) t; \
clasohm@969
   388
\      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
clasohm@969
   389
\      !!te x e t1 t2. \
clasohm@969
   390
\        [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> \
clasohm@969
   391
\        P te (fn x => e) (t1->t2); \
clasohm@969
   392
\      !!te f x e t1 t2. \
clasohm@969
   393
\        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
clasohm@969
   394
\           P (te + {f |=> t1->t2} + {x |=> t1}) e t2 \
clasohm@969
   395
\        |] ==> \
clasohm@969
   396
\        P te (fix f(x) = e) (t1->t2); \
clasohm@969
   397
\      !!te e1 e2 t1 t2. \
clasohm@969
   398
\        [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \
clasohm@969
   399
\           te |- e2 ===> t1; P te e2 t1 \
clasohm@969
   400
\        |] ==> \
clasohm@969
   401
\        P te (e1 @ e2) t2 \ 
clasohm@969
   402
\   |] ==> \
clasohm@969
   403
\   P te e t";
clasohm@969
   404
by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969
   405
by (rtac elab_ind0 1);
clasohm@969
   406
by (ALLGOALS (rtac infsys_pp1));
clasohm@969
   407
by (ALLGOALS (resolve_tac prems));
clasohm@969
   408
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969
   409
qed "elab_ind";
clasohm@969
   410
clasohm@969
   411
(* Weak elimination, case analysis on elaborations *)
clasohm@969
   412
clasohm@969
   413
val prems = goalw MT.thy [elab_def, elab_rel_def]
clasohm@969
   414
  " [| te |- e ===> t; \
clasohm@969
   415
\      !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
clasohm@969
   416
\      !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \
clasohm@969
   417
\      !!te x e t1 t2. \
clasohm@969
   418
\        te + {x |=> t1} |- e ===> t2 ==> P(<<te,fn x => e>,t1->t2>); \
clasohm@969
   419
\      !!te f x e t1 t2. \
clasohm@969
   420
\        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
clasohm@969
   421
\        P(<<te,fix f(x) = e>,t1->t2>); \
clasohm@969
   422
\      !!te e1 e2 t1 t2. \
clasohm@969
   423
\        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
clasohm@969
   424
\        P(<<te,e1 @ e2>,t2>) \
clasohm@969
   425
\   |] ==> \
clasohm@969
   426
\   P(<<te,e>,t>)";
clasohm@969
   427
by (resolve_tac (prems RL [lfp_elim2]) 1);
clasohm@969
   428
by (rtac elab_fun_mono 1);
clasohm@969
   429
by (rewtac elab_fun_def);
clasohm@969
   430
by (dtac CollectD 1);
clasohm@969
   431
by (safe_tac HOL_cs);
clasohm@969
   432
by (ALLGOALS (resolve_tac prems));
clasohm@969
   433
by (ALLGOALS (fast_tac set_cs));
clasohm@969
   434
qed "elab_elim0";
clasohm@969
   435
clasohm@969
   436
val prems = goal MT.thy
clasohm@969
   437
  " [| te |- e ===> t; \
clasohm@969
   438
\       !!te c t. c isof t ==> P te (e_const c) t; \
clasohm@969
   439
\      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
clasohm@969
   440
\      !!te x e t1 t2. \
clasohm@969
   441
\        te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); \
clasohm@969
   442
\      !!te f x e t1 t2. \
clasohm@969
   443
\        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
clasohm@969
   444
\        P te (fix f(x) = e) (t1->t2); \
clasohm@969
   445
\      !!te e1 e2 t1 t2. \
clasohm@969
   446
\        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
clasohm@969
   447
\        P te (e1 @ e2) t2 \ 
clasohm@969
   448
\   |] ==> \
clasohm@969
   449
\   P te e t";
clasohm@969
   450
by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969
   451
by (rtac elab_elim0 1);
clasohm@969
   452
by (ALLGOALS (rtac infsys_pp1));
clasohm@969
   453
by (ALLGOALS (resolve_tac prems));
clasohm@969
   454
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969
   455
qed "elab_elim";
clasohm@969
   456
clasohm@969
   457
(* Elimination rules for each expression *)
clasohm@969
   458
clasohm@969
   459
fun elab_e_elim_tac p = 
clasohm@969
   460
  ( (rtac elab_elim 1) THEN 
clasohm@969
   461
    (resolve_tac p 1) THEN 
clasohm@969
   462
    (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
clasohm@969
   463
  );
clasohm@969
   464
clasohm@969
   465
val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
clasohm@969
   466
by (elab_e_elim_tac prems);
clasohm@969
   467
qed "elab_const_elim_lem";
clasohm@969
   468
clasohm@969
   469
val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
clasohm@969
   470
by (cut_facts_tac prems 1);
clasohm@969
   471
by (dtac elab_const_elim_lem 1);
clasohm@969
   472
by (fast_tac prop_cs 1);
clasohm@969
   473
qed "elab_const_elim";
clasohm@969
   474
clasohm@969
   475
val prems = goal MT.thy 
clasohm@969
   476
  "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))";
clasohm@969
   477
by (elab_e_elim_tac prems);
clasohm@969
   478
qed "elab_var_elim_lem";
clasohm@969
   479
clasohm@969
   480
val prems = goal MT.thy 
clasohm@969
   481
  "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
clasohm@969
   482
by (cut_facts_tac prems 1);
clasohm@969
   483
by (dtac elab_var_elim_lem 1);
clasohm@969
   484
by (fast_tac prop_cs 1);
clasohm@969
   485
qed "elab_var_elim";
clasohm@969
   486
clasohm@969
   487
val prems = goal MT.thy 
clasohm@969
   488
  " te |- e ===> t ==> \
clasohm@969
   489
\   ( e = fn x1 => e1 --> \
clasohm@969
   490
\     (? t1 t2.t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
clasohm@969
   491
\   )";
clasohm@969
   492
by (elab_e_elim_tac prems);
clasohm@969
   493
qed "elab_fn_elim_lem";
clasohm@969
   494
clasohm@969
   495
val prems = goal MT.thy 
clasohm@969
   496
  " te |- fn x1 => e1 ===> t ==> \
clasohm@969
   497
\   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
clasohm@969
   498
by (cut_facts_tac prems 1);
clasohm@969
   499
by (dtac elab_fn_elim_lem 1);
clasohm@969
   500
by (fast_tac prop_cs 1);
clasohm@969
   501
qed "elab_fn_elim";
clasohm@969
   502
clasohm@969
   503
val prems = goal MT.thy 
clasohm@969
   504
  " te |- e ===> t ==> \
clasohm@969
   505
\   (e = fix f(x) = e1 --> \
clasohm@969
   506
\   (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; 
clasohm@969
   507
by (elab_e_elim_tac prems);
clasohm@969
   508
qed "elab_fix_elim_lem";
clasohm@969
   509
clasohm@969
   510
val prems = goal MT.thy 
clasohm@969
   511
  " te |- fix ev1(ev2) = e1 ===> t ==> \
clasohm@969
   512
\   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
clasohm@969
   513
by (cut_facts_tac prems 1);
clasohm@969
   514
by (dtac elab_fix_elim_lem 1);
clasohm@969
   515
by (fast_tac prop_cs 1);
clasohm@969
   516
qed "elab_fix_elim";
clasohm@969
   517
clasohm@969
   518
val prems = goal MT.thy 
clasohm@969
   519
  " te |- e ===> t2 ==> \
clasohm@969
   520
\   (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; 
clasohm@969
   521
by (elab_e_elim_tac prems);
clasohm@969
   522
qed "elab_app_elim_lem";
clasohm@969
   523
clasohm@969
   524
val prems = goal MT.thy 
clasohm@969
   525
  "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
clasohm@969
   526
by (cut_facts_tac prems 1);
clasohm@969
   527
by (dtac elab_app_elim_lem 1);
clasohm@969
   528
by (fast_tac prop_cs 1);
clasohm@969
   529
qed "elab_app_elim";
clasohm@969
   530
clasohm@969
   531
(* ############################################################ *)
clasohm@969
   532
(* The extended correspondence relation                       *)
clasohm@969
   533
(* ############################################################ *)
clasohm@969
   534
clasohm@969
   535
(* Monotonicity of hasty_fun *)
clasohm@969
   536
clasohm@969
   537
goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
clasohm@969
   538
by infsys_mono_tac;
clasohm@969
   539
bind_thm("mono_hasty_fun",  result());
clasohm@969
   540
clasohm@969
   541
(* 
clasohm@969
   542
  Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
clasohm@969
   543
  enjoys two strong indtroduction (co-induction) rules and an elimination rule.
clasohm@969
   544
*)
clasohm@969
   545
clasohm@969
   546
(* First strong indtroduction (co-induction) rule for hasty_rel *)
clasohm@969
   547
clasohm@969
   548
val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> <v_const(c),t> : hasty_rel";
clasohm@969
   549
by (cut_facts_tac prems 1);
clasohm@969
   550
by (rtac gfp_coind2 1);
clasohm@969
   551
by (rewtac MT.hasty_fun_def);
clasohm@969
   552
by (rtac CollectI 1);br disjI1 1;
clasohm@969
   553
by (fast_tac HOL_cs 1);
clasohm@969
   554
by (rtac mono_hasty_fun 1);
clasohm@969
   555
qed "hasty_rel_const_coind";
clasohm@969
   556
clasohm@969
   557
(* Second strong introduction (co-induction) rule for hasty_rel *)
clasohm@969
   558
clasohm@969
   559
val prems = goalw MT.thy [hasty_rel_def]
clasohm@969
   560
  " [|  te |- fn ev => e ===> t; \
clasohm@969
   561
\       ve_dom(ve) = te_dom(te); \
clasohm@969
   562
\       ! ev1. \
clasohm@969
   563
\         ev1:ve_dom(ve) --> \
clasohm@969
   564
\         <ve_app ve ev1,te_app te ev1> : {<v_clos(<|ev,e,ve|>),t>} Un hasty_rel \
clasohm@969
   565
\   |] ==> \
clasohm@969
   566
\   <v_clos(<|ev,e,ve|>),t> : hasty_rel";
clasohm@969
   567
by (cut_facts_tac prems 1);
clasohm@969
   568
by (rtac gfp_coind2 1);
clasohm@969
   569
by (rewtac hasty_fun_def);
clasohm@969
   570
by (rtac CollectI 1);br disjI2 1;
clasohm@969
   571
by (fast_tac HOL_cs 1);
clasohm@969
   572
by (rtac mono_hasty_fun 1);
clasohm@969
   573
qed "hasty_rel_clos_coind";
clasohm@969
   574
clasohm@969
   575
(* Elimination rule for hasty_rel *)
clasohm@969
   576
clasohm@969
   577
val prems = goalw MT.thy [hasty_rel_def]
clasohm@969
   578
  " [| !! c t.c isof t ==> P(<v_const(c),t>); \
clasohm@969
   579
\      !! te ev e t ve. \
clasohm@969
   580
\        [| te |- fn ev => e ===> t; \
clasohm@969
   581
\           ve_dom(ve) = te_dom(te); \
clasohm@969
   582
\           !ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
clasohm@969
   583
\        |] ==> P(<v_clos(<|ev,e,ve|>),t>); \
clasohm@969
   584
\      <v,t> : hasty_rel \
clasohm@969
   585
\   |] ==> P(<v,t>)";
clasohm@969
   586
by (cut_facts_tac prems 1);
clasohm@969
   587
by (etac gfp_elim2 1);
clasohm@969
   588
by (rtac mono_hasty_fun 1);
clasohm@969
   589
by (rewtac hasty_fun_def);
clasohm@969
   590
by (dtac CollectD 1);
clasohm@969
   591
by (fold_goals_tac [hasty_fun_def]);
clasohm@969
   592
by (safe_tac HOL_cs);
clasohm@969
   593
by (ALLGOALS (resolve_tac prems));
clasohm@969
   594
by (ALLGOALS (fast_tac set_cs));
clasohm@969
   595
qed "hasty_rel_elim0";
clasohm@969
   596
clasohm@969
   597
val prems = goal MT.thy 
clasohm@969
   598
  " [| <v,t> : hasty_rel; \
clasohm@969
   599
\      !! c t.c isof t ==> P (v_const c) t; \
clasohm@969
   600
\      !! te ev e t ve. \
clasohm@969
   601
\        [| te |- fn ev => e ===> t; \
clasohm@969
   602
\           ve_dom(ve) = te_dom(te); \
clasohm@969
   603
\           !ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
clasohm@969
   604
\        |] ==> P (v_clos <|ev,e,ve|>) t \
clasohm@969
   605
\   |] ==> P v t";
clasohm@969
   606
by (res_inst_tac [("P","P")] infsys_p2 1);
clasohm@969
   607
by (rtac hasty_rel_elim0 1);
clasohm@969
   608
by (ALLGOALS (rtac infsys_p1));
clasohm@969
   609
by (ALLGOALS (resolve_tac prems));
clasohm@969
   610
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
clasohm@969
   611
qed "hasty_rel_elim";
clasohm@969
   612
clasohm@969
   613
(* Introduction rules for hasty *)
clasohm@969
   614
clasohm@969
   615
val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
clasohm@969
   616
by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
clasohm@969
   617
qed "hasty_const";
clasohm@969
   618
clasohm@969
   619
val prems = goalw MT.thy [hasty_def,hasty_env_def] 
clasohm@969
   620
  "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
clasohm@969
   621
by (cut_facts_tac prems 1);
clasohm@969
   622
by (rtac hasty_rel_clos_coind 1);
clasohm@969
   623
by (ALLGOALS (fast_tac set_cs));
clasohm@969
   624
qed "hasty_clos";
clasohm@969
   625
clasohm@969
   626
(* Elimination on constants for hasty *)
clasohm@969
   627
clasohm@969
   628
val prems = goalw MT.thy [hasty_def] 
clasohm@969
   629
  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
clasohm@969
   630
by (cut_facts_tac prems 1);
clasohm@969
   631
by (rtac hasty_rel_elim 1);
clasohm@969
   632
by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
clasohm@969
   633
qed "hasty_elim_const_lem";
clasohm@969
   634
clasohm@969
   635
val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
clasohm@969
   636
by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
clasohm@969
   637
by (fast_tac HOL_cs 1);
clasohm@969
   638
qed "hasty_elim_const";
clasohm@969
   639
clasohm@969
   640
(* Elimination on closures for hasty *)
clasohm@969
   641
clasohm@969
   642
val prems = goalw MT.thy [hasty_env_def,hasty_def] 
clasohm@969
   643
  " v hasty t ==> \
clasohm@969
   644
\   ! x e ve. \
clasohm@969
   645
\     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
clasohm@969
   646
by (cut_facts_tac prems 1);
clasohm@969
   647
by (rtac hasty_rel_elim 1);
clasohm@969
   648
by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
clasohm@969
   649
qed "hasty_elim_clos_lem";
clasohm@969
   650
clasohm@969
   651
val prems = goal MT.thy 
clasohm@969
   652
  "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===> t & ve hastyenv te ";
clasohm@969
   653
by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
clasohm@969
   654
by (fast_tac HOL_cs 1);
clasohm@969
   655
qed "hasty_elim_clos";
clasohm@969
   656
clasohm@969
   657
(* ############################################################ *)
clasohm@969
   658
(* The pointwise extension of hasty to environments             *)
clasohm@969
   659
(* ############################################################ *)
clasohm@969
   660
clasohm@969
   661
val prems = goal MT.thy
clasohm@969
   662
  "[| ve hastyenv te; v hasty t |] ==> \
clasohm@969
   663
\  ve + {ev |-> v} hastyenv te + {ev |=> t}";
clasohm@969
   664
by (cut_facts_tac prems 1);
clasohm@969
   665
by (SELECT_GOAL (rewtac hasty_env_def) 1);
clasohm@969
   666
by (safe_tac HOL_cs);
clasohm@969
   667
by (rtac (ve_dom_owr RS ssubst) 1);
clasohm@969
   668
by (rtac (te_dom_owr RS ssubst) 1);
clasohm@969
   669
by (etac subst 1);br refl 1;
clasohm@969
   670
clasohm@969
   671
by (dtac (ve_dom_owr RS subst) 1);back();back();back();
clasohm@969
   672
by (etac UnSE 1);be conjE 1;
clasohm@969
   673
by (dtac notsingletonI 1);bd not_sym 1;
clasohm@969
   674
by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;
clasohm@969
   675
by (rtac (te_app_owr2 RS ssubst) 1);ba 1;
clasohm@969
   676
by (fast_tac HOL_cs 1);
clasohm@969
   677
by (dtac singletonD 1);by (hyp_subst_tac 1);
clasohm@969
   678
clasohm@969
   679
by (rtac (ve_app_owr1 RS ssubst) 1);
clasohm@969
   680
by (rtac (te_app_owr1 RS ssubst) 1);
clasohm@969
   681
by (assume_tac 1);
clasohm@969
   682
qed "hasty_env1";
clasohm@969
   683
clasohm@969
   684
(* ############################################################ *)
clasohm@969
   685
(* The Consistency theorem                                      *)
clasohm@969
   686
(* ############################################################ *)
clasohm@969
   687
clasohm@969
   688
val prems = goal MT.thy 
clasohm@969
   689
  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
clasohm@969
   690
by (cut_facts_tac prems 1);
clasohm@969
   691
by (dtac elab_const_elim 1);
clasohm@969
   692
by (etac hasty_const 1);
clasohm@969
   693
qed "consistency_const";
clasohm@969
   694
clasohm@969
   695
val prems = goalw MT.thy [hasty_env_def]
clasohm@969
   696
  " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
clasohm@969
   697
\   ve_app ve ev hasty t";
clasohm@969
   698
by (cut_facts_tac prems 1);
clasohm@969
   699
by (dtac elab_var_elim 1);
clasohm@969
   700
by (fast_tac HOL_cs 1);
clasohm@969
   701
qed "consistency_var";
clasohm@969
   702
clasohm@969
   703
val prems = goal MT.thy
clasohm@969
   704
  " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
clasohm@969
   705
\   v_clos(<| ev, e, ve |>) hasty t";
clasohm@969
   706
by (cut_facts_tac prems 1);
clasohm@969
   707
by (rtac hasty_clos 1);
clasohm@969
   708
by (fast_tac prop_cs 1);
clasohm@969
   709
qed "consistency_fn";
clasohm@969
   710
clasohm@969
   711
val prems = goalw MT.thy [hasty_env_def,hasty_def]
clasohm@969
   712
  " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
clasohm@969
   713
\      ve hastyenv te ; \
clasohm@969
   714
\      te |- fix ev2  ev1  = e ===> t \
clasohm@969
   715
\   |] ==> \
clasohm@969
   716
\   v_clos(cl) hasty t";
clasohm@969
   717
by (cut_facts_tac prems 1);
clasohm@969
   718
by (dtac elab_fix_elim 1);
clasohm@969
   719
by (safe_tac HOL_cs);
clasohm@969
   720
by ((forward_tac [ssubst] 1) THEN (assume_tac 2) THEN 
clasohm@969
   721
    (rtac hasty_rel_clos_coind 1));
clasohm@969
   722
by (etac elab_fn 1);
clasohm@969
   723
clasohm@969
   724
by (rtac (ve_dom_owr RS ssubst) 1);
clasohm@969
   725
by (rtac (te_dom_owr RS ssubst) 1);
clasohm@969
   726
by ((etac subst 1) THEN (rtac refl 1));
clasohm@969
   727
clasohm@969
   728
by (rtac (ve_dom_owr RS ssubst) 1);
clasohm@969
   729
by (safe_tac HOL_cs);
clasohm@969
   730
by (dtac (Un_commute RS subst) 1);
clasohm@969
   731
by (etac UnSE 1);
clasohm@969
   732
clasohm@969
   733
by (safe_tac HOL_cs);
clasohm@969
   734
by (dtac notsingletonI 1);bd not_sym 1;
clasohm@969
   735
by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;
clasohm@969
   736
by (rtac (te_app_owr2 RS ssubst) 1);ba 1;
clasohm@969
   737
by (fast_tac set_cs 1);
clasohm@969
   738
clasohm@969
   739
by (etac singletonE 1);
clasohm@969
   740
by (hyp_subst_tac 1);
clasohm@969
   741
by (rtac (ve_app_owr1 RS ssubst) 1);
clasohm@969
   742
by (rtac (te_app_owr1 RS ssubst) 1);
clasohm@969
   743
by (etac subst 1);
clasohm@969
   744
by (fast_tac set_cs 1);
clasohm@969
   745
qed "consistency_fix";
clasohm@969
   746
clasohm@969
   747
val prems = goal MT.thy 
clasohm@969
   748
  " [| ! t te. ve hastyenv te  --> te |- e1 ===> t --> v_const(c1) hasty t; \
clasohm@969
   749
\      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
clasohm@969
   750
\      ve hastyenv te ; te |- e1 @ e2 ===> t \
clasohm@969
   751
\   |] ==> \
clasohm@969
   752
\   v_const(c_app c1 c2) hasty t";
clasohm@969
   753
by (cut_facts_tac prems 1);
clasohm@969
   754
by (dtac elab_app_elim 1);
clasohm@969
   755
by (safe_tac HOL_cs);
clasohm@969
   756
by (rtac hasty_const 1);
clasohm@969
   757
by (rtac isof_app 1);
clasohm@969
   758
by (rtac hasty_elim_const 1);
clasohm@969
   759
by (fast_tac HOL_cs 1);
clasohm@969
   760
by (rtac hasty_elim_const 1);
clasohm@969
   761
by (fast_tac HOL_cs 1);
clasohm@969
   762
qed "consistency_app1";
clasohm@969
   763
clasohm@969
   764
val prems = goal MT.thy 
clasohm@969
   765
  " [| ! t te. \
clasohm@969
   766
\        ve hastyenv te  --> \
clasohm@969
   767
\        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
clasohm@969
   768
\      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
clasohm@969
   769
\      ! t te. \
clasohm@969
   770
\        vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t; \
clasohm@969
   771
\      ve hastyenv te ; \
clasohm@969
   772
\      te |- e1 @ e2 ===> t \
clasohm@969
   773
\   |] ==> \
clasohm@969
   774
\   v hasty t";
clasohm@969
   775
by (cut_facts_tac prems 1);
clasohm@969
   776
by (dtac elab_app_elim 1);
clasohm@969
   777
by (safe_tac HOL_cs);
clasohm@969
   778
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;
clasohm@969
   779
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;
clasohm@969
   780
by (dtac hasty_elim_clos 1);
clasohm@969
   781
by (safe_tac HOL_cs);
clasohm@969
   782
by (dtac elab_fn_elim 1);
clasohm@969
   783
by (safe_tac HOL_cs);
clasohm@969
   784
by (dtac t_fun_inj 1);
clasohm@969
   785
by (safe_tac prop_cs);
clasohm@969
   786
by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
clasohm@969
   787
qed "consistency_app2";
clasohm@969
   788
clasohm@969
   789
val prems = goal MT.thy 
clasohm@969
   790
  "ve |- e ---> v ==> (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
clasohm@969
   791
clasohm@969
   792
(* Proof by induction on the structure of evaluations *)
clasohm@969
   793
clasohm@969
   794
by (resolve_tac (prems RL [eval_ind]) 1);
clasohm@969
   795
by (safe_tac HOL_cs);
clasohm@969
   796
clasohm@969
   797
by (rtac consistency_const 1);ba 1;ba 1;
clasohm@969
   798
by (rtac consistency_var 1);ba 1;ba 1;ba 1;
clasohm@969
   799
by (rtac consistency_fn 1);ba 1;ba 1;
clasohm@969
   800
by (rtac consistency_fix 1);ba 1;ba 1;ba 1;
clasohm@969
   801
by (rtac consistency_app1 1);ba 1;ba 1;ba 1;ba 1;
clasohm@969
   802
by (rtac consistency_app2 1);ba 5;ba 4;ba 3;ba 2;ba 1;
clasohm@969
   803
qed "consistency";
clasohm@969
   804
clasohm@969
   805
(* ############################################################ *)
clasohm@969
   806
(* The Basic Consistency theorem                                *)
clasohm@969
   807
(* ############################################################ *)
clasohm@969
   808
clasohm@969
   809
val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
clasohm@969
   810
  "ve isofenv te ==> ve hastyenv te";
clasohm@969
   811
by (cut_facts_tac prems 1);
clasohm@969
   812
by (safe_tac HOL_cs);
clasohm@969
   813
by (etac allE 1);be impE 1;ba 1;be exE 1;be conjE 1;
clasohm@969
   814
by (dtac hasty_const 1);
clasohm@969
   815
by ((rtac ssubst 1) THEN (assume_tac 1) THEN (assume_tac 1));
clasohm@969
   816
qed "basic_consistency_lem";
clasohm@969
   817
clasohm@969
   818
val prems = goal MT.thy
clasohm@969
   819
  "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
clasohm@969
   820
by (cut_facts_tac prems 1);
clasohm@969
   821
by (rtac hasty_elim_const 1);
clasohm@969
   822
by (dtac consistency 1);
clasohm@969
   823
by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
clasohm@969
   824
qed "basic_consistency";
clasohm@969
   825
clasohm@969
   826