tuned proofs -- avoid implicit prems;
authorwenzelm
Fri Nov 09 19:37:33 2007 +0100 (2007-11-09)
changeset 253647f012f56efa3
parent 25363 fbdfceb8de15
child 25365 4e7a1dabd7ef
tuned proofs -- avoid implicit prems;
src/HOL/Statespace/DistinctTreeProver.thy
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Fri Nov 09 19:37:32 2007 +0100
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Fri Nov 09 19:37:33 2007 +0100
     1.3 @@ -120,7 +120,7 @@
     1.4    case Tip thus ?case by simp
     1.5  next
     1.6    case (Node l y d r)
     1.7 -  have del: "delete x (Node l y d r) = Some t'".
     1.8 +  have del: "delete x (Node l y d r) = Some t'" by fact
     1.9    show ?case
    1.10    proof (cases "delete x l")
    1.11      case (Some l')
    1.12 @@ -170,8 +170,8 @@
    1.13    case Tip thus ?case by simp
    1.14  next
    1.15    case (Node l y d r)
    1.16 -  have del: "delete x (Node l y d r) = Some t'".
    1.17 -  have "all_distinct (Node l y d r)".
    1.18 +  have del: "delete x (Node l y d r) = Some t'" by fact
    1.19 +  have "all_distinct (Node l y d r)" by fact
    1.20    then obtain
    1.21      dist_l: "all_distinct l" and
    1.22      dist_r: "all_distinct r" and
    1.23 @@ -243,7 +243,7 @@
    1.24    case Tip thus ?case by simp
    1.25  next
    1.26    case (Node l y d r)
    1.27 -  have del: "delete x (Node l y d r) = Some t'".
    1.28 +  have del: "delete x (Node l y d r) = Some t'" by fact
    1.29    show ?case
    1.30    proof (cases "delete x l")
    1.31      case (Some l')
    1.32 @@ -310,7 +310,7 @@
    1.33    case Tip thus ?case by simp
    1.34  next
    1.35    case (Node l x b r)
    1.36 -  have sub: "subtract (Node l x b r) t\<^isub>2 = Some t".
    1.37 +  have sub: "subtract (Node l x b r) t\<^isub>2 = Some t" by fact
    1.38    show ?case
    1.39    proof (cases "delete x t\<^isub>2")
    1.40      case (Some t\<^isub>2')
    1.41 @@ -355,7 +355,7 @@
    1.42    case Tip thus ?case by simp
    1.43  next
    1.44    case (Node l x d r)
    1.45 -  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
    1.46 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
    1.47    show ?case
    1.48    proof (cases "delete x t\<^isub>2")
    1.49      case (Some t\<^isub>2')
    1.50 @@ -405,8 +405,8 @@
    1.51    case Tip thus ?case by simp
    1.52  next
    1.53    case (Node l x d r)
    1.54 -  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
    1.55 -  have dist_t2: "all_distinct t\<^isub>2".
    1.56 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
    1.57 +  have dist_t2: "all_distinct t\<^isub>2" by fact
    1.58    show ?case
    1.59    proof (cases "delete x t\<^isub>2")
    1.60      case (Some t\<^isub>2')
    1.61 @@ -507,8 +507,8 @@
    1.62    case Tip thus ?case by simp
    1.63  next
    1.64    case (Node l x d r)
    1.65 -  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
    1.66 -  have dist_t2: "all_distinct t\<^isub>2".
    1.67 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
    1.68 +  have dist_t2: "all_distinct t\<^isub>2" by fact
    1.69    show ?case
    1.70    proof (cases "delete x t\<^isub>2")
    1.71      case (Some t\<^isub>2')