(* Title: HOLCF/Porder
ID: $Id$
Author: Franz Regensburger
License: GPL (GNU GENERAL PUBLIC LICENSE)
Conservative extension of theory Porder0 by constant definitions
*)
(* ------------------------------------------------------------------------ *)
(* lubs are unique *)
(* ------------------------------------------------------------------------ *)
Goalw [is_lub_def, is_ub_def]
"[| S <<| x ; S <<| y |] ==> x=y";
by (blast_tac (claset() addIs [antisym_less]) 1);
qed "unique_lub";
(* ------------------------------------------------------------------------ *)
(* chains are monotone functions *)
(* ------------------------------------------------------------------------ *)
Goalw [chain_def] "chain F ==> x<y --> F x<<F y";
by (induct_tac "y" 1);
by Auto_tac;
by (blast_tac (claset() addIs [trans_less]) 2);
by (blast_tac (claset() addSEs [less_SucE]) 1);
qed_spec_mp "chain_mono";
Goal "[| chain F; x <= y |] ==> F x << F y";
by (dtac le_imp_less_or_eq 1);
by (blast_tac (claset() addIs [chain_mono]) 1);
qed "chain_mono3";
(* ------------------------------------------------------------------------ *)
(* The range of a chain is a totally ordered << *)
(* ------------------------------------------------------------------------ *)
Goalw [tord_def] "chain(F) ==> tord(range(F))";
by Safe_tac;
by (rtac nat_less_cases 1);
by (ALLGOALS (fast_tac (claset() addIs [chain_mono])));
qed "chain_tord";
(* ------------------------------------------------------------------------ *)
(* technical lemmas about lub and is_lub *)
(* ------------------------------------------------------------------------ *)
bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
Goal "EX x. M <<| x ==> M <<| lub(M)";
by (asm_full_simp_tac (simpset() addsimps [lub, some_eq_ex]) 1);
bind_thm ("lubI", exI RS result());
Goal "M <<| l ==> lub(M) = l";
by (rtac unique_lub 1);
by (stac lub 1);
by (etac someI 1);
by (atac 1);
qed "thelubI";
Goal "lub{x} = x";
by (simp_tac (simpset() addsimps [thelubI,is_lub_def,is_ub_def]) 1);
qed "lub_singleton";
Addsimps [lub_singleton];
(* ------------------------------------------------------------------------ *)
(* access to some definition as inference rule *)
(* ------------------------------------------------------------------------ *)
Goalw [is_lub_def] "S <<| x ==> S <| x";
by Auto_tac;
qed "is_lubD1";
Goalw [is_lub_def] "[| S <<| x; S <| u |] ==> x << u";
by Auto_tac;
qed "is_lub_lub";
val prems = Goalw [is_lub_def]
"[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x";
by (blast_tac (claset() addIs prems) 1);
qed "is_lubI";
Goalw [chain_def] "chain F ==> F(i) << F(Suc(i))";
by Auto_tac;
qed "chainE";
val prems = Goalw [chain_def] "(!!i. F i << F(Suc i)) ==> chain F";
by (blast_tac (claset() addIs prems) 1);
qed "chainI";
Goal "chain Y ==> chain (%i. Y (i + j))";
by (rtac chainI 1);
by (Clarsimp_tac 1);
by (etac chainE 1);
qed "chain_shift";
(* ------------------------------------------------------------------------ *)
(* technical lemmas about (least) upper bounds of chains *)
(* ------------------------------------------------------------------------ *)
Goalw [is_ub_def] "range S <| x ==> S(i) << x";
by (Blast_tac 1);
qed "ub_rangeD";
val prems = Goalw [is_ub_def] "(!!i. S i << x) ==> range S <| x";
by (blast_tac (claset() addIs prems) 1);
qed "ub_rangeI";
bind_thm ("is_ub_lub", is_lubD1 RS ub_rangeD);
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)
(* ------------------------------------------------------------------------ *)
(* results about finite chains *)
(* ------------------------------------------------------------------------ *)
Goalw [max_in_chain_def]
"[| chain C; max_in_chain i C|] ==> range C <<| C i";
by (rtac is_lubI 1);
by (rtac ub_rangeI 1);
by (res_inst_tac [("m","i")] nat_less_cases 1);
by (rtac (antisym_less_inverse RS conjunct2) 1);
by (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1);
by (etac spec 1);
by (rtac (antisym_less_inverse RS conjunct2) 1);
by (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1);
by (etac spec 1);
by (etac chain_mono 1);
by (atac 1);
by (etac (ub_rangeD) 1);
qed "lub_finch1";
Goalw [finite_chain_def]
"finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)";
by (rtac lub_finch1 1);
by (best_tac (claset() addIs [someI]) 2);
by (Blast_tac 1);
qed "lub_finch2";
Goal "x<<y ==> chain (%i. if i=0 then x else y)";
by (rtac chainI 1);
by (induct_tac "i" 1);
by Auto_tac;
qed "bin_chain";
Goalw [max_in_chain_def,le_def]
"x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)";
by (rtac allI 1);
by (induct_tac "j" 1);
by Auto_tac;
qed "bin_chainmax";
Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y";
by (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1
THEN rtac lub_finch1 2);
by (etac bin_chain 2);
by (etac bin_chainmax 2);
by (Simp_tac 1);
qed "lub_bin_chain";
(* ------------------------------------------------------------------------ *)
(* the maximal element in a chain is its lub *)
(* ------------------------------------------------------------------------ *)
Goal "[| Y i = c; ALL i. Y i<<c |] ==> lub(range Y) = c";
by (blast_tac (claset() addDs [ub_rangeD]
addIs [thelubI, is_lubI, ub_rangeI]) 1);
qed "lub_chain_maxelem";
(* ------------------------------------------------------------------------ *)
(* the lub of a constant chain is the constant *)
(* ------------------------------------------------------------------------ *)
Goal "range(%x. c) <<| c";
by (blast_tac (claset() addDs [ub_rangeD] addIs [is_lubI, ub_rangeI]) 1);
qed "lub_const";