equal
deleted
inserted
replaced
57 by (REPEAT (ares_tac prems 1)); |
57 by (REPEAT (ares_tac prems 1)); |
58 qed "Domain_findRelE"; |
58 qed "Domain_findRelE"; |
59 |
59 |
60 val prems = goal thy |
60 val prems = goal thy |
61 "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"; |
61 "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"; |
62 by (Step_tac 1); |
62 by (Clarify_tac 1); |
63 by (etac findRel.induct 1); |
63 by (etac findRel.induct 1); |
64 by (blast_tac (!claset addIs (findRel.intrs@prems)) 1); |
64 by (blast_tac (!claset addIs (findRel.intrs@prems)) 1); |
65 by (blast_tac (!claset addIs findRel.intrs) 1); |
65 by (blast_tac (!claset addIs findRel.intrs) 1); |
66 qed "Domain_findRel_mono"; |
66 qed "Domain_findRel_mono"; |
67 |
67 |
87 Addsimps [diverge_find_LNil]; |
87 Addsimps [diverge_find_LNil]; |
88 |
88 |
89 goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l"; |
89 goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l"; |
90 by (case_tac "LCons x l : Domain(findRel p)" 1); |
90 by (case_tac "LCons x l : Domain(findRel p)" 1); |
91 by (Asm_full_simp_tac 2); |
91 by (Asm_full_simp_tac 2); |
92 by (Step_tac 1); |
92 by (Clarify_tac 1); |
93 by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1); |
93 by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1); |
94 by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1); |
94 by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1); |
95 qed "find_LCons_seek"; |
95 qed "find_LCons_seek"; |
96 |
96 |
97 goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)"; |
97 goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)"; |
333 by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2); |
333 by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2); |
334 by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3); |
334 by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3); |
335 by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2); |
335 by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2); |
336 by (etac Domain_findRelE 1); |
336 by (etac Domain_findRelE 1); |
337 by (forward_tac [lmap_LCons_findRel] 1); |
337 by (forward_tac [lmap_LCons_findRel] 1); |
338 by (Step_tac 1); |
338 by (Clarify_tac 1); |
339 by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1); |
339 by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1); |
340 by (Blast_tac 1); |
340 by (Blast_tac 1); |
341 qed "lfilter_lmap"; |
341 qed "lfilter_lmap"; |