equal
deleted
inserted
replaced
83 by (asm_full_simp_tac (simpset() addsimps [cons_val_k]) 1); |
83 by (asm_full_simp_tac (simpset() addsimps [cons_val_k]) 1); |
84 qed "restrict_cons_eq"; |
84 qed "restrict_cons_eq"; |
85 |
85 |
86 Goal "[| Ord(k); i:k |] ==> succ(i) : succ(k)"; |
86 Goal "[| Ord(k); i:k |] ==> succ(i) : succ(k)"; |
87 by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3)); |
87 by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3)); |
88 by (REPEAT (fast_tac (claset() addSIs [Ord_succ] |
88 by (REPEAT (fast_tac (claset() addEs [Ord_in_Ord, mem_irrefl, mem_asym]) 1)); |
89 addEs [Ord_in_Ord, mem_irrefl, mem_asym] |
|
90 addSDs [succ_inject]) 1)); |
|
91 qed "succ_in_succ"; |
89 qed "succ_in_succ"; |
92 |
90 |
93 Goalw [restrict_def] |
91 Goalw [restrict_def] |
94 "[| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; |
92 "[| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; |
95 by (etac subst 1); |
93 by (etac subst 1); |