author haftmann Wed Nov 28 09:01:37 2007 +0100 (2007-11-28) changeset 25482 4ed49eccb1eb parent 25481 aa16cd919dcc child 25483 65de74f62874
dropped implicit assumption proof
 src/HOL/Equiv_Relations.thy file | annotate | diff | revisions src/HOL/Lattices.thy file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/Equiv_Relations.thy	Wed Nov 28 09:01:34 2007 +0100
1.2 +++ b/src/HOL/Equiv_Relations.thy	Wed Nov 28 09:01:37 2007 +0100
1.3 @@ -288,7 +288,7 @@
1.4     apply (rule commute [THEN trans])
1.5       apply (rule_tac  commute [THEN trans, symmetric])
1.6         apply (rule_tac  sym)
1.7 -       apply (assumption | rule congt |
1.8 +       apply (rule congt | assumption |
1.9           erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
1.10    done
1.11

     2.1 --- a/src/HOL/Lattices.thy	Wed Nov 28 09:01:34 2007 +0100
2.2 +++ b/src/HOL/Lattices.thy	Wed Nov 28 09:01:37 2007 +0100
2.3 @@ -39,7 +39,8 @@
2.4    assumes "a \<sqsubseteq> x"
2.5    shows "a \<sqinter> b \<sqsubseteq> x"
2.6  proof (rule order_trans)
2.7 -  show "a \<sqinter> b \<sqsubseteq> a" and "a \<sqsubseteq> x" using assms by simp
2.8 +  from assms show "a \<sqsubseteq> x" .
2.9 +  show "a \<sqinter> b \<sqsubseteq> a" by simp
2.10  qed
2.11  lemmas (in -) [rule del] = le_infI1
2.12
2.13 @@ -47,7 +48,8 @@
2.14    assumes "b \<sqsubseteq> x"
2.15    shows "a \<sqinter> b \<sqsubseteq> x"
2.16  proof (rule order_trans)
2.17 -  show "a \<sqinter> b \<sqsubseteq> b" and "b \<sqsubseteq> x" using assms by simp
2.18 +  from assms show "b \<sqsubseteq> x" .
2.19 +  show "a \<sqinter> b \<sqsubseteq> b" by simp
2.20  qed
2.21  lemmas (in -) [rule del] = le_infI2
2.22

     3.1 --- a/src/HOL/Nat.thy	Wed Nov 28 09:01:34 2007 +0100
3.2 +++ b/src/HOL/Nat.thy	Wed Nov 28 09:01:37 2007 +0100
3.3 @@ -813,20 +813,20 @@
3.4  \item case smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
3.5  \end{itemize}
3.6  NB: the proof also shows how to use the previous lemma. *}
3.7 -corollary infinite_descent0_measure[case_names 0 smaller]:
3.8 -assumes 0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
3.9 -and     1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
3.10 -shows "P x"
3.11 +corollary infinite_descent0_measure [case_names 0 smaller]:
3.12 +  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
3.13 +    and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
3.14 +  shows "P x"
3.15  proof -
3.16    obtain n where "n = V x" by auto
3.17 -  moreover have "!!x. V x = n \<Longrightarrow> P x"
3.18 +  moreover have "\<And>x. V x = n \<Longrightarrow> P x"
3.19    proof (induct n rule: infinite_descent0)
3.20      case 0 -- "i.e. $V(x) = 0$"
3.21 -    with 0 show "P x" by auto
3.22 +    with A0 show "P x" by auto
3.23    next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
3.24      case (smaller n)
3.25      then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
3.26 -    with 1 obtain y where "V y < V x \<and> \<not> P y" by auto
3.27 +    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
3.28      with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
3.29      thus ?case by auto
3.30    qed