# HG changeset patch
# User nipkow
# Date 889544846 -3600
# Node ID a291e858061c480e0d1e0ae67d595fdc58edb331
# Parent  245d70532eed6a892092e326b39a08db9d47fd53
Asm_full_simp_tac now reorients asm c = t to t = c.

diff -r 245d70532eed -r a291e858061c src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 14:27:44 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 16:47:26 1998 +0100
@@ -414,8 +414,6 @@
 (* nil*)
 by (strip_tac 1);
 by (Seq_case_simp_tac "x" 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 (* cons *)
 by (strip_tac 1);
diff -r 245d70532eed -r a291e858061c src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Tue Mar 10 14:27:44 1998 +0100
+++ b/src/HOLCF/ex/Hoare.ML	Tue Mar 10 16:47:26 1998 +0100
@@ -178,7 +178,7 @@
 
 val hoare_lemma11 = prove_goal Hoare.thy 
 "(? n. b1`(iterate n g x) ~= TT) ==>\
-\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
+\ k=(LEAST n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
 \ --> p`x = iterate k g x"
  (fn prems =>
         [
@@ -191,9 +191,6 @@
         (rtac trans 1),
         (rtac p_def3 1),
         (asm_simp_tac HOLCF_ss 1),
-        (eres_inst_tac
-           [("s","0"),("t","Least(%n. b1`(iterate n g x) ~= TT)")] subst 1),
-        (Simp_tac 1),
         (hyp_subst_tac 1),
         (strip_tac 1),
         (etac conjE 1),
diff -r 245d70532eed -r a291e858061c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Mar 10 14:27:44 1998 +0100
+++ b/src/Pure/thm.ML	Tue Mar 10 16:47:26 1998 +0100
@@ -1597,8 +1597,8 @@
   not ((term_tvars erhs) subset
        (term_tvars elhs  union  List.concat(map term_tvars prems)));
 
-(*simple test for looping rewrite*)
-fun looptest sign prems lhs rhs =
+(*Simple test for looping rewrite rules and stupid orientations*)
+fun reorient sign prems lhs rhs =
    rewrite_rule_extra_vars prems lhs rhs
   orelse
    is_Var (head_of lhs)
@@ -1607,10 +1607,11 @@
   orelse
    (null prems andalso
     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
-(*the condition "null prems" in the last cases is necessary because
-  conditional rewrites with extra variables in the conditions may terminate
-  although the rhs is an instance of the lhs. Example:
-  ?m < ?n ==> f(?n) == f(?m)*)
+    (*the condition "null prems" is necessary because conditional rewrites
+      with extra variables in the conditions may terminate although
+      the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
+  orelse
+   (is_Const lhs andalso not(is_Const rhs))
 
 fun decomp_simp(thm as Thm {sign_ref, prop, ...}) =
   let val sign = Sign.deref sign_ref;
@@ -1653,8 +1654,8 @@
 fun orient_rrule mss thm =
   let val (sign,prems,lhs,rhs,perm) = decomp_simp thm
   in if perm then [{thm=thm,lhs=lhs,perm=true}]
-     else if looptest sign prems lhs rhs
-          then if looptest sign prems rhs lhs
+     else if reorient sign prems lhs rhs
+          then if reorient sign prems rhs lhs
                then mk_eq_True mss thm
                else let val Mss{mk_rews={mk_sym,...},...} = mss
                     in case mk_sym thm of
@@ -2052,11 +2053,13 @@
                    val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1)
                in (rrules1, lhss1, mss1) end
 
-        fun rebuild(conc2,(shyps2,hyps2,ders2)) =
+        fun disch1(conc2,(shyps2,hyps2,ders2)) =
           let val hyps2' = if gen_mem (op aconv) (prem1, hyps1)
                            then hyps2 else hyps2\prem1
-              val trec = (Logic.mk_implies(prem1,conc2),
-                          (shyps2,hyps2',ders2))
+          in (Logic.mk_implies(prem1,conc2),(shyps2,hyps2',ders2)) end
+
+        fun rebuild trec2 =
+          let val trec = disch1 trec2
           in case rewritec (prover,sign_ref,maxidx) mss trec of
                None => (None,trec)
              | Some(Const("==>",_)$prem$conc,etc) =>
@@ -2068,10 +2071,10 @@
           case conc of
             Const("==>",_)$s$t =>
               (case impc(prems@[prem1],s,t,mss1,etc1) of
-                 (Some(i,prem),(conc2,etc2)) =>
-                    let val impl = Logic.mk_implies(prem1,conc2)
-                    in if i=0 then impc1(prems,prem,impl,mss,etc2)
-                       else (Some(i-1,prem),(impl,etc2))
+                 (Some(i,prem),trec2) =>
+                    let val trec2' = disch1 trec2
+                    in if i=0 then impc1(prems,prem,fst trec2',mss,snd trec2')
+                       else (Some(i-1,prem),trec2')
                     end
                | (None,trec) => rebuild(trec))
           | _ => rebuild(try_botc mss1 (conc,etc1))
diff -r 245d70532eed -r a291e858061c src/ZF/AC/AC7_AC9.ML
--- a/src/ZF/AC/AC7_AC9.ML	Tue Mar 10 14:27:44 1998 +0100
+++ b/src/ZF/AC/AC7_AC9.ML	Tue Mar 10 16:47:26 1998 +0100
@@ -140,7 +140,6 @@
 by (REPEAT (eresolve_tac [exE,conjE] 1));
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addSEs [sym RS equals0D]) 1);
 val lemma1 = result();
 
 goal thy "!!A. [| f: (PROD X:RepFun(A,p). X); D:A |]  \