src/HOLCF/fun1.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
nipkow@243
     1
(*  Title: 	HOLCF/fun1.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 fun1.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Fun1;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* less_fun is a partial order on 'a => 'b                                  *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
nipkow@243
    15
val refl_less_fun = prove_goalw Fun1.thy [less_fun_def] "less_fun(f,f)"
nipkow@243
    16
(fn prems =>
nipkow@243
    17
	[
nipkow@243
    18
	(fast_tac (HOL_cs addSIs [refl_less]) 1)
nipkow@243
    19
	]);
nipkow@243
    20
nipkow@243
    21
val antisym_less_fun = prove_goalw Fun1.thy [less_fun_def] 
nipkow@243
    22
	"[|less_fun(f1,f2); less_fun(f2,f1)|] ==> f1 = f2"
nipkow@243
    23
(fn prems =>
nipkow@243
    24
	[
nipkow@243
    25
	(cut_facts_tac prems 1),
nipkow@243
    26
	(rtac (expand_fun_eq RS ssubst) 1),
nipkow@243
    27
	(fast_tac (HOL_cs addSIs [antisym_less]) 1)
nipkow@243
    28
	]);
nipkow@243
    29
nipkow@243
    30
val trans_less_fun = prove_goalw Fun1.thy [less_fun_def] 
nipkow@243
    31
	"[|less_fun(f1,f2); less_fun(f2,f3)|] ==> less_fun(f1,f3)"
nipkow@243
    32
(fn prems =>
nipkow@243
    33
	[
nipkow@243
    34
	(cut_facts_tac prems 1),
nipkow@243
    35
	(strip_tac 1),
nipkow@243
    36
	(rtac trans_less 1),
nipkow@243
    37
	(etac allE 1),
nipkow@243
    38
	(atac 1),
nipkow@243
    39
	((etac allE 1) THEN (atac 1))
nipkow@243
    40
	]);
nipkow@243
    41
nipkow@243
    42
(* 
nipkow@243
    43
 -------------------------------------------------------------------------- 
nipkow@243
    44
   Since less_fun :: "['a::term=>'b::po,'a::term=>'b::po] => bool" the
nipkow@243
    45
   lemmas refl_less_fun, antisym_less_fun, trans_less_fun justify
nipkow@243
    46
   the class arity fun::(term,po)po !!
nipkow@243
    47
 -------------------------------------------------------------------------- 
nipkow@243
    48
*)
nipkow@243
    49