author paulson Fri, 03 Dec 2004 17:03:05 +0100 changeset 15371 40f5045c5985 parent 15370 05b03ea0f18d child 15372 2ecc0befd98f
fixes to clause conversion
```--- a/src/HOL/Tools/res_axioms.ML	Fri Dec 03 15:28:12 2004 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Dec 03 17:03:05 2004 +0100
@@ -21,10 +21,9 @@

struct

-
fun elimRule_tac thm =
((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
-    REPEAT(Blast_tac 1);
+    REPEAT(Fast_tac 1);

(* This following version fails sometimes, need to investigate, do not use it now. *)
@@ -56,38 +55,56 @@
| strip_trueprop _ = raise TRUEPROP("not a prop!");

+fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) \$ P;
+
+
+fun is_neg (Const("Trueprop",_) \$ (Const("Not",_) \$ Free(p,_))) (Const("Trueprop",_) \$ Free(q,_))= (p = q)
+  | is_neg _ _ = false;
+

exception STRIP_CONCL;

-fun strip_concl prems bvs (Const ("all", _) \$ Abs (x,xtp,body))  = strip_concl prems ((x,xtp)::bvs) body
-  | strip_concl prems bvs (Const ("==>",_) \$ P \$ Q) =
+fun strip_concl' prems bvs (Const ("==>",_) \$ P \$ Q) =
let val P' = strip_trueprop P
val prems' = P'::prems
in
-	strip_concl prems' bvs  Q
+	strip_concl' prems' bvs  Q
end
-  | strip_concl prems bvs _ = add_EX (make_conjs prems) bvs;
+  | strip_concl' prems bvs P =
+    let val P' = neg (strip_trueprop P)
+    in
+    end;
+
+
+fun strip_concl prems bvs concl (Const ("all", _) \$ Abs (x,xtp,body))  = strip_concl prems ((x,xtp)::bvs) concl body
+  | strip_concl prems bvs concl (Const ("==>",_) \$ P \$ Q) =
+    if (is_neg P concl) then (strip_concl' prems bvs Q)
+    else
+	(let val P' = strip_trueprop P
+	     val prems' = P'::prems
+	 in
+	     strip_concl prems' bvs  concl Q
+	 end)
+  | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;

-fun trans_elim (main,others) =
-    let val others' = map (strip_concl [] []) others
+fun trans_elim (main,others,concl) =
+    let val others' = map (strip_concl [] [] concl) others
val disjs = make_disjs others'
in
make_imp(strip_trueprop main,disjs)
end;

-fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) \$ P;
-
-
-fun elimR2Fol_aux prems =
+fun elimR2Fol_aux prems concl =
let val nprems = length prems
val main = hd prems
in
if (nprems = 1) then neg (strip_trueprop main)
-        else trans_elim (main, tl prems)
+        else trans_elim (main, tl prems, concl)
end;

@@ -99,14 +116,13 @@
val (prems,concl) = (prems_of elimR', concl_of elimR')
in
case concl of Const("Trueprop",_) \$ Free(_,Type("bool",[]))
-		      => trueprop (elimR2Fol_aux prems)
-                    | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems)
+		      => trueprop (elimR2Fol_aux prems concl)
+                    | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems concl)
| _ => raise ELIMR2FOL("Not an elimination rule!")
end;

-
(**** use prove_goalw_cterm to prove ****)

fun transform_elim thm =```