summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/PiSets.ML

changeset 5521 | 7970832271cc |

parent 5318 | 72bf8039b53f |

child 5845 | eb183b062eae |

--- a/src/HOL/ex/PiSets.ML Mon Sep 21 23:06:37 1998 +0200 +++ b/src/HOL/ex/PiSets.ML Mon Sep 21 23:12:31 1998 +0200 @@ -613,9 +613,7 @@ \ ==> f x = g x"; by (etac equalityE 1); by (rewtac subset_def); -by (dres_inst_tac [("x","(x, f x)")] bspec 1); -by (Fast_tac 1); -by (Fast_tac 1); +by (Auto_tac); val set_eq_lemma = result(); goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)"; @@ -639,64 +637,59 @@ goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B"; by (rtac equalityI 1); -by (afs [image_def] 1); -by (rtac subsetI 1); -by (Asm_full_simp_tac 1); -by (etac bexE 1); -by (etac ssubst 1); -by (afs [PiBij_in_Graph] 1); +by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1); by (rtac subsetI 1); by (afs [image_def] 1); by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1); -by (rtac restrictI_Pi 2); -by (strip 2); -by (rtac ex1E 2); -by (afs [Graph_def] 2); -by (etac conjE 2); -by (dtac bspec 2); -by (assume_tac 2); -by (assume_tac 2); -by (stac select_equality 2); -by (assume_tac 2); -by (Blast_tac 2); + by (rtac restrictI_Pi 2); + by (strip 2); + by (rtac ex1E 2); + by (afs [Graph_def] 2); + by (etac conjE 2); + by (dtac bspec 2); + by (assume_tac 2); + by (assume_tac 2); + by (stac select_equality 2); + by (assume_tac 2); + by (Blast_tac 2); (* gets hung up on by (afs [Graph_def] 2); *) -by (SELECT_GOAL (rewtac Graph_def) 2); -by (Blast_tac 2); + by (SELECT_GOAL (rewtac Graph_def) 2); + by (Blast_tac 2); (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *) by (afs [PiBij_def,Graph_def] 1); by (stac restrictE1 1); -by (rtac restrictI_Pi 1); + by (rtac restrictI_Pi 1); (* again like the old 2. subgoal *) -by (strip 1); -by (rtac ex1E 1); -by (etac conjE 1); -by (dtac bspec 1); -by (assume_tac 1); -by (assume_tac 1); -by (stac select_equality 1); -by (assume_tac 1); -by (Blast_tac 1); -by (Blast_tac 1); + by (strip 1); + by (rtac ex1E 1); + by (etac conjE 1); + by (dtac bspec 1); + by (assume_tac 1); + by (assume_tac 1); + by (stac select_equality 1); + by (assume_tac 1); + by (Blast_tac 1); + by (Blast_tac 1); (* *) by (rtac equalityI 1); by (rtac subsetI 1); -by (rtac CollectI 1); -by (split_all_tac 1); -by (Simp_tac 1); -by (rtac conjI 1); -by (Blast_tac 1); -by (etac conjE 1); -by (dtac subsetD 1); -by (assume_tac 1); -by (dtac SigmaD1 1); -by (dtac bspec 1); -by (assume_tac 1); -by (stac restrictE1 1); -by (assume_tac 1); -by (rtac sym 1); -by (rtac select_equality 1); -by (assume_tac 1); -by (Blast_tac 1); + by (rtac CollectI 1); + by (split_all_tac 1); + by (Simp_tac 1); + by (rtac conjI 1); + by (Blast_tac 1); + by (etac conjE 1); + by (dtac subsetD 1); + by (assume_tac 1); + by (dtac SigmaD1 1); + by (dtac bspec 1); + by (assume_tac 1); + by (stac restrictE1 1); + by (assume_tac 1); + by (rtac sym 1); + by (rtac select_equality 1); + by (assume_tac 1); + by (Blast_tac 1); (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x *) by (rtac subsetI 1); by (Asm_full_simp_tac 1); @@ -706,7 +699,7 @@ by (etac conjE 1); by (afs [restrictE1] 1); by (dtac bspec 1); -by (assume_tac 1); + by (assume_tac 1); by (dtac Ex1_Ex 1); by (rewtac Ex_def); by (assume_tac 1);