| author | wenzelm |
| Thu Aug 27 20:46:36 1998 +0200 (1998-08-27) | |
| changeset 5400 | 645f46a24c72 |
| parent 3323 | 194ae2e0c193 |
| child 9245 | 428385c4bc50 |
| permissions | -rw-r--r-- |
| slotosch@2640 | 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 |
|
| slotosch@2640 | 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 |
(* less_sprod is a partial order on Sprod *) |
| nipkow@243 | 13 |
(* ------------------------------------------------------------------------ *) |
| nipkow@243 | 14 |
|
| slotosch@3323 | 15 |
qed_goalw "refl_less_sprod" thy [less_sprod_def]"(p::'a ** 'b) << p" |
| slotosch@2640 | 16 |
(fn prems => [(fast_tac (HOL_cs addIs [refl_less]) 1)]); |
| nipkow@243 | 17 |
|
| slotosch@2640 | 18 |
qed_goalw "antisym_less_sprod" thy [less_sprod_def] |
| slotosch@3323 | 19 |
"[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2" |
| slotosch@2640 | 20 |
(fn prems => |
| clasohm@1461 | 21 |
[ |
| clasohm@1461 | 22 |
(cut_facts_tac prems 1), |
| slotosch@2640 | 23 |
(rtac Sel_injective_Sprod 1), |
| slotosch@2640 | 24 |
(fast_tac (HOL_cs addIs [antisym_less]) 1), |
| slotosch@2640 | 25 |
(fast_tac (HOL_cs addIs [antisym_less]) 1) |
| clasohm@1461 | 26 |
]); |
| nipkow@243 | 27 |
|
| slotosch@2640 | 28 |
qed_goalw "trans_less_sprod" thy [less_sprod_def] |
| slotosch@3323 | 29 |
"[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3" |
| slotosch@2640 | 30 |
(fn prems => |
| slotosch@2640 | 31 |
[ |
| slotosch@2640 | 32 |
(cut_facts_tac prems 1), |
| slotosch@2640 | 33 |
(rtac conjI 1), |
| slotosch@2640 | 34 |
(fast_tac (HOL_cs addIs [trans_less]) 1), |
| slotosch@2640 | 35 |
(fast_tac (HOL_cs addIs [trans_less]) 1) |
| slotosch@2640 | 36 |
]); |