src/LCF/LCF_lemmas.ML

removed obsolete ML files;

(*  Title:      LCF/lcf.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1992  University of Cambridge
*)

(* Standard abbreviations *)

val rstac = resolve_tac;
fun stac th = rtac(th RS sym RS subst);
fun sstac ths = EVERY' (map stac ths);

fun strip_tac i = REPEAT(rstac [impI,allI] i);

bind_thm ("eq_imp_less1", prove_goal (the_context ()) "x=y ==> x << y"
        (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]));

bind_thm ("eq_imp_less2", prove_goal (the_context ()) "x=y ==> y << x"
        (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]));

bind_thm ("less_refl", refl RS eq_imp_less1);

bind_thm ("less_anti_sym", prove_goal (the_context ()) "[| x << y; y << x |] ==> x=y"
        (fn prems => [rewtac eq_def,
                      REPEAT(rstac(conjI::prems)1)]));

bind_thm ("ext", prove_goal (the_context ())
        "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
        (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
                                    prem RS eq_imp_less1,
                                    prem RS eq_imp_less2]1)]));

bind_thm ("cong", prove_goal (the_context ()) "[| f=g; x=y |] ==> f(x)=g(y)"
        (fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,
                      rtac refl 1]));

bind_thm ("less_ap_term", less_refl RS mono);
bind_thm ("less_ap_thm", less_refl RSN (2,mono));
bind_thm ("ap_term", refl RS cong);
bind_thm ("ap_thm", refl RSN (2,cong));

bind_thm ("UU_abs", prove_goal (the_context ()) "(%x::'a::cpo. UU) = UU"
        (fn _ => [rtac less_anti_sym 1, rtac minimal 2,
                  rtac less_ext 1, rtac allI 1, rtac minimal 1]));

bind_thm ("UU_app", UU_abs RS sym RS ap_thm);

bind_thm ("less_UU", prove_goal (the_context ()) "x << UU ==> x=UU"
        (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]));


bind_thm ("tr_induct", prove_goal (the_context ()) "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
        (fn prems => [rtac allI 1, rtac mp 1,
                      res_inst_tac[("p","b")]tr_cases 2,
                      fast_tac (FOL_cs addIs prems) 1]));


bind_thm ("Contrapos", prove_goal (the_context ()) "(A ==> B) ==> (~B ==> ~A)"
        (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,
                      rstac prems 1, atac 1]));

bind_thm ("not_less_imp_not_eq1", eq_imp_less1 COMP Contrapos);
bind_thm ("not_less_imp_not_eq2", eq_imp_less2 COMP Contrapos);

bind_thm ("not_UU_eq_TT", not_TT_less_UU RS not_less_imp_not_eq2);
bind_thm ("not_UU_eq_FF", not_FF_less_UU RS not_less_imp_not_eq2);
bind_thm ("not_TT_eq_UU", not_TT_less_UU RS not_less_imp_not_eq1);
bind_thm ("not_TT_eq_FF", not_TT_less_FF RS not_less_imp_not_eq1);
bind_thm ("not_FF_eq_UU", not_FF_less_UU RS not_less_imp_not_eq1);
bind_thm ("not_FF_eq_TT", not_FF_less_TT RS not_less_imp_not_eq1);


bind_thm ("COND_cases_iff", (prove_goal (the_context ())
  "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
        (fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,
                                 not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1,
                  rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2,
                  stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)]))  RS spec);

val lemma = prove_goal (the_context ()) "A<->B ==> B ==> A"
        (fn prems => [cut_facts_tac prems 1, rewtac iff_def,
                      fast_tac FOL_cs 1]);

bind_thm ("COND_cases", conjI RSN (2,conjI RS (COND_cases_iff RS lemma)));


val LCF_ss = FOL_ss addsimps
        [minimal,
         UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm,
         not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU,
         not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF,
         not_FF_eq_UU,not_FF_eq_TT,
         COND_UU,COND_TT,COND_FF,
         surj_pairing,FST,SND];

change_simpset (fn _ => LCF_ss);