equal
deleted
inserted
replaced
59 (*** Leastness of eclose ***) |
59 (*** Leastness of eclose ***) |
60 |
60 |
61 (** eclose(A) is the least transitive set including A as a subset. **) |
61 (** eclose(A) is the least transitive set including A as a subset. **) |
62 |
62 |
63 Goalw [Transset_def] |
63 Goalw [Transset_def] |
64 "!!X A n. [| Transset(X); A<=X; n: nat |] ==> \ |
64 "[| Transset(X); A<=X; n: nat |] ==> \ |
65 \ nat_rec(n, A, %m r. Union(r)) <= X"; |
65 \ nat_rec(n, A, %m r. Union(r)) <= X"; |
66 by (etac nat_induct 1); |
66 by (etac nat_induct 1); |
67 by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1); |
67 by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1); |
68 by (asm_simp_tac (simpset() addsimps [nat_rec_succ]) 1); |
68 by (asm_simp_tac (simpset() addsimps [nat_rec_succ]) 1); |
69 by (Blast_tac 1); |
69 by (Blast_tac 1); |
70 qed "eclose_least_lemma"; |
70 qed "eclose_least_lemma"; |
71 |
71 |
72 Goalw [eclose_def] |
72 Goalw [eclose_def] |
73 "!!X A. [| Transset(X); A<=X |] ==> eclose(A) <= X"; |
73 "[| Transset(X); A<=X |] ==> eclose(A) <= X"; |
74 by (rtac (eclose_least_lemma RS UN_least) 1); |
74 by (rtac (eclose_least_lemma RS UN_least) 1); |
75 by (REPEAT (assume_tac 1)); |
75 by (REPEAT (assume_tac 1)); |
76 qed "eclose_least"; |
76 qed "eclose_least"; |
77 |
77 |
78 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) |
78 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) |
103 by (REPEAT (assume_tac 1)); |
103 by (REPEAT (assume_tac 1)); |
104 qed "mem_eclose_trans"; |
104 qed "mem_eclose_trans"; |
105 |
105 |
106 (*Variant of the previous lemma in a useable form for the sequel*) |
106 (*Variant of the previous lemma in a useable form for the sequel*) |
107 Goal |
107 Goal |
108 "!!A B C. [| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})"; |
108 "[| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})"; |
109 by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1); |
109 by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1); |
110 by (REPEAT (assume_tac 1)); |
110 by (REPEAT (assume_tac 1)); |
111 qed "mem_eclose_sing_trans"; |
111 qed "mem_eclose_sing_trans"; |
112 |
112 |
113 Goalw [Transset_def] |
113 Goalw [Transset_def] |
114 "!!i j. [| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; |
114 "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; |
115 by (blast_tac (claset() addSIs [MemrelI] addSEs [MemrelE]) 1); |
115 by (blast_tac (claset() addSIs [MemrelI] addSEs [MemrelE]) 1); |
116 qed "under_Memrel"; |
116 qed "under_Memrel"; |
117 |
117 |
118 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) |
118 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) |
119 val under_Memrel_eclose = Transset_eclose RS under_Memrel; |
119 val under_Memrel_eclose = Transset_eclose RS under_Memrel; |