# HG changeset patch # User wenzelm # Date 1723380356 -7200 # Node ID e451d6230535732c828bd66f0c0355925b8403f1 # Parent f65b65814b81c44525afe4a1696698f50704e9a2 tuned: more antiquotations; diff -r f65b65814b81 -r e451d6230535 src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Sun Aug 11 14:18:40 2024 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Sun Aug 11 14:45:56 2024 +0200 @@ -16,20 +16,16 @@ structure Qelim: QELIM = struct -val all_not_ex = mk_meta_eq @{thm "all_not_ex"}; - fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv = let fun conv env p = - case Thm.term_of p of - Const(s,T)$_$_ => - if domain_type T = HOLogic.boolT - andalso member (op =) [\<^const_name>\HOL.conj\, \<^const_name>\HOL.disj\, - \<^const_name>\HOL.implies\, \<^const_name>\HOL.eq\] s - then Conv.binop_conv (conv env) p - else atcv env p - | Const(\<^const_name>\Not\,_)$_ => Conv.arg_conv (conv env) p - | Const(\<^const_name>\Ex\,_)$Abs (s, _, _) => + (case Thm.term_of p of + \<^Const_>\conj for _ _\ => Conv.binop_conv (conv env) p + | \<^Const_>\disj for _ _\ => Conv.binop_conv (conv env) p + | \<^Const_>\implies for _ _\ => Conv.binop_conv (conv env) p + | \<^Const_>\HOL.eq _ for _ _\ => Conv.binop_conv (conv env) p + | \<^Const_>\Not for _\ => Conv.arg_conv (conv env) p + | \<^Const_>\Ex _ for \Abs (s, _, _)\\ => let val (e,p0) = Thm.dest_comb p val (x,p') = Thm.dest_abs_global p0 @@ -43,15 +39,15 @@ if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th)) else Thm.transitive (Thm.transitive th th') (conv env r) end - | Const(\<^const_name>\Ex\,_)$ _ => (Thm.eta_long_conversion then_conv conv env) p - | Const(\<^const_name>\All\, _)$_ => + | \<^Const_>\Ex _ for _\ => (Thm.eta_long_conversion then_conv conv env) p + | \<^Const_>\All _ for _\ => let val allT = Thm.ctyp_of_cterm (Thm.dest_fun p) val T = Thm.dest_ctyp0 (Thm.dest_ctyp0 allT) - val p = Thm.dest_arg p - val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex + val P = Thm.dest_arg p + val th = \<^instantiate>\'a = T and P in lemma "\x::'a. P x \ \x. \ P x" by simp\ in Thm.transitive th (conv env (Thm.rhs_of th)) end - | _ => atcv env p + | _ => atcv env p) in precv then_conv (conv env) then_conv postcv end