src/HOL/Wellfounded.thy
 changeset 32960 69916a850301 parent 32704 6f0a56d255f4 child 33215 6fd85372981e
```     1.1 --- a/src/HOL/Wellfounded.thy	Sat Oct 17 01:05:59 2009 +0200
1.2 +++ b/src/HOL/Wellfounded.thy	Sat Oct 17 14:43:18 2009 +0200
1.3 @@ -1,7 +1,8 @@
1.4 -(*  Author:     Tobias Nipkow
1.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.6 -    Author:     Konrad Slind, Alexander Krauss
1.7 -    Copyright   1992-2008  University of Cambridge and TU Muenchen
1.8 +(*  Title:      HOL/Wellfounded.thy
1.9 +    Author:     Tobias Nipkow
1.10 +    Author:     Lawrence C Paulson
1.12 +    Author:     Alexander Krauss
1.13  *)
1.14
1.16 @@ -94,21 +95,21 @@
1.17        fix y assume "(y, x) : r^+"
1.18        with `wf r` show "P y"
1.19        proof (induct x arbitrary: y)
1.20 -	case (less x)
1.21 -	note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'`
1.22 -	from `(y, x) : r^+` show "P y"
1.23 -	proof cases
1.24 -	  case base
1.25 -	  show "P y"
1.26 -	  proof (rule induct_step)
1.27 -	    fix y' assume "(y', y) : r^+"
1.28 -	    with `(y, x) : r` show "P y'" by (rule hyp [of y y'])
1.29 -	  qed
1.30 -	next
1.31 -	  case step
1.32 -	  then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp
1.33 -	  then show "P y" by (rule hyp [of x' y])
1.34 -	qed
1.35 +        case (less x)
1.36 +        note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'`
1.37 +        from `(y, x) : r^+` show "P y"
1.38 +        proof cases
1.39 +          case base
1.40 +          show "P y"
1.41 +          proof (rule induct_step)
1.42 +            fix y' assume "(y', y) : r^+"
1.43 +            with `(y, x) : r` show "P y'" by (rule hyp [of y y'])
1.44 +          qed
1.45 +        next
1.46 +          case step
1.47 +          then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp
1.48 +          then show "P y" by (rule hyp [of x' y])
1.49 +        qed
1.50        qed
1.51      qed
1.52    } then show ?thesis unfolding wf_def by blast
```