20 (rtac exI 1), |
20 (rtac exI 1), |
21 (res_inst_tac [("f","Abs_Lift")] arg_cong 1), |
21 (res_inst_tac [("f","Abs_Lift")] arg_cong 1), |
22 (atac 1) |
22 (atac 1) |
23 ]); |
23 ]); |
24 |
24 |
25 val inj_Abs_Lift = prove_goal Lift1.thy "inj(Abs_Lift)" |
25 qed_goal "inj_Abs_Lift" Lift1.thy "inj(Abs_Lift)" |
26 (fn prems => |
26 (fn prems => |
27 [ |
27 [ |
28 (rtac inj_inverseI 1), |
28 (rtac inj_inverseI 1), |
29 (rtac Abs_Lift_inverse 1) |
29 (rtac Abs_Lift_inverse 1) |
30 ]); |
30 ]); |
31 |
31 |
32 val inj_Rep_Lift = prove_goal Lift1.thy "inj(Rep_Lift)" |
32 qed_goal "inj_Rep_Lift" Lift1.thy "inj(Rep_Lift)" |
33 (fn prems => |
33 (fn prems => |
34 [ |
34 [ |
35 (rtac inj_inverseI 1), |
35 (rtac inj_inverseI 1), |
36 (rtac Rep_Lift_inverse 1) |
36 (rtac Rep_Lift_inverse 1) |
37 ]); |
37 ]); |
38 |
38 |
39 val inject_Iup = prove_goalw Lift1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y" |
39 qed_goalw "inject_Iup" Lift1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y" |
40 (fn prems => |
40 (fn prems => |
41 [ |
41 [ |
42 (cut_facts_tac prems 1), |
42 (cut_facts_tac prems 1), |
43 (rtac (inj_Inr RS injD) 1), |
43 (rtac (inj_Inr RS injD) 1), |
44 (rtac (inj_Abs_Lift RS injD) 1), |
44 (rtac (inj_Abs_Lift RS injD) 1), |
45 (atac 1) |
45 (atac 1) |
46 ]); |
46 ]); |
47 |
47 |
48 val defined_Iup=prove_goalw Lift1.thy [Iup_def,UU_lift_def] "~ Iup(x)=UU_lift" |
48 qed_goalw "defined_Iup" Lift1.thy [Iup_def,UU_lift_def] "~ Iup(x)=UU_lift" |
49 (fn prems => |
49 (fn prems => |
50 [ |
50 [ |
51 (rtac notI 1), |
51 (rtac notI 1), |
52 (rtac notE 1), |
52 (rtac notE 1), |
53 (rtac Inl_not_Inr 1), |
53 (rtac Inl_not_Inr 1), |
54 (rtac sym 1), |
54 (rtac sym 1), |
55 (etac (inj_Abs_Lift RS injD) 1) |
55 (etac (inj_Abs_Lift RS injD) 1) |
56 ]); |
56 ]); |
57 |
57 |
58 |
58 |
59 val liftE = prove_goal Lift1.thy |
59 qed_goal "liftE" Lift1.thy |
60 "[| p=UU_lift ==> Q; !!x. p=Iup(x)==>Q|] ==>Q" |
60 "[| p=UU_lift ==> Q; !!x. p=Iup(x)==>Q|] ==>Q" |
61 (fn prems => |
61 (fn prems => |
62 [ |
62 [ |
63 (rtac (Exh_Lift RS disjE) 1), |
63 (rtac (Exh_Lift RS disjE) 1), |
64 (eresolve_tac prems 1), |
64 (eresolve_tac prems 1), |
65 (etac exE 1), |
65 (etac exE 1), |
66 (eresolve_tac prems 1) |
66 (eresolve_tac prems 1) |
67 ]); |
67 ]); |
68 |
68 |
69 val Ilift1 = prove_goalw Lift1.thy [Ilift_def,UU_lift_def] |
69 qed_goalw "Ilift1" Lift1.thy [Ilift_def,UU_lift_def] |
70 "Ilift(f)(UU_lift)=UU" |
70 "Ilift(f)(UU_lift)=UU" |
71 (fn prems => |
71 (fn prems => |
72 [ |
72 [ |
73 (rtac (Abs_Lift_inverse RS ssubst) 1), |
73 (rtac (Abs_Lift_inverse RS ssubst) 1), |
74 (rtac (sum_case_Inl RS ssubst) 1), |
74 (rtac (sum_case_Inl RS ssubst) 1), |
75 (rtac refl 1) |
75 (rtac refl 1) |
76 ]); |
76 ]); |
77 |
77 |
78 val Ilift2 = prove_goalw Lift1.thy [Ilift_def,Iup_def] |
78 qed_goalw "Ilift2" Lift1.thy [Ilift_def,Iup_def] |
79 "Ilift(f)(Iup(x))=f[x]" |
79 "Ilift(f)(Iup(x))=f[x]" |
80 (fn prems => |
80 (fn prems => |
81 [ |
81 [ |
82 (rtac (Abs_Lift_inverse RS ssubst) 1), |
82 (rtac (Abs_Lift_inverse RS ssubst) 1), |
83 (rtac (sum_case_Inr RS ssubst) 1), |
83 (rtac (sum_case_Inr RS ssubst) 1), |
84 (rtac refl 1) |
84 (rtac refl 1) |
85 ]); |
85 ]); |
86 |
86 |
87 val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2]; |
87 val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2]; |
88 |
88 |
89 val less_lift1a = prove_goalw Lift1.thy [less_lift_def,UU_lift_def] |
89 qed_goalw "less_lift1a" Lift1.thy [less_lift_def,UU_lift_def] |
90 "less_lift(UU_lift)(z)" |
90 "less_lift(UU_lift)(z)" |
91 (fn prems => |
91 (fn prems => |
92 [ |
92 [ |
93 (rtac (Abs_Lift_inverse RS ssubst) 1), |
93 (rtac (Abs_Lift_inverse RS ssubst) 1), |
94 (rtac (sum_case_Inl RS ssubst) 1), |
94 (rtac (sum_case_Inl RS ssubst) 1), |
95 (rtac TrueI 1) |
95 (rtac TrueI 1) |
96 ]); |
96 ]); |
97 |
97 |
98 val less_lift1b = prove_goalw Lift1.thy [Iup_def,less_lift_def,UU_lift_def] |
98 qed_goalw "less_lift1b" Lift1.thy [Iup_def,less_lift_def,UU_lift_def] |
99 "~less_lift(Iup(x),UU_lift)" |
99 "~less_lift(Iup(x),UU_lift)" |
100 (fn prems => |
100 (fn prems => |
101 [ |
101 [ |
102 (rtac notI 1), |
102 (rtac notI 1), |
103 (rtac iffD1 1), |
103 (rtac iffD1 1), |
107 (rtac (sum_case_Inr RS ssubst) 1), |
107 (rtac (sum_case_Inr RS ssubst) 1), |
108 (rtac (sum_case_Inl RS ssubst) 1), |
108 (rtac (sum_case_Inl RS ssubst) 1), |
109 (rtac refl 1) |
109 (rtac refl 1) |
110 ]); |
110 ]); |
111 |
111 |
112 val less_lift1c = prove_goalw Lift1.thy [Iup_def,less_lift_def,UU_lift_def] |
112 qed_goalw "less_lift1c" Lift1.thy [Iup_def,less_lift_def,UU_lift_def] |
113 "less_lift(Iup(x),Iup(y))=(x<<y)" |
113 "less_lift(Iup(x),Iup(y))=(x<<y)" |
114 (fn prems => |
114 (fn prems => |
115 [ |
115 [ |
116 (rtac (Abs_Lift_inverse RS ssubst) 1), |
116 (rtac (Abs_Lift_inverse RS ssubst) 1), |
117 (rtac (Abs_Lift_inverse RS ssubst) 1), |
117 (rtac (Abs_Lift_inverse RS ssubst) 1), |
119 (rtac (sum_case_Inr RS ssubst) 1), |
119 (rtac (sum_case_Inr RS ssubst) 1), |
120 (rtac refl 1) |
120 (rtac refl 1) |
121 ]); |
121 ]); |
122 |
122 |
123 |
123 |
124 val refl_less_lift = prove_goal Lift1.thy "less_lift(p,p)" |
124 qed_goal "refl_less_lift" Lift1.thy "less_lift(p,p)" |
125 (fn prems => |
125 (fn prems => |
126 [ |
126 [ |
127 (res_inst_tac [("p","p")] liftE 1), |
127 (res_inst_tac [("p","p")] liftE 1), |
128 (hyp_subst_tac 1), |
128 (hyp_subst_tac 1), |
129 (rtac less_lift1a 1), |
129 (rtac less_lift1a 1), |
130 (hyp_subst_tac 1), |
130 (hyp_subst_tac 1), |
131 (rtac (less_lift1c RS iffD2) 1), |
131 (rtac (less_lift1c RS iffD2) 1), |
132 (rtac refl_less 1) |
132 (rtac refl_less 1) |
133 ]); |
133 ]); |
134 |
134 |
135 val antisym_less_lift = prove_goal Lift1.thy |
135 qed_goal "antisym_less_lift" Lift1.thy |
136 "[|less_lift(p1,p2);less_lift(p2,p1)|] ==> p1=p2" |
136 "[|less_lift(p1,p2);less_lift(p2,p1)|] ==> p1=p2" |
137 (fn prems => |
137 (fn prems => |
138 [ |
138 [ |
139 (cut_facts_tac prems 1), |
139 (cut_facts_tac prems 1), |
140 (res_inst_tac [("p","p1")] liftE 1), |
140 (res_inst_tac [("p","p1")] liftE 1), |
157 (rtac antisym_less 1), |
157 (rtac antisym_less 1), |
158 (etac (less_lift1c RS iffD1) 1), |
158 (etac (less_lift1c RS iffD1) 1), |
159 (etac (less_lift1c RS iffD1) 1) |
159 (etac (less_lift1c RS iffD1) 1) |
160 ]); |
160 ]); |
161 |
161 |
162 val trans_less_lift = prove_goal Lift1.thy |
162 qed_goal "trans_less_lift" Lift1.thy |
163 "[|less_lift(p1,p2);less_lift(p2,p3)|] ==> less_lift(p1,p3)" |
163 "[|less_lift(p1,p2);less_lift(p2,p3)|] ==> less_lift(p1,p3)" |
164 (fn prems => |
164 (fn prems => |
165 [ |
165 [ |
166 (cut_facts_tac prems 1), |
166 (cut_facts_tac prems 1), |
167 (res_inst_tac [("p","p1")] liftE 1), |
167 (res_inst_tac [("p","p1")] liftE 1), |