author | wenzelm |
Wed, 16 Dec 2015 16:31:36 +0100 | |
changeset 61853 | fb7756087101 |
parent 61144 | 5e94dfead1c2 |
child 62913 | 13252110a6fe |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/Quotient/quotient_tacs.ML |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk and Christian Urban |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
|
35788 | 4 |
Tactics for solving goal arising from lifting theorems to quotient |
5 |
types. |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
signature QUOTIENT_TACS = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
sig |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
val regularize_tac: Proof.context -> int -> tactic |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
val injection_tac: Proof.context -> int -> tactic |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
val all_injection_tac: Proof.context -> int -> tactic |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
val clean_tac: Proof.context -> int -> tactic |
41444 | 14 |
|
38859
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
15 |
val descend_procedure_tac: Proof.context -> thm list -> int -> tactic |
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
16 |
val descend_tac: Proof.context -> thm list -> int -> tactic |
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
17 |
val partiality_descend_procedure_tac: Proof.context -> thm list -> int -> tactic |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
18 |
val partiality_descend_tac: Proof.context -> thm list -> int -> tactic |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
19 |
|
41444 | 20 |
|
38859
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
21 |
val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic |
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
22 |
val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic |
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
23 |
|
38625
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
24 |
val lifted: Proof.context -> typ list -> thm list -> thm -> thm |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
val lifted_attrib: attribute |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
end; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
structure Quotient_Tacs: QUOTIENT_TACS = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
struct |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
(** various helper fuctions **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
(* Since HOL_basic_ss is too "big" for us, we *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
(* need to set up our own minimal simpset. *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
35 |
fun mk_minimal_simpset ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
36 |
empty_simpset ctxt |
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45350
diff
changeset
|
37 |
|> Simplifier.set_subgoaler asm_simp_tac |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45350
diff
changeset
|
38 |
|> Simplifier.set_mksimps (mksimps []) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
(* composition of two theorems, used in maps *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
fun OF1 thm1 thm2 = thm2 RS thm1 |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
43 |
fun atomize_thm ctxt thm = |
41444 | 44 |
let |
45 |
val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *) |
|
59582 | 46 |
val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm') |
41444 | 47 |
in |
48 |
@{thm equal_elim_rule1} OF [thm'', thm'] |
|
49 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
52 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
(*** Regularize Tactic ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
(** solvers for equivp and quotient assumptions **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
fun equiv_tac ctxt = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
58 |
REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
60 |
val equiv_solver = mk_solver "Equivalence goal solver" equiv_tac |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
fun quotient_tac ctxt = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
(REPEAT_ALL_NEW (FIRST' |
60752 | 64 |
[resolve_tac ctxt @{thms identity_quotient3}, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
65 |
resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems quot_thm}))])) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
67 |
val quotient_solver = mk_solver "Quotient goal solver" quotient_tac |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
68 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
fun solve_quotient_assm ctxt thm = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
case Seq.pull (quotient_tac ctxt 1 thm) of |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
SOME (t, _) => t |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
| _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing." |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
fun get_match_inst thy pat trm = |
41444 | 76 |
let |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
57960
diff
changeset
|
77 |
val univ = Unify.matchers (Context.Theory thy) [(pat, trm)] |
41444 | 78 |
val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *) |
79 |
val tenv = Vartab.dest (Envir.term_env env) |
|
80 |
val tyenv = Vartab.dest (Envir.type_env env) |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59638
diff
changeset
|
81 |
fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty) |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59638
diff
changeset
|
82 |
fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t) |
41444 | 83 |
in |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59638
diff
changeset
|
84 |
(map prep_ty tyenv, map prep_trm tenv) |
41444 | 85 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
86 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
87 |
(* Calculates the instantiations for the lemmas: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
88 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
89 |
ball_reg_eqv_range and bex_reg_eqv_range |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
90 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
91 |
Since the left-hand-side contains a non-pattern '?P (f ?x)' |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
92 |
we rely on unification/instantiation to check whether the |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
93 |
theorem applies and return NONE if it doesn't. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
94 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
95 |
fun calculate_inst ctxt ball_bex_thm redex R1 R2 = |
41444 | 96 |
let |
42361 | 97 |
val thy = Proof_Context.theory_of ctxt |
41444 | 98 |
fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
59638 | 99 |
val ty_inst = map (SOME o Thm.ctyp_of ctxt) [domain_type (fastype_of R2)] |
100 |
val trm_inst = map (SOME o Thm.cterm_of ctxt) [R2, R1] |
|
41444 | 101 |
in |
60801 | 102 |
(case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of |
41444 | 103 |
NONE => NONE |
104 |
| SOME thm' => |
|
61144 | 105 |
(case try (get_match_inst thy (get_lhs thm')) (Thm.term_of redex) of |
41444 | 106 |
NONE => NONE |
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42361
diff
changeset
|
107 |
| SOME inst2 => try (Drule.instantiate_normalize inst2) thm')) |
41444 | 108 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
109 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
110 |
fun ball_bex_range_simproc ctxt redex = |
61144 | 111 |
(case Thm.term_of redex of |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
112 |
(Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
55945 | 113 |
(Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) => |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
114 |
calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
116 |
| (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
55945 | 117 |
(Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) => |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
118 |
calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
119 |
|
61144 | 120 |
| _ => NONE) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
122 |
(* Regularize works as follows: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
123 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
124 |
0. preliminary simplification step according to |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
125 |
ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
126 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
127 |
1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
128 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
129 |
2. monos |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
130 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
131 |
3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
132 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
133 |
4. then rel-equalities, which need to be instantiated with 'eq_imp_rel' |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
to avoid loops |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
136 |
5. then simplification like 0 |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
137 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
138 |
finally jump back to 1 |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
139 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
|
37493
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36945
diff
changeset
|
141 |
fun reflp_get ctxt = |
59585 | 142 |
map_filter (fn th => if Thm.no_prems th then SOME (OF1 @{thm equivp_reflp} th) else NONE |
57960 | 143 |
handle THM _ => NONE) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv})) |
37493
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36945
diff
changeset
|
144 |
|
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36945
diff
changeset
|
145 |
val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)} |
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36945
diff
changeset
|
146 |
|
57960 | 147 |
fun eq_imp_rel_get ctxt = |
148 |
map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv})) |
|
37493
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36945
diff
changeset
|
149 |
|
61144 | 150 |
val regularize_simproc = |
151 |
Simplifier.make_simproc @{context} "regularize" |
|
152 |
{lhss = [@{term "Ball (Respects (R1 ===> R2)) P"}, @{term "Bex (Respects (R1 ===> R2)) P"}], |
|
153 |
proc = K ball_bex_range_simproc, |
|
154 |
identifier = []}; |
|
155 |
||
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
fun regularize_tac ctxt = |
41444 | 157 |
let |
42361 | 158 |
val thy = Proof_Context.theory_of ctxt |
41444 | 159 |
val simpset = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
160 |
mk_minimal_simpset ctxt |
41444 | 161 |
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
61144 | 162 |
addsimprocs [regularize_simproc] |
41444 | 163 |
addSolver equiv_solver addSolver quotient_solver |
164 |
val eq_eqvs = eq_imp_rel_get ctxt |
|
165 |
in |
|
166 |
simp_tac simpset THEN' |
|
44285
dd203341fd2b
Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43934
diff
changeset
|
167 |
TRY o REPEAT_ALL_NEW (CHANGED o FIRST' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
168 |
[resolve_tac ctxt @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
169 |
resolve_tac ctxt (Inductive.get_monos ctxt), |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
170 |
resolve_tac ctxt @{thms ball_all_comm bex_ex_comm}, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
171 |
resolve_tac ctxt eq_eqvs, |
41444 | 172 |
simp_tac simpset]) |
173 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
174 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
175 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
176 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
177 |
(*** Injection Tactic ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
178 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
179 |
(* Looks for Quot_True assumptions, and in case its parameter |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
180 |
is an application, it returns the function and the argument. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
181 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
182 |
fun find_qt_asm asms = |
41444 | 183 |
let |
184 |
fun find_fun trm = |
|
185 |
(case trm of |
|
186 |
(Const (@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true |
|
187 |
| _ => false) |
|
188 |
in |
|
189 |
(case find_first find_fun asms of |
|
190 |
SOME (_ $ (_ $ (f $ a))) => SOME (f, a) |
|
191 |
| _ => NONE) |
|
192 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
193 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
194 |
fun quot_true_simple_conv ctxt fnctn ctrm = |
59582 | 195 |
(case Thm.term_of ctrm of |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
196 |
(Const (@{const_name Quot_True}, _) $ x) => |
41444 | 197 |
let |
198 |
val fx = fnctn x; |
|
59638 | 199 |
val cx = Thm.cterm_of ctxt x; |
200 |
val cfx = Thm.cterm_of ctxt fx; |
|
201 |
val cxt = Thm.ctyp_of ctxt (fastype_of x); |
|
202 |
val cfxt = Thm.ctyp_of ctxt (fastype_of fx); |
|
60801 | 203 |
val thm = Thm.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp} |
41444 | 204 |
in |
205 |
Conv.rewr_conv thm ctrm |
|
59582 | 206 |
end) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
207 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
208 |
fun quot_true_conv ctxt fnctn ctrm = |
59582 | 209 |
(case Thm.term_of ctrm of |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
210 |
(Const (@{const_name Quot_True}, _) $ _) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
211 |
quot_true_simple_conv ctxt fnctn ctrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
212 |
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
213 |
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
41444 | 214 |
| _ => Conv.all_conv ctrm) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
215 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
216 |
fun quot_true_tac ctxt fnctn = |
41444 | 217 |
CONVERSION |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
218 |
((Conv.params_conv ~1 (fn ctxt => |
41444 | 219 |
(Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
220 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
221 |
fun dest_comb (f $ a) = (f, a) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
222 |
fun dest_bcomb ((_ $ l) $ r) = (l, r) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
223 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
224 |
fun unlam t = |
41444 | 225 |
(case t of |
226 |
Abs a => snd (Term.dest_abs a) |
|
227 |
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
228 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
229 |
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
230 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
231 |
(* We apply apply_rsp only in case if the type needs lifting. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
232 |
This is the case if the type of the data in the Quot_True |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
233 |
assumption is different from the corresponding type in the goal. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
234 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
235 |
val apply_rsp_tac = |
59638 | 236 |
Subgoal.FOCUS (fn {concl, asms, context = ctxt,...} => |
41444 | 237 |
let |
59582 | 238 |
val bare_concl = HOLogic.dest_Trueprop (Thm.term_of concl) |
239 |
val qt_asm = find_qt_asm (map Thm.term_of asms) |
|
41444 | 240 |
in |
241 |
case (bare_concl, qt_asm) of |
|
242 |
(R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => |
|
243 |
if fastype_of qt_fun = fastype_of f |
|
244 |
then no_tac |
|
245 |
else |
|
246 |
let |
|
247 |
val ty_x = fastype_of x |
|
248 |
val ty_b = fastype_of qt_arg |
|
249 |
val ty_f = range_type (fastype_of f) |
|
59638 | 250 |
val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_x, ty_b, ty_f] |
251 |
val t_inst = map (SOME o Thm.cterm_of ctxt) [R2, f, g, x, y]; |
|
60801 | 252 |
val inst_thm = Thm.instantiate' ty_inst |
47308 | 253 |
([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3} |
41444 | 254 |
in |
60752 | 255 |
(resolve_tac ctxt [inst_thm] THEN' SOLVED' (quotient_tac ctxt)) 1 |
41444 | 256 |
end |
257 |
| _ => no_tac |
|
258 |
end) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
259 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
260 |
(* Instantiates and applies 'equals_rsp'. Since the theorem is |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
261 |
complex we rely on instantiation to tell us if it applies |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
262 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
263 |
fun equals_rsp_tac R ctxt = |
59638 | 264 |
case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *) (* FIXME fragile *) |
265 |
SOME ctm => |
|
266 |
let |
|
267 |
val ty = domain_type (fastype_of R) |
|
268 |
in |
|
60801 | 269 |
case try (Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)] |
59638 | 270 |
[SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of |
60752 | 271 |
SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt |
59638 | 272 |
| NONE => K no_tac |
273 |
end |
|
274 |
| _ => K no_tac |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
275 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
276 |
fun rep_abs_rsp_tac ctxt = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
277 |
SUBGOAL (fn (goal, i) => |
41444 | 278 |
(case try bare_concl goal of |
43934
2108763f298d
Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43596
diff
changeset
|
279 |
SOME (rel $ _ $ (rep $ (abs $ _))) => |
2108763f298d
Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43596
diff
changeset
|
280 |
(let |
40840 | 281 |
val (ty_a, ty_b) = dest_funT (fastype_of abs); |
59638 | 282 |
val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b]; |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
283 |
in |
59638 | 284 |
case try (map (SOME o Thm.cterm_of ctxt)) [rel, abs, rep] of |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
285 |
SOME t_inst => |
60801 | 286 |
(case try (Thm.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of |
60752 | 287 |
SOME inst_thm => (resolve_tac ctxt [inst_thm] THEN' quotient_tac ctxt) i |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
288 |
| NONE => no_tac) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
289 |
| NONE => no_tac |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
290 |
end |
43934
2108763f298d
Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43596
diff
changeset
|
291 |
handle TERM _ => no_tac) |
41444 | 292 |
| _ => no_tac)) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
293 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
294 |
|
38718 | 295 |
(* Injection means to prove that the regularized theorem implies |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
296 |
the abs/rep injected one. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
297 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
298 |
The deterministic part: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
299 |
- remove lambdas from both sides |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
300 |
- prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp |
55945 | 301 |
- prove Ball/Bex relations using rel_funI |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
302 |
- reflexivity of equality |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
303 |
- prove equality of relations using equals_rsp |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
304 |
- use user-supplied RSP theorems |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
305 |
- solve 'relation of relations' goals using quot_rel_rsp |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
306 |
- remove rep_abs from the right side |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
307 |
(Lambdas under respects may have left us some assumptions) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
308 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
309 |
Then in order: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
310 |
- split applications of lifted type (apply_rsp) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
311 |
- split applications of non-lifted type (cong_tac) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
312 |
- apply extentionality |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
313 |
- assumption |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
314 |
- reflexivity of the relation |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
315 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
316 |
fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) => |
41444 | 317 |
(case bare_concl goal of |
318 |
(* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) |
|
55945 | 319 |
(Const (@{const_name rel_fun}, _) $ _ $ _) $ (Abs _) $ (Abs _) |
60752 | 320 |
=> resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
321 |
|
41444 | 322 |
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) |
323 |
| (Const (@{const_name HOL.eq},_) $ |
|
324 |
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
325 |
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
|
60752 | 326 |
=> resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all} |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
327 |
|
41444 | 328 |
(* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *) |
55945 | 329 |
| (Const (@{const_name rel_fun}, _) $ _ $ _) $ |
41444 | 330 |
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
331 |
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
60752 | 332 |
=> resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
333 |
|
41444 | 334 |
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *) |
335 |
| Const (@{const_name HOL.eq},_) $ |
|
336 |
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
337 |
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
60752 | 338 |
=> resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex} |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
339 |
|
41444 | 340 |
(* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) |
55945 | 341 |
| (Const (@{const_name rel_fun}, _) $ _ $ _) $ |
41444 | 342 |
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
343 |
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
60752 | 344 |
=> resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
345 |
|
55945 | 346 |
| (Const (@{const_name rel_fun}, _) $ _ $ _) $ |
41444 | 347 |
(Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) |
60752 | 348 |
=> resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
349 |
|
41444 | 350 |
| (_ $ |
351 |
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
352 |
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
|
60752 | 353 |
=> resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
354 |
|
41444 | 355 |
| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) => |
60752 | 356 |
(resolve_tac ctxt @{thms refl} ORELSE' |
41444 | 357 |
(equals_rsp_tac R ctxt THEN' RANGE [ |
358 |
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
359 |
|
41444 | 360 |
(* reflexivity of operators arising from Cong_tac *) |
60752 | 361 |
| Const (@{const_name HOL.eq},_) $ _ $ _ => resolve_tac ctxt @{thms refl} |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
362 |
|
41444 | 363 |
(* respectfulness of constants; in particular of a simple relation *) |
55945 | 364 |
| _ $ (Const _) $ (Const _) (* rel_fun, list_rel, etc but not equality *) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
365 |
=> resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems quot_respect})) |
57960 | 366 |
THEN_ALL_NEW quotient_tac ctxt |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
367 |
|
41444 | 368 |
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *) |
369 |
(* observe map_fun *) |
|
370 |
| _ $ _ $ _ |
|
60752 | 371 |
=> (resolve_tac ctxt @{thms quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) |
41444 | 372 |
ORELSE' rep_abs_rsp_tac ctxt |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
373 |
|
41444 | 374 |
| _ => K no_tac) i) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
375 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
376 |
fun injection_step_tac ctxt rel_refl = |
41444 | 377 |
FIRST' [ |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
378 |
injection_match_tac ctxt, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
379 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
380 |
(* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
381 |
apply_rsp_tac ctxt THEN' |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
382 |
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
383 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
384 |
(* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
385 |
(* merge with previous tactic *) |
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset
|
386 |
Cong_Tac.cong_tac ctxt @{thm cong} THEN' |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
387 |
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
388 |
|
44285
dd203341fd2b
Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43934
diff
changeset
|
389 |
(* resolving with R x y assumptions *) |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
390 |
assume_tac ctxt, |
44285
dd203341fd2b
Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43934
diff
changeset
|
391 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
392 |
(* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) |
60752 | 393 |
resolve_tac ctxt @{thms ext} THEN' quot_true_tac ctxt unlam, |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
394 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
395 |
(* reflexivity of the basic relations *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
396 |
(* R ... ... *) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
397 |
resolve_tac ctxt rel_refl] |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
398 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
399 |
fun injection_tac ctxt = |
41444 | 400 |
let |
401 |
val rel_refl = reflp_get ctxt |
|
402 |
in |
|
403 |
injection_step_tac ctxt rel_refl |
|
404 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
405 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
406 |
fun all_injection_tac ctxt = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
407 |
REPEAT_ALL_NEW (injection_tac ctxt) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
408 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
409 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
410 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
411 |
(*** Cleaning of the Theorem ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
412 |
|
40602 | 413 |
(* expands all map_funs, except in front of the (bound) variables listed in xs *) |
414 |
fun map_fun_simple_conv xs ctrm = |
|
59582 | 415 |
(case Thm.term_of ctrm of |
40602 | 416 |
((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) => |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
417 |
if member (op=) xs h |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
418 |
then Conv.all_conv ctrm |
40602 | 419 |
else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm |
41444 | 420 |
| _ => Conv.all_conv ctrm) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
421 |
|
40602 | 422 |
fun map_fun_conv xs ctxt ctrm = |
59582 | 423 |
(case Thm.term_of ctrm of |
41444 | 424 |
_ $ _ => |
425 |
(Conv.comb_conv (map_fun_conv xs ctxt) then_conv |
|
426 |
map_fun_simple_conv xs) ctrm |
|
59582 | 427 |
| Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv (Thm.term_of x :: xs) ctxt) ctxt ctrm |
41444 | 428 |
| _ => Conv.all_conv ctrm) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
429 |
|
40602 | 430 |
fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
431 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
432 |
(* custom matching functions *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
433 |
fun mk_abs u i t = |
41444 | 434 |
if incr_boundvars i u aconv t then Bound i |
435 |
else |
|
436 |
case t of |
|
437 |
t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2 |
|
438 |
| Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
|
439 |
| Bound j => if i = j then error "make_inst" else t |
|
440 |
| _ => t |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
441 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
442 |
fun make_inst lhs t = |
41444 | 443 |
let |
444 |
val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
|
445 |
val _ $ (Abs (_, _, (_ $ g))) = t; |
|
446 |
in |
|
447 |
(f, Abs ("x", T, mk_abs u 0 g)) |
|
448 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
449 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
450 |
fun make_inst_id lhs t = |
41444 | 451 |
let |
452 |
val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
|
453 |
val _ $ (Abs (_, _, g)) = t; |
|
454 |
in |
|
455 |
(f, Abs ("x", T, mk_abs u 0 g)) |
|
456 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
457 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
458 |
(* Simplifies a redex using the 'lambda_prs' theorem. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
459 |
First instantiates the types and known subterms. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
460 |
Then solves the quotient assumptions to get Rep2 and Abs1 |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
461 |
Finally instantiates the function f using make_inst |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
462 |
If Rep2 is an identity then the pattern is simpler and |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
463 |
make_inst_id is used |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
464 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
465 |
fun lambda_prs_simple_conv ctxt ctrm = |
59582 | 466 |
(case Thm.term_of ctrm of |
40602 | 467 |
(Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) => |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
468 |
let |
40840 | 469 |
val (ty_b, ty_a) = dest_funT (fastype_of r1) |
470 |
val (ty_c, ty_d) = dest_funT (fastype_of a2) |
|
59638 | 471 |
val tyinst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b, ty_c, ty_d] |
472 |
val tinst = [NONE, NONE, SOME (Thm.cterm_of ctxt r1), NONE, SOME (Thm.cterm_of ctxt a2)] |
|
60801 | 473 |
val thm1 = Thm.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
474 |
val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
475 |
val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2 |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
476 |
val (insp, inst) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
477 |
if ty_c = ty_d |
59582 | 478 |
then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm) |
479 |
else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm) |
|
480 |
val thm4 = |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59638
diff
changeset
|
481 |
Drule.instantiate_normalize ([], [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3 |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
482 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
483 |
Conv.rewr_conv thm4 ctrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
484 |
end |
41444 | 485 |
| _ => Conv.all_conv ctrm) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
486 |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36850
diff
changeset
|
487 |
fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
488 |
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
489 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
490 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
491 |
(* Cleaning consists of: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
492 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
493 |
1. unfolding of ---> in front of everything, except |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
494 |
bound variables (this prevents lambda_prs from |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
495 |
becoming stuck) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
496 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
497 |
2. simplification with lambda_prs |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
498 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
499 |
3. simplification with: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
500 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
501 |
- Quotient_abs_rep Quotient_rel_rep |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
502 |
babs_prs all_prs ex_prs ex1_prs |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
503 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
504 |
- id_simps and preservation lemmas and |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
505 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
506 |
- symmetric versions of the definitions |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
507 |
(that is definitions of quotient constants |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
508 |
are folded) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
509 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
510 |
4. test for refl |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
511 |
*) |
57960 | 512 |
fun clean_tac ctxt = |
41444 | 513 |
let |
57960 | 514 |
val thy = Proof_Context.theory_of ctxt |
45350
257d0b179f0d
more use of global operations (see 98ec8b51af9c)
Christian Urban <urbanc@in.tum.de>
parents:
45279
diff
changeset
|
515 |
val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts_global thy) |
57960 | 516 |
val prs = rev (Named_Theorems.get ctxt @{named_theorems quot_preserve}) |
517 |
val ids = rev (Named_Theorems.get ctxt @{named_theorems id_simps}) |
|
41444 | 518 |
val thms = |
47308 | 519 |
@{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
520 |
|
57960 | 521 |
val simpset = (mk_minimal_simpset ctxt) addsimps thms addSolver quotient_solver |
41444 | 522 |
in |
41451 | 523 |
EVERY' [ |
57960 | 524 |
map_fun_tac ctxt, |
525 |
lambda_prs_tac ctxt, |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
526 |
simp_tac simpset, |
60752 | 527 |
TRY o resolve_tac ctxt [refl]] |
41444 | 528 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
529 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
530 |
|
38718 | 531 |
(* Tactic for Generalising Free Variables in a Goal *) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
532 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
533 |
fun inst_spec ctrm = |
60801 | 534 |
Thm.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec} |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
535 |
|
60752 | 536 |
fun inst_spec_tac ctxt ctrms = |
537 |
EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
538 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
539 |
fun all_list xs trm = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
540 |
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
541 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
542 |
fun apply_under_Trueprop f = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
543 |
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
544 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
545 |
fun gen_frees_tac ctxt = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
546 |
SUBGOAL (fn (concl, i) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
547 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
548 |
val vrs = Term.add_frees concl [] |
59638 | 549 |
val cvrs = map (Thm.cterm_of ctxt o Free) vrs |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
550 |
val concl' = apply_under_Trueprop (all_list vrs) concl |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
551 |
val goal = Logic.mk_implies (concl', concl) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
552 |
val rule = Goal.prove ctxt [] [] goal |
60752 | 553 |
(K (EVERY1 [inst_spec_tac ctxt (rev cvrs), assume_tac ctxt])) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
554 |
in |
60752 | 555 |
resolve_tac ctxt [rule] i |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
556 |
end) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
557 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
558 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
559 |
(** The General Shape of the Lifting Procedure **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
560 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
561 |
(* - A is the original raw theorem |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
562 |
- B is the regularized theorem |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
563 |
- C is the rep/abs injected version of B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
564 |
- D is the lifted theorem |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
565 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
566 |
- 1st prem is the regularization step |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
567 |
- 2nd prem is the rep/abs injection step |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
568 |
- 3rd prem is the cleaning part |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
569 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
570 |
the Quot_True premise in 2nd records the lifted theorem |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
571 |
*) |
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
572 |
val procedure_thm = |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
573 |
@{lemma "[|A; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
574 |
A --> B; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
575 |
Quot_True D ==> B = C; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
576 |
C = D|] ==> D" |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
577 |
by (simp add: Quot_True_def)} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
578 |
|
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
579 |
(* in case of partial equivalence relations, this form of the |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
580 |
procedure theorem results in solvable proof obligations |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
581 |
*) |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
582 |
val partiality_procedure_thm = |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
583 |
@{lemma "[|B; |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
584 |
Quot_True D ==> B = C; |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
585 |
C = D|] ==> D" |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
586 |
by (simp add: Quot_True_def)} |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
587 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
588 |
fun lift_match_error ctxt msg rtrm qtrm = |
41444 | 589 |
let |
590 |
val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
591 |
val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
592 |
val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, |
|
593 |
"", "does not match with original theorem", rtrm_str] |
|
594 |
in |
|
595 |
error msg |
|
596 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
597 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
598 |
fun procedure_inst ctxt rtrm qtrm = |
41444 | 599 |
let |
600 |
val rtrm' = HOLogic.dest_Trueprop rtrm |
|
601 |
val qtrm' = HOLogic.dest_Trueprop qtrm |
|
41451 | 602 |
val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm') |
603 |
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm |
|
604 |
val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
|
605 |
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm |
|
41444 | 606 |
in |
60801 | 607 |
Thm.instantiate' [] |
59638 | 608 |
[SOME (Thm.cterm_of ctxt rtrm'), |
609 |
SOME (Thm.cterm_of ctxt reg_goal), |
|
41444 | 610 |
NONE, |
59638 | 611 |
SOME (Thm.cterm_of ctxt inj_goal)] procedure_thm |
41444 | 612 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
613 |
|
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
614 |
|
38860
749d09f52fde
quotient package: added a list of pre-simplification rules for Ball, Bex and mem
Christian Urban <urbanc@in.tum.de>
parents:
38859
diff
changeset
|
615 |
(* Since we use Ball and Bex during the lifting and descending, |
38862
2795499a20bd
Quotient Package: dont unfold mem_def, use rsp and prs instead
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38860
diff
changeset
|
616 |
we cannot deal with lemmas containing them, unless we unfold |
2795499a20bd
Quotient Package: dont unfold mem_def, use rsp and prs instead
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38860
diff
changeset
|
617 |
them by default. *) |
38860
749d09f52fde
quotient package: added a list of pre-simplification rules for Ball, Bex and mem
Christian Urban <urbanc@in.tum.de>
parents:
38859
diff
changeset
|
618 |
|
38862
2795499a20bd
Quotient Package: dont unfold mem_def, use rsp and prs instead
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38860
diff
changeset
|
619 |
val default_unfolds = @{thms Ball_def Bex_def} |
38860
749d09f52fde
quotient package: added a list of pre-simplification rules for Ball, Bex and mem
Christian Urban <urbanc@in.tum.de>
parents:
38859
diff
changeset
|
620 |
|
749d09f52fde
quotient package: added a list of pre-simplification rules for Ball, Bex and mem
Christian Urban <urbanc@in.tum.de>
parents:
38859
diff
changeset
|
621 |
|
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
622 |
(** descending as tactic **) |
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
623 |
|
38859
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
624 |
fun descend_procedure_tac ctxt simps = |
41444 | 625 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
626 |
val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds) |
41444 | 627 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
628 |
full_simp_tac simpset |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
629 |
THEN' Object_Logic.full_atomize_tac ctxt |
41444 | 630 |
THEN' gen_frees_tac ctxt |
631 |
THEN' SUBGOAL (fn (goal, i) => |
|
632 |
let |
|
45279 | 633 |
val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt) |
41451 | 634 |
val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal |
41444 | 635 |
val rule = procedure_inst ctxt rtrm goal |
636 |
in |
|
60752 | 637 |
resolve_tac ctxt [rule] i |
41444 | 638 |
end) |
639 |
end |
|
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
640 |
|
38859
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
641 |
fun descend_tac ctxt simps = |
41444 | 642 |
let |
643 |
val mk_tac_raw = |
|
644 |
descend_procedure_tac ctxt simps |
|
645 |
THEN' RANGE |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
646 |
[Object_Logic.rulify_tac ctxt THEN' (K all_tac), |
41444 | 647 |
regularize_tac ctxt, |
648 |
all_injection_tac ctxt, |
|
649 |
clean_tac ctxt] |
|
650 |
in |
|
651 |
Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw |
|
652 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
653 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
654 |
|
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
655 |
(** descending for partial equivalence relations **) |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
656 |
|
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
657 |
fun partiality_procedure_inst ctxt rtrm qtrm = |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
658 |
let |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
659 |
val rtrm' = HOLogic.dest_Trueprop rtrm |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
660 |
val qtrm' = HOLogic.dest_Trueprop qtrm |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
661 |
val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm') |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
662 |
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
663 |
val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
664 |
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
665 |
in |
60801 | 666 |
Thm.instantiate' [] |
59638 | 667 |
[SOME (Thm.cterm_of ctxt reg_goal), |
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
668 |
NONE, |
59638 | 669 |
SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm |
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
670 |
end |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
671 |
|
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
672 |
|
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
673 |
fun partiality_descend_procedure_tac ctxt simps = |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
674 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
675 |
val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds) |
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
676 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
677 |
full_simp_tac simpset |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
678 |
THEN' Object_Logic.full_atomize_tac ctxt |
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
679 |
THEN' gen_frees_tac ctxt |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
680 |
THEN' SUBGOAL (fn (goal, i) => |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
681 |
let |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
682 |
val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt) |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
683 |
val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
684 |
val rule = partiality_procedure_inst ctxt rtrm goal |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
685 |
in |
60752 | 686 |
resolve_tac ctxt [rule] i |
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
687 |
end) |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
688 |
end |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
689 |
|
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
690 |
fun partiality_descend_tac ctxt simps = |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
691 |
let |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
692 |
val mk_tac_raw = |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
693 |
partiality_descend_procedure_tac ctxt simps |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
694 |
THEN' RANGE |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
695 |
[Object_Logic.rulify_tac ctxt THEN' (K all_tac), |
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
696 |
all_injection_tac ctxt, |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
697 |
clean_tac ctxt] |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
698 |
in |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
699 |
Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
700 |
end |
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
701 |
|
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
702 |
|
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45625
diff
changeset
|
703 |
|
38625
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
704 |
(** lifting as a tactic **) |
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
705 |
|
38718 | 706 |
|
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
707 |
(* the tactic leaves three subgoals to be proved *) |
38859
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
708 |
fun lift_procedure_tac ctxt simps rthm = |
41444 | 709 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
710 |
val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds) |
41444 | 711 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
712 |
full_simp_tac simpset |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
713 |
THEN' Object_Logic.full_atomize_tac ctxt |
41444 | 714 |
THEN' gen_frees_tac ctxt |
715 |
THEN' SUBGOAL (fn (goal, i) => |
|
716 |
let |
|
717 |
(* full_atomize_tac contracts eta redexes, |
|
718 |
so we do it also in the original theorem *) |
|
719 |
val rthm' = |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47308
diff
changeset
|
720 |
rthm |> full_simplify simpset |
41444 | 721 |
|> Drule.eta_contraction_rule |
722 |
|> Thm.forall_intr_frees |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
723 |
|> atomize_thm ctxt |
38717
a365f1fc5081
quotient package: deal correctly with frees in lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38694
diff
changeset
|
724 |
|
59582 | 725 |
val rule = procedure_inst ctxt (Thm.prop_of rthm') goal |
41444 | 726 |
in |
60752 | 727 |
(resolve_tac ctxt [rule] THEN' resolve_tac ctxt [rthm']) i |
41444 | 728 |
end) |
729 |
end |
|
38625
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
730 |
|
41444 | 731 |
fun lift_single_tac ctxt simps rthm = |
38859
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
732 |
lift_procedure_tac ctxt simps rthm |
38625
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
733 |
THEN' RANGE |
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
734 |
[ regularize_tac ctxt, |
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
735 |
all_injection_tac ctxt, |
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
736 |
clean_tac ctxt ] |
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
737 |
|
38859
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
738 |
fun lift_tac ctxt simps rthms = |
41444 | 739 |
Goal.conjunction_tac |
38859
053c69cb4a0e
quotient package: lemmas to be lifted and descended can be pre-simplified
Christian Urban <urbanc@in.tum.de>
parents:
38719
diff
changeset
|
740 |
THEN' RANGE (map (lift_single_tac ctxt simps) rthms) |
38625
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
741 |
|
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
742 |
|
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
743 |
(* automated lifting with pre-simplification of the theorems; |
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
744 |
for internal usage *) |
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
745 |
fun lifted ctxt qtys simps rthm = |
41444 | 746 |
let |
747 |
val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt |
|
59582 | 748 |
val goal = Quotient_Term.derive_qtrm ctxt' qtys (Thm.prop_of rthm') |
41444 | 749 |
in |
750 |
Goal.prove ctxt' [] [] goal |
|
751 |
(K (HEADGOAL (lift_single_tac ctxt' simps rthm'))) |
|
42361 | 752 |
|> singleton (Proof_Context.export ctxt' ctxt) |
41444 | 753 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
754 |
|
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
755 |
|
38625
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
756 |
(* lifting as an attribute *) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
757 |
|
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61144
diff
changeset
|
758 |
val lifted_attrib = Thm.rule_attribute [] (fn context => |
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
759 |
let |
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
760 |
val ctxt = Context.proof_of context |
45279 | 761 |
val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt) |
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
762 |
in |
38625
b97bd93fb9e2
allow for pre-simplification of lifted theorems
Christian Urban <urbanc@in.tum.de>
parents:
38624
diff
changeset
|
763 |
lifted ctxt qtys [] |
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37592
diff
changeset
|
764 |
end) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
765 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
766 |
end; (* structure *) |