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]
     1 (*  Title: 	HOLCF/cfun1.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for cfun1.thy 
     7 *)
     8 
     9 open Cfun1;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* A non-emptyness result for Cfun                                          *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
    16  (fn prems =>
    17 	[
    18 	(rtac (mem_Collect_eq RS ssubst) 1),
    19 	(rtac contX_id 1)
    20 	]);
    21 
    22 
    23 (* ------------------------------------------------------------------------ *)
    24 (* less_cfun is a partial order on type 'a -> 'b                            *)
    25 (* ------------------------------------------------------------------------ *)
    26 
    27 qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun(f,f)"
    28 (fn prems =>
    29 	[
    30 	(rtac refl_less 1)
    31 	]);
    32 
    33 qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def] 
    34 	"[|less_cfun(f1,f2); less_cfun(f2,f1)|] ==> f1 = f2"
    35 (fn prems =>
    36 	[
    37 	(cut_facts_tac prems 1),
    38 	(rtac injD 1),
    39 	(rtac antisym_less 2),
    40 	(atac 3),
    41 	(atac 2),
    42 	(rtac inj_inverseI 1),
    43 	(rtac Rep_Cfun_inverse 1)
    44 	]);
    45 
    46 qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def] 
    47 	"[|less_cfun(f1,f2); less_cfun(f2,f3)|] ==> less_cfun(f1,f3)"
    48 (fn prems =>
    49 	[
    50 	(cut_facts_tac prems 1),
    51 	(etac trans_less 1),
    52 	(atac 1)
    53 	]);
    54 
    55 (* ------------------------------------------------------------------------ *)
    56 (* lemmas about application of continuous functions                         *)
    57 (* ------------------------------------------------------------------------ *)
    58 
    59 qed_goal "cfun_cong" Cfun1.thy 
    60 	 "[| f=g; x=y |] ==> f[x] = g[y]"
    61 (fn prems =>
    62 	[
    63 	(cut_facts_tac prems 1),
    64 	(fast_tac HOL_cs 1)
    65 	]);
    66 
    67 qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f[x] = g[x]"
    68 (fn prems =>
    69 	[
    70 	(cut_facts_tac prems 1),
    71 	(etac cfun_cong 1),
    72 	(rtac refl 1)
    73 	]);
    74 
    75 qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f[x] = f[y]"
    76 (fn prems =>
    77 	[
    78 	(cut_facts_tac prems 1),
    79 	(rtac cfun_cong 1),
    80 	(rtac refl 1),
    81 	(atac 1)
    82 	]);
    83 
    84 
    85 (* ------------------------------------------------------------------------ *)
    86 (* additional lemma about the isomorphism between -> and Cfun               *)
    87 (* ------------------------------------------------------------------------ *)
    88 
    89 qed_goal "Abs_Cfun_inverse2" Cfun1.thy "contX(f) ==> fapp(fabs(f)) = f"
    90 (fn prems =>
    91 	[
    92 	(cut_facts_tac prems 1),
    93 	(rtac Abs_Cfun_inverse 1),
    94 	(rewrite_goals_tac [Cfun_def]),
    95 	(etac (mem_Collect_eq RS ssubst) 1)
    96 	]);
    97 
    98 (* ------------------------------------------------------------------------ *)
    99 (* simplification of application                                            *)
   100 (* ------------------------------------------------------------------------ *)
   101 
   102 qed_goal "Cfunapp2" Cfun1.thy 
   103 	"contX(f) ==> (fabs(f))[x] = f(x)"
   104 (fn prems =>
   105 	[
   106 	(cut_facts_tac prems 1),
   107 	(etac (Abs_Cfun_inverse2 RS fun_cong) 1)
   108 	]);
   109 
   110 (* ------------------------------------------------------------------------ *)
   111 (* beta - equality for continuous functions                                 *)
   112 (* ------------------------------------------------------------------------ *)
   113 
   114 qed_goal "beta_cfun" Cfun1.thy 
   115 	"contX(c1) ==> (LAM x .c1(x))[u] = c1(u)"
   116 (fn prems =>
   117 	[
   118 	(cut_facts_tac prems 1),
   119 	(rtac Cfunapp2 1),
   120 	(atac 1)
   121 	]);
   122