src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
changeset 53374 a14d2a854c02
parent 53072 acc495621d72
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -54,7 +54,8 @@
     1.4    sorted_single [code_pred_intro]
     1.5    sorted_many [code_pred_intro]
     1.6  
     1.7 -code_pred sorted proof -
     1.8 +code_pred sorted
     1.9 +proof -
    1.10    assume "sorted xa"
    1.11    assume 1: "xa = [] \<Longrightarrow> thesis"
    1.12    assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
    1.13 @@ -65,9 +66,12 @@
    1.14      case (Cons x xs) show ?thesis proof (cases xs)
    1.15        case Nil with Cons 2 show ?thesis by simp
    1.16      next
    1.17 -      case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
    1.18 -      moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
    1.19 -      ultimately show ?thesis by (rule 3)
    1.20 +      case (Cons y zs)
    1.21 +      show ?thesis
    1.22 +      proof (rule 3)
    1.23 +        from Cons `xa = x # xs` show "xa = x # y # zs" by simp
    1.24 +        with `sorted xa` show "x \<le> y" and "sorted (y # zs)" by simp_all
    1.25 +      qed
    1.26      qed
    1.27    qed
    1.28  qed