isabelle: src/HOLCF/fun1.ML@645f46a24c72

     1 (*  Title: 	HOLCF/fun1.ML

     2     ID:         $Id$

     3     Author: 	Franz Regensburger

     4     Copyright   1993  Technische Universitaet Muenchen

     6 Lemmas for fun1.thy

     7 *)

     9 open Fun1;

    11 (* ------------------------------------------------------------------------ *)

    12 (* less_fun is a partial order on 'a => 'b                                  *)

    13 (* ------------------------------------------------------------------------ *)

    15 val refl_less_fun = prove_goalw Fun1.thy [less_fun_def] "less_fun(f,f)"

    16 (fn prems =>

    17 	[

    18 	(fast_tac (HOL_cs addSIs [refl_less]) 1)

    19 	]);

    21 val antisym_less_fun = prove_goalw Fun1.thy [less_fun_def]

    22 	"[|less_fun(f1,f2); less_fun(f2,f1)|] ==> f1 = f2"

    23 (fn prems =>

    24 	[

    25 	(cut_facts_tac prems 1),

    26 	(rtac (expand_fun_eq RS ssubst) 1),

    27 	(fast_tac (HOL_cs addSIs [antisym_less]) 1)

    28 	]);

    30 val trans_less_fun = prove_goalw Fun1.thy [less_fun_def]

    31 	"[|less_fun(f1,f2); less_fun(f2,f3)|] ==> less_fun(f1,f3)"

    32 (fn prems =>

    33 	[

    34 	(cut_facts_tac prems 1),

    35 	(strip_tac 1),

    36 	(rtac trans_less 1),

    37 	(etac allE 1),

    38 	(atac 1),

    39 	((etac allE 1) THEN (atac 1))

    40 	]);

    42 (*

    43  --------------------------------------------------------------------------

    44    Since less_fun :: "['a::term=>'b::po,'a::term=>'b::po] => bool" the

    45    lemmas refl_less_fun, antisym_less_fun, trans_less_fun justify

    46    the class arity fun::(term,po)po !!

    47  --------------------------------------------------------------------------

    48 *)

author	wenzelm
	Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400	645f46a24c72
parent 243	c22b85994e17
permissions	-rw-r--r--