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.11 +    Author:     Konrad Slind
    1.12 +    Author:     Alexander Krauss
    1.13  *)
    1.14  
    1.15  header {*Well-founded Recursion*}
    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