author wenzelm Fri Nov 09 19:37:33 2007 +0100 (2007-11-09) changeset 25364 7f012f56efa3 parent 25363 fbdfceb8de15 child 25365 4e7a1dabd7ef
tuned proofs -- avoid implicit prems;
```     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')
```