author chaieb Sun, 22 Jul 2007 17:53:54 +0200 changeset 23906 e61361aa23b2 parent 23905 717a6cb1c659 child 23907 cca404a62173
Quantifier elimination for Dense linear orders after Langford
```--- /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 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```