equal
deleted
inserted
replaced
71 Goalw [Node_def] "(%k. 0,a) : Node"; |
71 Goalw [Node_def] "(%k. 0,a) : Node"; |
72 by (Blast_tac 1); |
72 by (Blast_tac 1); |
73 qed "Node_K0_I"; |
73 qed "Node_K0_I"; |
74 |
74 |
75 Goalw [Node_def,Push_def] |
75 Goalw [Node_def,Push_def] |
76 "!!p. p: Node ==> apfst (Push i) p : Node"; |
76 "p: Node ==> apfst (Push i) p : Node"; |
77 by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1); |
77 by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1); |
78 qed "Node_Push_I"; |
78 qed "Node_Push_I"; |
79 |
79 |
80 |
80 |
81 (*** Distinctness of constructors ***) |
81 (*** Distinctness of constructors ***) |
487 qed "diagE"; |
487 qed "diagE"; |
488 |
488 |
489 (*** Equality for Cartesian Product ***) |
489 (*** Equality for Cartesian Product ***) |
490 |
490 |
491 Goalw [dprod_def] |
491 Goalw [dprod_def] |
492 "!!r s. [| (M,M'):r; (N,N'):s |] ==> (M$N, M'$N') : r<**>s"; |
492 "[| (M,M'):r; (N,N'):s |] ==> (M$N, M'$N') : r<**>s"; |
493 by (Blast_tac 1); |
493 by (Blast_tac 1); |
494 qed "dprodI"; |
494 qed "dprodI"; |
495 |
495 |
496 (*The general elimination rule*) |
496 (*The general elimination rule*) |
497 val major::prems = goalw Univ.thy [dprod_def] |
497 val major::prems = goalw Univ.thy [dprod_def] |