File Marvin_lemmas.ML

Goal "X <= {b} ==> X = {b} | X = {}";
by (Blast_tac 1);
qed "single_subs_cases";

Goal "A b ==> {b} Int Collect(A) = {b}";
by (Blast_tac 1);
qed "single_int_collect";

Goal "~ A b ==> {b} Int Collect(A) = {}";
by (Blast_tac 1);
qed "not_single_int_collect";


Goal "~ s:dom(f) ==> f(s) = None"; 
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
qed "apply_None";


Goal "[| A ~= {x}; A <= {x} |] ==> A = {}";
by (Blast_tac 1);
qed "single_set_empty";

Goal "[| A Un B = {x}; A <= {x}; B <= {x}|] ==> A = {x} | B = {x}";
by (resolve_tac [ccontr] 1);
by (Asm_full_simp_tac 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (dresolve_tac [single_set_empty] 1);
by (Asm_full_simp_tac 1);
by (dresolve_tac [single_set_empty] 1);
by (Asm_full_simp_tac 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
qed "single_Un";

Goal "a: dom(f) \<Longrightarrow> (f(a) = Some(b)) = (the (f a) = b)";
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
by (dresolve_tac [exE] 1);
by (Asm_full_simp_tac 2);
by (eresolve_tac [ssubst] 1);
by (simp_tac (simpset() addsimps []) 1);

qed "some_the_equiv";


Goal "[| a: dom(f); the (f a) = b |] ==> (f(a)) = Some(b)";
by (asm_full_simp_tac (simpset() addsimps [some_the_equiv]) 1);
qed "some_in_dom";


Goal "(? y. (if P then Some f else None) = Some y) = P";
by (resolve_tac [iffI] 1);
by (resolve_tac [exI] 2);
by (simp_tac (simpset() addsimps []) 2);
by (Asm_simp_tac 2);
by (resolve_tac [ccontr] 1);
by (forward_tac [exE] 1);
by (cut_inst_tac [("P","P"),("x","Some f"),("y","None")] if_not_P 1);
by (eq_assume_tac 1);
by (dresolve_tac [subst] 1);
by (rotate_tac 2 1);
by (assume_tac 1);
by (Asm_simp_tac 2);
by (resolve_tac [notE] 1);
by (rotate_tac 3 2);
by (assume_tac 2);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "if_eq_Some_simp";

Goal "((if P then Some x else None) = Some y) = (P & x = y)";
by (resolve_tac [iffI] 1);
by (forward_tac [conjunct1] 2);
by (dresolve_tac [conjunct2] 2);
by (asm_full_simp_tac (simpset() addsimps [if_P]) 2);
by (case_tac "P" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 2);
by (Asm_simp_tac 2);
by (cut_inst_tac [("P","P"),("x","Some x"),("y","None")] if_not_P 2);
by (eq_assume_tac 2);
by (dresolve_tac [subst] 2);
by (rotate_tac 1 2);
by (assume_tac 2);
by (blast_tac (claset() addIs [] addEs []) 2);
by (asm_full_simp_tac (simpset() addsimps [if_P]) 1);
qed "if_Some_point";



Goal "[| dom f = dom g; ! x : dom f . (f x) = (g x) |] ==> f = g";
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset () addsimps [expand_fun_eq]) 1);
by (Auto_tac);
by (res_inst_tac [("Q","x: dom f")] (excluded_middle RS disjE) 1);
by (Auto_tac);
by (dresolve_tac [ssubst] 1);
by (rotate_tac 1 1);
by (assume_tac 1);
by (asm_full_simp_tac (simpset () addsimps [dom_def]) 1);
qed "expand_partial_fun_eq";