src/HOL/AxClasses/Lattice/CLattice.ML

New record type of programs

open CLattice;


(** basic properties of "Inf" and "Sup" **)

(* unique existence *)

Goalw [Inf_def] "is_Inf A (Inf A)";
  by (rtac (ex_Inf RS spec RS selectI1) 1);
qed "Inf_is_Inf";

Goal "is_Inf A inf --> Inf A = inf";
  by (rtac impI 1);
  by (rtac (is_Inf_uniq RS mp) 1);
  by (rtac conjI 1);
  by (rtac Inf_is_Inf 1);
  by (assume_tac 1);
qed "Inf_uniq";

Goalw [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
  by Safe_tac;
  by (Step_tac 1);
  by (Step_tac 1);
  by (rtac Inf_is_Inf 1);
  by (rtac (Inf_uniq RS mp RS sym) 1);
  by (assume_tac 1);
qed "ex1_Inf";


Goalw [Sup_def] "is_Sup A (Sup A)";
  by (rtac (ex_Sup RS spec RS selectI1) 1);
qed "Sup_is_Sup";

Goal "is_Sup A sup --> Sup A = sup";
  by (rtac impI 1);
  by (rtac (is_Sup_uniq RS mp) 1);
  by (rtac conjI 1);
  by (rtac Sup_is_Sup 1);
  by (assume_tac 1);
qed "Sup_uniq";

Goalw [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
  by Safe_tac;
  by (Step_tac 1);
  by (Step_tac 1);
  by (rtac Sup_is_Sup 1);
  by (rtac (Sup_uniq RS mp RS sym) 1);
  by (assume_tac 1);
qed "ex1_Sup";


(* "Inf" yields g.l.bs, "Sup" yields l.u.bs. --- in pieces *)

val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
  by (cut_facts_tac prems 1);
  by (rtac selectI2 1);
  by (rtac Inf_is_Inf 1);
  by (rewtac is_Inf_def);
  by (Fast_tac 1);
qed "Inf_lb";

val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
  by (rtac selectI2 1);
  by (rtac Inf_is_Inf 1);
  by (rewtac is_Inf_def);
  by (Step_tac 1);
  by (Step_tac 1);
  by (etac mp 1);
  by (rtac ballI 1);
  by (etac prem 1);
qed "Inf_ub_lbs";


val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
  by (cut_facts_tac prems 1);
  by (rtac selectI2 1);
  by (rtac Sup_is_Sup 1);
  by (rewtac is_Sup_def);
  by (Fast_tac 1);
qed "Sup_ub";

val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
  by (rtac selectI2 1);
  by (rtac Sup_is_Sup 1);
  by (rewtac is_Sup_def);
  by (Step_tac 1);
  by (Step_tac 1);
  by (etac mp 1);
  by (rtac ballI 1);
  by (etac prem 1);
qed "Sup_lb_ubs";


(** minorized Infs / majorized Sups **)

Goal "(x [= Inf A) = (ALL y:A. x [= y)";
  by (rtac iffI 1);
  (*==>*)
    by (rtac ballI 1);
    by (rtac (le_trans RS mp) 1);
    by (etac conjI 1);
    by (etac Inf_lb 1);
  (*<==*)
    by (rtac Inf_ub_lbs 1);
    by (Fast_tac 1);
qed "le_Inf_eq";

Goal "(Sup A [= x) = (ALL y:A. y [= x)";
  by (rtac iffI 1);
  (*==>*)
    by (rtac ballI 1);
    by (rtac (le_trans RS mp) 1);
    by (rtac conjI 1);
    by (etac Sup_ub 1);
    by (assume_tac 1);
  (*<==*)
    by (rtac Sup_lb_ubs 1);
    by (Fast_tac 1);
qed "ge_Sup_eq";



(** Subsets and limits **)

Goal "A <= B --> Inf B [= Inf A";
  by (rtac impI 1);
  by (stac le_Inf_eq 1);
  by (rewtac Ball_def);
  by Safe_tac;
  by (dtac subsetD 1);
  by (assume_tac 1);
  by (etac Inf_lb 1);
qed "Inf_subset_antimon";

Goal "A <= B --> Sup A [= Sup B";
  by (rtac impI 1);
  by (stac ge_Sup_eq 1);
  by (rewtac Ball_def);
  by Safe_tac;
  by (dtac subsetD 1);
  by (assume_tac 1);
  by (etac Sup_ub 1);
qed "Sup_subset_mon";


(** singleton / empty limits **)

Goal "Inf {x} = x";
  by (rtac (Inf_uniq RS mp) 1);
  by (rewtac is_Inf_def);
  by Safe_tac;
  by (rtac le_refl 1);
  by (Fast_tac 1);
qed "sing_Inf_eq";

Goal "Sup {x} = x";
  by (rtac (Sup_uniq RS mp) 1);
  by (rewtac is_Sup_def);
  by Safe_tac;
  by (rtac le_refl 1);
  by (Fast_tac 1);
qed "sing_Sup_eq";


Goal "Inf {} = Sup {x. True}";
  by (rtac (Inf_uniq RS mp) 1);
  by (rewtac is_Inf_def);
  by Safe_tac;
  by (rtac (sing_Sup_eq RS subst) 1);
  back();
  by (rtac (Sup_subset_mon RS mp) 1);
  by (Fast_tac 1);
qed "empty_Inf_eq";

Goal "Sup {} = Inf {x. True}";
  by (rtac (Sup_uniq RS mp) 1);
  by (rewtac is_Sup_def);
  by Safe_tac;
  by (rtac (sing_Inf_eq RS subst) 1);
  by (rtac (Inf_subset_antimon RS mp) 1);
  by (Fast_tac 1);
qed "empty_Sup_eq";