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