Theory QEdlo_ex

(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo_ex imports QEdlo
begin

(* tweaking the reflection setup *)

definition "interpret" :: "atom fm => 'a::dlo list => bool" where
"interpret = Logic.interpret I⇣d⇣l⇣o"

lemma interpret_Atoms:
  "interpret (Atom (Eq i j)) xs = (xs!i = xs!j)" 
  "interpret (Atom (Less i j)) xs = (xs!i < xs!j)"
by(simp_all add:interpret_def)

lemma interpret_others:
  "interpret (Neg(ExQ (Neg f))) xs = (∀x. interpret f (x#xs))"
  "interpret (Or (Neg f1) f2) xs = (interpret f1 xs --> interpret f2 xs)"
by(simp_all add:interpret_def)

lemmas reify_eqs[reify] =
  Logic.interpret.simps(1,2,4-7)[of I⇣d⇣l⇣o, folded interpret_def]
  interpret_others interpret_Atoms

corollary [reflection]: "interpret (qe_dlo f) xs = interpret f xs"
by(simp add:I_qe_dlo interpret_def)

method_setup reify = {*
  Attrib.thms --
    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
  (fn (eqs, to) => fn ctxt =>
    Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to
     THEN' simp_tac (HOL_basic_ss addsimps [@{thm"interpret_def"}])))
*} "dlo reification"

(* leave just enough equations in to convert back to True/False by eval *)
declare I⇣d⇣l⇣o.simps(1)[code]
declare Logic.interpret.simps[code del]
declare Logic.interpret.simps(1-2)[code]

subsection{* Examples *}

lemma "∀x::real. ¬ x < x"
apply reify
apply(subst I_qe_dlo[symmetric])
by eval

lemma "∀x y::real. ∃z. x < y --> x < z & z < y"
apply reify
apply(subst I_qe_dlo[symmetric])
by eval

(* FIXME
lemma "∀ x y::real. ∃ z. x < y --> x < z & z < y"
by(reflection)

lemma "∃ x::real. a+b < x & x < c*d"
apply(reflection)
oops
*)

lemma "∀x::real. ¬ x < x"
apply reify
apply(subst I_qe_dlo[symmetric])
by eval

lemma "∀x y::real. ∃z. x < y --> x < z & z < y"
apply reify
apply(subst I_qe_dlo[symmetric])
by eval

(* 160 secs *)
lemma "¬(∃x y z. ∀u::real. x < x | ¬ x<u | x<y & y<z & ¬ x<z)"
apply reify
apply(subst I_qe_dlo[symmetric])
by eval

lemma "qe_dlo(AllQ (Imp (Atom(Less 0 1)) (Atom(Less 1 0)))) = FalseF"
by eval

lemma "qe_dlo(AllQ(AllQ (Imp (Atom(Less 0 1)) (Atom(Less 0 1))))) = TrueF"
by eval

lemma
  "qe_dlo(AllQ(ExQ(AllQ (And (Atom(Less 2 1)) (Atom(Less 1 0)))))) = FalseF"
by eval

lemma "qe_dlo(AllQ(ExQ(ExQ (And (Atom(Less 1 2)) (Atom(Less 2 0)))))) = TrueF"
by eval

lemma
  "qe_dlo(AllQ(AllQ(ExQ (And (Atom(Less 1 0)) (Atom(Less 0 2)))))) = FalseF"
by eval

lemma "qe_dlo(AllQ(AllQ(ExQ (Imp (Atom(Less 1 2)) (And (Atom(Less 1 0)) (Atom(Less 0 2))))))) = TrueF"
by eval

value [nbe] "qe_dlo(AllQ (Imp (Atom(Less 0 1)) (Atom(Less 0 2))))"

end