src/HOLCF/holcfb.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
nipkow@243
     1
(*  Title: 	HOLCF/holcfb.ML
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993  Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Lemmas for Holcfb.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Holcfb;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* <::nat=>nat=>bool is well-founded                                        *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
nipkow@243
    15
val well_founded_nat = prove_goal  Nat.thy 
nipkow@243
    16
	"!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))"
nipkow@243
    17
 (fn prems =>
nipkow@243
    18
	[
nipkow@243
    19
	(res_inst_tac [("n","x")] less_induct 1),
nipkow@243
    20
	(strip_tac 1),
nipkow@243
    21
	(res_inst_tac [("Q","? k.k<n & P(k)")] (excluded_middle RS disjE) 1),
nipkow@243
    22
	(etac exE 2),
nipkow@243
    23
	(etac conjE 2),
nipkow@243
    24
	(rtac mp 2),
nipkow@243
    25
	(etac allE 2),
nipkow@243
    26
	(etac impE 2),
nipkow@243
    27
	(atac 2),
nipkow@243
    28
	(etac spec 2),
nipkow@243
    29
	(atac 2),
nipkow@243
    30
	(res_inst_tac [("x","n")] exI 1),
nipkow@243
    31
	(rtac conjI 1),
nipkow@243
    32
	(atac 1),
nipkow@243
    33
	(strip_tac 1),
nipkow@243
    34
	(rtac leI  1),
nipkow@243
    35
	(fast_tac HOL_cs 1)
nipkow@243
    36
	]);
nipkow@243
    37
nipkow@243
    38
nipkow@243
    39
(* ------------------------------------------------------------------------ *)
nipkow@243
    40
(* Lemmas for selecting the least element in a nonempty set                 *)
nipkow@243
    41
(* ------------------------------------------------------------------------ *)
nipkow@243
    42
nipkow@243
    43
val theleast = prove_goalw  Holcfb.thy [theleast_def] 
nipkow@243
    44
"P(x) ==> P(theleast(P)) & (!x.P(x)--> theleast(P) <= x)"
nipkow@243
    45
 (fn prems =>
nipkow@243
    46
	[
nipkow@243
    47
	(cut_facts_tac prems 1),
nipkow@243
    48
	(rtac (well_founded_nat RS spec RS mp RS exE) 1),
nipkow@243
    49
	(atac 1),
nipkow@243
    50
	(rtac selectI 1),
nipkow@243
    51
	(atac 1)
nipkow@243
    52
	]);
nipkow@243
    53
nipkow@243
    54
val theleast1= theleast RS conjunct1;
nipkow@243
    55
(* ?P1(?x1) ==> ?P1(theleast(?P1)) *)
nipkow@243
    56
nipkow@243
    57
val theleast2 = prove_goal  Holcfb.thy  "P(x) ==> theleast(P) <= x"
nipkow@243
    58
 (fn prems =>
nipkow@243
    59
	[
nipkow@243
    60
	(rtac (theleast RS conjunct2 RS spec RS mp) 1),
nipkow@243
    61
	(resolve_tac prems 1),
nipkow@243
    62
	(resolve_tac prems 1)
nipkow@243
    63
	]);
nipkow@243
    64
nipkow@243
    65
nipkow@243
    66
(* ------------------------------------------------------------------------ *)
nipkow@243
    67
(* Some lemmas in HOL.thy                                                   *)
nipkow@243
    68
(* ------------------------------------------------------------------------ *)
nipkow@243
    69
nipkow@243
    70
nipkow@243
    71
val de_morgan1 = prove_goal HOL.thy "(~a & ~b)=(~(a | b))"
nipkow@243
    72
(fn prems =>
nipkow@243
    73
	[
nipkow@243
    74
	(rtac iffI 1),
nipkow@243
    75
	(fast_tac HOL_cs 1),
nipkow@243
    76
	(fast_tac HOL_cs 1)
nipkow@243
    77
	]);
nipkow@243
    78
nipkow@243
    79
val de_morgan2 = prove_goal HOL.thy "(~a | ~b)=(~(a & b))"
nipkow@243
    80
(fn prems =>
nipkow@243
    81
	[
nipkow@243
    82
	(rtac iffI 1),
nipkow@243
    83
	(fast_tac HOL_cs 1),
nipkow@243
    84
	(fast_tac HOL_cs 1)
nipkow@243
    85
	]);
nipkow@243
    86
nipkow@243
    87
nipkow@243
    88
val notall2ex = prove_goal HOL.thy "(~ (!x.P(x))) = (? x.~P(x))"
nipkow@243
    89
(fn prems =>
nipkow@243
    90
	[
nipkow@243
    91
	(rtac iffI 1),
nipkow@243
    92
	(fast_tac HOL_cs 1),
nipkow@243
    93
	(fast_tac HOL_cs 1)
nipkow@243
    94
	]);
nipkow@243
    95
nipkow@243
    96
val notex2all = prove_goal HOL.thy "(~ (? x.P(x))) = (!x.~P(x))"
nipkow@243
    97
(fn prems =>
nipkow@243
    98
	[
nipkow@243
    99
	(rtac iffI 1),
nipkow@243
   100
	(fast_tac HOL_cs 1),
nipkow@243
   101
	(fast_tac HOL_cs 1)
nipkow@243
   102
	]);
nipkow@243
   103
nipkow@243
   104
nipkow@243
   105
val selectI2 = prove_goal HOL.thy "(? x. P(x)) ==> P(@ x.P(x))"
nipkow@243
   106
(fn prems =>
nipkow@243
   107
	[
nipkow@243
   108
	(cut_facts_tac prems 1),
nipkow@243
   109
	(etac exE 1),
nipkow@243
   110
	(etac selectI 1)
nipkow@243
   111
	]);
nipkow@243
   112
nipkow@243
   113
val selectE = prove_goal HOL.thy "P(@ x.P(x)) ==> (? x. P(x))"
nipkow@243
   114
(fn prems =>
nipkow@243
   115
	[
nipkow@243
   116
	(cut_facts_tac prems 1),
nipkow@243
   117
	(etac exI 1)
nipkow@243
   118
	]);
nipkow@243
   119
nipkow@243
   120
val select_eq_Ex = prove_goal HOL.thy "(P(@ x.P(x))) =  (? x. P(x))"
nipkow@243
   121
(fn prems =>
nipkow@243
   122
	[
nipkow@243
   123
	(rtac (iff RS mp  RS mp) 1),
nipkow@243
   124
	(strip_tac 1),
nipkow@243
   125
	(etac selectE 1),
nipkow@243
   126
	(strip_tac 1),
nipkow@243
   127
	(etac selectI2 1)
nipkow@243
   128
	]);
nipkow@243
   129
nipkow@243
   130
nipkow@243
   131
val notnotI = prove_goal HOL.thy "P ==> ~~P"
nipkow@243
   132
(fn prems =>
nipkow@243
   133
	[
nipkow@243
   134
	(cut_facts_tac prems 1),
nipkow@243
   135
	(fast_tac HOL_cs 1)
nipkow@243
   136
	]);
nipkow@243
   137
nipkow@243
   138
nipkow@243
   139
val classical2 = prove_goal HOL.thy "[|Q ==> R; ~Q ==> R|]==>R"
nipkow@243
   140
 (fn prems =>
nipkow@243
   141
	[
nipkow@243
   142
	(rtac disjE 1),
nipkow@243
   143
	(rtac excluded_middle 1),
nipkow@243
   144
	(eresolve_tac prems 1),
nipkow@243
   145
	(eresolve_tac prems 1)
nipkow@243
   146
	]);
nipkow@243
   147
nipkow@243
   148
nipkow@243
   149
nipkow@243
   150
val classical3 = (notE RS notI);
nipkow@243
   151
(* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
nipkow@243
   152