Asm_full_simp_tac now reorients asm c = t to t = c.
authornipkow
Tue Mar 10 16:47:26 1998 +0100 (1998-03-10)
changeset 4716a291e858061c
parent 4715 245d70532eed
child 4717 1370ad043564
Asm_full_simp_tac now reorients asm c = t to t = c.
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/ex/Hoare.ML
src/Pure/thm.ML
src/ZF/AC/AC7_AC9.ML
     1.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 14:27:44 1998 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 16:47:26 1998 +0100
     1.3 @@ -414,8 +414,6 @@
     1.4  (* nil*)
     1.5  by (strip_tac 1);
     1.6  by (Seq_case_simp_tac "x" 1);
     1.7 -by (hyp_subst_tac 1);
     1.8 -by (Asm_full_simp_tac 1);
     1.9  by (Asm_full_simp_tac 1);
    1.10  (* cons *)
    1.11  by (strip_tac 1);
     2.1 --- a/src/HOLCF/ex/Hoare.ML	Tue Mar 10 14:27:44 1998 +0100
     2.2 +++ b/src/HOLCF/ex/Hoare.ML	Tue Mar 10 16:47:26 1998 +0100
     2.3 @@ -178,7 +178,7 @@
     2.4  
     2.5  val hoare_lemma11 = prove_goal Hoare.thy 
     2.6  "(? n. b1`(iterate n g x) ~= TT) ==>\
     2.7 -\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
     2.8 +\ k=(LEAST n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
     2.9  \ --> p`x = iterate k g x"
    2.10   (fn prems =>
    2.11          [
    2.12 @@ -191,9 +191,6 @@
    2.13          (rtac trans 1),
    2.14          (rtac p_def3 1),
    2.15          (asm_simp_tac HOLCF_ss 1),
    2.16 -        (eres_inst_tac
    2.17 -           [("s","0"),("t","Least(%n. b1`(iterate n g x) ~= TT)")] subst 1),
    2.18 -        (Simp_tac 1),
    2.19          (hyp_subst_tac 1),
    2.20          (strip_tac 1),
    2.21          (etac conjE 1),
     3.1 --- a/src/Pure/thm.ML	Tue Mar 10 14:27:44 1998 +0100
     3.2 +++ b/src/Pure/thm.ML	Tue Mar 10 16:47:26 1998 +0100
     3.3 @@ -1597,8 +1597,8 @@
     3.4    not ((term_tvars erhs) subset
     3.5         (term_tvars elhs  union  List.concat(map term_tvars prems)));
     3.6  
     3.7 -(*simple test for looping rewrite*)
     3.8 -fun looptest sign prems lhs rhs =
     3.9 +(*Simple test for looping rewrite rules and stupid orientations*)
    3.10 +fun reorient sign prems lhs rhs =
    3.11     rewrite_rule_extra_vars prems lhs rhs
    3.12    orelse
    3.13     is_Var (head_of lhs)
    3.14 @@ -1607,10 +1607,11 @@
    3.15    orelse
    3.16     (null prems andalso
    3.17      Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
    3.18 -(*the condition "null prems" in the last cases is necessary because
    3.19 -  conditional rewrites with extra variables in the conditions may terminate
    3.20 -  although the rhs is an instance of the lhs. Example:
    3.21 -  ?m < ?n ==> f(?n) == f(?m)*)
    3.22 +    (*the condition "null prems" is necessary because conditional rewrites
    3.23 +      with extra variables in the conditions may terminate although
    3.24 +      the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
    3.25 +  orelse
    3.26 +   (is_Const lhs andalso not(is_Const rhs))
    3.27  
    3.28  fun decomp_simp(thm as Thm {sign_ref, prop, ...}) =
    3.29    let val sign = Sign.deref sign_ref;
    3.30 @@ -1653,8 +1654,8 @@
    3.31  fun orient_rrule mss thm =
    3.32    let val (sign,prems,lhs,rhs,perm) = decomp_simp thm
    3.33    in if perm then [{thm=thm,lhs=lhs,perm=true}]
    3.34 -     else if looptest sign prems lhs rhs
    3.35 -          then if looptest sign prems rhs lhs
    3.36 +     else if reorient sign prems lhs rhs
    3.37 +          then if reorient sign prems rhs lhs
    3.38                 then mk_eq_True mss thm
    3.39                 else let val Mss{mk_rews={mk_sym,...},...} = mss
    3.40                      in case mk_sym thm of
    3.41 @@ -2052,11 +2053,13 @@
    3.42                     val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1)
    3.43                 in (rrules1, lhss1, mss1) end
    3.44  
    3.45 -        fun rebuild(conc2,(shyps2,hyps2,ders2)) =
    3.46 +        fun disch1(conc2,(shyps2,hyps2,ders2)) =
    3.47            let val hyps2' = if gen_mem (op aconv) (prem1, hyps1)
    3.48                             then hyps2 else hyps2\prem1
    3.49 -              val trec = (Logic.mk_implies(prem1,conc2),
    3.50 -                          (shyps2,hyps2',ders2))
    3.51 +          in (Logic.mk_implies(prem1,conc2),(shyps2,hyps2',ders2)) end
    3.52 +
    3.53 +        fun rebuild trec2 =
    3.54 +          let val trec = disch1 trec2
    3.55            in case rewritec (prover,sign_ref,maxidx) mss trec of
    3.56                 None => (None,trec)
    3.57               | Some(Const("==>",_)$prem$conc,etc) =>
    3.58 @@ -2068,10 +2071,10 @@
    3.59            case conc of
    3.60              Const("==>",_)$s$t =>
    3.61                (case impc(prems@[prem1],s,t,mss1,etc1) of
    3.62 -                 (Some(i,prem),(conc2,etc2)) =>
    3.63 -                    let val impl = Logic.mk_implies(prem1,conc2)
    3.64 -                    in if i=0 then impc1(prems,prem,impl,mss,etc2)
    3.65 -                       else (Some(i-1,prem),(impl,etc2))
    3.66 +                 (Some(i,prem),trec2) =>
    3.67 +                    let val trec2' = disch1 trec2
    3.68 +                    in if i=0 then impc1(prems,prem,fst trec2',mss,snd trec2')
    3.69 +                       else (Some(i-1,prem),trec2')
    3.70                      end
    3.71                 | (None,trec) => rebuild(trec))
    3.72            | _ => rebuild(try_botc mss1 (conc,etc1))
     4.1 --- a/src/ZF/AC/AC7_AC9.ML	Tue Mar 10 14:27:44 1998 +0100
     4.2 +++ b/src/ZF/AC/AC7_AC9.ML	Tue Mar 10 16:47:26 1998 +0100
     4.3 @@ -140,7 +140,6 @@
     4.4  by (REPEAT (eresolve_tac [exE,conjE] 1));
     4.5  by (hyp_subst_tac 1);
     4.6  by (Asm_full_simp_tac 1);
     4.7 -by (fast_tac (claset() addSEs [sym RS equals0D]) 1);
     4.8  val lemma1 = result();
     4.9  
    4.10  goal thy "!!A. [| f: (PROD X:RepFun(A,p). X); D:A |]  \