src/HOL/AxClasses/Lattice/OrdDefs.ML

isatool fixgoal;

open OrdDefs;


(** lifting of quasi / partial orders **)

(* pairs *)

Goalw [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
  by (rtac conjI 1);
  by (rtac le_refl 1);
  by (rtac le_refl 1);
qed "le_prod_refl";

Goalw [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
  by Safe_tac;
  by (etac (conjI RS (le_trans RS mp)) 1);
  by (assume_tac 1);
  by (etac (conjI RS (le_trans RS mp)) 1);
  by (assume_tac 1);
qed "le_prod_trans";

Goalw [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
  by Safe_tac;
  by (stac Pair_fst_snd_eq 1);
  by (rtac conjI 1);
  by (etac (conjI RS (le_antisym RS mp)) 1);
  by (assume_tac 1);
  by (etac (conjI RS (le_antisym RS mp)) 1);
  by (assume_tac 1);
qed "le_prod_antisym";


(* functions *)

Goalw [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
  by (rtac allI 1);
  by (rtac le_refl 1);
qed "le_fun_refl";

Goalw [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
  by Safe_tac;
  by (rtac (le_trans RS mp) 1);
  by (Fast_tac 1);
qed "le_fun_trans";

Goalw [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
  by Safe_tac;
  by (rtac ext 1);
  by (rtac (le_antisym RS mp) 1);
  by (Fast_tac 1);
qed "le_fun_antisym";



(** duals **)

(*"'a dual" is even an isotype*)
Goal "Rep_dual (Abs_dual y) = y";
  by (rtac Abs_dual_inverse 1);
  by (rewtac dual_def);
  by (Fast_tac 1);
qed "Abs_dual_inverse'";


Goalw [le_dual_def] "x [= (x::'a::quasi_order dual)";
  by (rtac le_refl 1);
qed "le_dual_refl";

Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
  by (stac conj_commut 1);
  by (rtac le_trans 1);
qed "le_dual_trans";

Goalw [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
  by Safe_tac;
  by (rtac (Rep_dual_inverse RS subst) 1);
  by (rtac sym 1);
  by (rtac (Rep_dual_inverse RS subst) 1);
  by (rtac arg_cong 1);
  back();
  by (etac (conjI RS (le_antisym RS mp)) 1);
  by (assume_tac 1);
qed "le_dual_antisym";

Goalw [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
  by (rtac le_linear 1);
qed "le_dual_linear";