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.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",
```