src/HOLCF/domain/theorems.ML
changeset 2445 51993fea433f
parent 2276 3eb9a113029e
child 2446 c2a9bf6c0948
     1.1 --- a/src/HOLCF/domain/theorems.ML	Wed Dec 18 15:13:50 1996 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Dec 18 15:16:13 1996 +0100
     1.3 @@ -1,7 +1,9 @@
     1.4  (*  Title:      HOLCF/domain/theorems.ML
     1.5 -    ID:         $ $
     1.6 +    ID:         $Id$
     1.7      Author : David von Oheimb
     1.8      Copyright 1995, 1996 TU Muenchen
     1.9 +
    1.10 +proof generator for domain section
    1.11  *)
    1.12  
    1.13  structure Domain_Theorems = struct
    1.14 @@ -42,30 +44,16 @@
    1.15  
    1.16  (* ----- general proofs ----------------------------------------------------- *)
    1.17  
    1.18 -val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[
    1.19 -                fast_tac HOL_cs 1]))["(!x. P x & Q)=((!x. P x) & Q)",
    1.20 -                                     "(!x. P & Q x) = (P & (!x. Q x))"]);
    1.21 -
    1.22  val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
    1.23   (fn prems =>[
    1.24                                  resolve_tac prems 1,
    1.25                                  cut_facts_tac prems 1,
    1.26                                  fast_tac HOL_cs 1]);
    1.27  
    1.28 -val swap3 = prove_goal HOL.thy "[| Q ==> P; ~P |] ==> ~Q" (fn prems => [
    1.29 -                                cut_facts_tac prems 1,
    1.30 -                                etac swap 1,
    1.31 -                                dtac notnotD 1,
    1.32 -                                etac (hd prems) 1]);
    1.33 -
    1.34  val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
    1.35 -                                rtac swap3 1,
    1.36 +                                rtac rev_contrapos 1,
    1.37                                  etac (antisym_less_inverse RS conjunct1) 1,
    1.38                                  resolve_tac prems 1]);
    1.39 -val cfst_strict  = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [
    1.40 -                        (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
    1.41 -val csnd_strict  = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [
    1.42 -                        (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
    1.43  
    1.44  in
    1.45  
    1.46 @@ -221,7 +209,7 @@
    1.47  val con_defins = map (fn (con,args) => pg []
    1.48                          (lift_defined % (nonlazy args,
    1.49                                  mk_trp(defined(con_app con args)))) ([
    1.50 -                          rtac swap3 1, 
    1.51 +                          rtac rev_contrapos 1, 
    1.52                            eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
    1.53                            asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
    1.54  val con_rews = con_stricts @ con_defins;
    1.55 @@ -257,7 +245,7 @@
    1.56      fun dist (con1, args1) (con2, args2) = pg []
    1.57                (lift_defined % ((nonlazy args1),
    1.58                          (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
    1.59 -                        rtac swap3 1,
    1.60 +                        rtac rev_contrapos 1,
    1.61                          eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
    1.62                        @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
    1.63                        @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
    1.64 @@ -371,7 +359,7 @@
    1.65    val copy_con_rews  = copy_rews @ con_rews;
    1.66    val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
    1.67    val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
    1.68 -            (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
    1.69 +            strict(dc_take dn $ %"n")) eqs)))([
    1.70                          nat_ind_tac "n" 1,
    1.71                          simp_tac iterate_Cprod_ss 1,
    1.72                          asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
    1.73 @@ -442,7 +430,7 @@
    1.74  val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$
    1.75                               (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [
    1.76                                  quant_tac 1,
    1.77 -                                simp_tac quant_ss 1,
    1.78 +                                simp_tac HOL_ss 1,
    1.79                                  nat_ind_tac "n" 1,
    1.80                                  simp_tac (take_ss addsimps prems) 1,
    1.81                                  TRY(safe_tac HOL_cs)]
    1.82 @@ -512,7 +500,7 @@
    1.83                                        asm_simp_tac take_ss 1])
    1.84                                      (nonlazy_rec args)))
    1.85                                    cons))
    1.86 -                                1 (conss~~casess))) handle ERROR => raise ERROR;
    1.87 +                                1 (conss~~casess)));
    1.88      val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp(
    1.89                                                  %%(dn^"_finite") $ %"x"))[
    1.90                                  case_UU_tac take_rews 1 "x",