6 Lemmas for fun2.thy |
6 Lemmas for fun2.thy |
7 *) |
7 *) |
8 |
8 |
9 open Fun2; |
9 open Fun2; |
10 |
10 |
|
11 (* for compatibility with old HOLCF-Version *) |
|
12 qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x.f x << g x)" |
|
13 (fn prems => |
|
14 [ |
|
15 (fold_goals_tac [po_def,less_fun_def]), |
|
16 (rtac refl 1) |
|
17 ]); |
|
18 |
11 (* ------------------------------------------------------------------------ *) |
19 (* ------------------------------------------------------------------------ *) |
12 (* Type 'a::term => 'b::pcpo is pointed *) |
20 (* Type 'a::term => 'b::pcpo is pointed *) |
13 (* ------------------------------------------------------------------------ *) |
21 (* ------------------------------------------------------------------------ *) |
14 |
22 |
15 qed_goalw "minimal_fun" Fun2.thy [UU_fun_def] "UU_fun << f" |
23 qed_goal "minimal_fun" thy "(%z.UU) << x" |
16 (fn prems => |
24 (fn prems => |
17 [ |
25 [ |
18 (stac inst_fun_po 1), |
26 (simp_tac (!simpset addsimps [inst_fun_po,minimal]) 1) |
19 (rewtac less_fun_def), |
27 ]); |
20 (fast_tac (HOL_cs addSIs [minimal]) 1) |
28 |
|
29 bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym); |
|
30 |
|
31 qed_goal "least_fun" thy "? x::'a=>'b::pcpo.!y.x<<y" |
|
32 (fn prems => |
|
33 [ |
|
34 (res_inst_tac [("x","(%z.UU)")] exI 1), |
|
35 (rtac (minimal_fun RS allI) 1) |
21 ]); |
36 ]); |
22 |
37 |
23 (* ------------------------------------------------------------------------ *) |
38 (* ------------------------------------------------------------------------ *) |
24 (* make the symbol << accessible for type fun *) |
39 (* make the symbol << accessible for type fun *) |
25 (* ------------------------------------------------------------------------ *) |
40 (* ------------------------------------------------------------------------ *) |
26 |
41 |
27 qed_goal "less_fun" Fun2.thy "(f1 << f2) = (! x. f1(x) << f2(x))" |
42 qed_goal "less_fun" thy "(f1 << f2) = (! x. f1(x) << f2(x))" |
28 (fn prems => |
43 (fn prems => |
29 [ |
44 [ |
30 (stac inst_fun_po 1), |
45 (stac inst_fun_po 1), |
31 (fold_goals_tac [less_fun_def]), |
46 (fold_goals_tac [less_fun_def]), |
32 (rtac refl 1) |
47 (rtac refl 1) |
34 |
49 |
35 (* ------------------------------------------------------------------------ *) |
50 (* ------------------------------------------------------------------------ *) |
36 (* chains of functions yield chains in the po range *) |
51 (* chains of functions yield chains in the po range *) |
37 (* ------------------------------------------------------------------------ *) |
52 (* ------------------------------------------------------------------------ *) |
38 |
53 |
39 qed_goal "ch2ch_fun" Fun2.thy |
54 qed_goal "ch2ch_fun" thy |
40 "is_chain(S::nat=>('a::term => 'b::po)) ==> is_chain(% i.S(i)(x))" |
55 "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i.S(i)(x))" |
41 (fn prems => |
56 (fn prems => |
42 [ |
57 [ |
43 (cut_facts_tac prems 1), |
58 (cut_facts_tac prems 1), |
44 (rewtac is_chain), |
59 (rewtac is_chain), |
45 (rtac allI 1), |
60 (rtac allI 1), |