src/HOLCF/Fun1.ML
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--
made tutorial first;
slotosch@2640
     1
(*  Title:      HOLCF/Fun1.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 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
slotosch@3323
    15
qed_goalw "refl_less_fun" thy [less_fun_def] "(f::'a::term =>'b::po) << f"
nipkow@243
    16
(fn prems =>
clasohm@1461
    17
        [
clasohm@1461
    18
        (fast_tac (HOL_cs addSIs [refl_less]) 1)
clasohm@1461
    19
        ]);
nipkow@243
    20
clasohm@892
    21
qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def] 
slotosch@3323
    22
        "[|(f1::'a::term =>'b::po) << f2; f2 << f1|] ==> f1 = f2"
nipkow@243
    23
(fn prems =>
clasohm@1461
    24
        [
clasohm@1461
    25
        (cut_facts_tac prems 1),
paulson@2033
    26
        (stac expand_fun_eq 1),
clasohm@1461
    27
        (fast_tac (HOL_cs addSIs [antisym_less]) 1)
clasohm@1461
    28
        ]);
nipkow@243
    29
clasohm@892
    30
qed_goalw "trans_less_fun" Fun1.thy [less_fun_def] 
slotosch@3323
    31
        "[|(f1::'a::term =>'b::po) << f2; f2 << f3 |] ==> f1 << f3"
nipkow@243
    32
(fn prems =>
clasohm@1461
    33
        [
clasohm@1461
    34
        (cut_facts_tac prems 1),
clasohm@1461
    35
        (strip_tac 1),
clasohm@1461
    36
        (rtac trans_less 1),
clasohm@1461
    37
        (etac allE 1),
clasohm@1461
    38
        (atac 1),
clasohm@1461
    39
        ((etac allE 1) THEN (atac 1))
clasohm@1461
    40
        ]);