src/LCF/LCF.ML
author nipkow
Tue, 17 Oct 2000 08:00:46 +0200
changeset 10228 e653cb933293
parent 3837 d7f033c74b38
permissions -rw-r--r--
added intermediate value thms
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
     1
(*  Title:      LCF/lcf.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
     3
    Author:     Tobias Nipkow
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For lcf.thy.  Basic lemmas about LCF
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open LCF;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
signature LCF_LEMMAS =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  val ap_term: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  val ap_thm: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val COND_cases: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val COND_cases_iff: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val Contrapos: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val cong: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val ext: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val eq_imp_less1: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  val eq_imp_less2: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  val less_anti_sym: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  val less_ap_term: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  val less_ap_thm: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  val less_refl: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  val less_UU: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  val not_UU_eq_TT: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val not_UU_eq_FF: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val not_TT_eq_UU: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val not_TT_eq_FF: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val not_FF_eq_UU: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val not_FF_eq_TT: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val rstac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val stac: thm -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val sstac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  val strip_tac: int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  val tr_induct: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  val UU_abs: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  val UU_app: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
structure LCF_Lemmas : LCF_LEMMAS =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
(* Standard abbreviations *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
val rstac = resolve_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
fun stac th = rtac(th RS sym RS subst);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
fun sstac ths = EVERY' (map stac ths);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
fun strip_tac i = REPEAT(rstac [impI,allI] i); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val eq_imp_less1 = prove_goal thy "x=y ==> x << y"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    56
        (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val eq_imp_less2 = prove_goal thy "x=y ==> y << x"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    59
        (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val less_refl = refl RS eq_imp_less1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
val less_anti_sym = prove_goal thy "[| x << y; y << x |] ==> x=y"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    64
        (fn prems => [rewtac eq_def,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    65
                      REPEAT(rstac(conjI::prems)1)]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val ext = prove_goal thy
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1461
diff changeset
    68
        "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    69
        (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    70
                                    prem RS eq_imp_less1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    71
                                    prem RS eq_imp_less2]1)]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val cong = prove_goal thy "[| f=g; x=y |] ==> f(x)=g(y)"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    74
        (fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    75
                      rtac refl 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
val less_ap_term = less_refl RS mono;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val less_ap_thm = less_refl RSN (2,mono);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val ap_term = refl RS cong;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
val ap_thm = refl RSN (2,cong);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1461
diff changeset
    82
val UU_abs = prove_goal thy "(%x::'a::cpo. UU) = UU"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    83
        (fn _ => [rtac less_anti_sym 1, rtac minimal 2,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    84
                  rtac less_ext 1, rtac allI 1, rtac minimal 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
val UU_app = UU_abs RS sym RS ap_thm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val less_UU = prove_goal thy "x << UU ==> x=UU"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    89
        (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1461
diff changeset
    92
val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    93
        (fn prems => [rtac allI 1, rtac mp 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    94
                      res_inst_tac[("p","b")]tr_cases 2,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    95
                      fast_tac (FOL_cs addIs prems) 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
    99
        (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
   100
                      rstac prems 1, atac 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val not_UU_eq_FF = not_FF_less_UU RS not_less_imp_not_eq2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
val not_TT_eq_UU = not_TT_less_UU RS not_less_imp_not_eq1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val not_TT_eq_FF = not_TT_less_FF RS not_less_imp_not_eq1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
val not_FF_eq_UU = not_FF_less_UU RS not_less_imp_not_eq1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
val COND_cases_iff = (prove_goal thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
  "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
   115
        (fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
   116
                                 not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
   117
                  rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
   118
                  stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)]))  RS spec;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
val lemma = prove_goal thy "A<->B ==> B ==> A"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
   121
        (fn prems => [cut_facts_tac prems 1, rewtac iff_def,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 442
diff changeset
   122
                      fast_tac FOL_cs 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
open LCF_Lemmas;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129