14 (* ------------------------------------------------------------------------ *) |
14 (* ------------------------------------------------------------------------ *) |
15 |
15 |
16 |
16 |
17 qed_goalw "ID1" ccc1.thy [ID_def] "ID`x=x" |
17 qed_goalw "ID1" ccc1.thy [ID_def] "ID`x=x" |
18 (fn prems => |
18 (fn prems => |
19 [ |
19 [ |
20 (rtac (beta_cfun RS ssubst) 1), |
20 (rtac (beta_cfun RS ssubst) 1), |
21 (rtac cont_id 1), |
21 (rtac cont_id 1), |
22 (rtac refl 1) |
22 (rtac refl 1) |
23 ]); |
23 ]); |
24 |
24 |
25 qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" |
25 qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" |
26 (fn prems => |
26 (fn prems => |
27 [ |
27 [ |
28 (rtac (beta_cfun RS ssubst) 1), |
28 (rtac (beta_cfun RS ssubst) 1), |
29 (cont_tacR 1), |
29 (cont_tacR 1), |
30 (rtac (beta_cfun RS ssubst) 1), |
30 (rtac (beta_cfun RS ssubst) 1), |
31 (cont_tacR 1), |
31 (cont_tacR 1), |
32 (rtac refl 1) |
32 (rtac refl 1) |
33 ]); |
33 ]); |
34 |
34 |
35 qed_goal "cfcomp2" ccc1.thy "(f oo g)`x=f`(g`x)" |
35 qed_goal "cfcomp2" ccc1.thy "(f oo g)`x=f`(g`x)" |
36 (fn prems => |
36 (fn prems => |
37 [ |
37 [ |
38 (rtac (cfcomp1 RS ssubst) 1), |
38 (rtac (cfcomp1 RS ssubst) 1), |
39 (rtac (beta_cfun RS ssubst) 1), |
39 (rtac (beta_cfun RS ssubst) 1), |
40 (cont_tacR 1), |
40 (cont_tacR 1), |
41 (rtac refl 1) |
41 (rtac refl 1) |
42 ]); |
42 ]); |
43 |
43 |
44 |
44 |
45 (* ------------------------------------------------------------------------ *) |
45 (* ------------------------------------------------------------------------ *) |
46 (* Show that interpretation of (pcpo,_->_) is a category *) |
46 (* Show that interpretation of (pcpo,_->_) is a category *) |
47 (* The class of objects is interpretation of syntactical class pcpo *) |
47 (* The class of objects is interpretation of syntactical class pcpo *) |
51 (* ------------------------------------------------------------------------ *) |
51 (* ------------------------------------------------------------------------ *) |
52 |
52 |
53 |
53 |
54 qed_goal "ID2" ccc1.thy "f oo ID = f " |
54 qed_goal "ID2" ccc1.thy "f oo ID = f " |
55 (fn prems => |
55 (fn prems => |
56 [ |
56 [ |
57 (rtac ext_cfun 1), |
57 (rtac ext_cfun 1), |
58 (rtac (cfcomp2 RS ssubst) 1), |
58 (rtac (cfcomp2 RS ssubst) 1), |
59 (rtac (ID1 RS ssubst) 1), |
59 (rtac (ID1 RS ssubst) 1), |
60 (rtac refl 1) |
60 (rtac refl 1) |
61 ]); |
61 ]); |
62 |
62 |
63 qed_goal "ID3" ccc1.thy "ID oo f = f " |
63 qed_goal "ID3" ccc1.thy "ID oo f = f " |
64 (fn prems => |
64 (fn prems => |
65 [ |
65 [ |
66 (rtac ext_cfun 1), |
66 (rtac ext_cfun 1), |
67 (rtac (cfcomp2 RS ssubst) 1), |
67 (rtac (cfcomp2 RS ssubst) 1), |
68 (rtac (ID1 RS ssubst) 1), |
68 (rtac (ID1 RS ssubst) 1), |
69 (rtac refl 1) |
69 (rtac refl 1) |
70 ]); |
70 ]); |
71 |
71 |
72 |
72 |
73 qed_goal "assoc_oo" ccc1.thy "f oo (g oo h) = (f oo g) oo h" |
73 qed_goal "assoc_oo" ccc1.thy "f oo (g oo h) = (f oo g) oo h" |
74 (fn prems => |
74 (fn prems => |
75 [ |
75 [ |
76 (rtac ext_cfun 1), |
76 (rtac ext_cfun 1), |
77 (res_inst_tac [("s","f`(g`(h`x))")] trans 1), |
77 (res_inst_tac [("s","f`(g`(h`x))")] trans 1), |
78 (rtac (cfcomp2 RS ssubst) 1), |
78 (rtac (cfcomp2 RS ssubst) 1), |
79 (rtac (cfcomp2 RS ssubst) 1), |
79 (rtac (cfcomp2 RS ssubst) 1), |
80 (rtac refl 1), |
80 (rtac refl 1), |
81 (rtac (cfcomp2 RS ssubst) 1), |
81 (rtac (cfcomp2 RS ssubst) 1), |
82 (rtac (cfcomp2 RS ssubst) 1), |
82 (rtac (cfcomp2 RS ssubst) 1), |
83 (rtac refl 1) |
83 (rtac refl 1) |
84 ]); |
84 ]); |
85 |
85 |
86 (* ------------------------------------------------------------------------ *) |
86 (* ------------------------------------------------------------------------ *) |
87 (* Merge the different rewrite rules for the simplifier *) |
87 (* Merge the different rewrite rules for the simplifier *) |
88 (* ------------------------------------------------------------------------ *) |
88 (* ------------------------------------------------------------------------ *) |
89 |
89 |