# HG changeset patch # User chaieb # Date 1185119634 -7200 # Node ID e61361aa23b2a9b5a78186c1ae0d3fa687b8a659 # Parent 717a6cb1c659036c001cab6f9ab775d7a83e1cdf Quantifier elimination for Dense linear orders after Langford diff -r 717a6cb1c659 -r e61361aa23b2 src/HOL/Tools/Qelim/langford.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Qelim/langford.ML Sun Jul 22 17:53:54 2007 +0200 @@ -0,0 +1,217 @@ +signature LANGFORD_QE = +sig + val dlo_tac : Proof.context -> int -> tactic + val dlo_conv : Proof.context -> cterm -> thm +end + +structure LangfordQE:LANGFORD_QE = +struct + +val dest_set = + let + fun h acc ct = + case (term_of ct) of + Const("{}",_) => acc + | Const("insert",_)$_$t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct) +in h [] end; + +fun prove_finite cT u = +let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"} + fun ins x th = + implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) + (Thm.cprop_of th), SOME x] th1) th +in fold ins u th0 end; + +val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms)))); + +fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = + case term_of ep of + Const("Ex",_)$_ => + let + val p = Thm.dest_arg ep + val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid) + val (L,U) = + let + val (x,q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths)) + in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) + end + fun proveneF S = + let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg + val cT = ctyp_of_term a + val ne = instantiate' [SOME cT] [SOME a, SOME A] + @{thm insert_not_empty} + val f = prove_finite cT (dest_set S) + in (ne, f) end + + val qe = case (term_of L, term_of U) of + (Const("{}",_),_) => + let + val (neU,fU) = proveneF U + in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end + | (_,Const("{}",_)) => + let + val (neL,fL) = proveneF L + in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end + + | (_,_) => + let + val (neL,fL) = proveneF L + val (neU,fU) = proveneF U + in simp_rule (transitive ths (dlo_qeth OF [neL, neU, fL, fU])) + end + in qe end + | _ => error "dlo_qe : Not an existential formula"; + +val all_conjuncts = + let fun h acc ct = + case term_of ct of + @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct) + | _ => ct::acc +in h [] end; + +fun conjuncts ct = + case term_of ct of + @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct)) +| _ => [ct]; + +fun fold1 f = foldr1 (uncurry f); + +val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ; + +fun mk_conj_tab th = + let fun h acc th = + case prop_of th of + @{term "Trueprop"}$(@{term "op &"}$p$q) => + h (h acc (th RS conjunct2)) (th RS conjunct1) + | @{term "Trueprop"}$p => (p,th)::acc +in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end; + +fun is_conj (@{term "op &"}$_$_) = true + | is_conj _ = false; + +fun prove_conj tab cjs = + case cjs of + [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c + | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs]; + +fun conj_aci_rule eq = + let + val (l,r) = Thm.dest_equals eq + fun tabl c = valOf (Termtab.lookup (mk_conj_tab (assume l)) (term_of c)) + fun tabr c = valOf (Termtab.lookup (mk_conj_tab (assume r)) (term_of c)) + val ll = Thm.dest_arg l + val rr = Thm.dest_arg r + + val thl = prove_conj tabl (conjuncts rr) + |> Drule.implies_intr_hyps + val thr = prove_conj tabr (conjuncts ll) + |> Drule.implies_intr_hyps + val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI} + in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end; + +fun partition f [] = ([],[]) + | partition f (x::xs) = + let val (yes,no) = partition f xs + in if f x then (x::yes,no) else (yes, x::no) end; + +fun contains x ct = member (op aconv) (term_frees (term_of ct)) (term_of x); + +fun is_eqx x eq = case term_of eq of + Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x + | _ => false ; + +local +fun proc ct = + case term_of ct of + Const("Ex",_)$Abs (xn,_,_) => + let + val e = Thm.dest_fun ct + val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct) + val Pp = Thm.capply @{cterm "Trueprop"} p + val (eqs,neqs) = partition (is_eqx x) (all_conjuncts p) + in case eqs of + [] => + let + val (dx,ndx) = partition (contains x) neqs + in case ndx of [] => NONE + | _ => + conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp + (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx)))) + |> abstract_rule xn x |> Drule.arg_cong_rule e + |> Conv.fconv_rule (Conv.arg_conv + (Simplifier.rewrite + (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) + |> SOME + end + | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp + (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs)))) + |> abstract_rule xn x |> Drule.arg_cong_rule e + |> Conv.fconv_rule (Conv.arg_conv + (Simplifier.rewrite + (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) + |> SOME + end + | _ => NONE; +in val reduce_ex_simproc = + Simplifier.make_simproc + {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc", + proc = K (K proc) , identifier = []} +end; + +fun raw_dlo_conv dlo_ss + ({qe_bnds, qe_nolb, qe_noub, gst, gs, atoms}:Langford_Data.entry) = + let + val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc] + val dnfex_conv = Simplifier.rewrite ss + val pcv = Simplifier.rewrite + (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps) + @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]) + in fn p => + Qelim.gen_qelim_conv pcv pcv dnfex_conv cons + (Thm.add_cterm_frees p []) (K reflexive) (K reflexive) + (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p + end; + + +val grab_atom_bop = + let + fun h bounds tm = + (case term_of tm of + Const ("op =", T) $ _ $ _ => + if domain_type T = HOLogic.boolT then find_args bounds tm + else Thm.dest_fun2 tm + | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm) + | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm) + | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm) + | Const ("op &", _) $ _ $ _ => find_args bounds tm + | Const ("op |", _) $ _ $ _ => find_args bounds tm + | Const ("op -->", _) $ _ $ _ => find_args bounds tm + | Const ("==>", _) $ _ $ _ => find_args bounds tm + | Const ("==", _) $ _ $ _ => find_args bounds tm + | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm) + | _ => Thm.dest_fun2 tm) + and find_args bounds tm = + (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm) + and find_body bounds b = + let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b + in h (bounds + 1) b' end; +in h end; + +fun dlo_instance ctxt tm = + (fst (Langford_Data.get ctxt), + Langford_Data.match ctxt (grab_atom_bop 0 tm)); + +fun dlo_conv ctxt tm = + (case dlo_instance ctxt tm of + (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm]) + | (ss, SOME instance) => raw_dlo_conv ss instance tm); + +fun dlo_tac ctxt = CSUBGOAL (fn (p, i) => + (case dlo_instance ctxt p of + (ss, NONE) => simp_tac ss i + | (ss, SOME instance) => + ObjectLogic.full_atomize_tac i THEN + simp_tac ss i THEN + CONVERSION (ObjectLogic.judgment_conv (raw_dlo_conv ss instance)) i + THEN (TRY (simp_tac ss i)))); +end; \ No newline at end of file