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