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