wenzelm@1440: 
wenzelm@1440: open OrdDefs;
wenzelm@1440: 
wenzelm@1440: 
wenzelm@1440: (** lifting of quasi / partial orders **)
wenzelm@1440: 
wenzelm@1440: (* pairs *)
wenzelm@1440: 
wenzelm@5069: Goalw [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
paulson@4153:   by (rtac conjI 1);
paulson@4153:   by (rtac le_refl 1);
paulson@4153:   by (rtac le_refl 1);
wenzelm@1440: qed "le_prod_refl";
wenzelm@1440: 
wenzelm@5069: Goalw [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
paulson@4153:   by Safe_tac;
paulson@4153:   by (etac (conjI RS (le_trans RS mp)) 1);
paulson@4153:   by (assume_tac 1);
paulson@4153:   by (etac (conjI RS (le_trans RS mp)) 1);
paulson@4153:   by (assume_tac 1);
wenzelm@1440: qed "le_prod_trans";
wenzelm@1440: 
wenzelm@5069: Goalw [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
paulson@4153:   by Safe_tac;
wenzelm@1440:   by (stac Pair_fst_snd_eq 1);
paulson@4153:   by (rtac conjI 1);
paulson@4153:   by (etac (conjI RS (le_antisym RS mp)) 1);
paulson@4153:   by (assume_tac 1);
paulson@4153:   by (etac (conjI RS (le_antisym RS mp)) 1);
paulson@4153:   by (assume_tac 1);
wenzelm@1440: qed "le_prod_antisym";
wenzelm@1440: 
wenzelm@1440: 
wenzelm@1440: (* functions *)
wenzelm@1440: 
wenzelm@5069: Goalw [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
paulson@4153:   by (rtac allI 1);
paulson@4153:   by (rtac le_refl 1);
wenzelm@1440: qed "le_fun_refl";
wenzelm@1440: 
wenzelm@5069: Goalw [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
paulson@4153:   by Safe_tac;
paulson@4153:   by (rtac (le_trans RS mp) 1);
berghofe@1899:   by (Fast_tac 1);
wenzelm@1440: qed "le_fun_trans";
wenzelm@1440: 
wenzelm@5069: Goalw [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
paulson@4153:   by Safe_tac;
paulson@4153:   by (rtac ext 1);
paulson@4153:   by (rtac (le_antisym RS mp) 1);
berghofe@1899:   by (Fast_tac 1);
wenzelm@1440: qed "le_fun_antisym";
wenzelm@1440: 
wenzelm@1440: 
wenzelm@1440: 
wenzelm@1440: (** duals **)
wenzelm@1440: 
wenzelm@1440: (*"'a dual" is even an isotype*)
wenzelm@5069: Goal "Rep_dual (Abs_dual y) = y";
paulson@4153:   by (rtac Abs_dual_inverse 1);
clasohm@1465:   by (rewtac dual_def);
berghofe@1899:   by (Fast_tac 1);
wenzelm@1440: qed "Abs_dual_inverse'";
wenzelm@1440: 
wenzelm@1440: 
wenzelm@5069: Goalw [le_dual_def] "x [= (x::'a::quasi_order dual)";
paulson@4153:   by (rtac le_refl 1);
wenzelm@1440: qed "le_dual_refl";
wenzelm@1440: 
wenzelm@5069: Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
wenzelm@1440:   by (stac conj_commut 1);
paulson@4153:   by (rtac le_trans 1);
wenzelm@1440: qed "le_dual_trans";
wenzelm@1440: 
wenzelm@5069: Goalw [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
paulson@4153:   by Safe_tac;
paulson@4153:   by (rtac (Rep_dual_inverse RS subst) 1);
paulson@4153:   by (rtac sym 1);
paulson@4153:   by (rtac (Rep_dual_inverse RS subst) 1);
paulson@4153:   by (rtac arg_cong 1);
wenzelm@1440:   back();
paulson@4153:   by (etac (conjI RS (le_antisym RS mp)) 1);
paulson@4153:   by (assume_tac 1);
wenzelm@1440: qed "le_dual_antisym";
wenzelm@1440: 
wenzelm@5069: Goalw [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
paulson@4153:   by (rtac le_linear 1);
wenzelm@2606: qed "le_dual_linear";