equal
deleted
inserted
replaced
6 Lemmas for theory cprod1.thy |
6 Lemmas for theory cprod1.thy |
7 *) |
7 *) |
8 |
8 |
9 open Cprod1; |
9 open Cprod1; |
10 |
10 |
11 val less_cprod1b = prove_goalw Cprod1.thy [less_cprod_def] |
11 qed_goalw "less_cprod1b" Cprod1.thy [less_cprod_def] |
12 "less_cprod(p1,p2) = ( fst(p1) << fst(p2) & snd(p1) << snd(p2))" |
12 "less_cprod(p1,p2) = ( fst(p1) << fst(p2) & snd(p1) << snd(p2))" |
13 (fn prems => |
13 (fn prems => |
14 [ |
14 [ |
15 (rtac refl 1) |
15 (rtac refl 1) |
16 ]); |
16 ]); |
17 |
17 |
18 val less_cprod2a = prove_goalw Cprod1.thy [less_cprod_def] |
18 qed_goalw "less_cprod2a" Cprod1.thy [less_cprod_def] |
19 "less_cprod(<x,y>,<UU,UU>) ==> x = UU & y = UU" |
19 "less_cprod(<x,y>,<UU,UU>) ==> x = UU & y = UU" |
20 (fn prems => |
20 (fn prems => |
21 [ |
21 [ |
22 (cut_facts_tac prems 1), |
22 (cut_facts_tac prems 1), |
23 (etac conjE 1), |
23 (etac conjE 1), |
30 (rtac conjI 1), |
30 (rtac conjI 1), |
31 (etac UU_I 1), |
31 (etac UU_I 1), |
32 (etac UU_I 1) |
32 (etac UU_I 1) |
33 ]); |
33 ]); |
34 |
34 |
35 val less_cprod2b = prove_goal Cprod1.thy |
35 qed_goal "less_cprod2b" Cprod1.thy |
36 "less_cprod(p,<UU,UU>) ==> p=<UU,UU>" |
36 "less_cprod(p,<UU,UU>) ==> p=<UU,UU>" |
37 (fn prems => |
37 (fn prems => |
38 [ |
38 [ |
39 (cut_facts_tac prems 1), |
39 (cut_facts_tac prems 1), |
40 (res_inst_tac [("p","p")] PairE 1), |
40 (res_inst_tac [("p","p")] PairE 1), |
41 (hyp_subst_tac 1), |
41 (hyp_subst_tac 1), |
42 (dtac less_cprod2a 1), |
42 (dtac less_cprod2a 1), |
43 (asm_simp_tac HOL_ss 1) |
43 (asm_simp_tac HOL_ss 1) |
44 ]); |
44 ]); |
45 |
45 |
46 val less_cprod2c = prove_goalw Cprod1.thy [less_cprod_def] |
46 qed_goalw "less_cprod2c" Cprod1.thy [less_cprod_def] |
47 "less_cprod(<x1,y1>,<x2,y2>) ==> x1 << x2 & y1 << y2" |
47 "less_cprod(<x1,y1>,<x2,y2>) ==> x1 << x2 & y1 << y2" |
48 (fn prems => |
48 (fn prems => |
49 [ |
49 [ |
50 (cut_facts_tac prems 1), |
50 (cut_facts_tac prems 1), |
51 (etac conjE 1), |
51 (etac conjE 1), |
62 |
62 |
63 (* ------------------------------------------------------------------------ *) |
63 (* ------------------------------------------------------------------------ *) |
64 (* less_cprod is a partial order on 'a * 'b *) |
64 (* less_cprod is a partial order on 'a * 'b *) |
65 (* ------------------------------------------------------------------------ *) |
65 (* ------------------------------------------------------------------------ *) |
66 |
66 |
67 val refl_less_cprod = prove_goalw Cprod1.thy [less_cprod_def] "less_cprod(p,p)" |
67 qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less_cprod(p,p)" |
68 (fn prems => |
68 (fn prems => |
69 [ |
69 [ |
70 (res_inst_tac [("p","p")] PairE 1), |
70 (res_inst_tac [("p","p")] PairE 1), |
71 (hyp_subst_tac 1), |
71 (hyp_subst_tac 1), |
72 (simp_tac pair_ss 1), |
72 (simp_tac pair_ss 1), |
73 (simp_tac Cfun_ss 1) |
73 (simp_tac Cfun_ss 1) |
74 ]); |
74 ]); |
75 |
75 |
76 val antisym_less_cprod = prove_goal Cprod1.thy |
76 qed_goal "antisym_less_cprod" Cprod1.thy |
77 "[|less_cprod(p1,p2);less_cprod(p2,p1)|] ==> p1=p2" |
77 "[|less_cprod(p1,p2);less_cprod(p2,p1)|] ==> p1=p2" |
78 (fn prems => |
78 (fn prems => |
79 [ |
79 [ |
80 (cut_facts_tac prems 1), |
80 (cut_facts_tac prems 1), |
81 (res_inst_tac [("p","p1")] PairE 1), |
81 (res_inst_tac [("p","p1")] PairE 1), |
89 (rtac (Pair_eq RS ssubst) 1), |
89 (rtac (Pair_eq RS ssubst) 1), |
90 (fast_tac (HOL_cs addSIs [antisym_less]) 1) |
90 (fast_tac (HOL_cs addSIs [antisym_less]) 1) |
91 ]); |
91 ]); |
92 |
92 |
93 |
93 |
94 val trans_less_cprod = prove_goal Cprod1.thy |
94 qed_goal "trans_less_cprod" Cprod1.thy |
95 "[|less_cprod(p1,p2);less_cprod(p2,p3)|] ==> less_cprod(p1,p3)" |
95 "[|less_cprod(p1,p2);less_cprod(p2,p3)|] ==> less_cprod(p1,p3)" |
96 (fn prems => |
96 (fn prems => |
97 [ |
97 [ |
98 (cut_facts_tac prems 1), |
98 (cut_facts_tac prems 1), |
99 (res_inst_tac [("p","p1")] PairE 1), |
99 (res_inst_tac [("p","p1")] PairE 1), |