src/HOLCF/Cfun1.ML
author clasohm
Tue Feb 07 11:59:32 1995 +0100 (1995-02-07)
changeset 892 d0dc8d057929
parent 752 b89462f9d5f1
child 1168 74be52691d62
permissions -rw-r--r--
added qed, qed_goal[w]
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),
nipkow@243
    19
	(rtac contX_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
clasohm@892
    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] 
nipkow@243
    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] 
nipkow@243
    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 
nipkow@243
    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
clasohm@892
    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
clasohm@892
    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
clasohm@892
    89
qed_goal "Abs_Cfun_inverse2" Cfun1.thy "contX(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 
nipkow@243
   103
	"contX(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 
nipkow@243
   115
	"contX(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