File Pred.ML

goal Pred.thy "bnds(P && Q) =(bnds(P) Int bnds(Q))";
by (simp_tac (simpset() addsimps [bnds_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "bnds_land";



Goal "bnds(lnot P) = UNIV - bnds(P)";
by (simp_tac (simpset() addsimps [bnds_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "bnds_lnot";

(*
goal Pred.thy "bnds(lnot P) = (Compl(bnds(P)))";
by (simp_tac (simpset() addsimps [bnds_def,lnot_def]) 1);
by (simp_tac (simpset() addsimps [Collect_mem_eq]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "bnds_lnot";
*)


goal Pred.thy "bnds(p1 <=> p2) = (bnds(p1) Int bnds(p2)) Un (UNIV - (bnds(p1) Un bnds(p2)))";
by (simp_tac (simpset() addsimps [bnds_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "bnds_equiv";


goal Pred.thy "bnds(p1 || p2) = (bnds(p1) Un bnds(p2)) ";
by (simp_tac (simpset() addsimps [bnds_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "bnds_lor";



goal Pred.thy "bnds(p1 => p2) = ((UNIV - (bnds(p1))) Un bnds(p2)) ";
by (simp_tac (simpset() addsimps [bnds_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "bnds_implies";


(*
val [prem1] = goal Pred.thy "[| !! b. (p1 <=> p2)(b) |] ==> bnds(p1) = bnds(p2)";
by (asm_full_simp_tac (simpset() addsimps [prem1,equiv_def,bnds_def]) 1);
by (resolve_tac [Collect_cong] 1);
by (Asm_simp_tac 1);
by (cut_facts_tac [prem1] 1);
by (asm_full_simp_tac (simpset() addsimps [equiv_def]) 1);
qed "equiv_bnds_eq";
*)

val prems = goal Pred.thy "|[P <=> Q]| ==> bnds(P) = bnds(Q)";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [everywhere_def,bnds_def]) 1);
qed "bnds_equiv_every_eq";



val prems = goal Pred.thy "|[P => Q]| ==> bnds(P) <= bnds(Q)";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [everywhere_def,bnds_def]) 1);
by (resolve_tac [subsetI] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "bnds_implies_subset";

(*
val prems = goal Pred.thy "[| v:Var_set; x:Val; b: Bnds_set |] ==> (b (+) {v |--> x}) : Bnds_set";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [Bnds_set_def]) 1);
by (resolve_tac [override_single_total_function] 1);
by (eq_assume_tac 1);
by (eq_assume_tac 1);
by (eq_assume_tac 1);
qed "override_bindings";   *)

Goal "entails A P ==> |[A]| --> |[P]|";
by (asm_full_simp_tac (simpset() addsimps [entails_def,everywhere_def]) 1);
qed "entails_everywhere_imp";

Goal "|[P]| ==> entails A P";
by (asm_full_simp_tac (simpset() addsimps [entails_def,everywhere_def]) 1);
qed "remove_context";


Goal "[|entails S T; entails T U|] ==> entails S U";
by (asm_full_simp_tac (simpset() addsimps [entails_def]) 1);
qed "entails_trans";

Goal "[| entails X A; entails X B |] ==> entails X (A && B)";
by (asm_full_simp_tac (simpset() addsimps [entails_def]) 1);
qed "entails_and";

(*
Goal "|[A && B]| = |[A ]| & |[ B]|"; 
by (simp_tac (simpset() addsimps [everywhere_def]) 1);
by (Blast_tac 1);
qed "everywhere_and";
*)

Goal "[|entails A B; |[A]| |] ==> |[B]|";
by (asm_full_simp_tac (simpset() addsimps [entails_def,everywhere_def]) 1);
qed "everywhere_mp";


Goal "|[ A => B ]| = entails A B"; 
by (asm_full_simp_tac (simpset() addsimps [entails_def,everywhere_def]) 1);
qed "entails_everywhere";

Goal "entails A (B => C) = entails (A && B) C";
by (simp_tac (simpset() addsimps [entails_def]) 1);
by (Blast_tac 1);
qed "entails_implies";

Goal "entails A B ==> entails (A && C) B";
by (asm_full_simp_tac (simpset() addsimps [entails_def]) 1);
qed "entails_landE1";

Goal "entails A B ==> entails (C && A) B";
by (asm_full_simp_tac (simpset() addsimps [entails_def]) 1);
qed "entails_landE2";

Addsimps [entails_implies];


Goal "[| entails T U; entails S T |] ==> entails S U";
by (asm_full_simp_tac (simpset() addsimps [entails_def]) 1);
qed "entails_trans2";