equal
deleted
inserted
replaced
1 (* Title: HOL/univ |
1 (* Title: HOL/Univ |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 For univ.thy |
6 For univ.thy |
145 goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'"; |
145 goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'"; |
146 by (blast_tac (!claset addSDs [Push_Node_inject]) 1); |
146 by (blast_tac (!claset addSDs [Push_Node_inject]) 1); |
147 qed "Scons_inject_lemma1"; |
147 qed "Scons_inject_lemma1"; |
148 |
148 |
149 goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'"; |
149 goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'"; |
150 by (fast_tac (!claset addSDs [Push_Node_inject]) 1); |
150 by (blast_tac (!claset addSDs [Push_Node_inject]) 1); |
151 qed "Scons_inject_lemma2"; |
151 qed "Scons_inject_lemma2"; |
152 |
152 |
153 val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'"; |
153 val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'"; |
154 by (rtac (major RS equalityE) 1); |
154 by (rtac (major RS equalityE) 1); |
155 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1)); |
155 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1)); |