93 val PPQ = Logic.mk_implies(P,PQ) |
93 val PPQ = Logic.mk_implies(P,PQ) |
94 val cP = cert P |
94 val cP = cert P |
95 val cQ = cert Q |
95 val cQ = cert Q |
96 val cPQ = cert PQ |
96 val cPQ = cert PQ |
97 val cPPQ = cert PPQ |
97 val cPPQ = cert PPQ |
98 val th1 = assume cPQ |> implies_intr_list [cPQ,cP] |
98 val th1 = Thm.assume cPQ |> implies_intr_list [cPQ,cP] |
99 val th3 = assume cP |
99 val th3 = Thm.assume cP |
100 val th4 = implies_elim_list (assume cPPQ) [th3,th3] |
100 val th4 = implies_elim_list (Thm.assume cPPQ) [th3,th3] |
101 |> implies_intr_list [cPPQ,cP] |
101 |> implies_intr_list [cPPQ,cP] |
102 in |
102 in |
103 equal_intr th4 th1 |> Drule.export_without_context |
103 Thm.equal_intr th4 th1 |> Drule.export_without_context |
104 end |
104 end |
105 |
105 |
106 val imp_comm = |
106 val imp_comm = |
107 let |
107 let |
108 val cert = cterm_of Pure.thy |
108 val cert = cterm_of Pure.thy |
113 val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R)) |
113 val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R)) |
114 val cP = cert P |
114 val cP = cert P |
115 val cQ = cert Q |
115 val cQ = cert Q |
116 val cPQR = cert PQR |
116 val cPQR = cert PQR |
117 val cQPR = cert QPR |
117 val cQPR = cert QPR |
118 val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ] |
118 val th1 = implies_elim_list (Thm.assume cPQR) [Thm.assume cP,Thm.assume cQ] |
119 |> implies_intr_list [cPQR,cQ,cP] |
119 |> implies_intr_list [cPQR,cQ,cP] |
120 val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP] |
120 val th2 = implies_elim_list (Thm.assume cQPR) [Thm.assume cQ,Thm.assume cP] |
121 |> implies_intr_list [cQPR,cP,cQ] |
121 |> implies_intr_list [cQPR,cP,cQ] |
122 in |
122 in |
123 equal_intr th1 th2 |> Drule.export_without_context |
123 Thm.equal_intr th1 th2 |> Drule.export_without_context |
124 end |
124 end |
125 |
125 |
126 val def_norm = |
126 val def_norm = |
127 let |
127 let |
128 val cert = cterm_of Pure.thy |
128 val cert = cterm_of Pure.thy |
132 val P = Free("P",aT-->bT) |
132 val P = Free("P",aT-->bT) |
133 val Q = Free("Q",aT-->bT) |
133 val Q = Free("Q",aT-->bT) |
134 val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0))) |
134 val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0))) |
135 val cPQ = cert (Logic.mk_equals(P,Q)) |
135 val cPQ = cert (Logic.mk_equals(P,Q)) |
136 val cv = cert v |
136 val cv = cert v |
137 val rew = assume cvPQ |
137 val rew = Thm.assume cvPQ |
138 |> forall_elim cv |
138 |> Thm.forall_elim cv |
139 |> abstract_rule "v" cv |
139 |> Thm.abstract_rule "v" cv |
140 val (lhs,rhs) = Logic.dest_equals(concl_of rew) |
140 val (lhs,rhs) = Logic.dest_equals(concl_of rew) |
141 val th1 = transitive (transitive |
141 val th1 = Thm.transitive (Thm.transitive |
142 (eta_conversion (cert lhs) |> symmetric) |
142 (Thm.eta_conversion (cert lhs) |> Thm.symmetric) |
143 rew) |
143 rew) |
144 (eta_conversion (cert rhs)) |
144 (Thm.eta_conversion (cert rhs)) |
145 |> implies_intr cvPQ |
145 |> Thm.implies_intr cvPQ |
146 val th2 = combination (assume cPQ) (reflexive cv) |
146 val th2 = Thm.combination (Thm.assume cPQ) (Thm.reflexive cv) |
147 |> forall_intr cv |
147 |> Thm.forall_intr cv |
148 |> implies_intr cPQ |
148 |> Thm.implies_intr cPQ |
149 in |
149 in |
150 equal_intr th1 th2 |> Drule.export_without_context |
150 Thm.equal_intr th1 th2 |> Drule.export_without_context |
151 end |
151 end |
152 |
152 |
153 val all_comm = |
153 val all_comm = |
154 let |
154 let |
155 val cert = cterm_of Pure.thy |
155 val cert = cterm_of Pure.thy |
162 val rhs = Logic.all y (Logic.all x (P $ x $ y)) |
162 val rhs = Logic.all y (Logic.all x (P $ x $ y)) |
163 val cl = cert lhs |
163 val cl = cert lhs |
164 val cr = cert rhs |
164 val cr = cert rhs |
165 val cx = cert x |
165 val cx = cert x |
166 val cy = cert y |
166 val cy = cert y |
167 val th1 = assume cr |
167 val th1 = Thm.assume cr |
168 |> forall_elim_list [cy,cx] |
168 |> forall_elim_list [cy,cx] |
169 |> forall_intr_list [cx,cy] |
169 |> forall_intr_list [cx,cy] |
170 |> implies_intr cr |
170 |> Thm.implies_intr cr |
171 val th2 = assume cl |
171 val th2 = Thm.assume cl |
172 |> forall_elim_list [cx,cy] |
172 |> forall_elim_list [cx,cy] |
173 |> forall_intr_list [cy,cx] |
173 |> forall_intr_list [cy,cx] |
174 |> implies_intr cl |
174 |> Thm.implies_intr cl |
175 in |
175 in |
176 equal_intr th1 th2 |> Drule.export_without_context |
176 Thm.equal_intr th1 th2 |> Drule.export_without_context |
177 end |
177 end |
178 |
178 |
179 val equiv_comm = |
179 val equiv_comm = |
180 let |
180 let |
181 val cert = cterm_of Pure.thy |
181 val cert = cterm_of Pure.thy |
182 val T = TFree("'a",[]) |
182 val T = TFree("'a",[]) |
183 val t = Free("t",T) |
183 val t = Free("t",T) |
184 val u = Free("u",T) |
184 val u = Free("u",T) |
185 val ctu = cert (Logic.mk_equals(t,u)) |
185 val ctu = cert (Logic.mk_equals(t,u)) |
186 val cut = cert (Logic.mk_equals(u,t)) |
186 val cut = cert (Logic.mk_equals(u,t)) |
187 val th1 = assume ctu |> symmetric |> implies_intr ctu |
187 val th1 = Thm.assume ctu |> Thm.symmetric |> Thm.implies_intr ctu |
188 val th2 = assume cut |> symmetric |> implies_intr cut |
188 val th2 = Thm.assume cut |> Thm.symmetric |> Thm.implies_intr cut |
189 in |
189 in |
190 equal_intr th1 th2 |> Drule.export_without_context |
190 Thm.equal_intr th1 th2 |> Drule.export_without_context |
191 end |
191 end |
192 |
192 |
193 (* This simplification procedure rewrites !!x y. P x y |
193 (* This simplification procedure rewrites !!x y. P x y |
194 deterministicly, in order for the normalization function, defined |
194 deterministicly, in order for the normalization function, defined |
195 below, to handle nested quantifiers robustly *) |
195 below, to handle nested quantifiers robustly *) |
215 fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t = |
215 fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t = |
216 let |
216 let |
217 val lhs = list_all ([xv,yv],t) |
217 val lhs = list_all ([xv,yv],t) |
218 val rhs = list_all ([yv,xv],swap_bound 0 t) |
218 val rhs = list_all ([yv,xv],swap_bound 0 t) |
219 val rew = Logic.mk_equals (lhs,rhs) |
219 val rew = Logic.mk_equals (lhs,rhs) |
220 val init = trivial (cterm_of thy rew) |
220 val init = Thm.trivial (cterm_of thy rew) |
221 in |
221 in |
222 (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e)) |
222 (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e)) |
223 end |
223 end |
224 |
224 |
225 fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) = |
225 fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) = |
230 0 => SOME (rew_th thy (x,xT) (y,yT) body) |
230 0 => SOME (rew_th thy (x,xT) (y,yT) body) |
231 | 1 => if string_ord(y,x) = LESS |
231 | 1 => if string_ord(y,x) = LESS |
232 then |
232 then |
233 let |
233 let |
234 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body))) |
234 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body))) |
235 val t_th = reflexive (cterm_of thy t) |
235 val t_th = Thm.reflexive (cterm_of thy t) |
236 val newt_th = reflexive (cterm_of thy newt) |
236 val newt_th = Thm.reflexive (cterm_of thy newt) |
237 in |
237 in |
238 SOME (transitive t_th newt_th) |
238 SOME (Thm.transitive t_th newt_th) |
239 end |
239 end |
240 else NONE |
240 else NONE |
241 | _ => error "norm_term (quant_rewrite) internal error" |
241 | _ => error "norm_term (quant_rewrite) internal error" |
242 end |
242 end |
243 | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE) |
243 | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE) |
292 | eta_redex _ = false |
292 | eta_redex _ = false |
293 |
293 |
294 fun eta_contract thy assumes origt = |
294 fun eta_contract thy assumes origt = |
295 let |
295 let |
296 val (typet,Tinst) = freeze_thaw_term origt |
296 val (typet,Tinst) = freeze_thaw_term origt |
297 val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet)) |
297 val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet)) |
298 val final = inst_tfrees thy Tinst o thaw |
298 val final = inst_tfrees thy Tinst o thaw |
299 val t = #1 (Logic.dest_equals (prop_of init)) |
299 val t = #1 (Logic.dest_equals (prop_of init)) |
300 val _ = |
300 val _ = |
301 let |
301 let |
302 val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
302 val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
320 let |
320 let |
321 val cert = cterm_of thy |
321 val cert = cterm_of thy |
322 val v = Free (Name.variant (Term.add_free_names t []) "v", xT) |
322 val v = Free (Name.variant (Term.add_free_names t []) "v", xT) |
323 val cv = cert v |
323 val cv = cert v |
324 val ct = cert t |
324 val ct = cert t |
325 val th = (assume ct) |
325 val th = (Thm.assume ct) |
326 |> forall_elim cv |
326 |> Thm.forall_elim cv |
327 |> abstract_rule x cv |
327 |> Thm.abstract_rule x cv |
328 val ext_th = eta_conversion (cert (Abs(x,xT,P))) |
328 val ext_th = Thm.eta_conversion (cert (Abs(x,xT,P))) |
329 val th' = transitive (symmetric ext_th) th |
329 val th' = Thm.transitive (Thm.symmetric ext_th) th |
330 val cu = cert (prop_of th') |
330 val cu = cert (prop_of th') |
331 val uth = combination (assume cu) (reflexive cv) |
331 val uth = Thm.combination (Thm.assume cu) (Thm.reflexive cv) |
332 val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v))) |
332 val uth' = (Thm.beta_conversion false (cert (Abs(x,xT,Q) $ v))) |
333 |> transitive uth |
333 |> Thm.transitive uth |
334 |> forall_intr cv |
334 |> Thm.forall_intr cv |
335 |> implies_intr cu |
335 |> Thm.implies_intr cu |
336 val rew_th = equal_intr (th' |> implies_intr ct) uth' |
336 val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth' |
337 val res = final rew_th |
337 val res = final rew_th |
338 val lhs = (#1 (Logic.dest_equals (prop_of res))) |
338 val lhs = (#1 (Logic.dest_equals (prop_of res))) |
339 in |
339 in |
340 SOME res |
340 SOME res |
341 end |
341 end |
343 handle e => OldGoals.print_exn e) |
343 handle e => OldGoals.print_exn e) |
344 | _ => NONE |
344 | _ => NONE |
345 end |
345 end |
346 |
346 |
347 fun beta_fun thy assume t = |
347 fun beta_fun thy assume t = |
348 SOME (beta_conversion true (cterm_of thy t)) |
348 SOME (Thm.beta_conversion true (cterm_of thy t)) |
349 |
349 |
350 val meta_sym_rew = thm "refl" |
350 val meta_sym_rew = thm "refl" |
351 |
351 |
352 fun equals_fun thy assume t = |
352 fun equals_fun thy assume t = |
353 case t of |
353 case t of |
355 | _ => NONE |
355 | _ => NONE |
356 |
356 |
357 fun eta_expand thy assumes origt = |
357 fun eta_expand thy assumes origt = |
358 let |
358 let |
359 val (typet,Tinst) = freeze_thaw_term origt |
359 val (typet,Tinst) = freeze_thaw_term origt |
360 val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet)) |
360 val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet)) |
361 val final = inst_tfrees thy Tinst o thaw |
361 val final = inst_tfrees thy Tinst o thaw |
362 val t = #1 (Logic.dest_equals (prop_of init)) |
362 val t = #1 (Logic.dest_equals (prop_of init)) |
363 val _ = |
363 val _ = |
364 let |
364 let |
365 val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
365 val lhs = #1 (Logic.dest_equals (prop_of (final init))) |
385 val cert = cterm_of thy |
385 val cert = cterm_of thy |
386 val vname = Name.variant (Term.add_free_names t []) "v" |
386 val vname = Name.variant (Term.add_free_names t []) "v" |
387 val v = Free(vname,aT) |
387 val v = Free(vname,aT) |
388 val cv = cert v |
388 val cv = cert v |
389 val ct = cert t |
389 val ct = cert t |
390 val th1 = (combination (assume ct) (reflexive cv)) |
390 val th1 = (Thm.combination (Thm.assume ct) (Thm.reflexive cv)) |
391 |> forall_intr cv |
391 |> Thm.forall_intr cv |
392 |> implies_intr ct |
392 |> Thm.implies_intr ct |
393 val concl = cert (concl_of th1) |
393 val concl = cert (concl_of th1) |
394 val th2 = (assume concl) |
394 val th2 = (Thm.assume concl) |
395 |> forall_elim cv |
395 |> Thm.forall_elim cv |
396 |> abstract_rule vname cv |
396 |> Thm.abstract_rule vname cv |
397 val (lhs,rhs) = Logic.dest_equals (prop_of th2) |
397 val (lhs,rhs) = Logic.dest_equals (prop_of th2) |
398 val elhs = eta_conversion (cert lhs) |
398 val elhs = Thm.eta_conversion (cert lhs) |
399 val erhs = eta_conversion (cert rhs) |
399 val erhs = Thm.eta_conversion (cert rhs) |
400 val th2' = transitive |
400 val th2' = Thm.transitive |
401 (transitive (symmetric elhs) th2) |
401 (Thm.transitive (Thm.symmetric elhs) th2) |
402 erhs |
402 erhs |
403 val res = equal_intr th1 (th2' |> implies_intr concl) |
403 val res = Thm.equal_intr th1 (th2' |> Thm.implies_intr concl) |
404 val res' = final res |
404 val res' = final res |
405 in |
405 in |
406 SOME res' |
406 SOME res' |
407 end |
407 end |
408 | _ => NONE) |
408 | _ => NONE) |
494 addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy] |
494 addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy] |
495 fun chain f th = |
495 fun chain f th = |
496 let |
496 let |
497 val rhs = Thm.rhs_of th |
497 val rhs = Thm.rhs_of th |
498 in |
498 in |
499 transitive th (f rhs) |
499 Thm.transitive th (f rhs) |
500 end |
500 end |
501 val th = |
501 val th = |
502 t |> disamb_bound thy |
502 t |> disamb_bound thy |
503 |> chain (Simplifier.full_rewrite ss) |
503 |> chain (Simplifier.full_rewrite ss) |
504 |> chain eta_conversion |
504 |> chain Thm.eta_conversion |
505 |> Thm.strip_shyps |
505 |> Thm.strip_shyps |
506 val _ = message ("norm_term: " ^ (string_of_thm th)) |
506 val _ = message ("norm_term: " ^ (string_of_thm th)) |
507 in |
507 in |
508 th |
508 th |
509 end |
509 end |
527 |
527 |
528 fun norm_thm thy th = |
528 fun norm_thm thy th = |
529 let |
529 let |
530 val c = prop_of th |
530 val c = prop_of th |
531 in |
531 in |
532 equal_elim (norm_term thy c) th |
532 Thm.equal_elim (norm_term thy c) th |
533 end |
533 end |
534 |
534 |
535 (* make_equal thy t u tries to construct the theorem t == u under the |
535 (* make_equal thy t u tries to construct the theorem t == u under the |
536 signature thy. If it succeeds, SOME (t == u) is returned, otherwise |
536 signature thy. If it succeeds, SOME (t == u) is returned, otherwise |
537 NONE is returned. *) |
537 NONE is returned. *) |
538 |
538 |
539 fun make_equal thy t u = |
539 fun make_equal thy t u = |
540 let |
540 let |
541 val t_is_t' = norm_term thy t |
541 val t_is_t' = norm_term thy t |
542 val u_is_u' = norm_term thy u |
542 val u_is_u' = norm_term thy u |
543 val th = transitive t_is_t' (symmetric u_is_u') |
543 val th = Thm.transitive t_is_t' (Thm.symmetric u_is_u') |
544 val _ = message ("make_equal: SOME " ^ (string_of_thm th)) |
544 val _ = message ("make_equal: SOME " ^ (string_of_thm th)) |
545 in |
545 in |
546 SOME th |
546 SOME th |
547 end |
547 end |
548 handle e as THM _ => (message "make_equal: NONE";NONE) |
548 handle e as THM _ => (message "make_equal: NONE";NONE) |
591 val shuffles = ShuffleData.get thy |
591 val shuffles = ShuffleData.get thy |
592 fun process [] = NONE |
592 fun process [] = NONE |
593 | process ((name,th)::thms) = |
593 | process ((name,th)::thms) = |
594 let |
594 let |
595 val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th))) |
595 val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th))) |
596 val triv_th = trivial rhs |
596 val triv_th = Thm.trivial rhs |
597 val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th)) |
597 val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th)) |
598 val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of |
598 val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of |
599 SOME(th,_) => SOME th |
599 SOME(th,_) => SOME th |
600 | NONE => NONE |
600 | NONE => NONE |
601 in |
601 in |
602 case mod_th of |
602 case mod_th of |
603 SOME mod_th => |
603 SOME mod_th => |
604 let |
604 let |
605 val closed_th = equal_elim (symmetric rew_th) mod_th |
605 val closed_th = Thm.equal_elim (Thm.symmetric rew_th) mod_th |
606 in |
606 in |
607 message ("Shuffler.set_prop succeeded by " ^ name); |
607 message ("Shuffler.set_prop succeeded by " ^ name); |
608 SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th) |
608 SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th) |
609 end |
609 end |
610 | NONE => process thms |
610 | NONE => process thms |