src/HOLCF/Cprod1.ML
author nipkow
Wed Jan 19 17:35:01 1994 +0100 (1994-01-19)
changeset 243 c22b85994e17
child 892 d0dc8d057929
permissions -rw-r--r--
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
nipkow@243
     1
(*  Title: 	HOLCF/cprod1.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 theory cprod1.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Cprod1;
nipkow@243
    10
nipkow@243
    11
val less_cprod1b = prove_goalw Cprod1.thy [less_cprod_def]
nipkow@243
    12
 "less_cprod(p1,p2) = ( fst(p1) << fst(p2) & snd(p1) << snd(p2))"
nipkow@243
    13
 (fn prems =>
nipkow@243
    14
	[
nipkow@243
    15
	(rtac refl 1)
nipkow@243
    16
	]);
nipkow@243
    17
nipkow@243
    18
val less_cprod2a = prove_goalw Cprod1.thy [less_cprod_def]
nipkow@243
    19
 "less_cprod(<x,y>,<UU,UU>) ==> x = UU & y = UU"
nipkow@243
    20
 (fn prems =>
nipkow@243
    21
	[
nipkow@243
    22
	(cut_facts_tac prems 1),
nipkow@243
    23
	(etac conjE 1),
nipkow@243
    24
	(dtac (fst_conv RS subst) 1),
nipkow@243
    25
	(dtac (fst_conv RS subst) 1),
nipkow@243
    26
	(dtac (fst_conv RS subst) 1),
nipkow@243
    27
	(dtac (snd_conv RS subst) 1),
nipkow@243
    28
	(dtac (snd_conv RS subst) 1),
nipkow@243
    29
	(dtac (snd_conv RS subst) 1),
nipkow@243
    30
	(rtac conjI 1),
nipkow@243
    31
	(etac UU_I 1),
nipkow@243
    32
	(etac UU_I 1)
nipkow@243
    33
	]);
nipkow@243
    34
nipkow@243
    35
val less_cprod2b = prove_goal Cprod1.thy 
nipkow@243
    36
 "less_cprod(p,<UU,UU>) ==> p=<UU,UU>"
nipkow@243
    37
 (fn prems =>
nipkow@243
    38
	[
nipkow@243
    39
	(cut_facts_tac prems 1),
nipkow@243
    40
	(res_inst_tac [("p","p")] PairE 1),
nipkow@243
    41
	(hyp_subst_tac 1),
nipkow@243
    42
	(dtac less_cprod2a 1),
nipkow@243
    43
	(asm_simp_tac HOL_ss 1)
nipkow@243
    44
	]);
nipkow@243
    45
nipkow@243
    46
val less_cprod2c = prove_goalw Cprod1.thy [less_cprod_def]
nipkow@243
    47
 "less_cprod(<x1,y1>,<x2,y2>) ==> x1 << x2 & y1 << y2"
nipkow@243
    48
 (fn prems =>
nipkow@243
    49
	[
nipkow@243
    50
	(cut_facts_tac prems 1),
nipkow@243
    51
	(etac conjE 1),
nipkow@243
    52
	(dtac (fst_conv RS subst) 1),
nipkow@243
    53
	(dtac (fst_conv RS subst) 1),
nipkow@243
    54
	(dtac (fst_conv RS subst) 1),
nipkow@243
    55
	(dtac (snd_conv RS subst) 1),
nipkow@243
    56
	(dtac (snd_conv RS subst) 1),
nipkow@243
    57
	(dtac (snd_conv RS subst) 1),
nipkow@243
    58
	(rtac conjI 1),
nipkow@243
    59
	(atac 1),
nipkow@243
    60
	(atac 1)
nipkow@243
    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
nipkow@243
    67
val refl_less_cprod = prove_goalw Cprod1.thy [less_cprod_def] "less_cprod(p,p)"
nipkow@243
    68
 (fn prems =>
nipkow@243
    69
	[
nipkow@243
    70
	(res_inst_tac [("p","p")] PairE 1),
nipkow@243
    71
	(hyp_subst_tac 1),
nipkow@243
    72
	(simp_tac pair_ss 1),
nipkow@243
    73
	(simp_tac Cfun_ss 1)
nipkow@243
    74
	]);
nipkow@243
    75
nipkow@243
    76
val antisym_less_cprod = prove_goal Cprod1.thy 
nipkow@243
    77
 "[|less_cprod(p1,p2);less_cprod(p2,p1)|] ==> p1=p2"
nipkow@243
    78
 (fn prems =>
nipkow@243
    79
	[
nipkow@243
    80
	(cut_facts_tac prems 1),
nipkow@243
    81
	(res_inst_tac [("p","p1")] PairE 1),
nipkow@243
    82
	(hyp_subst_tac 1),
nipkow@243
    83
	(res_inst_tac [("p","p2")] PairE 1),
nipkow@243
    84
	(hyp_subst_tac 1),
nipkow@243
    85
	(dtac less_cprod2c 1),
nipkow@243
    86
	(dtac less_cprod2c 1),
nipkow@243
    87
	(etac conjE 1),
nipkow@243
    88
	(etac conjE 1),
nipkow@243
    89
	(rtac (Pair_eq RS ssubst) 1),
nipkow@243
    90
	(fast_tac (HOL_cs addSIs [antisym_less]) 1)
nipkow@243
    91
	]);
nipkow@243
    92
nipkow@243
    93
nipkow@243
    94
val trans_less_cprod = prove_goal Cprod1.thy 
nipkow@243
    95
 "[|less_cprod(p1,p2);less_cprod(p2,p3)|] ==> less_cprod(p1,p3)"
nipkow@243
    96
 (fn prems =>
nipkow@243
    97
	[
nipkow@243
    98
	(cut_facts_tac prems 1),
nipkow@243
    99
	(res_inst_tac [("p","p1")] PairE 1),
nipkow@243
   100
	(hyp_subst_tac 1),
nipkow@243
   101
	(res_inst_tac [("p","p3")] PairE 1),
nipkow@243
   102
	(hyp_subst_tac 1),
nipkow@243
   103
	(res_inst_tac [("p","p2")] PairE 1),
nipkow@243
   104
	(hyp_subst_tac 1),
nipkow@243
   105
	(dtac less_cprod2c 1),
nipkow@243
   106
	(dtac less_cprod2c 1),
nipkow@243
   107
	(rtac (less_cprod1b RS ssubst) 1),
nipkow@243
   108
	(simp_tac pair_ss 1),
nipkow@243
   109
	(etac conjE 1),
nipkow@243
   110
	(etac conjE 1),
nipkow@243
   111
	(rtac conjI 1),
nipkow@243
   112
	(etac trans_less 1),
nipkow@243
   113
	(atac 1),
nipkow@243
   114
	(etac trans_less 1),
nipkow@243
   115
	(atac 1)
nipkow@243
   116
	]);
nipkow@243
   117