dropped implicit assumption proof
authorhaftmann
Wed Nov 28 09:01:37 2007 +0100 (2007-11-28)
changeset 254824ed49eccb1eb
parent 25481 aa16cd919dcc
child 25483 65de74f62874
dropped implicit assumption proof
src/HOL/Equiv_Relations.thy
src/HOL/Lattices.thy
src/HOL/Nat.thy
     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 [3] commute [THEN trans, symmetric])
     1.6         apply (rule_tac [5] 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