Changes of HOLCF from Oscar Slotosch:
1. axclass instead of class
* less instead of
less_fun,
less_cfun,
less_sprod,
less_cprod,
less_ssum,
less_up,
less_lift
* @x.!y.x<<y instead of UUU instead of
UU_fun, UU_cfun, ...
* no witness type void needed (eliminated Void.thy.Void.ML)
* inst_<typ>_<class> derived as theorems
2. improved some proves on less_sprod and less_cprod
* eliminated the following theorems
Sprod1.ML: less_sprod1a
Sprod1.ML: less_sprod1b
Sprod1.ML: less_sprod2a
Sprod1.ML: less_sprod2b
Sprod1.ML: less_sprod2c
Sprod2.ML: less_sprod3a
Sprod2.ML: less_sprod3b
Sprod2.ML: less_sprod4b
Sprod2.ML: less_sprod4c
Sprod3.ML: less_sprod5b
Sprod3.ML: less_sprod5c
Cprod1.ML: less_cprod1b
Cprod1.ML: less_cprod2a
Cprod1.ML: less_cprod2b
Cprod1.ML: less_cprod2c
Cprod2.ML: less_cprod3a
Cprod2.ML: less_cprod3b
3. new classes:
* cpo<po,
* chfin<pcpo,
* flat<pcpo,
* derived: flat<chfin
to do: show instances for lift
4. Data Type One
* Used lift for the definition: one = unit lift
* Changed the constant one into ONE
5. Data Type Tr
* Used lift for the definition: tr = bool lift
* adopted definitions of if,andalso,orelse,neg
* only one theory Tr.thy,Tr.ML instead of
Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML
* reintroduced ceils for =TT,=FF
6. typedef
* Using typedef instead of faking type definitions
to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun
7. adopted examples and domain construct to theses changes
These changes eliminated all rules and arities from HOLCF
(* Title: HOLCF/Porder.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Lemmas for theory Porder.thy
*)
open Porder;
(* ------------------------------------------------------------------------ *)
(* the reverse law of anti--symmetrie of << *)
(* ------------------------------------------------------------------------ *)
qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac conjI 1),
((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
]);
qed_goal "box_less" thy
"[| a << b; c << a; b << d|] ==> c << d"
(fn prems =>
[
(cut_facts_tac prems 1),
(etac trans_less 1),
(etac trans_less 1),
(atac 1)
]);
(* ------------------------------------------------------------------------ *)
(* lubs are unique *)
(* ------------------------------------------------------------------------ *)
qed_goalw "unique_lub "thy [is_lub, is_ub]
"[| S <<| x ; S <<| y |] ==> x=y"
( fn prems =>
[
(cut_facts_tac prems 1),
(etac conjE 1),
(etac conjE 1),
(rtac antisym_less 1),
(rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)),
(rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1))
]);
(* ------------------------------------------------------------------------ *)
(* chains are monotone functions *)
(* ------------------------------------------------------------------------ *)
qed_goalw "chain_mono" thy [is_chain] "is_chain F ==> x<y --> F x<<F y"
( fn prems =>
[
(cut_facts_tac prems 1),
(nat_ind_tac "y" 1),
(rtac impI 1),
(etac less_zeroE 1),
(stac less_Suc_eq 1),
(strip_tac 1),
(etac disjE 1),
(rtac trans_less 1),
(etac allE 2),
(atac 2),
(fast_tac HOL_cs 1),
(hyp_subst_tac 1),
(etac allE 1),
(atac 1)
]);
qed_goal "chain_mono3" thy "[| is_chain F; x <= y |] ==> F x << F y"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac (le_imp_less_or_eq RS disjE) 1),
(atac 1),
(etac (chain_mono RS mp) 1),
(atac 1),
(hyp_subst_tac 1),
(rtac refl_less 1)
]);
(* ------------------------------------------------------------------------ *)
(* The range of a chain is a totaly ordered << *)
(* ------------------------------------------------------------------------ *)
qed_goalw "chain_is_tord" thy [is_tord]
"!!F. is_chain(F) ==> is_tord(range(F))"
(fn _ =>
[
(Step_tac 1),
(rtac nat_less_cases 1),
(ALLGOALS (fast_tac (!claset addIs [refl_less, chain_mono RS mp])))]);
(* ------------------------------------------------------------------------ *)
(* technical lemmas about lub and is_lub *)
(* ------------------------------------------------------------------------ *)
bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
qed_goal "lubI" thy "? x. M <<| x ==> M <<| lub(M)"
(fn prems =>
[
(cut_facts_tac prems 1),
(stac lub 1),
(etac (select_eq_Ex RS iffD2) 1)
]);
qed_goal "lubE" thy "M <<| lub(M) ==> ? x. M <<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
(etac exI 1)
]);
qed_goal "lub_eq" thy "(? x. M <<| x) = M <<| lub(M)"
(fn prems =>
[
(stac lub 1),
(rtac (select_eq_Ex RS subst) 1),
(rtac refl 1)
]);
qed_goal "thelubI" thy "M <<| l ==> lub(M) = l"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac unique_lub 1),
(stac lub 1),
(etac selectI 1),
(atac 1)
]);
(* ------------------------------------------------------------------------ *)
(* access to some definition as inference rule *)
(* ------------------------------------------------------------------------ *)
qed_goalw "is_lubE" thy [is_lub]
"S <<| x ==> S <| x & (! u. S <| u --> x << u)"
(fn prems =>
[
(cut_facts_tac prems 1),
(atac 1)
]);
qed_goalw "is_lubI" thy [is_lub]
"S <| x & (! u. S <| u --> x << u) ==> S <<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
(atac 1)
]);
qed_goalw "is_chainE" thy [is_chain] "is_chain F ==> !i. F(i) << F(Suc(i))"
(fn prems =>
[
(cut_facts_tac prems 1),
(atac 1)]);
qed_goalw "is_chainI" thy [is_chain] "!i. F i << F(Suc i) ==> is_chain F"
(fn prems =>
[
(cut_facts_tac prems 1),
(atac 1)]);
(* ------------------------------------------------------------------------ *)
(* technical lemmas about (least) upper bounds of chains *)
(* ------------------------------------------------------------------------ *)
qed_goalw "ub_rangeE" thy [is_ub] "range S <| x ==> !i. S(i) << x"
(fn prems =>
[
(cut_facts_tac prems 1),
(strip_tac 1),
(rtac mp 1),
(etac spec 1),
(rtac rangeI 1)
]);
qed_goalw "ub_rangeI" thy [is_ub] "!i. S i << x ==> range S <| x"
(fn prems =>
[
(cut_facts_tac prems 1),
(strip_tac 1),
(etac rangeE 1),
(hyp_subst_tac 1),
(etac spec 1)
]);
bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)
bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp);
(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *)
(* ------------------------------------------------------------------------ *)
(* results about finite chains *)
(* ------------------------------------------------------------------------ *)
qed_goalw "lub_finch1" thy [max_in_chain_def]
"[| is_chain C; max_in_chain i C|] ==> range C <<| C i"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac is_lubI 1),
(rtac conjI 1),
(rtac ub_rangeI 1),
(rtac allI 1),
(res_inst_tac [("m","i")] nat_less_cases 1),
(rtac (antisym_less_inverse RS conjunct2) 1),
(etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1),
(etac spec 1),
(rtac (antisym_less_inverse RS conjunct2) 1),
(etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1),
(etac spec 1),
(etac (chain_mono RS mp) 1),
(atac 1),
(strip_tac 1),
(etac (ub_rangeE RS spec) 1)
]);
qed_goalw "lub_finch2" thy [finite_chain_def]
"finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)"
(fn prems=>
[
(cut_facts_tac prems 1),
(rtac lub_finch1 1),
(etac conjunct1 1),
(rtac (select_eq_Ex RS iffD2) 1),
(etac conjunct2 1)
]);
qed_goal "bin_chain" thy "x<<y ==> is_chain (%i. if i=0 then x else y)"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac is_chainI 1),
(rtac allI 1),
(nat_ind_tac "i" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(rtac refl_less 1)
]);
qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def]
"x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac allI 1),
(nat_ind_tac "j" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1)
]);
qed_goal "lub_bin_chain" thy
"x << y ==> range(%i. if (i=0) then x else y) <<| y"
(fn prems=>
[ (cut_facts_tac prems 1),
(res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1),
(rtac lub_finch1 2),
(etac bin_chain 2),
(etac bin_chainmax 2),
(Simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
(* the maximal element in a chain is its lub *)
(* ------------------------------------------------------------------------ *)
qed_goal "lub_chain_maxelem" thy
"[|? i.Y i=c;!i.Y i<<c|] ==> lub(range Y) = c"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac thelubI 1),
(rtac is_lubI 1),
(rtac conjI 1),
(etac ub_rangeI 1),
(strip_tac 1),
(etac exE 1),
(hyp_subst_tac 1),
(etac (ub_rangeE RS spec) 1)
]);
(* ------------------------------------------------------------------------ *)
(* the lub of a constant chain is the constant *)
(* ------------------------------------------------------------------------ *)
qed_goal "lub_const" thy "range(%x.c) <<| c"
(fn prems =>
[
(rtac is_lubI 1),
(rtac conjI 1),
(rtac ub_rangeI 1),
(strip_tac 1),
(rtac refl_less 1),
(strip_tac 1),
(etac (ub_rangeE RS spec) 1)
]);