summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 09 Nov 2007 19:37:33 +0100 | |

changeset 25364 | 7f012f56efa3 |

parent 25363 | fbdfceb8de15 |

child 25365 | 4e7a1dabd7ef |

tuned proofs -- avoid implicit prems;

--- a/src/HOL/Statespace/DistinctTreeProver.thy Fri Nov 09 19:37:32 2007 +0100 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Fri Nov 09 19:37:33 2007 +0100 @@ -120,7 +120,7 @@ case Tip thus ?case by simp next case (Node l y d r) - have del: "delete x (Node l y d r) = Some t'". + have del: "delete x (Node l y d r) = Some t'" by fact show ?case proof (cases "delete x l") case (Some l') @@ -170,8 +170,8 @@ case Tip thus ?case by simp next case (Node l y d r) - have del: "delete x (Node l y d r) = Some t'". - have "all_distinct (Node l y d r)". + have del: "delete x (Node l y d r) = Some t'" by fact + have "all_distinct (Node l y d r)" by fact then obtain dist_l: "all_distinct l" and dist_r: "all_distinct r" and @@ -243,7 +243,7 @@ case Tip thus ?case by simp next case (Node l y d r) - have del: "delete x (Node l y d r) = Some t'". + have del: "delete x (Node l y d r) = Some t'" by fact show ?case proof (cases "delete x l") case (Some l') @@ -310,7 +310,7 @@ case Tip thus ?case by simp next case (Node l x b r) - have sub: "subtract (Node l x b r) t\<^isub>2 = Some t". + have sub: "subtract (Node l x b r) t\<^isub>2 = Some t" by fact show ?case proof (cases "delete x t\<^isub>2") case (Some t\<^isub>2') @@ -355,7 +355,7 @@ case Tip thus ?case by simp next case (Node l x d r) - have sub: "subtract (Node l x d r) t\<^isub>2 = Some t". + have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact show ?case proof (cases "delete x t\<^isub>2") case (Some t\<^isub>2') @@ -405,8 +405,8 @@ case Tip thus ?case by simp next case (Node l x d r) - have sub: "subtract (Node l x d r) t\<^isub>2 = Some t". - have dist_t2: "all_distinct t\<^isub>2". + have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact + have dist_t2: "all_distinct t\<^isub>2" by fact show ?case proof (cases "delete x t\<^isub>2") case (Some t\<^isub>2') @@ -507,8 +507,8 @@ case Tip thus ?case by simp next case (Node l x d r) - have sub: "subtract (Node l x d r) t\<^isub>2 = Some t". - have dist_t2: "all_distinct t\<^isub>2". + have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact + have dist_t2: "all_distinct t\<^isub>2" by fact show ?case proof (cases "delete x t\<^isub>2") case (Some t\<^isub>2')