src/ZF/Coind/MT.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 1740 b50755328aad
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
     1
(*  Title:      ZF/Coind/MT.ML
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     5
*)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     6
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     7
open MT;
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     8
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     9
       
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    10
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    11
(* The Consistency theorem                                      *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    12
(* ############################################################ *)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    13
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    14
val prems = goal MT.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
    15
  "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==>         \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    16
\  <v_const(c), t> : HasTyRel";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    17
by (cut_facts_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    18
by (fast_tac htr_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    19
qed "consistency_const";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    20
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    21
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    22
val prems = goalw  MT.thy [hastyenv_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
    23
  "[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==>     \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    24
\  <ve_app(ve,x),t>:HasTyRel";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    25
by (cut_facts_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    26
by (fast_tac static_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    27
qed "consistency_var";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    28
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    29
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    30
val prems = goalw MT.thy [hastyenv_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
    31
  "[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te);       \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
    32
\     <te,e_fn(x,e),t>:ElabRel  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
    33
\  |] ==>       \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    34
\  <v_clos(x, e, ve), t> : HasTyRel";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    35
by (cut_facts_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    36
by (best_tac htr_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    37
qed "consistency_fn";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    38
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    39
val MT_cs = ZF_cs 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    40
  addIs (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    41
  addDs [te_owrE,(ElabRel.dom_subset RS subsetD)];
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    42
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    43
val MT_ss = 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    44
  ZF_ss addsimps 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    45
  [ve_dom_owr,te_dom_owr,ve_app_owr1,ve_app_owr2,te_app_owr1,te_app_owr2];
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    46
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    47
val clean_tac = 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    48
  REPEAT_FIRST (fn i => 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    49
    (eq_assume_tac i) ORELSE 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    50
    (match_tac (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) i) ORELSE
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    51
    (ematch_tac [te_owrE] i));
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    52
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    53
val prems = goalw MT.thy [hastyenv_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
    54
  "[| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;               \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
    55
\     v_clos(x,e,ve_owr(ve,f,cl)) = cl;                         \ 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
    56
\     hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==>       \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    57
\  <cl,t>:HasTyRel";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    58
by (cut_facts_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    59
by (etac elab_fixE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    60
by (safe_tac ZF_cs);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    61
by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    62
by clean_tac;
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    63
by (rtac ve_owrI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    64
by clean_tac;
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    65
by (dtac (ElabRel.dom_subset RS subsetD) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    66
by ( eres_inst_tac 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    67
     [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")] 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    68
     (SigmaD1 RS te_owrE) 1
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    69
   );
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    70
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    71
by (rtac ElabRel.elab_fnI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    72
by clean_tac;
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    73
by (asm_simp_tac MT_ss 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    74
by (rtac (ve_dom_owr RS ssubst) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    75
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    76
by (etac subst 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    77
by (rtac v_closNE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    78
by (asm_simp_tac ZF_ss 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    79
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    80
by (rtac PowI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    81
by (rtac (ve_dom_owr RS ssubst) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    82
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    83
by (etac subst 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    84
by (rtac v_closNE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    85
by (rtac subsetI 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    86
by (etac RepFunE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    87
by (dtac lem_fix 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    88
by (etac UnE' 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    89
by (rtac UnI1 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    90
by (etac singletonE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    91
by (asm_full_simp_tac MT_ss 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    92
by (rtac UnI2 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    93
by (etac notsingletonE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    94
by (dtac not_sym 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    95
by (asm_full_simp_tac MT_ss 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    96
qed "consistency_fix";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    97
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    98
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    99
val prems = goal MT.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   100
  " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   101
\     <ve,e1,v_const(c1)>:EvalRel;                      \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   102
\     ALL t te.                                         \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   103
\       hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   104
\     <ve, e2, v_const(c2)> : EvalRel;                  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   105
\     ALL t te.                                         \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   106
\       hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   107
\     hastyenv(ve, te);                                 \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   108
\     <te,e_app(e1,e2),t>:ElabRel |] ==>                \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   109
\   <v_const(c_app(c1, c2)),t>:HasTyRel";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   110
by (cut_facts_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   111
by (etac elab_appE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   112
by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   113
qed "consistency_app1";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   114
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   115
val prems = goal MT.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   116
  " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   117
\      <ve,e1,v_clos(xm,em,vem)>:EvalRel;       \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   118
\      ALL t te.                                \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   119
\        hastyenv(ve,te) -->                    \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   120
\        <te,e1,t>:ElabRel -->                  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   121
\        <v_clos(xm,em,vem),t>:HasTyRel;        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   122
\      <ve,e2,v2>:EvalRel;                      \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   123
\      ALL t te.                                \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   124
\        hastyenv(ve,te) -->                    \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   125
\        <te,e2,t>:ElabRel -->                  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   126
\        <v2,t>:HasTyRel;                       \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   127
\      <ve_owr(vem,xm,v2),em,v>:EvalRel;        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   128
\      ALL t te.                                \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   129
\        hastyenv(ve_owr(vem,xm,v2),te) -->     \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   130
\        <te,em,t>:ElabRel -->                  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   131
\        <v,t>:HasTyRel;                        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   132
\      hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==>      \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   133
\   <v,t>:HasTyRel ";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   134
by (cut_facts_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   135
by (etac elab_appE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   136
by (dtac (spec RS spec RS mp RS mp) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   137
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   138
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   139
by (dtac (spec RS spec RS mp RS mp) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   140
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   141
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   142
by (etac htr_closE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   143
by (etac elab_fnE 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   144
by (rewrite_tac Ty.con_defs);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   145
by (safe_tac sum_cs);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   146
by (dtac (spec RS spec RS mp RS mp) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   147
by (assume_tac 3);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   148
by (assume_tac 2);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   149
by (rtac hastyenv_owr 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   150
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   151
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   152
by (assume_tac 2);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   153
by (rewrite_tac [hastyenv_def]);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   154
by (fast_tac ZF_cs 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   155
qed "consistency_app2";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   156
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   157
fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac)); 
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   158
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   159
val prems = goal MT.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   160
  "<ve,e,v>:EvalRel ==>         \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   161
\  (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   162
by (rtac (EvalRel.mutual_induct RS spec RS spec RS spec RS impE) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   163
by (resolve_tac prems 7 THEN assume_tac 7);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   164
by (safe_tac ZF_cs);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   165
by (mt_cases_tac consistency_const);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   166
by (mt_cases_tac consistency_var);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   167
by (mt_cases_tac consistency_fn);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   168
by (mt_cases_tac consistency_fix);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   169
by (mt_cases_tac consistency_app1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   170
by (mt_cases_tac consistency_app2);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   171
qed "consistency";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   172
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   173
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   174
val prems = goal MT.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   175
  "[| ve:ValEnv; te:TyEnv;              \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   176
\     isofenv(ve,te);                   \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   177
\     <ve,e,v_const(c)>:EvalRel;        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   178
\     <te,e,t>:ElabRel                  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 915
diff changeset
   179
\  |] ==>                               \
915
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   180
\  isof(c,t)";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   181
by (cut_facts_tac prems 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   182
by (rtac (htr_constE) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   183
by (dtac consistency 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   184
by (fast_tac (ZF_cs addSIs [basic_consistency_lem]) 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   185
by (assume_tac 1);
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   186
qed "basic_consistency";
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   187
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   188
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   189
6dae0daf57b7 New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
   190