Added the second half of the W/I correspondence.

--- a/src/HOL/MiniML/I.ML	Wed May 22 16:54:16 1996 +0200
+++ b/src/HOL/MiniML/I.ML	Wed May 22 17:11:54 1996 +0200
@@ -128,71 +128,71 @@
 Wait until simplification of thms is possible.
 ***)
 
+val lemma = I_correct_wrt_W COMP swap_prems_rl;
+
 goal I.thy "!a m s. \
 \  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
 by (expr.induct_tac "e" 1);
   by(simp_tac (!simpset addsimps [app_subst_list]
                         setloop (split_tac [expand_if])) 1);
- by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+ by(Simp_tac 1);
+ by(strip_tac 1);
+ br conjI 1;
+  by(strip_tac 1);
+  by(subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
+   by(asm_simp_tac (HOL_ss addsimps
+        [new_tv_Suc_list, lessI RS less_imp_le RS new_tv_subst_le]) 1);
+  be conjE 1;
+  bd (new_tv_not_free_tv RS not_free_impl_id) 1;
+  by(Asm_simp_tac 1);
  by(strip_tac 1);
- br notI 1;
- bd eq_OkD 1;
- be swap 1;
- by(subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
-  by(asm_simp_tac HOL_ss 1);
-  by(fast_tac (HOL_cs addSIs [new_tv_Suc_list RS mp,
-                              lessI RS less_imp_le RS new_tv_subst_le]) 1);
- be conjE 1;
- bd (new_tv_not_free_tv RS not_free_impl_id) 1;
- by(Asm_simp_tac 1);
-by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+ be exE 1;
+ by(split_all_tac 1);
+ by(Full_simp_tac 1);
+by(Asm_simp_tac 1);
 by(strip_tac 1);
+be exE 1;
+by(REPEAT(etac conjE 1));
+by(split_all_tac 1);
+by(Full_simp_tac 1);
+bd lemma 1;
+ by(fast_tac HOL_cs 1);
+be exE 1;
+be conjE 1;
+by(hyp_subst_tac 1);
+by(Asm_simp_tac 1);
+br exI 1;
 br conjI 1;
- by(fast_tac (HOL_cs addSDs [eq_OkD]) 1);
-by(strip_tac 1);
-br conjI 1;
- by(strip_tac 1);
- br notI 1;
- by(forward_tac [conjunct1] 1);
- by(forward_tac [conjunct2] 1);
- bd I_correct_wrt_W 1;
-  ba 1;
- be exE 1;
- by(Asm_full_simp_tac 1);
- by(REPEAT(etac conjE 1));
- by(hyp_subst_tac 1);
+ br refl 1;
+by(Simp_tac 1);
+be disjE 1;
+ br disjI1 1;
  by(full_simp_tac (!simpset addsimps [o_def,subst_comp_tel]) 1);
- by(EVERY[dtac eq_OkD 1, etac notE 1, etac allE 1, etac allE 1, etac allE 1,
+ by(EVERY[etac allE 1, etac allE 1, etac allE 1,
           etac impE 1, etac impE 2, atac 2, atac 2]);
  br conjI 1;
   by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
  br new_tv_subst_comp_2 1;
   by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
  by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
-by(strip_tac 1);
-br notI 1;
-by(forward_tac [conjunct1] 1);
-by(forward_tac [conjunct2] 1);
-bd I_correct_wrt_W 1;
- ba 1;
+br disjI2 1;
 be exE 1;
-by(Asm_full_simp_tac 1);
-by(REPEAT(etac conjE 1));
+by(split_all_tac 1);
+be conjE 1;
+by(Full_simp_tac 1);
+bd lemma 1;
+ br conjI 1;
+  by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
+ br new_tv_subst_comp_1 1;
+   by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
+ by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
+be exE 1;
+be conjE 1;
 by(hyp_subst_tac 1);
-by(METAHYPS(fn [_,_,_,_,w1,_,i2,_,na,ns] =>
-               (cut_facts_tac[na RS (ns RS new_tv_subst_tel RS
-                      (w1 RSN (2,new_tv_W RS conjunct1) RS
-                       (ns RS (w1 RS W_var_ge RS new_tv_subst_le) RS
-                        new_tv_subst_comp_1 RS
-                        (na RS (w1 RS W_var_ge RS new_tv_list_le) RS
-                         (conjI RS (i2 RSN (2,I_correct_wrt_W)))))))]1))1);
-be exE 1;
 by(asm_full_simp_tac (!simpset addsimps
      [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
-by(REPEAT(etac conjE 1));
-by(hyp_subst_tac 1);
-by(asm_full_simp_tac (!simpset addsimps
-           [subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
+by(asm_simp_tac (!simpset addcongs [conj_cong] addsimps
+           [eq_sym_conv,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
 qed_spec_mp "I_complete_wrt_W";
 
 (***

--- a/src/HOL/MiniML/Maybe.ML	Wed May 22 16:54:16 1996 +0200
+++ b/src/HOL/MiniML/Maybe.ML	Wed May 22 17:11:54 1996 +0200
@@ -19,6 +19,10 @@
 by (Asm_simp_tac 1);
 qed "expand_bind";
 
-goal Maybe.thy "!!x. x = Ok y ==> x ~= Fail";
-by(Asm_simp_tac 1);
-qed "eq_OkD";
+goal Maybe.thy
+  "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
+by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by(fast_tac HOL_cs 1);
+qed "bind_eq_Fail";
+
+Addsimps [bind_eq_Fail];