54 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
54 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
55 |
55 |
56 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
56 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
57 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
57 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
58 |
58 |
59 fun solve_equiv_assm ctxt thm = |
|
60 case Seq.pull (equiv_tac ctxt 1 thm) of |
|
61 SOME (t, _) => t |
|
62 | _ => error "solve_equiv_assm failed." |
|
63 |
|
64 |
|
65 |
|
66 fun prep_trm thy (x, (T, t)) = |
59 fun prep_trm thy (x, (T, t)) = |
67 (cterm_of thy (Var (x, T)), cterm_of thy t) |
60 (cterm_of thy (Var (x, T)), cterm_of thy t) |
68 |
61 |
69 fun prep_ty thy (x, (S, ty)) = |
62 fun prep_ty thy (x, (S, ty)) = |
70 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
63 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
71 |
64 |
72 fun matching_prs thy pat trm = |
65 fun get_match_inst thy pat trm = |
73 let |
66 let |
74 val univ = Unify.matchers thy [(pat, trm)] |
67 val univ = Unify.matchers thy [(pat, trm)] |
75 val SOME (env, _) = Seq.pull univ |
68 val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) |
76 val tenv = Vartab.dest (Envir.term_env env) |
69 val tenv = Vartab.dest (Envir.term_env env) |
77 val tyenv = Vartab.dest (Envir.type_env env) |
70 val tyenv = Vartab.dest (Envir.type_env env) |
78 in |
71 in |
79 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
72 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
80 end |
73 end |
85 let |
78 let |
86 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
79 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
87 val thy = ProofContext.theory_of ctxt |
80 val thy = ProofContext.theory_of ctxt |
88 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
81 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
89 val trm_inst1 = map (SOME o cterm_of thy) [R2, R1] |
82 val trm_inst1 = map (SOME o cterm_of thy) [R2, R1] |
90 val thm' = Drule.instantiate' typ_inst1 trm_inst1 ball_bex_thm |
83 val thm' = Drule.instantiate' typ_inst1 trm_inst1 ball_bex_thm (* raises TYPE *) |
91 val inst2 = matching_prs thy (get_lhs thm') redex |
84 val inst2 = get_match_inst thy (get_lhs thm') redex |
92 val thm'' = Drule.instantiate inst2 thm' |
85 val thm'' = Drule.instantiate inst2 thm' (* raises THM *) |
93 in |
86 in |
94 SOME thm'' |
87 SOME thm'' |
95 end |
88 end |
96 handle _ => NONE |
89 handle _ => NONE |
97 (* FIXME/TODO: !!!CLEVER CODE!!! *) |
90 (* FIXME/TODO: !!!CLEVER CODE!!! *) |
103 |
96 |
104 fun ball_bex_range_simproc ss redex = |
97 fun ball_bex_range_simproc ss redex = |
105 let |
98 let |
106 val ctxt = Simplifier.the_context ss |
99 val ctxt = Simplifier.the_context ss |
107 in |
100 in |
108 case redex of |
101 case redex of |
109 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
102 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
110 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
103 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
111 calculate_instance ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 |
104 calculate_instance ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 |
112 |
105 |
113 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
106 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
151 (* finally jump back to 1 *) |
144 (* finally jump back to 1 *) |
152 |
145 |
153 fun regularize_tac ctxt = |
146 fun regularize_tac ctxt = |
154 let |
147 let |
155 val thy = ProofContext.theory_of ctxt |
148 val thy = ProofContext.theory_of ctxt |
156 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
149 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
157 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
150 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
158 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
151 val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) |
159 val simpset = (mk_minimal_ss ctxt) |
152 val simpset = (mk_minimal_ss ctxt) |
160 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
153 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
161 addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver |
154 addsimprocs [simproc] |
|
155 addSolver equiv_solver addSolver quotient_solver |
162 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
156 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
163 in |
157 in |
164 simp_tac simpset THEN' |
158 simp_tac simpset THEN' |
165 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
159 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
166 resolve_tac @{thms ball_reg_right bex_reg_left}, |
160 resolve_tac @{thms ball_reg_right bex_reg_left}, |