37 |
37 |
38 fun RANGE_WARN tacs = RANGE (map WARN tacs) |
38 fun RANGE_WARN tacs = RANGE (map WARN tacs) |
39 |
39 |
40 fun atomize_thm thm = |
40 fun atomize_thm thm = |
41 let |
41 let |
42 val thm' = Thm.freezeT (forall_intr_vars thm) (* TODO: is this proper Isar-technology? *) |
42 val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *) |
43 val thm'' = ObjectLogic.atomize (cprop_of thm') |
43 val thm'' = ObjectLogic.atomize (cprop_of thm') |
44 in |
44 in |
45 @{thm equal_elim_rule1} OF [thm'', thm'] |
45 @{thm equal_elim_rule1} OF [thm'', thm'] |
46 end |
46 end |
47 |
47 |
58 |
58 |
59 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
59 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
60 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
60 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
61 |
61 |
62 (* FIXME / TODO: test whether DETERM makes any runtime-difference *) |
62 (* FIXME / TODO: test whether DETERM makes any runtime-difference *) |
63 (* FIXME / TODO: reason: it might back-track over the two alternatives in FIRST' *) |
63 (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) |
64 fun quotient_tac ctxt = SOLVES' |
64 fun quotient_tac ctxt = SOLVES' |
65 (REPEAT_ALL_NEW (FIRST' |
65 (REPEAT_ALL_NEW (FIRST' |
66 [rtac @{thm identity_quotient}, |
66 [rtac @{thm identity_quotient}, |
67 resolve_tac (quotient_rules_get ctxt)])) |
67 resolve_tac (quotient_rules_get ctxt)])) |
68 |
68 |
82 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
82 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
83 |
83 |
84 fun get_match_inst thy pat trm = |
84 fun get_match_inst thy pat trm = |
85 let |
85 let |
86 val univ = Unify.matchers thy [(pat, trm)] |
86 val univ = Unify.matchers thy [(pat, trm)] |
87 val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) |
87 val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) |
88 val tenv = Vartab.dest (Envir.term_env env) |
88 val tenv = Vartab.dest (Envir.term_env env) |
89 val tyenv = Vartab.dest (Envir.type_env env) |
89 val tyenv = Vartab.dest (Envir.type_env env) |
90 in |
90 in |
91 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
91 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
92 end |
92 end |
93 |
93 |
94 (* calculates the instantiations for te lemmas *) |
94 (* calculates the instantiations for the lemmas *) |
95 (* ball_reg_eqv_range and bex_reg_eqv_range *) |
95 (* ball_reg_eqv_range and bex_reg_eqv_range *) |
96 fun calculate_inst ctxt ball_bex_thm redex R1 R2 = |
96 fun calculate_inst ctxt ball_bex_thm redex R1 R2 = |
97 let |
97 let |
98 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
98 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
99 val thy = ProofContext.theory_of ctxt |
99 val thy = ProofContext.theory_of ctxt |
100 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
100 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
104 val thm'' = Drule.instantiate inst2 thm' (* raises THM *) |
104 val thm'' = Drule.instantiate inst2 thm' (* raises THM *) |
105 in |
105 in |
106 SOME thm'' |
106 SOME thm'' |
107 end |
107 end |
108 handle _ => NONE |
108 handle _ => NONE |
109 (* FIXME/TODO: !!!CLEVER CODE!!! *) |
109 (* FIXME/TODO: !!!CLEVER CODE!!! *) |
110 (* FIXME/TODO: What is the place where the exception is raised, *) |
110 (* FIXME/TODO: What are the places where the exceptions are raised, *) |
111 (* FIXME/TODO: and which exception is it? *) |
111 (* FIXME/TODO: and which exception is it? *) |
112 (* FIXME/TODO: Can one not find out from the types of R1 or R2, *) |
112 (* FIXME/TODO: Can one not find out from the types of R1, R2 and redex *) |
113 (* FIXME/TODO: or from their form, when NONE should be returned? *) |
113 (* FIXME/TODO: when NONE should be returned? *) |
114 |
114 |
115 fun ball_bex_range_simproc ss redex = |
115 fun ball_bex_range_simproc ss redex = |
116 let |
116 let |
117 val ctxt = Simplifier.the_context ss |
117 val ctxt = Simplifier.the_context ss |
118 in |
118 in |
229 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
229 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
230 | dest_fun_type _ = error "dest_fun_type" |
230 | dest_fun_type _ = error "dest_fun_type" |
231 |
231 |
232 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
232 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
233 |
233 |
234 |
234 (* We apply apply_rsp only in case if the type needs lifting. *) |
235 (* We apply apply_rsp only in case if the type needs lifting. *) |
235 (* This is the case if the type of the data in the Quot_True *) |
236 (* This is the case if the type of the data in the Quot_True *) |
236 (* assumption is different from the corresponding type in the goal. *) |
237 (* assumption is different from the corresponding type in the goal *) |
|
238 val apply_rsp_tac = |
237 val apply_rsp_tac = |
239 Subgoal.FOCUS (fn {concl, asms, context,...} => |
238 Subgoal.FOCUS (fn {concl, asms, context,...} => |
240 let |
239 let |
241 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
240 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
242 val qt_asm = find_qt_asm (map term_of asms) |
241 val qt_asm = find_qt_asm (map term_of asms) |
267 val thm = Drule.instantiate' |
266 val thm = Drule.instantiate' |
268 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
267 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
269 in |
268 in |
270 rtac thm THEN' quotient_tac ctxt |
269 rtac thm THEN' quotient_tac ctxt |
271 end |
270 end |
272 (* TODO: Are they raised by instantiate'? *) |
271 (* TODO: Are they raised by instantiate'? *) |
273 (* TODO: Again, can one specify more concretely when no_tac should be returned? *) |
272 (* TODO: Again, can one specify more concretely *) |
|
273 (* TODO: in terms of R when no_tac should be returned? *) |
274 handle THM _ => K no_tac |
274 handle THM _ => K no_tac |
275 | TYPE _ => K no_tac |
275 | TYPE _ => K no_tac |
276 | TERM _ => K no_tac |
276 | TERM _ => K no_tac |
277 |
|
278 |
277 |
279 fun rep_abs_rsp_tac ctxt = |
278 fun rep_abs_rsp_tac ctxt = |
280 SUBGOAL (fn (goal, i) => |
279 SUBGOAL (fn (goal, i) => |
281 case (bare_concl goal) of |
280 case (bare_concl goal) of |
282 (rel $ _ $ (rep $ (abs $ _))) => |
281 (rel $ _ $ (rep $ (abs $ _))) => |
562 |
561 |
563 (**********************************************) |
562 (**********************************************) |
564 (* The General Shape of the Lifting Procedure *) |
563 (* The General Shape of the Lifting Procedure *) |
565 (**********************************************) |
564 (**********************************************) |
566 |
565 |
567 (* - A is the original raw theorem *) |
566 (* - A is the original raw theorem *) |
568 (* - B is the regularized theorem *) |
567 (* - B is the regularized theorem *) |
569 (* - C is the rep/abs injected version of B *) |
568 (* - C is the rep/abs injected version of B *) |
570 (* - D is the lifted theorem *) |
569 (* - D is the lifted theorem *) |
571 (* *) |
570 (* *) |
572 (* - 1st prem is the regularization step *) |
571 (* - 1st prem is the regularization step *) |
573 (* - 2nd prem is the rep/abs injection step *) |
572 (* - 2nd prem is the rep/abs injection step *) |
574 (* - 3rd prem is the cleaning part *) |
573 (* - 3rd prem is the cleaning part *) |
575 (* *) |
574 (* *) |
576 (* the Quot_True premise in 2 records the lifted theorem *) |
575 (* the Quot_True premise in 2nd records the lifted theorem *) |
577 |
576 |
578 val lifting_procedure_thm = |
577 val lifting_procedure_thm = |
579 @{lemma "[|A; |
578 @{lemma "[|A; |
580 A --> B; |
579 A --> B; |
581 Quot_True D ==> B = C; |
580 Quot_True D ==> B = C; |