# HG changeset patch
# User webertj
# Date 1180706653 -7200
# Node ID d45c4d6c5f15f8416092cf2e97d9b26dfe97c239
# Parent  4574ab8f3b218d8844034dd7a04329f6ca2e9b2b
fixed handling of meta-logic propositions

diff -r 4574ab8f3b21 -r d45c4d6c5f15 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Jun 01 15:57:45 2007 +0200
+++ b/src/HOL/arith_data.ML	Fri Jun 01 16:04:13 2007 +0200
@@ -181,8 +181,9 @@
     atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
   | _ => [thm];
 
-fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
-  | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
+fun neg_prop ((TP as Const("Trueprop",_)) $ (Const("Not",_) $ t)) = TP $ t
+  | neg_prop ((TP as Const("Trueprop",_)) $ t) = TP $ (HOLogic.Not $t)
+  | neg_prop t = raise TERM ("neg_prop", [t]);
 
 fun is_False thm =
   let val _ $ t = #prop(rep_thm thm)
@@ -401,9 +402,11 @@
 fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d)
   | negate NONE                        = NONE;
 
-fun decomp_negation data (_ $ (Const (rel, T) $ lhs $ rhs)) : decompT option =
+fun decomp_negation data
+  ((Const ("Trueprop", _)) $ (Const (rel, T) $ lhs $ rhs)) : decompT option =
       decomp_typecheck data (T, (rel, lhs, rhs))
-  | decomp_negation data (_ $ (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
+  | decomp_negation data ((Const ("Trueprop", _)) $
+  (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
       negate (decomp_typecheck data (T, (rel, lhs, rhs)))
   | decomp_negation data _ =
       NONE;
@@ -981,14 +984,14 @@
 in
 
   val simple_arith_tac = FIRST' [fast_arith_tac,
-    ObjectLogic.atomize_tac THEN' raw_arith_tac true];
+    ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac true];
 
   val arith_tac = FIRST' [fast_arith_tac,
-    ObjectLogic.atomize_tac THEN' raw_arith_tac true,
+    ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac true,
     arith_theory_tac];
 
   val silent_arith_tac = FIRST' [fast_arith_tac,
-    ObjectLogic.atomize_tac THEN' raw_arith_tac false,
+    ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac false,
     arith_theory_tac];
 
   fun arith_method prems =
diff -r 4574ab8f3b21 -r d45c4d6c5f15 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 01 15:57:45 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 01 16:04:13 2007 +0200
@@ -42,9 +42,11 @@
 mk_Eq(in) = `in == True'
 where `in' is an (in)equality.
 
-neg_prop(t) = neg  if t is wrapped up in Trueprop and
-  neg is the (logically) negated version of t, where the negation
-  of a negative term is the term itself (no double negation!);
+neg_prop(t) = neg  if t is wrapped up in Trueprop and neg is the
+  (logically) negated version of t (again wrapped up in Trueprop),
+  where the negation of a negative term is the term itself (no
+  double negation!); raises TERM ("neg_prop", [t]) if t is not of
+  the form 'Trueprop $ _'
 
 is_nat(parameter-types,t) =  t:nat
 mk_nat_thm(t) = "0 <= t"
@@ -697,6 +699,7 @@
 fun prove (sg : theory) (params : (string * Term.typ) list) (show_ex : bool)
           (do_pre : bool) (Hs : term list) (concl : term) : injust list option =
   let
+    val _ = trace_msg "prove:"
     (* append the negated conclusion to 'Hs' -- this corresponds to     *)
     (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *)
     (* theorem/tactic level                                             *)
@@ -704,7 +707,6 @@
     fun is_neq NONE                 = false
       | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
   in
-    trace_msg "prove";
     if count is_neq (map (LA_Data.decomp sg) Hs')
       > !fast_arith_neq_limit then (
       trace_msg ("fast_arith_neq_limit exceeded (current value is " ^
@@ -712,7 +714,12 @@
       NONE
     ) else
       refute sg params show_ex do_pre Hs'
-  end;
+  end handle TERM ("neg_prop", _) =>
+    (* since no meta-logic negation is available, we can only fail if   *)
+    (* the conclusion is not of the form 'Trueprop $ _' (simply         *)
+    (* dropping the conclusion doesn't work either, because even        *)
+    (* 'False' does not imply arbitrary 'concl::prop')                  *)
+    (trace_msg "prove failed (cannot negate conclusion)."; NONE);
 
 fun refute_tac ss (i, justs) =
   fn state =>