src/HOL/ex/MT.ML
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 22548 6ce4bddf3bcb
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
clasohm@1465
     1
(*  Title:      HOL/ex/MT.ML
clasohm@969
     2
    ID:         $Id$
clasohm@1465
     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).
lcp@1047
    14
lcp@1047
    15
NEEDS TO USE INDUCTIVE DEFS PACKAGE
clasohm@969
    16
*)
clasohm@969
    17
clasohm@969
    18
(* ############################################################ *)
clasohm@969
    19
(* Inference systems                                            *)
clasohm@969
    20
(* ############################################################ *)
clasohm@969
    21
paulson@15386
    22
val lfp_lemma2 = thm "lfp_lemma2";
paulson@15386
    23
val lfp_lemma3 = thm "lfp_lemma3";
paulson@15386
    24
val gfp_lemma2 = thm "gfp_lemma2";
paulson@15386
    25
val gfp_lemma3 = thm "gfp_lemma3";
paulson@15386
    26
paulson@2935
    27
val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
clasohm@969
    28
wenzelm@17289
    29
val prems = goal (the_context ()) "P a b ==> P (fst (a,b)) (snd (a,b))";
wenzelm@4089
    30
by (simp_tac (simpset() addsimps prems) 1);
clasohm@969
    31
qed "infsys_p1";
clasohm@969
    32
paulson@5148
    33
Goal "P (fst (a,b)) (snd (a,b)) ==> P a b";
clasohm@1266
    34
by (Asm_full_simp_tac 1);
clasohm@969
    35
qed "infsys_p2";
clasohm@969
    36
paulson@5148
    37
Goal "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
clasohm@1266
    38
by (Asm_full_simp_tac 1);
clasohm@969
    39
qed "infsys_pp1";
clasohm@969
    40
paulson@5148
    41
Goal "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
clasohm@1266
    42
by (Asm_full_simp_tac 1);
clasohm@969
    43
qed "infsys_pp2";
clasohm@969
    44
clasohm@969
    45
(* ############################################################ *)
clasohm@969
    46
(* Fixpoints                                                    *)
clasohm@969
    47
(* ############################################################ *)
clasohm@969
    48
clasohm@969
    49
(* Least fixpoints *)
clasohm@969
    50
wenzelm@17289
    51
val prems = goal (the_context ()) "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
clasohm@969
    52
by (rtac subsetD 1);
clasohm@969
    53
by (rtac lfp_lemma2 1);
lcp@1047
    54
by (resolve_tac prems 1);
lcp@1047
    55
by (resolve_tac prems 1);
clasohm@969
    56
qed "lfp_intro2";
clasohm@969
    57
wenzelm@17289
    58
val prems = goal (the_context ())
clasohm@969
    59
  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
clasohm@969
    60
\   P(x)";
clasohm@969
    61
by (cut_facts_tac prems 1);
lcp@1047
    62
by (resolve_tac prems 1);
lcp@1047
    63
by (rtac subsetD 1);
lcp@1047
    64
by (rtac lfp_lemma3 1);
lcp@1047
    65
by (assume_tac 1);
lcp@1047
    66
by (assume_tac 1);
clasohm@969
    67
qed "lfp_elim2";
clasohm@969
    68
wenzelm@17289
    69
val prems = goal (the_context ())
wenzelm@3842
    70
  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
clasohm@969
    71
\   P(x)";
clasohm@969
    72
by (cut_facts_tac prems 1);
berghofe@21026
    73
by (etac (thm "lfp_induct_set") 1);
lcp@1047
    74
by (assume_tac 1);
clasohm@969
    75
by (eresolve_tac prems 1);
clasohm@969
    76
qed "lfp_ind2";
clasohm@969
    77
clasohm@969
    78
(* Greatest fixpoints *)
clasohm@969
    79
clasohm@969
    80
(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
clasohm@969
    81
wenzelm@17289
    82
val [cih,monoh] = goal (the_context ()) "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
clasohm@969
    83
by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
haftmann@22548
    84
by (rtac (monoh RS @{thm monoD}) 1);
lcp@1047
    85
by (rtac (UnE RS subsetI) 1);
lcp@1047
    86
by (assume_tac 1);
wenzelm@4089
    87
by (blast_tac (claset() addSIs [cih]) 1);
haftmann@22548
    88
by (rtac (monoh RS @{thm monoD} RS subsetD) 1);
wenzelm@21669
    89
by (rtac (thm "Un_upper2") 1);
clasohm@969
    90
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
clasohm@969
    91
qed "gfp_coind2";
clasohm@969
    92
wenzelm@17289
    93
val [gfph,monoh,caseh] = goal (the_context ())
clasohm@969
    94
  "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
lcp@1047
    95
by (rtac caseh 1);
lcp@1047
    96
by (rtac subsetD 1);
lcp@1047
    97
by (rtac gfp_lemma2 1);
lcp@1047
    98
by (rtac monoh 1);
lcp@1047
    99
by (rtac gfph 1);
clasohm@969
   100
qed "gfp_elim2";
clasohm@969
   101
clasohm@969
   102
(* ############################################################ *)
clasohm@969
   103
(* Expressions                                                  *)
clasohm@969
   104
(* ############################################################ *)
clasohm@969
   105
clasohm@969
   106
val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
clasohm@969
   107
wenzelm@17289
   108
val e_disjs =
wenzelm@17289
   109
  [ e_disj_const_var,
wenzelm@17289
   110
    e_disj_const_fn,
wenzelm@17289
   111
    e_disj_const_fix,
clasohm@969
   112
    e_disj_const_app,
wenzelm@17289
   113
    e_disj_var_fn,
wenzelm@17289
   114
    e_disj_var_fix,
wenzelm@17289
   115
    e_disj_var_app,
wenzelm@17289
   116
    e_disj_fn_fix,
wenzelm@17289
   117
    e_disj_fn_app,
clasohm@969
   118
    e_disj_fix_app
clasohm@969
   119
  ];
clasohm@969
   120
clasohm@969
   121
val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
clasohm@969
   122
val e_disj_se = (e_disj_si RL [notE]);
clasohm@969
   123
clasohm@969
   124
fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
clasohm@969
   125
clasohm@969
   126
(* ############################################################ *)
clasohm@969
   127
(* Values                                                      *)
clasohm@969
   128
(* ############################################################ *)
clasohm@969
   129
clasohm@969
   130
val v_disjs = [v_disj_const_clos];
clasohm@969
   131
val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
clasohm@969
   132
val v_disj_se = (v_disj_si RL [notE]);
clasohm@969
   133
clasohm@969
   134
val v_injs = [v_const_inj, v_clos_inj];
clasohm@969
   135
clasohm@969
   136
fun v_ext_cs cs  = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
clasohm@969
   137
clasohm@969
   138
(* ############################################################ *)
clasohm@969
   139
(* Evaluations                                                  *)
clasohm@969
   140
(* ############################################################ *)
clasohm@969
   141
clasohm@969
   142
(* Monotonicity of eval_fun *)
clasohm@969
   143
wenzelm@21669
   144
Goalw [thm "mono_def", eval_fun_def] "mono(eval_fun)";
clasohm@969
   145
by infsys_mono_tac;
clasohm@969
   146
qed "eval_fun_mono";
clasohm@969
   147
clasohm@969
   148
(* Introduction rules *)
clasohm@969
   149
wenzelm@5069
   150
Goalw [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
clasohm@969
   151
by (rtac lfp_intro2 1);
clasohm@969
   152
by (rtac eval_fun_mono 1);
clasohm@969
   153
by (rewtac eval_fun_def);
wenzelm@17289
   154
        (*Naughty!  But the quantifiers are nested VERY deeply...*)
wenzelm@4089
   155
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969
   156
qed "eval_const";
clasohm@969
   157
wenzelm@17289
   158
Goalw [eval_def, eval_rel_def]
clasohm@969
   159
  "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
clasohm@969
   160
by (rtac lfp_intro2 1);
clasohm@969
   161
by (rtac eval_fun_mono 1);
clasohm@969
   162
by (rewtac eval_fun_def);
wenzelm@4089
   163
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@1266
   164
qed "eval_var2";
clasohm@969
   165
wenzelm@17289
   166
Goalw [eval_def, eval_rel_def]
clasohm@969
   167
  "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
clasohm@969
   168
by (rtac lfp_intro2 1);
clasohm@969
   169
by (rtac eval_fun_mono 1);
clasohm@969
   170
by (rewtac eval_fun_def);
wenzelm@4089
   171
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969
   172
qed "eval_fn";
clasohm@969
   173
wenzelm@17289
   174
Goalw [eval_def, eval_rel_def]
clasohm@969
   175
  " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@969
   176
\   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
clasohm@969
   177
by (rtac lfp_intro2 1);
clasohm@969
   178
by (rtac eval_fun_mono 1);
clasohm@969
   179
by (rewtac eval_fun_def);
wenzelm@4089
   180
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969
   181
qed "eval_fix";
clasohm@969
   182
paulson@5148
   183
Goalw [eval_def, eval_rel_def]
clasohm@969
   184
  " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
wenzelm@17289
   185
\   ve |- e1 @@ e2 ---> v_const(c_app c1 c2)";
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);
wenzelm@4089
   189
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969
   190
qed "eval_app1";
clasohm@969
   191
wenzelm@17289
   192
Goalw [eval_def, eval_rel_def]
clasohm@969
   193
  " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
clasohm@969
   194
\       ve |- e2 ---> v2; \
clasohm@969
   195
\       vem + {xm |-> v2} |- em ---> v \
clasohm@969
   196
\   |] ==> \
wenzelm@17289
   197
\   ve |- e1 @@ e2 ---> v";
clasohm@969
   198
by (rtac lfp_intro2 1);
clasohm@969
   199
by (rtac eval_fun_mono 1);
clasohm@969
   200
by (rewtac eval_fun_def);
wenzelm@4089
   201
by (blast_tac (claset() addSIs [disjI2]) 1);
clasohm@969
   202
qed "eval_app2";
clasohm@969
   203
clasohm@969
   204
(* Strong elimination, induction on evaluations *)
clasohm@969
   205
wenzelm@17289
   206
val prems = goalw (the_context ()) [eval_def, eval_rel_def]
clasohm@969
   207
  " [| ve |- e ---> v; \
clasohm@972
   208
\      !!ve c. P(((ve,e_const(c)),v_const(c))); \
clasohm@972
   209
\      !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
clasohm@972
   210
\      !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
clasohm@969
   211
\      !!ev1 ev2 ve cl e. \
clasohm@969
   212
\        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@972
   213
\        P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
clasohm@969
   214
\      !!ve c1 c2 e1 e2. \
clasohm@972
   215
\        [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
wenzelm@17289
   216
\        P(((ve,e1 @@ e2),v_const(c_app c1 c2))); \
clasohm@969
   217
\      !!ve vem xm e1 e2 em v v2. \
clasohm@972
   218
\        [|  P(((ve,e1),v_clos(<|xm,em,vem|>))); \
clasohm@972
   219
\            P(((ve,e2),v2)); \
clasohm@972
   220
\            P(((vem + {xm |-> v2},em),v)) \
clasohm@969
   221
\        |] ==> \
wenzelm@17289
   222
\        P(((ve,e1 @@ e2),v)) \
clasohm@969
   223
\   |] ==> \
clasohm@972
   224
\   P(((ve,e),v))";
clasohm@969
   225
by (resolve_tac (prems RL [lfp_ind2]) 1);
clasohm@969
   226
by (rtac eval_fun_mono 1);
clasohm@969
   227
by (rewtac eval_fun_def);
clasohm@969
   228
by (dtac CollectD 1);
paulson@4153
   229
by Safe_tac;
clasohm@969
   230
by (ALLGOALS (resolve_tac prems));
paulson@2935
   231
by (ALLGOALS (Blast_tac));
clasohm@969
   232
qed "eval_ind0";
clasohm@969
   233
wenzelm@17289
   234
val prems = goal (the_context ())
clasohm@969
   235
  " [| ve |- e ---> v; \
clasohm@969
   236
\      !!ve c. P ve (e_const c) (v_const c); \
clasohm@969
   237
\      !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \
clasohm@969
   238
\      !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); \
clasohm@969
   239
\      !!ev1 ev2 ve cl e. \
clasohm@969
   240
\        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@969
   241
\        P ve (fix ev2(ev1) = e) (v_clos cl); \
clasohm@969
   242
\      !!ve c1 c2 e1 e2. \
clasohm@969
   243
\        [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \
wenzelm@17289
   244
\        P ve (e1 @@ e2) (v_const(c_app c1 c2)); \
clasohm@969
   245
\      !!ve vem evm e1 e2 em v v2. \
clasohm@969
   246
\        [|  P ve e1 (v_clos <|evm,em,vem|>); \
clasohm@969
   247
\            P ve e2 v2; \
clasohm@969
   248
\            P (vem + {evm |-> v2}) em v \
wenzelm@17289
   249
\        |] ==> P ve (e1 @@ e2) v \
clasohm@969
   250
\   |] ==> P ve e v";
clasohm@969
   251
by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969
   252
by (rtac eval_ind0 1);
clasohm@969
   253
by (ALLGOALS (rtac infsys_pp1));
clasohm@969
   254
by (ALLGOALS (resolve_tac prems));
clasohm@969
   255
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969
   256
qed "eval_ind";
clasohm@969
   257
clasohm@969
   258
(* ############################################################ *)
clasohm@969
   259
(* Elaborations                                                 *)
clasohm@969
   260
(* ############################################################ *)
clasohm@969
   261
wenzelm@21669
   262
Goalw [thm "mono_def", elab_fun_def] "mono(elab_fun)";
clasohm@969
   263
by infsys_mono_tac;
clasohm@969
   264
qed "elab_fun_mono";
clasohm@969
   265
clasohm@969
   266
(* Introduction rules *)
clasohm@969
   267
wenzelm@17289
   268
Goalw [elab_def, elab_rel_def]
paulson@5148
   269
  "c isof ty ==> te |- e_const(c) ===> ty";
clasohm@969
   270
by (rtac lfp_intro2 1);
clasohm@969
   271
by (rtac elab_fun_mono 1);
clasohm@969
   272
by (rewtac elab_fun_def);
wenzelm@4089
   273
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969
   274
qed "elab_const";
clasohm@969
   275
wenzelm@17289
   276
Goalw [elab_def, elab_rel_def]
paulson@5148
   277
  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
clasohm@969
   278
by (rtac lfp_intro2 1);
clasohm@969
   279
by (rtac elab_fun_mono 1);
clasohm@969
   280
by (rewtac elab_fun_def);
wenzelm@4089
   281
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969
   282
qed "elab_var";
clasohm@969
   283
wenzelm@17289
   284
Goalw [elab_def, elab_rel_def]
paulson@5148
   285
  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
clasohm@969
   286
by (rtac lfp_intro2 1);
clasohm@969
   287
by (rtac elab_fun_mono 1);
clasohm@969
   288
by (rewtac elab_fun_def);
wenzelm@4089
   289
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969
   290
qed "elab_fn";
clasohm@969
   291
wenzelm@5069
   292
Goalw [elab_def, elab_rel_def]
paulson@5148
   293
  "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
paulson@2935
   294
\        te |- fix f(x) = e ===> ty1->ty2";
clasohm@969
   295
by (rtac lfp_intro2 1);
clasohm@969
   296
by (rtac elab_fun_mono 1);
clasohm@969
   297
by (rewtac elab_fun_def);
wenzelm@4089
   298
by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969
   299
qed "elab_fix";
clasohm@969
   300
wenzelm@17289
   301
Goalw [elab_def, elab_rel_def]
paulson@5148
   302
  "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
wenzelm@17289
   303
\        te |- e1 @@ e2 ===> ty2";
clasohm@969
   304
by (rtac lfp_intro2 1);
clasohm@969
   305
by (rtac elab_fun_mono 1);
clasohm@969
   306
by (rewtac elab_fun_def);
wenzelm@4089
   307
by (blast_tac (claset() addSIs [disjI2]) 1);
clasohm@969
   308
qed "elab_app";
clasohm@969
   309
clasohm@969
   310
(* Strong elimination, induction on elaborations *)
clasohm@969
   311
wenzelm@17289
   312
val prems = goalw (the_context ()) [elab_def, elab_rel_def]
clasohm@969
   313
  " [| te |- e ===> t; \
clasohm@972
   314
\      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
clasohm@972
   315
\      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
clasohm@969
   316
\      !!te x e t1 t2. \
clasohm@972
   317
\        [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
clasohm@972
   318
\        P(((te,fn x => e),t1->t2)); \
clasohm@969
   319
\      !!te f x e t1 t2. \
clasohm@969
   320
\        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
clasohm@972
   321
\           P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
clasohm@969
   322
\        |] ==> \
clasohm@972
   323
\        P(((te,fix f(x) = e),t1->t2)); \
clasohm@969
   324
\      !!te e1 e2 t1 t2. \
clasohm@972
   325
\        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
clasohm@972
   326
\           te |- e2 ===> t1; P(((te,e2),t1)) \
clasohm@969
   327
\        |] ==> \
wenzelm@17289
   328
\        P(((te,e1 @@ e2),t2)) \
clasohm@969
   329
\   |] ==> \
clasohm@972
   330
\   P(((te,e),t))";
clasohm@969
   331
by (resolve_tac (prems RL [lfp_ind2]) 1);
clasohm@969
   332
by (rtac elab_fun_mono 1);
clasohm@969
   333
by (rewtac elab_fun_def);
clasohm@969
   334
by (dtac CollectD 1);
paulson@4153
   335
by Safe_tac;
clasohm@969
   336
by (ALLGOALS (resolve_tac prems));
paulson@2935
   337
by (ALLGOALS (Blast_tac));
clasohm@969
   338
qed "elab_ind0";
clasohm@969
   339
wenzelm@17289
   340
val prems = goal (the_context ())
clasohm@969
   341
  " [| te |- e ===> t; \
clasohm@969
   342
\       !!te c t. c isof t ==> P te (e_const c) t; \
clasohm@969
   343
\      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
clasohm@969
   344
\      !!te x e t1 t2. \
clasohm@969
   345
\        [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> \
clasohm@969
   346
\        P te (fn x => e) (t1->t2); \
clasohm@969
   347
\      !!te f x e t1 t2. \
clasohm@969
   348
\        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
clasohm@969
   349
\           P (te + {f |=> t1->t2} + {x |=> t1}) e t2 \
clasohm@969
   350
\        |] ==> \
clasohm@969
   351
\        P te (fix f(x) = e) (t1->t2); \
clasohm@969
   352
\      !!te e1 e2 t1 t2. \
clasohm@969
   353
\        [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \
clasohm@969
   354
\           te |- e2 ===> t1; P te e2 t1 \
clasohm@969
   355
\        |] ==> \
wenzelm@17289
   356
\        P te (e1 @@ e2) t2 \
clasohm@969
   357
\   |] ==> \
clasohm@969
   358
\   P te e t";
clasohm@969
   359
by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969
   360
by (rtac elab_ind0 1);
clasohm@969
   361
by (ALLGOALS (rtac infsys_pp1));
clasohm@969
   362
by (ALLGOALS (resolve_tac prems));
clasohm@969
   363
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969
   364
qed "elab_ind";
clasohm@969
   365
clasohm@969
   366
(* Weak elimination, case analysis on elaborations *)
clasohm@969
   367
wenzelm@17289
   368
val prems = goalw (the_context ()) [elab_def, elab_rel_def]
clasohm@969
   369
  " [| te |- e ===> t; \
clasohm@972
   370
\      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
clasohm@972
   371
\      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
clasohm@969
   372
\      !!te x e t1 t2. \
clasohm@972
   373
\        te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
clasohm@969
   374
\      !!te f x e t1 t2. \
clasohm@969
   375
\        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
clasohm@972
   376
\        P(((te,fix f(x) = e),t1->t2)); \
clasohm@969
   377
\      !!te e1 e2 t1 t2. \
clasohm@969
   378
\        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
wenzelm@17289
   379
\        P(((te,e1 @@ e2),t2)) \
clasohm@969
   380
\   |] ==> \
clasohm@972
   381
\   P(((te,e),t))";
clasohm@969
   382
by (resolve_tac (prems RL [lfp_elim2]) 1);
clasohm@969
   383
by (rtac elab_fun_mono 1);
clasohm@969
   384
by (rewtac elab_fun_def);
clasohm@969
   385
by (dtac CollectD 1);
paulson@4153
   386
by Safe_tac;
clasohm@969
   387
by (ALLGOALS (resolve_tac prems));
paulson@2935
   388
by (ALLGOALS (Blast_tac));
clasohm@969
   389
qed "elab_elim0";
clasohm@969
   390
wenzelm@17289
   391
val prems = goal (the_context ())
clasohm@969
   392
  " [| te |- e ===> t; \
clasohm@969
   393
\       !!te c t. c isof t ==> P te (e_const c) t; \
clasohm@969
   394
\      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
clasohm@969
   395
\      !!te x e t1 t2. \
clasohm@969
   396
\        te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); \
clasohm@969
   397
\      !!te f x e t1 t2. \
clasohm@969
   398
\        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
clasohm@969
   399
\        P te (fix f(x) = e) (t1->t2); \
clasohm@969
   400
\      !!te e1 e2 t1 t2. \
clasohm@969
   401
\        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
wenzelm@17289
   402
\        P te (e1 @@ e2) t2 \
clasohm@969
   403
\   |] ==> \
clasohm@969
   404
\   P te e t";
clasohm@969
   405
by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969
   406
by (rtac elab_elim0 1);
clasohm@969
   407
by (ALLGOALS (rtac infsys_pp1));
clasohm@969
   408
by (ALLGOALS (resolve_tac prems));
clasohm@969
   409
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969
   410
qed "elab_elim";
clasohm@969
   411
clasohm@969
   412
(* Elimination rules for each expression *)
clasohm@969
   413
wenzelm@17289
   414
fun elab_e_elim_tac p =
wenzelm@17289
   415
  ( (rtac elab_elim 1) THEN
wenzelm@17289
   416
    (resolve_tac p 1) THEN
paulson@4353
   417
    (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
clasohm@969
   418
  );
clasohm@969
   419
wenzelm@17289
   420
val prems = goal (the_context ()) "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
clasohm@969
   421
by (elab_e_elim_tac prems);
clasohm@969
   422
qed "elab_const_elim_lem";
clasohm@969
   423
paulson@5148
   424
Goal "te |- e_const(c) ===> t ==> c isof t";
clasohm@969
   425
by (dtac elab_const_elim_lem 1);
paulson@2935
   426
by (Blast_tac 1);
clasohm@969
   427
qed "elab_const_elim";
clasohm@969
   428
wenzelm@17289
   429
val prems = goal (the_context ())
clasohm@969
   430
  "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))";
clasohm@969
   431
by (elab_e_elim_tac prems);
clasohm@969
   432
qed "elab_var_elim_lem";
clasohm@969
   433
paulson@5148
   434
Goal "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
clasohm@969
   435
by (dtac elab_var_elim_lem 1);
paulson@2935
   436
by (Blast_tac 1);
clasohm@969
   437
qed "elab_var_elim";
clasohm@969
   438
wenzelm@17289
   439
val prems = goal (the_context ())
clasohm@969
   440
  " te |- e ===> t ==> \
clasohm@969
   441
\   ( e = fn x1 => e1 --> \
wenzelm@3842
   442
\     (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
clasohm@969
   443
\   )";
clasohm@969
   444
by (elab_e_elim_tac prems);
clasohm@969
   445
qed "elab_fn_elim_lem";
clasohm@969
   446
paulson@5278
   447
Goal " te |- fn x1 => e1 ===> t ==> \
clasohm@969
   448
\   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
clasohm@969
   449
by (dtac elab_fn_elim_lem 1);
paulson@2935
   450
by (Blast_tac 1);
clasohm@969
   451
qed "elab_fn_elim";
clasohm@969
   452
wenzelm@17289
   453
val prems = goal (the_context ())
clasohm@969
   454
  " te |- e ===> t ==> \
clasohm@969
   455
\   (e = fix f(x) = e1 --> \
wenzelm@17289
   456
\   (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))";
clasohm@969
   457
by (elab_e_elim_tac prems);
clasohm@969
   458
qed "elab_fix_elim_lem";
clasohm@969
   459
paulson@5278
   460
Goal " te |- fix ev1(ev2) = e1 ===> t ==> \
clasohm@969
   461
\   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
clasohm@969
   462
by (dtac elab_fix_elim_lem 1);
paulson@2935
   463
by (Blast_tac 1);
clasohm@969
   464
qed "elab_fix_elim";
clasohm@969
   465
wenzelm@17289
   466
val prems = goal (the_context ())
clasohm@969
   467
  " te |- e ===> t2 ==> \
wenzelm@17289
   468
\   (e = e1 @@ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))";
clasohm@969
   469
by (elab_e_elim_tac prems);
clasohm@969
   470
qed "elab_app_elim_lem";
clasohm@969
   471
wenzelm@17289
   472
Goal "te |- e1 @@ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
clasohm@969
   473
by (dtac elab_app_elim_lem 1);
paulson@2935
   474
by (Blast_tac 1);
clasohm@969
   475
qed "elab_app_elim";
clasohm@969
   476
clasohm@969
   477
(* ############################################################ *)
clasohm@969
   478
(* The extended correspondence relation                       *)
clasohm@969
   479
(* ############################################################ *)
clasohm@969
   480
clasohm@969
   481
(* Monotonicity of hasty_fun *)
clasohm@969
   482
wenzelm@21669
   483
Goalw [thm "mono_def", hasty_fun_def] "mono(hasty_fun)";
clasohm@969
   484
by infsys_mono_tac;
paulson@2935
   485
by (Blast_tac 1);
paulson@2935
   486
qed "mono_hasty_fun";
clasohm@969
   487
wenzelm@17289
   488
(*
wenzelm@17289
   489
  Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
clasohm@969
   490
  enjoys two strong indtroduction (co-induction) rules and an elimination rule.
clasohm@969
   491
*)
clasohm@969
   492
clasohm@969
   493
(* First strong indtroduction (co-induction) rule for hasty_rel *)
clasohm@969
   494
wenzelm@5069
   495
Goalw [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
clasohm@969
   496
by (rtac gfp_coind2 1);
wenzelm@17289
   497
by (rewtac hasty_fun_def);
lcp@1047
   498
by (rtac CollectI 1);
lcp@1047
   499
by (rtac disjI1 1);
paulson@2935
   500
by (Blast_tac 1);
clasohm@969
   501
by (rtac mono_hasty_fun 1);
clasohm@969
   502
qed "hasty_rel_const_coind";
clasohm@969
   503
clasohm@969
   504
(* Second strong introduction (co-induction) rule for hasty_rel *)
clasohm@969
   505
paulson@5148
   506
Goalw [hasty_rel_def]
clasohm@969
   507
  " [|  te |- fn ev => e ===> t; \
clasohm@969
   508
\       ve_dom(ve) = te_dom(te); \
clasohm@969
   509
\       ! ev1. \
clasohm@969
   510
\         ev1:ve_dom(ve) --> \
clasohm@972
   511
\         (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
clasohm@969
   512
\   |] ==> \
clasohm@972
   513
\   (v_clos(<|ev,e,ve|>),t) : hasty_rel";
clasohm@969
   514
by (rtac gfp_coind2 1);
clasohm@969
   515
by (rewtac hasty_fun_def);
lcp@1047
   516
by (rtac CollectI 1);
lcp@1047
   517
by (rtac disjI2 1);
paulson@2935
   518
by (blast_tac HOL_cs 1);
clasohm@969
   519
by (rtac mono_hasty_fun 1);
clasohm@969
   520
qed "hasty_rel_clos_coind";
clasohm@969
   521
clasohm@969
   522
(* Elimination rule for hasty_rel *)
clasohm@969
   523
wenzelm@17289
   524
val prems = goalw (the_context ()) [hasty_rel_def]
wenzelm@3842
   525
  " [| !! c t. c isof t ==> P((v_const(c),t)); \
clasohm@969
   526
\      !! te ev e t ve. \
clasohm@969
   527
\        [| te |- fn ev => e ===> t; \
clasohm@969
   528
\           ve_dom(ve) = te_dom(te); \
wenzelm@3842
   529
\           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
clasohm@972
   530
\        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
clasohm@972
   531
\      (v,t) : hasty_rel \
paulson@8114
   532
\   |] ==> P(v,t)";
clasohm@969
   533
by (cut_facts_tac prems 1);
clasohm@969
   534
by (etac gfp_elim2 1);
clasohm@969
   535
by (rtac mono_hasty_fun 1);
clasohm@969
   536
by (rewtac hasty_fun_def);
clasohm@969
   537
by (dtac CollectD 1);
clasohm@969
   538
by (fold_goals_tac [hasty_fun_def]);
paulson@4153
   539
by Safe_tac;
paulson@2935
   540
by (REPEAT (ares_tac prems 1));
clasohm@969
   541
qed "hasty_rel_elim0";
clasohm@969
   542
wenzelm@17289
   543
val prems = goal (the_context ())
clasohm@972
   544
  " [| (v,t) : hasty_rel; \
wenzelm@3842
   545
\      !! c t. c isof t ==> P (v_const c) t; \
clasohm@969
   546
\      !! te ev e t ve. \
clasohm@969
   547
\        [| te |- fn ev => e ===> t; \
clasohm@969
   548
\           ve_dom(ve) = te_dom(te); \
wenzelm@3842
   549
\           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
clasohm@969
   550
\        |] ==> P (v_clos <|ev,e,ve|>) t \
clasohm@969
   551
\   |] ==> P v t";
clasohm@969
   552
by (res_inst_tac [("P","P")] infsys_p2 1);
clasohm@969
   553
by (rtac hasty_rel_elim0 1);
clasohm@969
   554
by (ALLGOALS (rtac infsys_p1));
clasohm@969
   555
by (ALLGOALS (resolve_tac prems));
clasohm@969
   556
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
clasohm@969
   557
qed "hasty_rel_elim";
clasohm@969
   558
clasohm@969
   559
(* Introduction rules for hasty *)
clasohm@969
   560
paulson@5143
   561
Goalw [hasty_def] "c isof t ==> v_const(c) hasty t";
paulson@2935
   562
by (etac hasty_rel_const_coind 1);
clasohm@969
   563
qed "hasty_const";
clasohm@969
   564
wenzelm@17289
   565
Goalw [hasty_def,hasty_env_def]
paulson@5148
   566
 "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
clasohm@969
   567
by (rtac hasty_rel_clos_coind 1);
wenzelm@4089
   568
by (ALLGOALS (blast_tac (claset() delrules [equalityI])));
clasohm@969
   569
qed "hasty_clos";
clasohm@969
   570
clasohm@969
   571
(* Elimination on constants for hasty *)
clasohm@969
   572
wenzelm@17289
   573
Goalw [hasty_def]
wenzelm@17289
   574
  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
clasohm@969
   575
by (rtac hasty_rel_elim 1);
paulson@2935
   576
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
clasohm@969
   577
qed "hasty_elim_const_lem";
clasohm@969
   578
paulson@5143
   579
Goal "v_const(c) hasty t ==> c isof t";
paulson@2935
   580
by (dtac hasty_elim_const_lem 1);
paulson@2935
   581
by (Blast_tac 1);
clasohm@969
   582
qed "hasty_elim_const";
clasohm@969
   583
clasohm@969
   584
(* Elimination on closures for hasty *)
clasohm@969
   585
wenzelm@17289
   586
Goalw [hasty_env_def,hasty_def]
clasohm@969
   587
  " v hasty t ==> \
clasohm@969
   588
\   ! x e ve. \
wenzelm@3842
   589
\     v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
clasohm@969
   590
by (rtac hasty_rel_elim 1);
paulson@2935
   591
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
clasohm@969
   592
qed "hasty_elim_clos_lem";
clasohm@969
   593
paulson@5278
   594
Goal "v_clos(<|ev,e,ve|>) hasty t ==>  \
wenzelm@3842
   595
\       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
paulson@2935
   596
by (dtac hasty_elim_clos_lem 1);
paulson@2935
   597
by (Blast_tac 1);
clasohm@969
   598
qed "hasty_elim_clos";
clasohm@969
   599
clasohm@969
   600
(* ############################################################ *)
clasohm@969
   601
(* The pointwise extension of hasty to environments             *)
clasohm@969
   602
(* ############################################################ *)
clasohm@969
   603
haftmann@20943
   604
fun excluded_middle_tac sP =
haftmann@21546
   605
  res_inst_tac [("Q", sP)] (excluded_middle RS disjE);
haftmann@20943
   606
paulson@5278
   607
Goal "[| ve hastyenv te; v hasty t |] ==> \
lcp@1047
   608
\        ve + {ev |-> v} hastyenv te + {ev |=> t}";
lcp@1047
   609
by (rewtac hasty_env_def);
wenzelm@21669
   610
by (asm_full_simp_tac (simpset() delsimps thms "mem_simps"
clasohm@1266
   611
                                addsimps [ve_dom_owr, te_dom_owr]) 1);
paulson@2935
   612
by (safe_tac HOL_cs);
lcp@1047
   613
by (excluded_middle_tac "ev=x" 1);
wenzelm@4089
   614
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
wenzelm@4089
   615
by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1);
clasohm@969
   616
qed "hasty_env1";
clasohm@969
   617
clasohm@969
   618
(* ############################################################ *)
clasohm@969
   619
(* The Consistency theorem                                      *)
clasohm@969
   620
(* ############################################################ *)
clasohm@969
   621
paulson@5278
   622
Goal "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
clasohm@969
   623
by (dtac elab_const_elim 1);
clasohm@969
   624
by (etac hasty_const 1);
clasohm@969
   625
qed "consistency_const";
clasohm@969
   626
wenzelm@5069
   627
Goalw [hasty_env_def]
paulson@5148
   628
  "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
paulson@2935
   629
\       ve_app ve ev hasty t";
clasohm@969
   630
by (dtac elab_var_elim 1);
paulson@2935
   631
by (Blast_tac 1);
clasohm@969
   632
qed "consistency_var";
clasohm@969
   633
paulson@5278
   634
Goal "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
paulson@2935
   635
\       v_clos(<| ev, e, ve |>) hasty t";
clasohm@969
   636
by (rtac hasty_clos 1);
paulson@2935
   637
by (Blast_tac 1);
clasohm@969
   638
qed "consistency_fn";
clasohm@969
   639
wenzelm@5069
   640
Goalw [hasty_env_def,hasty_def]
paulson@5148
   641
  "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
clasohm@969
   642
\      ve hastyenv te ; \
clasohm@969
   643
\      te |- fix ev2  ev1  = e ===> t \
clasohm@969
   644
\   |] ==> \
clasohm@969
   645
\   v_clos(cl) hasty t";
clasohm@969
   646
by (dtac elab_fix_elim 1);
paulson@2935
   647
by (safe_tac HOL_cs);
lcp@1047
   648
(*Do a single unfolding of cl*)
wenzelm@7499
   649
by ((ftac ssubst 1) THEN (assume_tac 2));
lcp@1047
   650
by (rtac hasty_rel_clos_coind 1);
clasohm@969
   651
by (etac elab_fn 1);
wenzelm@4089
   652
by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);
clasohm@969
   653
wenzelm@21669
   654
by (asm_simp_tac (simpset() delsimps thms "mem_simps" addsimps [ve_dom_owr]) 1);
paulson@2935
   655
by (safe_tac HOL_cs);
lcp@1047
   656
by (excluded_middle_tac "ev2=ev1a" 1);
wenzelm@4089
   657
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
clasohm@969
   658
wenzelm@21669
   659
by (asm_simp_tac (simpset() delsimps thms "mem_simps"
clasohm@1266
   660
                           addsimps [ve_app_owr1, te_app_owr1]) 1);
paulson@2935
   661
by (Blast_tac 1);
clasohm@969
   662
qed "consistency_fix";
clasohm@969
   663
paulson@5278
   664
Goal "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
clasohm@969
   665
\      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
wenzelm@17289
   666
\      ve hastyenv te ; te |- e1 @@ e2 ===> t \
clasohm@969
   667
\   |] ==> \
clasohm@969
   668
\   v_const(c_app c1 c2) hasty t";
clasohm@969
   669
by (dtac elab_app_elim 1);
paulson@4153
   670
by Safe_tac;
clasohm@969
   671
by (rtac hasty_const 1);
clasohm@969
   672
by (rtac isof_app 1);
clasohm@969
   673
by (rtac hasty_elim_const 1);
paulson@2935
   674
by (Blast_tac 1);
clasohm@969
   675
by (rtac hasty_elim_const 1);
paulson@2935
   676
by (Blast_tac 1);
clasohm@969
   677
qed "consistency_app1";
clasohm@969
   678
paulson@5278
   679
Goal "[| ! t te. \
clasohm@969
   680
\        ve hastyenv te  --> \
clasohm@969
   681
\        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
clasohm@969
   682
\      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
clasohm@969
   683
\      ! t te. \
clasohm@969
   684
\        vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t; \
clasohm@969
   685
\      ve hastyenv te ; \
wenzelm@17289
   686
\      te |- e1 @@ e2 ===> t \
clasohm@969
   687
\   |] ==> \
clasohm@969
   688
\   v hasty t";
clasohm@969
   689
by (dtac elab_app_elim 1);
paulson@4153
   690
by Safe_tac;
lcp@1047
   691
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
lcp@1047
   692
by (assume_tac 1);
lcp@1047
   693
by (etac impE 1);
lcp@1047
   694
by (assume_tac 1);
lcp@1047
   695
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
lcp@1047
   696
by (assume_tac 1);
lcp@1047
   697
by (etac impE 1);
lcp@1047
   698
by (assume_tac 1);
clasohm@969
   699
by (dtac hasty_elim_clos 1);
paulson@4153
   700
by Safe_tac;
clasohm@969
   701
by (dtac elab_fn_elim 1);
wenzelm@4089
   702
by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
clasohm@969
   703
qed "consistency_app2";
clasohm@969
   704
paulson@5278
   705
Goal "ve |- e ---> v ==> \
lcp@1047
   706
\  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
clasohm@969
   707
clasohm@969
   708
(* Proof by induction on the structure of evaluations *)
clasohm@969
   709
paulson@5148
   710
by (etac eval_ind 1);
paulson@4153
   711
by Safe_tac;
wenzelm@17289
   712
by (DEPTH_SOLVE
lcp@1047
   713
    (ares_tac [consistency_const, consistency_var, consistency_fn,
clasohm@1465
   714
               consistency_fix, consistency_app1, consistency_app2] 1));
clasohm@969
   715
qed "consistency";
clasohm@969
   716
clasohm@969
   717
(* ############################################################ *)
clasohm@969
   718
(* The Basic Consistency theorem                                *)
clasohm@969
   719
(* ############################################################ *)
clasohm@969
   720
wenzelm@17289
   721
Goalw [isof_env_def,hasty_env_def]
clasohm@969
   722
  "ve isofenv te ==> ve hastyenv te";
paulson@4153
   723
by Safe_tac;
lcp@1047
   724
by (etac allE 1);
lcp@1047
   725
by (etac impE 1);
lcp@1047
   726
by (assume_tac 1);
lcp@1047
   727
by (etac exE 1);
lcp@1047
   728
by (etac conjE 1);
clasohm@969
   729
by (dtac hasty_const 1);
clasohm@1266
   730
by (Asm_simp_tac 1);
clasohm@969
   731
qed "basic_consistency_lem";
clasohm@969
   732
paulson@5278
   733
Goal "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
clasohm@969
   734
by (rtac hasty_elim_const 1);
clasohm@969
   735
by (dtac consistency 1);
wenzelm@4089
   736
by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
clasohm@969
   737
qed "basic_consistency";