src/HOLCF/Sprod1.ML
author clasohm
Tue Jan 30 13:42:57 1996 +0100 (1996-01-30)
changeset 1461 6bcb44e4d6e5
parent 1277 caef3601c0b2
child 2033 639de962ded4
permissions -rw-r--r--
expanded tabs
clasohm@1461
     1
(*  Title:      HOLCF/sprod1.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 sprod1.thy
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Sprod1;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* reduction properties for less_sprod                                      *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
nipkow@243
    15
clasohm@892
    16
qed_goalw "less_sprod1a" Sprod1.thy [less_sprod_def]
clasohm@1461
    17
        "p1=Ispair UU UU ==> less_sprod p1 p2"
regensbu@1168
    18
 (fn prems =>
clasohm@1461
    19
        [
clasohm@1461
    20
        (cut_facts_tac prems 1),
regensbu@1277
    21
        (asm_simp_tac HOL_ss 1)
clasohm@1461
    22
        ]);
nipkow@243
    23
clasohm@892
    24
qed_goalw "less_sprod1b" Sprod1.thy [less_sprod_def]
regensbu@1168
    25
 "p1~=Ispair UU UU ==> \
regensbu@1168
    26
\ less_sprod p1 p2 = ( Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2)"
regensbu@1168
    27
 (fn prems =>
clasohm@1461
    28
        [
clasohm@1461
    29
        (cut_facts_tac prems 1),
regensbu@1277
    30
        (asm_simp_tac HOL_ss 1)
clasohm@1461
    31
        ]);
nipkow@243
    32
clasohm@892
    33
qed_goal "less_sprod2a" Sprod1.thy
clasohm@1461
    34
        "less_sprod(Ispair x y)(Ispair UU UU) ==> x = UU | y = UU"
nipkow@243
    35
(fn prems =>
clasohm@1461
    36
        [
clasohm@1461
    37
        (cut_facts_tac prems 1),
clasohm@1461
    38
        (rtac (excluded_middle RS disjE) 1),
clasohm@1461
    39
        (atac 2),
clasohm@1461
    40
        (rtac disjI1 1),
clasohm@1461
    41
        (rtac antisym_less 1),
clasohm@1461
    42
        (rtac minimal 2),
clasohm@1461
    43
        (res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1),
clasohm@1461
    44
        (rtac Isfst 1),
clasohm@1461
    45
        (fast_tac HOL_cs 1),
clasohm@1461
    46
        (fast_tac HOL_cs 1),
clasohm@1461
    47
        (res_inst_tac [("s","Isfst(Ispair UU UU)"),("t","UU")] subst 1),
regensbu@1277
    48
        (simp_tac Sprod0_ss 1),
clasohm@1461
    49
        (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
clasohm@1461
    50
        (REPEAT (fast_tac HOL_cs 1))
clasohm@1461
    51
        ]);
nipkow@243
    52
clasohm@892
    53
qed_goal "less_sprod2b" Sprod1.thy
regensbu@1168
    54
 "less_sprod p (Ispair UU UU) ==> p = Ispair UU UU"
nipkow@243
    55
(fn prems =>
clasohm@1461
    56
        [
clasohm@1461
    57
        (cut_facts_tac prems 1),
clasohm@1461
    58
        (res_inst_tac [("p","p")] IsprodE 1),
clasohm@1461
    59
        (atac 1),
clasohm@1461
    60
        (hyp_subst_tac 1),
clasohm@1461
    61
        (rtac strict_Ispair 1),
clasohm@1461
    62
        (etac less_sprod2a 1)
clasohm@1461
    63
        ]);
nipkow@243
    64
clasohm@892
    65
qed_goal "less_sprod2c" Sprod1.thy 
regensbu@1168
    66
 "[|less_sprod(Ispair xa ya)(Ispair x y);\
regensbu@1168
    67
\  xa ~= UU ; ya ~= UU; x ~= UU ;  y ~= UU |] ==> xa << x & ya << y"
nipkow@243
    68
(fn prems =>
clasohm@1461
    69
        [
clasohm@1461
    70
        (rtac conjI 1),
clasohm@1461
    71
        (res_inst_tac [("s","Isfst(Ispair xa ya)"),("t","xa")] subst 1),
regensbu@1277
    72
        (simp_tac (Sprod0_ss addsimps prems)1),
clasohm@1461
    73
        (res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1),
regensbu@1277
    74
        (simp_tac (Sprod0_ss addsimps prems)1),
clasohm@1461
    75
        (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
clasohm@1461
    76
        (resolve_tac prems 1),
clasohm@1461
    77
        (resolve_tac prems 1),
regensbu@1277
    78
        (simp_tac (Sprod0_ss addsimps prems)1),
clasohm@1461
    79
        (res_inst_tac [("s","Issnd(Ispair xa ya)"),("t","ya")] subst 1),
regensbu@1277
    80
        (simp_tac (Sprod0_ss addsimps prems)1),
clasohm@1461
    81
        (res_inst_tac [("s","Issnd(Ispair x y)"),("t","y")] subst 1),
regensbu@1277
    82
        (simp_tac (Sprod0_ss addsimps prems)1),
clasohm@1461
    83
        (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1),
clasohm@1461
    84
        (resolve_tac prems 1),
clasohm@1461
    85
        (resolve_tac prems 1),
regensbu@1277
    86
        (simp_tac (Sprod0_ss addsimps prems)1)
clasohm@1461
    87
        ]);
nipkow@243
    88
nipkow@243
    89
(* ------------------------------------------------------------------------ *)
nipkow@243
    90
(* less_sprod is a partial order on Sprod                                   *)
nipkow@243
    91
(* ------------------------------------------------------------------------ *)
nipkow@243
    92
regensbu@1168
    93
qed_goal "refl_less_sprod" Sprod1.thy "less_sprod p p"
nipkow@243
    94
(fn prems =>
clasohm@1461
    95
        [
clasohm@1461
    96
        (res_inst_tac [("p","p")] IsprodE 1),
clasohm@1461
    97
        (etac less_sprod1a 1),
clasohm@1461
    98
        (hyp_subst_tac 1),
clasohm@1461
    99
        (rtac (less_sprod1b RS ssubst) 1),
clasohm@1461
   100
        (rtac defined_Ispair 1),
clasohm@1461
   101
        (REPEAT (fast_tac (HOL_cs addIs [refl_less]) 1))
clasohm@1461
   102
        ]);
nipkow@243
   103
nipkow@243
   104
clasohm@892
   105
qed_goal "antisym_less_sprod" Sprod1.thy 
regensbu@1168
   106
 "[|less_sprod p1 p2;less_sprod p2 p1|] ==> p1=p2"
nipkow@243
   107
 (fn prems =>
clasohm@1461
   108
        [
clasohm@1461
   109
        (cut_facts_tac prems 1),
clasohm@1461
   110
        (res_inst_tac [("p","p1")] IsprodE 1),
clasohm@1461
   111
        (hyp_subst_tac 1),
clasohm@1461
   112
        (res_inst_tac [("p","p2")] IsprodE 1),
clasohm@1461
   113
        (hyp_subst_tac 1),
clasohm@1461
   114
        (rtac refl 1),
clasohm@1461
   115
        (hyp_subst_tac 1),
clasohm@1461
   116
        (rtac (strict_Ispair RS sym) 1),
clasohm@1461
   117
        (etac less_sprod2a 1),
clasohm@1461
   118
        (hyp_subst_tac 1),
clasohm@1461
   119
        (res_inst_tac [("p","p2")] IsprodE 1),
clasohm@1461
   120
        (hyp_subst_tac 1),
clasohm@1461
   121
        (rtac (strict_Ispair) 1),
clasohm@1461
   122
        (etac less_sprod2a 1),
clasohm@1461
   123
        (hyp_subst_tac 1),
clasohm@1461
   124
        (res_inst_tac [("x1","x"),("y1","xa"),("x","y"),("y","ya")] (arg_cong RS cong) 1),
clasohm@1461
   125
        (rtac antisym_less 1),
regensbu@1277
   126
        (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
regensbu@1277
   127
        (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
clasohm@1461
   128
        (rtac antisym_less 1),
regensbu@1277
   129
        (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1),
regensbu@1277
   130
        (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1)
clasohm@1461
   131
        ]);
nipkow@243
   132
clasohm@892
   133
qed_goal "trans_less_sprod" Sprod1.thy 
regensbu@1168
   134
 "[|less_sprod (p1::'a**'b) p2;less_sprod p2 p3|] ==> less_sprod p1 p3"
regensbu@961
   135
 (fn prems =>
clasohm@1461
   136
        [
clasohm@1461
   137
        (cut_facts_tac prems 1),
clasohm@1461
   138
        (res_inst_tac [("p","p1")] IsprodE 1),
clasohm@1461
   139
        (etac less_sprod1a 1),
clasohm@1461
   140
        (hyp_subst_tac 1),
clasohm@1461
   141
        (res_inst_tac [("p","p3")] IsprodE 1),
clasohm@1461
   142
        (hyp_subst_tac 1),
clasohm@1461
   143
        (res_inst_tac [("s","p2"),("t","Ispair (UU::'a)(UU::'b)")] subst 1),
clasohm@1461
   144
        (etac less_sprod2b 1),
clasohm@1461
   145
        (atac 1),
clasohm@1461
   146
        (hyp_subst_tac 1),
clasohm@1461
   147
        (res_inst_tac [("Q","p2=Ispair(UU::'a)(UU::'b)")]
clasohm@1461
   148
                 (excluded_middle RS disjE) 1),
clasohm@1461
   149
        (rtac (defined_Ispair RS less_sprod1b RS ssubst) 1),
clasohm@1461
   150
        (REPEAT (atac 1)),
clasohm@1461
   151
        (rtac conjI 1),
clasohm@1461
   152
        (res_inst_tac [("y","Isfst(p2)")] trans_less 1),
clasohm@1461
   153
        (rtac conjunct1 1),
clasohm@1461
   154
        (rtac (less_sprod1b RS subst) 1),
clasohm@1461
   155
        (rtac defined_Ispair 1),
clasohm@1461
   156
        (REPEAT (atac 1)),
clasohm@1461
   157
        (rtac conjunct1 1),
clasohm@1461
   158
        (rtac (less_sprod1b RS subst) 1),
clasohm@1461
   159
        (REPEAT (atac 1)),
clasohm@1461
   160
        (res_inst_tac [("y","Issnd(p2)")] trans_less 1),
clasohm@1461
   161
        (rtac conjunct2 1),
clasohm@1461
   162
        (rtac (less_sprod1b RS subst) 1),
clasohm@1461
   163
        (rtac defined_Ispair 1),
clasohm@1461
   164
        (REPEAT (atac 1)),
clasohm@1461
   165
        (rtac conjunct2 1),
clasohm@1461
   166
        (rtac (less_sprod1b RS subst) 1),
clasohm@1461
   167
        (REPEAT (atac 1)),
clasohm@1461
   168
        (hyp_subst_tac 1),
clasohm@1461
   169
        (res_inst_tac [("s","Ispair(UU::'a)(UU::'b)"),("t","Ispair x y")] 
clasohm@1461
   170
                subst 1),
clasohm@1461
   171
        (etac (less_sprod2b RS sym) 1),
clasohm@1461
   172
        (atac 1)
clasohm@1461
   173
        ]);
nipkow@243
   174
nipkow@243
   175
nipkow@243
   176
nipkow@243
   177
nipkow@243
   178
nipkow@243
   179
nipkow@243
   180
nipkow@243
   181
nipkow@243
   182
nipkow@243
   183