src/HOL/MiniML/I.ML
author nipkow
Mon Apr 22 15:42:20 1996 +0200 (1996-04-22)
changeset 1669 e56cdf711729
parent 1486 7b95d7b49f7a
child 1673 d22110ddd0af
permissions -rw-r--r--
inserted Suc_less_eq explictly in a few proofs.
inserted o_def explictly in a few proofs because the new split_tac causes
fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML
     1 open I;
     2 
     3 goal thy
     4   "! a m s s' t n.  \
     5 \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
     6 \    ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
     7 by (expr.induct_tac "e" 1);
     8 
     9   (* case Var n *)
    10   by (simp_tac (!simpset addsimps [app_subst_list]
    11       setloop (split_tac [expand_if])) 1);
    12   by (fast_tac (HOL_cs addss !simpset) 1);
    13 
    14  (* case Abs e *)
    15  by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    16  by (strip_tac 1);
    17  by (rtac conjI 1);
    18   by (strip_tac 1);
    19   by (REPEAT (etac allE 1));
    20   by (etac impE 1);
    21    by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
    22   by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
    23                               less_imp_le,lessI]) 1); 
    24 
    25  by (strip_tac 1);
    26  by (REPEAT (etac allE 1));
    27  by (etac impE 1);
    28   by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
    29  by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
    30                              less_imp_le,lessI]) 1);
    31 
    32 (* case App e1 e2 *)
    33 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    34 by (strip_tac 1);
    35 by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
    36 by (rtac conjI 1);
    37  by (fast_tac (HOL_cs addss !simpset) 1);
    38 by (strip_tac 1);
    39 by (rename_tac "s1 t1' n1'" 1);
    40 by (eres_inst_tac [("x","a")] allE 1);
    41 by (eres_inst_tac [("x","m")] allE 1);
    42 by (eres_inst_tac [("x","s")] allE 1);
    43 by (eres_inst_tac [("x","s1'")] allE 1);
    44 by (eres_inst_tac [("x","t1")] allE 1);
    45 by (eres_inst_tac [("x","n1")] allE 1);
    46 by (eres_inst_tac [("x","a")] allE 1);
    47 by (eres_inst_tac [("x","n1")] allE 1);
    48 by (eres_inst_tac [("x","s1'")] allE 1);
    49 by (eres_inst_tac [("x","s2'")] allE 1);
    50 by (eres_inst_tac [("x","t2")] allE 1);
    51 by (eres_inst_tac [("x","n2")] allE 1);
    52 by (rtac conjI 1);
    53  by (strip_tac 1);
    54  by (mp_tac 1);
    55  by (mp_tac 1);
    56  by (etac exE 1);
    57  by (etac conjE 1);
    58  by (etac impE 1);
    59   by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
    60   by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
    61   by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
    62                        addss !simpset) 1);
    63  by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);
    64 by (strip_tac 1);
    65 by (rename_tac "s2 t2' n2'" 1);
    66 by (rtac conjI 1);
    67  by (strip_tac 1);
    68  by (mp_tac 1);
    69  by (mp_tac 1);
    70  by (etac exE 1);
    71  by (etac conjE 1);
    72  by (etac impE 1);
    73   by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
    74   by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
    75   by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
    76                        addss !simpset) 1);
    77  by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);
    78 by (strip_tac 1);
    79 by (mp_tac 1);
    80 by (mp_tac 1);
    81 by (etac exE 1);
    82 by (etac conjE 1);
    83 by (etac impE 1);
    84  by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
    85  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
    86  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
    87                       addss !simpset) 1);
    88 by (mp_tac 1);
    89 by (REPEAT (eresolve_tac [exE,conjE] 1));
    90 by (REPEAT(EVERY1
    91      [asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]),
    92       REPEAT o etac conjE, hyp_subst_tac]));
    93 by (rtac exI 1);
    94 by (safe_tac HOL_cs);
    95   by (fast_tac HOL_cs 1);
    96  by (simp_tac (!simpset addsimps [o_def,subst_comp_te]) 2);
    97 by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
    98  by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
    99 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
   100 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   101 by (safe_tac HOL_cs);
   102   by (fast_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   103                        addss !simpset) 1);
   104  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   105                       addss !simpset) 1);
   106 by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
   107 by ((dtac new_tv_subst_tel 1) THEN (atac 1));
   108 by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
   109 by ((dtac new_tv_subst_tel 1) THEN (atac 1));
   110 by (fast_tac (HOL_cs addDs [new_tv_W] addss 
   111     (!simpset addsimps [subst_comp_tel])) 1);
   112 qed_spec_mp "I_correct_wrt_W";