1 (* Title: HOLCF/fun1.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for fun1.thy |
|
7 *) |
|
8 |
|
9 open Fun1; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* less_fun is a partial order on 'a => 'b *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
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 ]); |
|
20 |
|
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 ]); |
|
29 |
|
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 ]); |
|
41 |
|
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 *) |
|
49 |
|