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