src/HOLCF/cprod1.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/cprod1.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for theory cprod1.thy 
     7 *)
     8 
     9 open Cprod1;
    10 
    11 val less_cprod1b = prove_goalw Cprod1.thy [less_cprod_def]
    12  "less_cprod(p1,p2) = ( fst(p1) << fst(p2) & snd(p1) << snd(p2))"
    13  (fn prems =>
    14 	[
    15 	(rtac refl 1)
    16 	]);
    17 
    18 val less_cprod2a = prove_goalw Cprod1.thy [less_cprod_def]
    19  "less_cprod(<x,y>,<UU,UU>) ==> x = UU & y = UU"
    20  (fn prems =>
    21 	[
    22 	(cut_facts_tac prems 1),
    23 	(etac conjE 1),
    24 	(dtac (fst_conv RS subst) 1),
    25 	(dtac (fst_conv RS subst) 1),
    26 	(dtac (fst_conv RS subst) 1),
    27 	(dtac (snd_conv RS subst) 1),
    28 	(dtac (snd_conv RS subst) 1),
    29 	(dtac (snd_conv RS subst) 1),
    30 	(rtac conjI 1),
    31 	(etac UU_I 1),
    32 	(etac UU_I 1)
    33 	]);
    34 
    35 val less_cprod2b = prove_goal Cprod1.thy 
    36  "less_cprod(p,<UU,UU>) ==> p=<UU,UU>"
    37  (fn prems =>
    38 	[
    39 	(cut_facts_tac prems 1),
    40 	(res_inst_tac [("p","p")] PairE 1),
    41 	(hyp_subst_tac 1),
    42 	(dtac less_cprod2a 1),
    43 	(asm_simp_tac HOL_ss 1)
    44 	]);
    45 
    46 val less_cprod2c = prove_goalw Cprod1.thy [less_cprod_def]
    47  "less_cprod(<x1,y1>,<x2,y2>) ==> x1 << x2 & y1 << y2"
    48  (fn prems =>
    49 	[
    50 	(cut_facts_tac prems 1),
    51 	(etac conjE 1),
    52 	(dtac (fst_conv RS subst) 1),
    53 	(dtac (fst_conv RS subst) 1),
    54 	(dtac (fst_conv RS subst) 1),
    55 	(dtac (snd_conv RS subst) 1),
    56 	(dtac (snd_conv RS subst) 1),
    57 	(dtac (snd_conv RS subst) 1),
    58 	(rtac conjI 1),
    59 	(atac 1),
    60 	(atac 1)
    61 	]);
    62 
    63 (* ------------------------------------------------------------------------ *)
    64 (* less_cprod is a partial order on 'a * 'b                                 *)
    65 (* ------------------------------------------------------------------------ *)
    66 
    67 val refl_less_cprod = prove_goalw Cprod1.thy [less_cprod_def] "less_cprod(p,p)"
    68  (fn prems =>
    69 	[
    70 	(res_inst_tac [("p","p")] PairE 1),
    71 	(hyp_subst_tac 1),
    72 	(simp_tac pair_ss 1),
    73 	(simp_tac Cfun_ss 1)
    74 	]);
    75 
    76 val antisym_less_cprod = prove_goal Cprod1.thy 
    77  "[|less_cprod(p1,p2);less_cprod(p2,p1)|] ==> p1=p2"
    78  (fn prems =>
    79 	[
    80 	(cut_facts_tac prems 1),
    81 	(res_inst_tac [("p","p1")] PairE 1),
    82 	(hyp_subst_tac 1),
    83 	(res_inst_tac [("p","p2")] PairE 1),
    84 	(hyp_subst_tac 1),
    85 	(dtac less_cprod2c 1),
    86 	(dtac less_cprod2c 1),
    87 	(etac conjE 1),
    88 	(etac conjE 1),
    89 	(rtac (Pair_eq RS ssubst) 1),
    90 	(fast_tac (HOL_cs addSIs [antisym_less]) 1)
    91 	]);
    92 
    93 
    94 val trans_less_cprod = prove_goal Cprod1.thy 
    95  "[|less_cprod(p1,p2);less_cprod(p2,p3)|] ==> less_cprod(p1,p3)"
    96  (fn prems =>
    97 	[
    98 	(cut_facts_tac prems 1),
    99 	(res_inst_tac [("p","p1")] PairE 1),
   100 	(hyp_subst_tac 1),
   101 	(res_inst_tac [("p","p3")] PairE 1),
   102 	(hyp_subst_tac 1),
   103 	(res_inst_tac [("p","p2")] PairE 1),
   104 	(hyp_subst_tac 1),
   105 	(dtac less_cprod2c 1),
   106 	(dtac less_cprod2c 1),
   107 	(rtac (less_cprod1b RS ssubst) 1),
   108 	(simp_tac pair_ss 1),
   109 	(etac conjE 1),
   110 	(etac conjE 1),
   111 	(rtac conjI 1),
   112 	(etac trans_less 1),
   113 	(atac 1),
   114 	(etac trans_less 1),
   115 	(atac 1)
   116 	]);
   117