10 |
10 |
11 (* ------------------------------------------------------------------------ *) |
11 (* ------------------------------------------------------------------------ *) |
12 (* less_fun is a partial order on 'a => 'b *) |
12 (* less_fun is a partial order on 'a => 'b *) |
13 (* ------------------------------------------------------------------------ *) |
13 (* ------------------------------------------------------------------------ *) |
14 |
14 |
15 qed_goalw "refl_less_fun" Fun1.thy [less_fun_def] "less_fun(f,f)" |
15 qed_goalw "refl_less_fun" Fun1.thy [less_fun_def] "less_fun f f" |
16 (fn prems => |
16 (fn prems => |
17 [ |
17 [ |
18 (fast_tac (HOL_cs addSIs [refl_less]) 1) |
18 (fast_tac (HOL_cs addSIs [refl_less]) 1) |
19 ]); |
19 ]); |
20 |
20 |
21 qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def] |
21 qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def] |
22 "[|less_fun(f1,f2); less_fun(f2,f1)|] ==> f1 = f2" |
22 "[|less_fun f1 f2; less_fun f2 f1|] ==> f1 = f2" |
23 (fn prems => |
23 (fn prems => |
24 [ |
24 [ |
25 (cut_facts_tac prems 1), |
25 (cut_facts_tac prems 1), |
26 (rtac (expand_fun_eq RS ssubst) 1), |
26 (rtac (expand_fun_eq RS ssubst) 1), |
27 (fast_tac (HOL_cs addSIs [antisym_less]) 1) |
27 (fast_tac (HOL_cs addSIs [antisym_less]) 1) |
28 ]); |
28 ]); |
29 |
29 |
30 qed_goalw "trans_less_fun" Fun1.thy [less_fun_def] |
30 qed_goalw "trans_less_fun" Fun1.thy [less_fun_def] |
31 "[|less_fun(f1,f2); less_fun(f2,f3)|] ==> less_fun(f1,f3)" |
31 "[|less_fun f1 f2; less_fun f2 f3 |] ==> less_fun f1 f3" |
32 (fn prems => |
32 (fn prems => |
33 [ |
33 [ |
34 (cut_facts_tac prems 1), |
34 (cut_facts_tac prems 1), |
35 (strip_tac 1), |
35 (strip_tac 1), |
36 (rtac trans_less 1), |
36 (rtac trans_less 1), |