author nipkow Wed Apr 22 12:11:48 2015 +0200 (2015-04-22) changeset 60143 2cd31c81e0e7 parent 60138 b11401808dac child 60144 50eb4fdd5860
 src/HOL/Algebra/Divisibility.thy file | annotate | diff | revisions src/HOL/Decision_Procs/commutative_ring_tac.ML file | annotate | diff | revisions src/HOL/HOL.thy file | annotate | diff | revisions src/HOL/Nominal/Examples/Class2.thy file | annotate | diff | revisions src/HOL/Proofs/Lambda/WeakNorm.thy file | annotate | diff | revisions
```     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.6  apply(drule_tac x="x" in meta_spec)
4.8 -apply(rotate_tac 10)
4.9 -apply(drule_tac x="a" in meta_spec)
4.11 -apply(rotate_tac 10)
4.12 -apply(drule_tac x="a" in meta_spec)
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])
```