69 val Ilift1 = prove_goalw Lift1.thy [Ilift_def,UU_lift_def] |
69 val Ilift1 = prove_goalw 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 (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 val Ilift2 = prove_goalw 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 (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 val less_lift1a = prove_goalw 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 (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 val less_lift1b = prove_goalw Lift1.thy [Iup_def,less_lift_def,UU_lift_def] |
99 "~less_lift(Iup(x),UU_lift)" |
99 "~less_lift(Iup(x),UU_lift)" |
102 (rtac notI 1), |
102 (rtac notI 1), |
103 (rtac iffD1 1), |
103 (rtac iffD1 1), |
104 (atac 2), |
104 (atac 2), |
105 (rtac (Abs_Lift_inverse RS ssubst) 1), |
105 (rtac (Abs_Lift_inverse RS ssubst) 1), |
106 (rtac (Abs_Lift_inverse RS ssubst) 1), |
106 (rtac (Abs_Lift_inverse RS ssubst) 1), |
107 (rtac (case_Inr RS ssubst) 1), |
107 (rtac (sum_case_Inr RS ssubst) 1), |
108 (rtac (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 val less_lift1c = prove_goalw 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), |
118 (rtac (case_Inr RS ssubst) 1), |
118 (rtac (sum_case_Inr RS ssubst) 1), |
119 (rtac (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 val refl_less_lift = prove_goal Lift1.thy "less_lift(p,p)" |