0
+ − 1 theory QuotMain
6
+ − 2 imports QuotScript QuotList Prove
264
+ − 3 uses ("quotient_info.ML")
+ − 4 ("quotient.ML")
277
+ − 5 ("quotient_def.ML")
0
+ − 6 begin
+ − 7
+ − 8 locale QUOT_TYPE =
+ − 9 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ − 10 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ − 11 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ − 12 assumes equiv: "EQUIV R"
+ − 13 and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ − 14 and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ − 15 and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ − 16 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
15
+ − 17 begin
0
+ − 18
+ − 19 definition
200
+ − 20 ABS::"'a \<Rightarrow> 'b"
+ − 21 where
0
+ − 22 "ABS x \<equiv> Abs (R x)"
+ − 23
+ − 24 definition
200
+ − 25 REP::"'b \<Rightarrow> 'a"
+ − 26 where
0
+ − 27 "REP a = Eps (Rep a)"
+ − 28
15
+ − 29 lemma lem9:
0
+ − 30 shows "R (Eps (R x)) = R x"
+ − 31 proof -
+ − 32 have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
+ − 33 then have "R x (Eps (R x))" by (rule someI)
15
+ − 34 then show "R (Eps (R x)) = R x"
0
+ − 35 using equiv unfolding EQUIV_def by simp
+ − 36 qed
+ − 37
+ − 38 theorem thm10:
24
+ − 39 shows "ABS (REP a) \<equiv> a"
+ − 40 apply (rule eq_reflection)
+ − 41 unfolding ABS_def REP_def
0
+ − 42 proof -
15
+ − 43 from rep_prop
0
+ − 44 obtain x where eq: "Rep a = R x" by auto
+ − 45 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+ − 46 also have "\<dots> = Abs (R x)" using lem9 by simp
+ − 47 also have "\<dots> = Abs (Rep a)" using eq by simp
+ − 48 also have "\<dots> = a" using rep_inverse by simp
+ − 49 finally
+ − 50 show "Abs (R (Eps (Rep a))) = a" by simp
+ − 51 qed
+ − 52
15
+ − 53 lemma REP_refl:
0
+ − 54 shows "R (REP a) (REP a)"
+ − 55 unfolding REP_def
+ − 56 by (simp add: equiv[simplified EQUIV_def])
+ − 57
+ − 58 lemma lem7:
22
+ − 59 shows "(R x = R y) = (Abs (R x) = Abs (R y))"
0
+ − 60 apply(rule iffI)
+ − 61 apply(simp)
+ − 62 apply(drule rep_inject[THEN iffD2])
+ − 63 apply(simp add: abs_inverse)
+ − 64 done
15
+ − 65
0
+ − 66 theorem thm11:
+ − 67 shows "R r r' = (ABS r = ABS r')"
+ − 68 unfolding ABS_def
+ − 69 by (simp only: equiv[simplified EQUIV_def] lem7)
+ − 70
4
+ − 71
2
+ − 72 lemma REP_ABS_rsp:
4
+ − 73 shows "R f (REP (ABS g)) = R f g"
+ − 74 and "R (REP (ABS g)) f = R g f"
23
+ − 75 by (simp_all add: thm10 thm11)
4
+ − 76
0
+ − 77 lemma QUOTIENT:
+ − 78 "QUOTIENT R ABS REP"
+ − 79 apply(unfold QUOTIENT_def)
+ − 80 apply(simp add: thm10)
+ − 81 apply(simp add: REP_refl)
+ − 82 apply(subst thm11[symmetric])
+ − 83 apply(simp add: equiv[simplified EQUIV_def])
+ − 84 done
+ − 85
21
+ − 86 lemma R_trans:
49
+ − 87 assumes ab: "R a b"
+ − 88 and bc: "R b c"
22
+ − 89 shows "R a c"
21
+ − 90 proof -
+ − 91 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ − 92 moreover have ab: "R a b" by fact
+ − 93 moreover have bc: "R b c" by fact
22
+ − 94 ultimately show "R a c" unfolding TRANS_def by blast
21
+ − 95 qed
+ − 96
+ − 97 lemma R_sym:
49
+ − 98 assumes ab: "R a b"
22
+ − 99 shows "R b a"
21
+ − 100 proof -
+ − 101 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
22
+ − 102 then show "R b a" using ab unfolding SYM_def by blast
21
+ − 103 qed
+ − 104
49
+ − 105 lemma R_trans2:
+ − 106 assumes ac: "R a c"
22
+ − 107 and bd: "R b d"
21
+ − 108 shows "R a b = R c d"
200
+ − 109 using ac bd
+ − 110 by (blast intro: R_trans R_sym)
21
+ − 111
+ − 112 lemma REPS_same:
25
+ − 113 shows "R (REP a) (REP b) \<equiv> (a = b)"
38
+ − 114 proof -
+ − 115 have "R (REP a) (REP b) = (a = b)"
+ − 116 proof
+ − 117 assume as: "R (REP a) (REP b)"
+ − 118 from rep_prop
+ − 119 obtain x y
+ − 120 where eqs: "Rep a = R x" "Rep b = R y" by blast
+ − 121 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+ − 122 then have "R x (Eps (R y))" using lem9 by simp
+ − 123 then have "R (Eps (R y)) x" using R_sym by blast
+ − 124 then have "R y x" using lem9 by simp
+ − 125 then have "R x y" using R_sym by blast
+ − 126 then have "ABS x = ABS y" using thm11 by simp
+ − 127 then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+ − 128 then show "a = b" using rep_inverse by simp
+ − 129 next
+ − 130 assume ab: "a = b"
+ − 131 have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ − 132 then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+ − 133 qed
+ − 134 then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
21
+ − 135 qed
+ − 136
0
+ − 137 end
+ − 138
127
b054cf6bd179
the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
0
+ − 140 section {* type definition for the quotient type *}
+ − 141
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142 (* the auxiliary data for the quotient types *)
264
+ − 143 use "quotient_info.ML"
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
185
+ − 145 declare [[map list = (map, LIST_REL)]]
+ − 146 declare [[map * = (prod_fun, prod_rel)]]
+ − 147 declare [[map "fun" = (fun_map, FUN_REL)]]
+ − 148
+ − 149 ML {* maps_lookup @{theory} "List.list" *}
+ − 150 ML {* maps_lookup @{theory} "*" *}
+ − 151 ML {* maps_lookup @{theory} "fun" *}
174
+ − 152
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154 (* definition of the quotient types *)
277
+ − 155 (* FIXME: should be called quotient_typ.ML *)
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 156 use "quotient.ML"
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 157
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 158
277
+ − 159 (* lifting of constants *)
+ − 160 use "quotient_def.ML"
+ − 161
+ − 162
218
+ − 163 text {* FIXME: auxiliary function *}
193
+ − 164 ML {*
14
+ − 165 val no_vars = Thm.rule_attribute (fn context => fn th =>
+ − 166 let
+ − 167 val ctxt = Variable.set_body false (Context.proof_of context);
+ − 168 val ((_, [th']), _) = Variable.import true [th] ctxt;
+ − 169 in th' end);
+ − 170 *}
+ − 171
139
+ − 172 section {* ATOMIZE *}
+ − 173
+ − 174 text {*
+ − 175 Unabs_def converts a definition given as
+ − 176
+ − 177 c \<equiv> %x. %y. f x y
+ − 178
+ − 179 to a theorem of the form
+ − 180
+ − 181 c x y \<equiv> f x y
+ − 182
+ − 183 This function is needed to rewrite the right-hand
+ − 184 side to the left-hand side.
+ − 185 *}
+ − 186
+ − 187 ML {*
+ − 188 fun unabs_def ctxt def =
+ − 189 let
+ − 190 val (lhs, rhs) = Thm.dest_equals (cprop_of def)
+ − 191 val xs = strip_abs_vars (term_of rhs)
+ − 192 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
+ − 193
+ − 194 val thy = ProofContext.theory_of ctxt'
+ − 195 val cxs = map (cterm_of thy o Free) xs
+ − 196 val new_lhs = Drule.list_comb (lhs, cxs)
+ − 197
+ − 198 fun get_conv [] = Conv.rewr_conv def
+ − 199 | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
+ − 200 in
+ − 201 get_conv xs new_lhs |>
+ − 202 singleton (ProofContext.export ctxt' ctxt)
+ − 203 end
+ − 204 *}
+ − 205
+ − 206 lemma atomize_eqv[atomize]:
+ − 207 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+ − 208 proof
+ − 209 assume "A \<equiv> B"
+ − 210 then show "Trueprop A \<equiv> Trueprop B" by unfold
+ − 211 next
+ − 212 assume *: "Trueprop A \<equiv> Trueprop B"
+ − 213 have "A = B"
+ − 214 proof (cases A)
+ − 215 case True
+ − 216 have "A" by fact
+ − 217 then show "A = B" using * by simp
+ − 218 next
+ − 219 case False
+ − 220 have "\<not>A" by fact
+ − 221 then show "A = B" using * by auto
+ − 222 qed
+ − 223 then show "A \<equiv> B" by (rule eq_reflection)
+ − 224 qed
+ − 225
+ − 226 ML {*
+ − 227 fun atomize_thm thm =
+ − 228 let
221
+ − 229 val thm' = Thm.freezeT (forall_intr_vars thm)
139
+ − 230 val thm'' = ObjectLogic.atomize (cprop_of thm')
+ − 231 in
221
+ − 232 @{thm Pure.equal_elim_rule1} OF [thm'', thm']
139
+ − 233 end
+ − 234 *}
+ − 235
140
+ − 236 ML {* atomize_thm @{thm list.induct} *}
139
+ − 237
+ − 238 section {* REGULARIZE *}
282
+ − 239 (*
+ − 240
+ − 241 Regularizing a theorem means:
+ − 242 - Quantifiers over a type that needs lifting are replaced by
+ − 243 bounded quantifiers, for example:
+ − 244 \<forall>x. P \<Longrightarrow> \<forall>x\<in>(Respects R). P
+ − 245 - Abstractions over a type that needs lifting are replaced
+ − 246 by bounded abstactions:
+ − 247 \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+ − 248
+ − 249 - Equalities over the type being lifted are replaced by
+ − 250 appropriate relations:
+ − 251 A = B \<Longrightarrow> A \<approx> B
+ − 252 Example with more complicated types of A, B:
+ − 253 A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
+ − 254
+ − 255 Regularizing is done in 3 phases:
+ − 256 - First a regularized term is created
+ − 257 - Next we prove that the original theorem implies the new one
+ − 258 - Finally using MP we get the new theorem.
+ − 259
+ − 260 To prove that the old theorem implies the new one, we first
+ − 261 atomize it and then try:
+ − 262 - Reflexivity of the relation
+ − 263 - Assumption
+ − 264 - Elimnating quantifiers on both sides of toplevel implication
+ − 265 - Simplifying implications on both sides of toplevel implication
+ − 266 - Ball (Respects ?E) ?P = All ?P
+ − 267 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+ − 268
+ − 269 *)
139
+ − 270
+ − 271 text {* tyRel takes a type and builds a relation that a quantifier over this
+ − 272 type needs to respect. *}
+ − 273 ML {*
257
+ − 274 fun matches (ty1, ty2) =
+ − 275 Type.raw_instance (ty1, Logic.varifyT ty2);
+ − 276
139
+ − 277 fun tyRel ty rty rel lthy =
257
+ − 278 if matches (rty, ty)
139
+ − 279 then rel
+ − 280 else (case ty of
+ − 281 Type (s, tys) =>
+ − 282 let
+ − 283 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
+ − 284 val ty_out = ty --> ty --> @{typ bool};
+ − 285 val tys_out = tys_rel ---> ty_out;
+ − 286 in
+ − 287 (case (maps_lookup (ProofContext.theory_of lthy) s) of
+ − 288 SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
+ − 289 | NONE => HOLogic.eq_const ty
+ − 290 )
+ − 291 end
+ − 292 | _ => HOLogic.eq_const ty)
+ − 293 *}
+ − 294
+ − 295 definition
+ − 296 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ − 297 where
+ − 298 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+ − 299 (* TODO: Consider defining it with an "if"; sth like:
+ − 300 Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+ − 301 *)
+ − 302
+ − 303 ML {*
+ − 304 fun needs_lift (rty as Type (rty_s, _)) ty =
+ − 305 case ty of
+ − 306 Type (s, tys) =>
+ − 307 (s = rty_s) orelse (exists (needs_lift rty) tys)
+ − 308 | _ => false
+ − 309
+ − 310 *}
+ − 311
+ − 312 ML {*
+ − 313 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
+ − 314 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
+ − 315 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
+ − 316 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
+ − 317 *}
+ − 318
+ − 319 (* applies f to the subterm of an abstractions, otherwise to the given term *)
+ − 320 ML {*
+ − 321 fun apply_subt f trm =
+ − 322 case trm of
145
+ − 323 Abs (x, T, t) =>
+ − 324 let
+ − 325 val (x', t') = Term.dest_abs (x, T, t)
+ − 326 in
+ − 327 Term.absfree (x', T, f t')
+ − 328 end
139
+ − 329 | _ => f trm
+ − 330 *}
+ − 331
+ − 332 (* FIXME: if there are more than one quotient, then you have to look up the relation *)
+ − 333 ML {*
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 334 fun my_reg lthy rel rty trm =
139
+ − 335 case trm of
+ − 336 Abs (x, T, t) =>
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 337 if (needs_lift rty T) then
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 338 let
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 339 val rrel = tyRel T rty rel lthy
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 340 in
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 341 (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 342 end
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 343 else
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 344 Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 345 | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 346 let
139
+ − 347 val ty1 = domain_type ty
+ − 348 val ty2 = domain_type ty1
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 349 val rrel = tyRel T rty rel lthy
139
+ − 350 in
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 351 if (needs_lift rty T) then
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 352 (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 353 else
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 354 Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
139
+ − 355 end
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 356 | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 357 let
139
+ − 358 val ty1 = domain_type ty
+ − 359 val ty2 = domain_type ty1
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 360 val rrel = tyRel T rty rel lthy
139
+ − 361 in
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 362 if (needs_lift rty T) then
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 363 (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 364 else
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 365 Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
139
+ − 366 end
251
+ − 367 | Const (@{const_name "op ="}, ty) $ t =>
+ − 368 if needs_lift rty (fastype_of t) then
+ − 369 (tyRel (fastype_of t) rty rel lthy) $ t
+ − 370 else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 371 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
139
+ − 372 | _ => trm
+ − 373 *}
+ − 374
141
+ − 375 text {* Assumes that the given theorem is atomized *}
140
+ − 376 ML {*
+ − 377 fun build_regularize_goal thm rty rel lthy =
+ − 378 Logic.mk_implies
+ − 379 ((prop_of thm),
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 380 (my_reg lthy rel rty (prop_of thm)))
140
+ − 381 *}
+ − 382
277
+ − 383 lemma universal_twice:
+ − 384 "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 385 by auto
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 386
277
+ − 387 lemma implication_twice:
+ − 388 "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 389 by auto
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 390
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 391 (*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 392 by auto*)
251
+ − 393
187
+ − 394 ML {*
251
+ − 395 fun regularize thm rty rel rel_eqv rel_refl lthy =
187
+ − 396 let
+ − 397 val g = build_regularize_goal thm rty rel lthy;
+ − 398 fun tac ctxt =
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 399 (ObjectLogic.full_atomize_tac) THEN'
251
+ − 400 REPEAT_ALL_NEW (FIRST' [
+ − 401 rtac rel_refl,
+ − 402 atac,
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 403 rtac @{thm universal_twice},
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 404 (rtac @{thm impI} THEN' atac),
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 405 rtac @{thm implication_twice},
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 406 (*rtac @{thm equality_twice},*)
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 407 EqSubst.eqsubst_tac ctxt [0]
187
+ − 408 [(@{thm equiv_res_forall} OF [rel_eqv]),
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 409 (@{thm equiv_res_exists} OF [rel_eqv])],
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 410 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 411 (rtac @{thm RIGHT_RES_FORALL_REGULAR})
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 412 ]);
187
+ − 413 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
+ − 414 in
+ − 415 cthm OF [thm]
+ − 416 end
+ − 417 *}
+ − 418
140
+ − 419 section {* RepAbs injection *}
139
+ − 420
161
+ − 421 (* Needed to have a meta-equality *)
+ − 422 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
+ − 423 by (simp add: id_def)
+ − 424
139
+ − 425 ML {*
218
+ − 426 fun old_exchange_ty rty qty ty =
+ − 427 if ty = rty
+ − 428 then qty
+ − 429 else
+ − 430 (case ty of
+ − 431 Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
+ − 432 | _ => ty
+ − 433 )
+ − 434 *}
+ − 435
277
+ − 436
218
+ − 437 ML {*
+ − 438 fun old_get_fun flag rty qty lthy ty =
+ − 439 get_fun flag [(qty, rty)] lthy ty
+ − 440
+ − 441 fun old_make_const_def nconst_bname otrm mx rty qty lthy =
277
+ − 442 make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy
218
+ − 443 *}
+ − 444
235
+ − 445 text {* Does the same as 'subst' in a given prop or theorem *}
+ − 446 ML {*
+ − 447 fun eqsubst_prop ctxt thms t =
+ − 448 let
+ − 449 val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
+ − 450 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+ − 451 NONE => error "eqsubst_prop"
+ − 452 | SOME th => cprem_of th 1
+ − 453 in term_of a' end
+ − 454 *}
+ − 455
+ − 456 ML {*
+ − 457 fun repeat_eqsubst_prop ctxt thms t =
+ − 458 repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
+ − 459 handle _ => t
+ − 460 *}
+ − 461
+ − 462
+ − 463 ML {*
+ − 464 fun eqsubst_thm ctxt thms thm =
+ − 465 let
+ − 466 val goalstate = Goal.init (Thm.cprop_of thm)
+ − 467 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+ − 468 NONE => error "eqsubst_thm"
+ − 469 | SOME th => cprem_of th 1
+ − 470 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+ − 471 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
+ − 472 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
+ − 473 in
+ − 474 @{thm Pure.equal_elim_rule1} OF [rt,thm]
+ − 475 end
+ − 476 *}
+ − 477
+ − 478 ML {*
+ − 479 fun repeat_eqsubst_thm ctxt thms thm =
+ − 480 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
+ − 481 handle _ => thm
+ − 482 *}
+ − 483
218
+ − 484 ML {*
140
+ − 485 fun build_repabs_term lthy thm constructors rty qty =
139
+ − 486 let
+ − 487 fun mk_rep tm =
+ − 488 let
218
+ − 489 val ty = old_exchange_ty rty qty (fastype_of tm)
+ − 490 in fst (old_get_fun repF rty qty lthy ty) $ tm end
139
+ − 491
+ − 492 fun mk_abs tm =
+ − 493 let
218
+ − 494 val ty = old_exchange_ty rty qty (fastype_of tm) in
+ − 495 fst (old_get_fun absF rty qty lthy ty) $ tm end
139
+ − 496
+ − 497 fun is_constructor (Const (x, _)) = member (op =) constructors x
+ − 498 | is_constructor _ = false;
+ − 499
+ − 500 fun build_aux lthy tm =
+ − 501 case tm of
+ − 502 Abs (a as (_, vty, _)) =>
+ − 503 let
+ − 504 val (vs, t) = Term.dest_abs a;
+ − 505 val v = Free(vs, vty);
+ − 506 val t' = lambda v (build_aux lthy t)
+ − 507 in
+ − 508 if (not (needs_lift rty (fastype_of tm))) then t'
+ − 509 else mk_rep (mk_abs (
+ − 510 if not (needs_lift rty vty) then t'
+ − 511 else
+ − 512 let
+ − 513 val v' = mk_rep (mk_abs v);
+ − 514 val t1 = Envir.beta_norm (t' $ v')
+ − 515 in
+ − 516 lambda v t1
+ − 517 end
+ − 518 ))
+ − 519 end
+ − 520 | x =>
+ − 521 let
+ − 522 val (opp, tms0) = Term.strip_comb tm
+ − 523 val tms = map (build_aux lthy) tms0
+ − 524 val ty = fastype_of tm
+ − 525 in
+ − 526 if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
+ − 527 then (list_comb (opp, (hd tms0) :: (tl tms)))
+ − 528 else if (is_constructor opp andalso needs_lift rty ty) then
+ − 529 mk_rep (mk_abs (list_comb (opp,tms)))
+ − 530 else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
149
+ − 531 mk_rep(mk_abs(list_comb(opp,tms)))
139
+ − 532 else if tms = [] then opp
+ − 533 else list_comb(opp, tms)
+ − 534 end
+ − 535 in
235
+ − 536 repeat_eqsubst_prop lthy @{thms id_def_sym}
161
+ − 537 (build_aux lthy (Thm.prop_of thm))
139
+ − 538 end
+ − 539 *}
+ − 540
141
+ − 541 text {* Assumes that it is given a regularized theorem *}
139
+ − 542 ML {*
140
+ − 543 fun build_repabs_goal ctxt thm cons rty qty =
+ − 544 Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
139
+ − 545 *}
+ − 546
187
+ − 547 ML {*
+ − 548 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+ − 549 let
+ − 550 val pat = Drule.strip_imp_concl (cprop_of thm)
+ − 551 val insts = Thm.match (pat, concl)
+ − 552 in
+ − 553 rtac (Drule.instantiate insts thm) 1
152
53277fbb2dba
Simplified the proof with some tactic... Still hangs sometimes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 554 end
187
+ − 555 handle _ => no_tac
+ − 556 )
+ − 557 *}
+ − 558
+ − 559
+ − 560
+ − 561 ML {*
+ − 562 fun quotient_tac quot_thm =
+ − 563 REPEAT_ALL_NEW (FIRST' [
+ − 564 rtac @{thm FUN_QUOTIENT},
+ − 565 rtac quot_thm,
+ − 566 rtac @{thm IDENTITY_QUOTIENT}
+ − 567 ])
+ − 568 *}
+ − 569
+ − 570 ML {*
+ − 571 fun LAMBDA_RES_TAC ctxt i st =
+ − 572 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ − 573 (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
+ − 574 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 575 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 576 | _ => fn _ => no_tac) i st
+ − 577 *}
+ − 578
+ − 579 ML {*
+ − 580 fun WEAK_LAMBDA_RES_TAC ctxt i st =
+ − 581 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ − 582 (_ $ (_ $ _$(Abs(_,_,_)))) =>
+ − 583 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 584 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 585 | (_ $ (_ $ (Abs(_,_,_))$_)) =>
+ − 586 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 587 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 588 | _ => fn _ => no_tac) i st
+ − 589 *}
+ − 590
206
+ − 591 ML {*
+ − 592 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
+ − 593 let
+ − 594 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
+ − 595 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+ − 596 val insts = Thm.match (pat, concl)
+ − 597 in
+ − 598 if needs_lift rty (type_of f) then
+ − 599 rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+ − 600 else no_tac
+ − 601 end
+ − 602 handle _ => no_tac)
+ − 603 *}
187
+ − 604
+ − 605 ML {*
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 606 val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 607 let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 608 val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 609 in
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 610 ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 611 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 612 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 613 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 614 end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 615 handle _ => no_tac
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 616 )
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 617 *}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 618
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 619 ML {*
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 620 val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 621 let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 622 val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 623 in
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 624 ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 625 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 626 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 627 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 628 end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 629 handle _ => no_tac
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 630 )
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 631 *}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 632
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 633 ML {*
206
+ − 634 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
187
+ − 635 (FIRST' [
259
+ − 636 (* rtac @{thm FUN_QUOTIENT},
187
+ − 637 rtac quot_thm,
259
+ − 638 rtac @{thm IDENTITY_QUOTIENT},*)
187
+ − 639 rtac trans_thm,
+ − 640 LAMBDA_RES_TAC ctxt,
+ − 641 res_forall_rsp_tac ctxt,
+ − 642 res_exists_rsp_tac ctxt,
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 643 FIRST' (map rtac rsp_thms),
187
+ − 644 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+ − 645 rtac refl,
206
+ − 646 (* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
+ − 647 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+ − 648 Cong_Tac.cong_tac @{thm cong},
+ − 649 rtac @{thm ext},
187
+ − 650 rtac reflex_thm,
+ − 651 atac,
+ − 652 (
+ − 653 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+ − 654 THEN_ALL_NEW (fn _ => no_tac)
+ − 655 ),
+ − 656 WEAK_LAMBDA_RES_TAC ctxt
+ − 657 ])
+ − 658 *}
+ − 659
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 660 ML {*
210
+ − 661 fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 662 let
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 663 val rt = build_repabs_term lthy thm constructors rty qty;
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 664 val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 665 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
206
+ − 666 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 667 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 668 in
210
+ − 669 @{thm Pure.equal_elim_rule1} OF [cthm, thm]
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 670 end
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 671 *}
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 672
187
+ − 673 section {* Cleaning the goal *}
+ − 674
236
+ − 675 lemma prod_fun_id: "prod_fun id id = id"
+ − 676 apply (simp add: prod_fun_def)
+ − 677 done
+ − 678 lemma map_id: "map id x = x"
+ − 679 apply (induct x)
+ − 680 apply (simp_all add: map.simps)
+ − 681 done
+ − 682
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 683 text {* expects atomized definition *}
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 684 ML {*
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 685 fun add_lower_defs_aux ctxt thm =
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 686 let
209
+ − 687 val e1 = @{thm fun_cong} OF [thm];
+ − 688 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;
+ − 689 val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;
236
+ − 690 val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 691 in
236
+ − 692 thm :: (add_lower_defs_aux ctxt h)
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 693 end
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 694 handle _ => [thm]
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 695 *}
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 696
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 697 ML {*
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 698 fun add_lower_defs ctxt defs =
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 699 let
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 700 val defs_pre_sym = map symmetric defs
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 701 val defs_atom = map atomize_thm defs_pre_sym
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 702 val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 703 in
214
+ − 704 map Thm.varifyT defs_all
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 705 end
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 706 *}
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 707
191
+ − 708 ML {*
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 709 fun findabs_all rty tm =
191
+ − 710 case tm of
+ − 711 Abs(_, T, b) =>
+ − 712 let
+ − 713 val b' = subst_bound ((Free ("x", T)), b);
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 714 val tys = findabs_all rty b'
191
+ − 715 val ty = fastype_of tm
+ − 716 in if needs_lift rty ty then (ty :: tys) else tys
+ − 717 end
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 718 | f $ a => (findabs_all rty f) @ (findabs_all rty a)
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 719 | _ => [];
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 720 fun findabs rty tm = distinct (op =) (findabs_all rty tm)
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 721 *}
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 722
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 723
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 724 ML {*
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 725 fun findaps_all rty tm =
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 726 case tm of
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 727 Abs(_, T, b) =>
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 728 findaps_all rty (subst_bound ((Free ("x", T)), b))
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 729 | (f $ a) => (findaps_all rty f @ findaps_all rty a)
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 730 | Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else [])
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 731 | _ => [];
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 732 fun findaps rty tm = distinct (op =) (findaps_all rty tm)
191
+ − 733 *}
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 734
197
+ − 735 ML {*
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 736 fun make_simp_prs_thm lthy quot_thm thm typ =
197
+ − 737 let
+ − 738 val (_, [lty, rty]) = dest_Type typ;
+ − 739 val thy = ProofContext.theory_of lthy;
+ − 740 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
+ − 741 val inst = [SOME lcty, NONE, SOME rcty];
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 742 val lpi = Drule.instantiate' inst [] thm;
197
+ − 743 val tac =
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 744 (compose_tac (false, lpi, 2)) THEN_ALL_NEW
197
+ − 745 (quotient_tac quot_thm);
259
+ − 746 val gc = Drule.strip_imp_concl (cprop_of lpi);
+ − 747 val t = Goal.prove_internal [] gc (fn _ => tac 1)
197
+ − 748 in
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 749 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
197
+ − 750 end
+ − 751 *}
+ − 752
+ − 753 ML {*
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 754 fun findallex_all rty qty tm =
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 755 case tm of
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 756 Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 757 let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 758 val (tya, tye) = findallex_all rty qty s
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 759 in if needs_lift rty T then
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 760 ((T :: tya), tye)
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 761 else (tya, tye) end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 762 | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 763 let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 764 val (tya, tye) = findallex_all rty qty s
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 765 in if needs_lift rty T then
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 766 (tya, (T :: tye))
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 767 else (tya, tye) end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 768 | Abs(_, T, b) =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 769 findallex_all rty qty (subst_bound ((Free ("x", T)), b))
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 770 | f $ a =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 771 let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 772 val (a1, e1) = findallex_all rty qty f;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 773 val (a2, e2) = findallex_all rty qty a;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 774 in (a1 @ a2, e1 @ e2) end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 775 | _ => ([], []);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 776 *}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 777 ML {*
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 778 fun findallex rty qty tm =
197
+ − 779 let
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 780 val (a, e) = findallex_all rty qty tm;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 781 val (ad, ed) = (map domain_type a, map domain_type e);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 782 val (au, eu) = (distinct (op =) ad, distinct (op =) ed)
197
+ − 783 in
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 784 (map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu)
197
+ − 785 end
+ − 786 *}
+ − 787
198
+ − 788 ML {*
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 789 fun make_allex_prs_thm lthy quot_thm thm typ =
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 790 let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 791 val (_, [lty, rty]) = dest_Type typ;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 792 val thy = ProofContext.theory_of lthy;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 793 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 794 val inst = [NONE, SOME lcty];
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 795 val lpi = Drule.instantiate' inst [] thm;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 796 val tac =
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 797 (compose_tac (false, lpi, 1)) THEN_ALL_NEW
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 798 (quotient_tac quot_thm);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 799 val gc = Drule.strip_imp_concl (cprop_of lpi);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 800 val t = Goal.prove_internal [] gc (fn _ => tac 1)
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 801 val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 802 val t_sym = @{thm "HOL.sym"} OF [t_noid];
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 803 val t_eq = @{thm "eq_reflection"} OF [t_sym]
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 804 in
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 805 t_eq
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 806 end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 807 *}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 808
269
+ − 809 ML {*
+ − 810 fun applic_prs lthy rty qty absrep ty =
+ − 811 let
+ − 812 fun absty ty =
+ − 813 old_exchange_ty rty qty ty
+ − 814 fun mk_rep tm =
+ − 815 let
+ − 816 val ty = old_exchange_ty rty qty (fastype_of tm)
+ − 817 in fst (old_get_fun repF rty qty lthy ty) $ tm end;
+ − 818 fun mk_abs tm =
+ − 819 let
+ − 820 val ty = old_exchange_ty rty qty (fastype_of tm) in
+ − 821 fst (old_get_fun absF rty qty lthy ty) $ tm end;
+ − 822 val (l, ltl) = Term.strip_type ty;
+ − 823 val nl = map absty l;
+ − 824 val vs = map (fn _ => "x") l;
+ − 825 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+ − 826 val args = map Free (vfs ~~ nl);
+ − 827 val lhs = list_comb((Free (fname, nl ---> ltl)), args);
+ − 828 val rargs = map mk_rep args;
+ − 829 val f = Free (fname, nl ---> ltl);
+ − 830 val rhs = mk_abs (list_comb((mk_rep f), rargs));
+ − 831 val eq = Logic.mk_equals (rhs, lhs);
+ − 832 val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+ − 833 val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps});
+ − 834 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+ − 835 val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
+ − 836 in
+ − 837 singleton (ProofContext.export lthy' lthy) t_id
+ − 838 end
+ − 839 *}
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 840
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 841 ML {*
239
+ − 842 fun lookup_quot_data lthy qty =
+ − 843 let
257
+ − 844 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+ − 845 val rty = Logic.unvarifyT (#rtyp quotdata)
239
+ − 846 val rel = #rel quotdata
+ − 847 val rel_eqv = #equiv_thm quotdata
+ − 848 val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]
+ − 849 val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]
+ − 850 in
+ − 851 (rty, rel, rel_refl, rel_eqv)
+ − 852 end
+ − 853 *}
+ − 854
+ − 855 ML {*
+ − 856 fun lookup_quot_thms lthy qty_name =
+ − 857 let
+ − 858 val thy = ProofContext.theory_of lthy;
+ − 859 val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
+ − 860 val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
269
+ − 861 val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
239
+ − 862 val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
+ − 863 in
269
+ − 864 (trans2, reps_same, absrep, quot)
239
+ − 865 end
+ − 866 *}
+ − 867
+ − 868 ML {*
+ − 869 fun lookup_quot_consts defs =
+ − 870 let
+ − 871 fun dest_term (a $ b) = (a, b);
+ − 872 val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
+ − 873 in
+ − 874 map (fst o dest_Const o snd o dest_term) def_terms
+ − 875 end
+ − 876 *}
+ − 877
275
+ − 878
239
+ − 879 ML {*
+ − 880 fun lift_thm lthy qty qty_name rsp_thms defs t = let
+ − 881 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
269
+ − 882 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
239
+ − 883 val consts = lookup_quot_consts defs;
198
+ − 884 val t_a = atomize_thm t;
251
+ − 885 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
210
+ − 886 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 887 val (alls, exs) = findallex rty qty (prop_of t_a);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 888 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 889 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 890 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
198
+ − 891 val abs = findabs rty (prop_of t_a);
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 892 val aps = findaps rty (prop_of t_a);
269
+ − 893 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 894 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
259
+ − 895 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
239
+ − 896 val defs_sym = add_lower_defs lthy defs;
259
+ − 897 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
+ − 898 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;
+ − 899 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
198
+ − 900 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+ − 901 in
+ − 902 ObjectLogic.rulify t_r
187
+ − 903 end
198
+ − 904 *}
+ − 905
273
+ − 906 ML {*
+ − 907 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
+ − 908 let
+ − 909 val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
+ − 910 val (_, lthy2) = note (name, lifted_thm) lthy;
+ − 911 in
+ − 912 lthy2
+ − 913 end;
+ − 914 *}
+ − 915
239
+ − 916
198
+ − 917 end
239
+ − 918