src/HOLCF/Cfun1.ML
author regensbu
Thu Jun 29 16:28:40 1995 +0200 (1995-06-29)
changeset 1168 74be52691d62
parent 892 d0dc8d057929
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
The curried version of HOLCF is now just called HOLCF. The old
uncurried version is no longer supported
nipkow@243
     1
(*  Title: 	HOLCF/cfun1.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 cfun1.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Cfun1;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* A non-emptyness result for Cfun                                          *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
clasohm@892
    15
qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
nipkow@243
    16
 (fn prems =>
nipkow@243
    17
	[
nipkow@243
    18
	(rtac (mem_Collect_eq RS ssubst) 1),
regensbu@1168
    19
	(rtac cont_id 1)
nipkow@243
    20
	]);
nipkow@243
    21
nipkow@243
    22
nipkow@243
    23
(* ------------------------------------------------------------------------ *)
nipkow@243
    24
(* less_cfun is a partial order on type 'a -> 'b                            *)
nipkow@243
    25
(* ------------------------------------------------------------------------ *)
nipkow@243
    26
regensbu@1168
    27
qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun f f"
nipkow@243
    28
(fn prems =>
nipkow@243
    29
	[
nipkow@243
    30
	(rtac refl_less 1)
nipkow@243
    31
	]);
nipkow@243
    32
clasohm@892
    33
qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def] 
regensbu@1168
    34
	"[|less_cfun f1 f2; less_cfun f2 f1|] ==> f1 = f2"
nipkow@243
    35
(fn prems =>
nipkow@243
    36
	[
nipkow@243
    37
	(cut_facts_tac prems 1),
nipkow@243
    38
	(rtac injD 1),
nipkow@243
    39
	(rtac antisym_less 2),
nipkow@243
    40
	(atac 3),
nipkow@243
    41
	(atac 2),
nipkow@243
    42
	(rtac inj_inverseI 1),
nipkow@243
    43
	(rtac Rep_Cfun_inverse 1)
nipkow@243
    44
	]);
nipkow@243
    45
clasohm@892
    46
qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def] 
regensbu@1168
    47
	"[|less_cfun f1 f2; less_cfun f2 f3|] ==> less_cfun f1 f3"
nipkow@243
    48
(fn prems =>
nipkow@243
    49
	[
nipkow@243
    50
	(cut_facts_tac prems 1),
nipkow@243
    51
	(etac trans_less 1),
nipkow@243
    52
	(atac 1)
nipkow@243
    53
	]);
nipkow@243
    54
nipkow@243
    55
(* ------------------------------------------------------------------------ *)
nipkow@243
    56
(* lemmas about application of continuous functions                         *)
nipkow@243
    57
(* ------------------------------------------------------------------------ *)
nipkow@243
    58
clasohm@892
    59
qed_goal "cfun_cong" Cfun1.thy 
regensbu@1168
    60
	 "[| f=g; x=y |] ==> f`x = g`y"
nipkow@243
    61
(fn prems =>
nipkow@243
    62
	[
nipkow@243
    63
	(cut_facts_tac prems 1),
nipkow@243
    64
	(fast_tac HOL_cs 1)
nipkow@243
    65
	]);
nipkow@243
    66
regensbu@1168
    67
qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f`x = g`x"
nipkow@243
    68
(fn prems =>
nipkow@243
    69
	[
nipkow@243
    70
	(cut_facts_tac prems 1),
nipkow@243
    71
	(etac cfun_cong 1),
nipkow@243
    72
	(rtac refl 1)
nipkow@243
    73
	]);
nipkow@243
    74
regensbu@1168
    75
qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f`x = f`y"
nipkow@243
    76
(fn prems =>
nipkow@243
    77
	[
nipkow@243
    78
	(cut_facts_tac prems 1),
nipkow@243
    79
	(rtac cfun_cong 1),
nipkow@243
    80
	(rtac refl 1),
nipkow@243
    81
	(atac 1)
nipkow@243
    82
	]);
nipkow@243
    83
nipkow@243
    84
nipkow@243
    85
(* ------------------------------------------------------------------------ *)
nipkow@243
    86
(* additional lemma about the isomorphism between -> and Cfun               *)
nipkow@243
    87
(* ------------------------------------------------------------------------ *)
nipkow@243
    88
regensbu@1168
    89
qed_goal "Abs_Cfun_inverse2" Cfun1.thy "cont(f) ==> fapp(fabs(f)) = f"
nipkow@243
    90
(fn prems =>
nipkow@243
    91
	[
nipkow@243
    92
	(cut_facts_tac prems 1),
nipkow@243
    93
	(rtac Abs_Cfun_inverse 1),
nipkow@243
    94
	(rewrite_goals_tac [Cfun_def]),
nipkow@243
    95
	(etac (mem_Collect_eq RS ssubst) 1)
nipkow@243
    96
	]);
nipkow@243
    97
nipkow@243
    98
(* ------------------------------------------------------------------------ *)
nipkow@243
    99
(* simplification of application                                            *)
nipkow@243
   100
(* ------------------------------------------------------------------------ *)
nipkow@243
   101
clasohm@892
   102
qed_goal "Cfunapp2" Cfun1.thy 
regensbu@1168
   103
	"cont(f) ==> (fabs f)`x = f x"
nipkow@243
   104
(fn prems =>
nipkow@243
   105
	[
nipkow@243
   106
	(cut_facts_tac prems 1),
nipkow@243
   107
	(etac (Abs_Cfun_inverse2 RS fun_cong) 1)
nipkow@243
   108
	]);
nipkow@243
   109
nipkow@243
   110
(* ------------------------------------------------------------------------ *)
nipkow@243
   111
(* beta - equality for continuous functions                                 *)
nipkow@243
   112
(* ------------------------------------------------------------------------ *)
nipkow@243
   113
clasohm@892
   114
qed_goal "beta_cfun" Cfun1.thy 
regensbu@1168
   115
	"cont(c1) ==> (LAM x .c1 x)`u = c1 u"
nipkow@243
   116
(fn prems =>
nipkow@243
   117
	[
nipkow@243
   118
	(cut_facts_tac prems 1),
nipkow@243
   119
	(rtac Cfunapp2 1),
nipkow@243
   120
	(atac 1)
nipkow@243
   121
	]);
nipkow@243
   122
regensbu@1168
   123
regensbu@1168
   124
regensbu@1168
   125