File Pointwise.ML

Goalw [PInt_def] "(m PInt empty) = empty";
by (Simp_tac 1);
by (simp_tac (simpset() addsimps [empty_def]) 1);
qed "PInt_empty";
Addsimps [PInt_empty];  


Goalw [dom_def,PInt_def] "dom(m PInt n) = dom n Int dom m";
by(Simp_tac 1);
by (Blast_tac 1);
qed "dom_PInt";
Addsimps [dom_PInt];                                                       

Goalw [PInt_def] "(f PInt g) = (g PInt f)";
by (simp_tac (simpset() addsimps []) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [Int_commute]) 1);
qed "PInt_commute";



Goalw [PUn_def] "(f PUn g) = (g PUn f)";
by (simp_tac (simpset() addsimps [Int_commute]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [Un_commute]) 1);
qed "PUn_commute";




Goalw [dom_def,PUn_def] "dom(m PUn n) = dom n Int dom m";
by(Simp_tac 1);
by (Blast_tac 1);
qed "dom_PUn";
Addsimps [dom_PUn];                                                       



goal Pointwise.thy "(f PInt g) PInt h = f PInt (g PInt h)";
by (simp_tac (simpset() addsimps [PInt_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [if_eq_Some_simp]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "PInt_assoc";

goal Pointwise.thy "(f PUn g) PUn h = f PUn (g PUn h)";
by (simp_tac (simpset() addsimps [PUn_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [if_eq_Some_simp]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "PUn_assoc";
 

goal Pointwise.thy "f PInt (g PUn h) = (f PInt g) PUn (f PInt h)";
by (simp_tac (simpset() addsimps [PInt_def,PUn_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [if_eq_Some_simp]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "distrib_PInt_PUn";

goal Pointwise.thy "f PUn (g PInt h) = (f PUn g) PInt (f PUn h)";
by (simp_tac (simpset() addsimps [PInt_def,PUn_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [if_eq_Some_simp]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "distrib_PUn_PInt";



val prems = goal Pointwise.thy "[| ran(f) <= Pow(A); ran(g) <= Pow(A) |] ==> ran(f PInt g) <= Pow(A)";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [ran_def,PInt_def]) 1);
by (Auto_tac);
by (dres_inst_tac [("c","the (f a)")] subsetD 1);
by (blast_tac (claset() addIs [] addEs []) 2);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (res_inst_tac [("x","a")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
qed "ran_PInt";

(*
val prems = goal Pointwise.thy "[| ran(f) <= Pow(A); ran(g) <= Pow(A) |] ==> ran(f PUn g) <= Pow(A)";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [PUn_def,ran_def]) 1);
by (Auto_tac);
by (dres_inst_tac [("c","the (f a)")] subsetD 1);
by (blast_tac (claset() addIs [] addEs []) 3);
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
by (res_inst_tac [("x","a")] exI 1);
by (Asm_simp_tac 1);
by (resolve_tac [trans] 1);
by (resolve_tac [sym] 2);
by (eresolve_tac [ssubst] 2);
by (Asm_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (rotate_tac 1 1);
by (dres_inst_tac [("c","the (g a)")] subsetD 1);
by (blast_tac (claset() addIs [] addEs []) 2);
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
by (res_inst_tac [("x","a")] exI 1);
by (rotate_tac 1 1);
by (dresolve_tac [exE] 1);
by (Asm_simp_tac 2);
by (resolve_tac [sym RS trans] 1);
by (eresolve_tac [ssubst] 2);
by (Asm_simp_tac 1);
by (simp_tac (simpset() addsimps []) 1);
qed "ran_PUn";

*)

val prems = goal Pointwise.thy "[| x: dom(f); x: dom(g) |] ==> (f PInt g)(x) = (Some ((the (f x)) Int (the (g x))))";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [PInt_def]) 1);
qed "PInt_apply";