added simp rules for ==>
authornipkow
Wed Apr 22 12:11:48 2015 +0200 (2015-04-22)
changeset 601432cd31c81e0e7
parent 60138 b11401808dac
child 60144 50eb4fdd5860
added simp rules for ==>
src/HOL/Algebra/Divisibility.thy
src/HOL/Decision_Procs/commutative_ring_tac.ML
src/HOL/HOL.thy
src/HOL/Nominal/Examples/Class2.thy
src/HOL/Proofs/Lambda/WeakNorm.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Apr 19 21:26:50 2015 +0200
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Wed Apr 22 12:11:48 2015 +0200
     1.3 @@ -2038,9 +2038,6 @@
     1.4    using elems
     1.5    unfolding Cs
     1.6      apply (induct Cs', simp)
     1.7 -    apply clarsimp
     1.8 -    apply (subgoal_tac "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and> 
     1.9 -                             multiset_of (map (assocs G) cs) = multiset_of Cs'")
    1.10    proof clarsimp
    1.11      fix a Cs' cs 
    1.12      assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
    1.13 @@ -2060,7 +2057,7 @@
    1.14      show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
    1.15                 multiset_of (map (assocs G) cs) =
    1.16                 multiset_of Cs' + {#a#}" by fast
    1.17 -  qed simp
    1.18 +  qed
    1.19    thus ?thesis by (simp add: fmset_def)
    1.20  qed
    1.21  
     2.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sun Apr 19 21:26:50 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Wed Apr 22 12:11:48 2015 +0200
     2.3 @@ -95,12 +95,12 @@
     2.4    let
     2.5      val cring_ctxt = ctxt addsimps cring_simps;  (*FIXME really the full simpset!?*)
     2.6      val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
     2.7 -    val norm_eq_th =
     2.8 +    val norm_eq_th = (* may collapse to True *)
     2.9        simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
    2.10    in
    2.11      cut_tac norm_eq_th i
    2.12      THEN (simp_tac cring_ctxt i)
    2.13 -    THEN (simp_tac cring_ctxt i)
    2.14 +    THEN TRY(simp_tac cring_ctxt i)
    2.15    end);
    2.16  
    2.17  end;
     3.1 --- a/src/HOL/HOL.thy	Sun Apr 19 21:26:50 2015 +0200
     3.2 +++ b/src/HOL/HOL.thy	Wed Apr 22 12:11:48 2015 +0200
     3.3 @@ -1292,7 +1292,8 @@
     3.4  
     3.5  lemmas [simp] =
     3.6    triv_forall_equality (*prunes params*)
     3.7 -  True_implies_equals  (*prune asms `True'*)
     3.8 +  True_implies_equals implies_True_equals (*prune True in asms*)
     3.9 +  False_implies_equals (*prune False in asms*)
    3.10    if_True
    3.11    if_False
    3.12    if_cancel
     4.1 --- a/src/HOL/Nominal/Examples/Class2.thy	Sun Apr 19 21:26:50 2015 +0200
     4.2 +++ b/src/HOL/Nominal/Examples/Class2.thy	Wed Apr 22 12:11:48 2015 +0200
     4.3 @@ -2865,13 +2865,7 @@
     4.4  using ty_cases sum_cases 
     4.5  apply(auto simp add: ty.inject)
     4.6  apply(drule_tac x="x" in meta_spec)
     4.7 -apply(auto simp add: ty.inject)
     4.8 -apply(rotate_tac 10)
     4.9 -apply(drule_tac x="a" in meta_spec)
    4.10 -apply(auto simp add: ty.inject)
    4.11 -apply(rotate_tac 10)
    4.12 -apply(drule_tac x="a" in meta_spec)
    4.13 -apply(auto simp add: ty.inject)
    4.14 +apply(fastforce simp add: ty.inject)
    4.15  done
    4.16  
    4.17  termination
     5.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Sun Apr 19 21:26:50 2015 +0200
     5.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Apr 22 12:11:48 2015 +0200
     5.3 @@ -173,7 +173,7 @@
     5.4        next
     5.5          assume neq: "x \<noteq> i"
     5.6          from App have "listall ?R ts" by (iprover dest: listall_conj2)
     5.7 -        with TrueI TrueI uNF uT argsT
     5.8 +        with uNF uT argsT
     5.9          have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and>
    5.10            NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
    5.11            by (rule norm_list [of "\<lambda>t. t", simplified])