1 (* Title: HOL/Tools/Qelim/langford.ML |
|
2 Author: Amine Chaieb, TU Muenchen |
|
3 *) |
|
4 |
|
5 signature LANGFORD_QE = |
|
6 sig |
|
7 val dlo_tac : Proof.context -> int -> tactic |
|
8 val dlo_conv : Proof.context -> cterm -> thm |
|
9 end |
|
10 |
|
11 structure LangfordQE :LANGFORD_QE = |
|
12 struct |
|
13 |
|
14 val dest_set = |
|
15 let |
|
16 fun h acc ct = |
|
17 case term_of ct of |
|
18 Const (@{const_name Orderings.bot}, _) => acc |
|
19 | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct) |
|
20 in h [] end; |
|
21 |
|
22 fun prove_finite cT u = |
|
23 let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"} |
|
24 fun ins x th = |
|
25 Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) |
|
26 (Thm.cprop_of th), SOME x] th1) th |
|
27 in fold ins u th0 end; |
|
28 |
|
29 val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms)))); |
|
30 |
|
31 fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = |
|
32 case term_of ep of |
|
33 Const("Ex",_)$_ => |
|
34 let |
|
35 val p = Thm.dest_arg ep |
|
36 val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid) |
|
37 val (L,U) = |
|
38 let |
|
39 val (x,q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths)) |
|
40 in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) |
|
41 end |
|
42 fun proveneF S = |
|
43 let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg |
|
44 val cT = ctyp_of_term a |
|
45 val ne = instantiate' [SOME cT] [SOME a, SOME A] |
|
46 @{thm insert_not_empty} |
|
47 val f = prove_finite cT (dest_set S) |
|
48 in (ne, f) end |
|
49 |
|
50 val qe = case (term_of L, term_of U) of |
|
51 (Const (@{const_name Orderings.bot}, _),_) => |
|
52 let |
|
53 val (neU,fU) = proveneF U |
|
54 in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end |
|
55 | (_,Const (@{const_name Orderings.bot}, _)) => |
|
56 let |
|
57 val (neL,fL) = proveneF L |
|
58 in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end |
|
59 |
|
60 | (_,_) => |
|
61 let |
|
62 val (neL,fL) = proveneF L |
|
63 val (neU,fU) = proveneF U |
|
64 in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) |
|
65 end |
|
66 in qe end |
|
67 | _ => error "dlo_qe : Not an existential formula"; |
|
68 |
|
69 val all_conjuncts = |
|
70 let fun h acc ct = |
|
71 case term_of ct of |
|
72 @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct) |
|
73 | _ => ct::acc |
|
74 in h [] end; |
|
75 |
|
76 fun conjuncts ct = |
|
77 case term_of ct of |
|
78 @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct)) |
|
79 | _ => [ct]; |
|
80 |
|
81 fun fold1 f = foldr1 (uncurry f); |
|
82 |
|
83 val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ; |
|
84 |
|
85 fun mk_conj_tab th = |
|
86 let fun h acc th = |
|
87 case prop_of th of |
|
88 @{term "Trueprop"}$(@{term "op &"}$p$q) => |
|
89 h (h acc (th RS conjunct2)) (th RS conjunct1) |
|
90 | @{term "Trueprop"}$p => (p,th)::acc |
|
91 in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end; |
|
92 |
|
93 fun is_conj (@{term "op &"}$_$_) = true |
|
94 | is_conj _ = false; |
|
95 |
|
96 fun prove_conj tab cjs = |
|
97 case cjs of |
|
98 [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c |
|
99 | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs]; |
|
100 |
|
101 fun conj_aci_rule eq = |
|
102 let |
|
103 val (l,r) = Thm.dest_equals eq |
|
104 fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c)) |
|
105 fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c)) |
|
106 val ll = Thm.dest_arg l |
|
107 val rr = Thm.dest_arg r |
|
108 |
|
109 val thl = prove_conj tabl (conjuncts rr) |
|
110 |> Drule.implies_intr_hyps |
|
111 val thr = prove_conj tabr (conjuncts ll) |
|
112 |> Drule.implies_intr_hyps |
|
113 val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI} |
|
114 in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end; |
|
115 |
|
116 fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x); |
|
117 |
|
118 fun is_eqx x eq = case term_of eq of |
|
119 Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x |
|
120 | _ => false ; |
|
121 |
|
122 local |
|
123 fun proc ct = |
|
124 case term_of ct of |
|
125 Const("Ex",_)$Abs (xn,_,_) => |
|
126 let |
|
127 val e = Thm.dest_fun ct |
|
128 val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct) |
|
129 val Pp = Thm.capply @{cterm "Trueprop"} p |
|
130 val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p) |
|
131 in case eqs of |
|
132 [] => |
|
133 let |
|
134 val (dx,ndx) = List.partition (contains x) neqs |
|
135 in case ndx of [] => NONE |
|
136 | _ => |
|
137 conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp |
|
138 (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx)))) |
|
139 |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |
|
140 |> Conv.fconv_rule (Conv.arg_conv |
|
141 (Simplifier.rewrite |
|
142 (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) |
|
143 |> SOME |
|
144 end |
|
145 | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp |
|
146 (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs)))) |
|
147 |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |
|
148 |> Conv.fconv_rule (Conv.arg_conv |
|
149 (Simplifier.rewrite |
|
150 (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) |
|
151 |> SOME |
|
152 end |
|
153 | _ => NONE; |
|
154 in val reduce_ex_simproc = |
|
155 Simplifier.make_simproc |
|
156 {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc", |
|
157 proc = K (K proc) , identifier = []} |
|
158 end; |
|
159 |
|
160 fun raw_dlo_conv dlo_ss |
|
161 ({qe_bnds, qe_nolb, qe_noub, gst, gs, atoms}:Langford_Data.entry) = |
|
162 let |
|
163 val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc] |
|
164 val dnfex_conv = Simplifier.rewrite ss |
|
165 val pcv = Simplifier.rewrite |
|
166 (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps) |
|
167 @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]) |
|
168 in fn p => |
|
169 Qelim.gen_qelim_conv pcv pcv dnfex_conv cons |
|
170 (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive) |
|
171 (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p |
|
172 end; |
|
173 |
|
174 |
|
175 val grab_atom_bop = |
|
176 let |
|
177 fun h bounds tm = |
|
178 (case term_of tm of |
|
179 Const ("op =", T) $ _ $ _ => |
|
180 if domain_type T = HOLogic.boolT then find_args bounds tm |
|
181 else Thm.dest_fun2 tm |
|
182 | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm) |
|
183 | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
184 | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
185 | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
186 | Const ("op &", _) $ _ $ _ => find_args bounds tm |
|
187 | Const ("op |", _) $ _ $ _ => find_args bounds tm |
|
188 | Const ("op -->", _) $ _ $ _ => find_args bounds tm |
|
189 | Const ("==>", _) $ _ $ _ => find_args bounds tm |
|
190 | Const ("==", _) $ _ $ _ => find_args bounds tm |
|
191 | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm) |
|
192 | _ => Thm.dest_fun2 tm) |
|
193 and find_args bounds tm = |
|
194 (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm)) |
|
195 and find_body bounds b = |
|
196 let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b |
|
197 in h (bounds + 1) b' end; |
|
198 in h end; |
|
199 |
|
200 fun dlo_instance ctxt tm = |
|
201 (fst (Langford_Data.get ctxt), |
|
202 Langford_Data.match ctxt (grab_atom_bop 0 tm)); |
|
203 |
|
204 fun dlo_conv ctxt tm = |
|
205 (case dlo_instance ctxt tm of |
|
206 (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm]) |
|
207 | (ss, SOME instance) => raw_dlo_conv ss instance tm); |
|
208 |
|
209 fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st => |
|
210 let |
|
211 fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} |
|
212 fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) |
|
213 val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) |
|
214 val p' = fold_rev gen ts p |
|
215 in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); |
|
216 |
|
217 |
|
218 fun cfrees ats ct = |
|
219 let |
|
220 val ins = insert (op aconvc) |
|
221 fun h acc t = |
|
222 case (term_of t) of |
|
223 b$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t) |
|
224 then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) |
|
225 else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
|
226 | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
|
227 | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc)) |
|
228 | Free _ => if member (op aconvc) ats t then acc else ins t acc |
|
229 | Var _ => if member (op aconvc) ats t then acc else ins t acc |
|
230 | _ => acc |
|
231 in h [] ct end |
|
232 |
|
233 fun dlo_tac ctxt = CSUBGOAL (fn (p, i) => |
|
234 (case dlo_instance ctxt p of |
|
235 (ss, NONE) => simp_tac ss i |
|
236 | (ss, SOME instance) => |
|
237 Object_Logic.full_atomize_tac i THEN |
|
238 simp_tac ss i |
|
239 THEN (CONVERSION Thm.eta_long_conversion) i |
|
240 THEN (TRY o generalize_tac (cfrees (#atoms instance))) i |
|
241 THEN Object_Logic.full_atomize_tac i |
|
242 THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i |
|
243 THEN (simp_tac ss i))); |
|
244 end; |
|