--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Dlist.ML Thu Mar 24 13:43:45 1994 +0100
@@ -0,0 +1,563 @@
+(* Title: HOLCF/dlist.ML
+ Author: Franz Regensburger
+ ID: $ $
+ Copyright 1994 Technische Universitaet Muenchen
+
+Lemmas for dlist.thy
+*)
+
+open Dlist;
+
+(* ------------------------------------------------------------------------*)
+(* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict *)
+(* ------------------------------------------------------------------------*)
+
+val dlist_iso_strict= dlist_rep_iso RS (dlist_abs_iso RS
+ (allI RSN (2,allI RS iso_strict)));
+
+val dlist_rews = [dlist_iso_strict RS conjunct1,
+ dlist_iso_strict RS conjunct2];
+
+(* ------------------------------------------------------------------------*)
+(* Properties of dlist_copy *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goalw Dlist.thy [dlist_copy_def] "dlist_copy[f][UU]=UU"
+ (fn prems =>
+ [
+ (asm_simp_tac (HOLCF_ss addsimps
+ (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
+ ]);
+
+val dlist_copy = [temp];
+
+
+val temp = prove_goalw Dlist.thy [dlist_copy_def,dnil_def]
+ "dlist_copy[f][dnil]=dnil"
+ (fn prems =>
+ [
+ (asm_simp_tac (HOLCF_ss addsimps
+ (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
+ ]);
+
+val dlist_copy = temp :: dlist_copy;
+
+
+val temp = prove_goalw Dlist.thy [dlist_copy_def,dcons_def]
+ "xl~=UU ==> dlist_copy[f][dcons[x][xl]]= dcons[x][f[xl]]"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps
+ (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps [defined_spair]) 1)
+ ]);
+
+val dlist_copy = temp :: dlist_copy;
+
+val dlist_rews = dlist_copy @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Exhaustion and elimination for dlists *)
+(* ------------------------------------------------------------------------*)
+
+val Exh_dlist = prove_goalw Dlist.thy [dcons_def,dnil_def]
+ "l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons[x][xl])"
+ (fn prems =>
+ [
+ (simp_tac HOLCF_ss 1),
+ (rtac (dlist_rep_iso RS subst) 1),
+ (res_inst_tac [("p","dlist_rep[l]")] ssumE 1),
+ (rtac disjI1 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (rtac disjI2 1),
+ (rtac disjI1 1),
+ (res_inst_tac [("p","x")] oneE 1),
+ (contr_tac 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (rtac disjI2 1),
+ (rtac disjI2 1),
+ (res_inst_tac [("p","y")] sprodE 1),
+ (contr_tac 1),
+ (rtac exI 1),
+ (rtac exI 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+
+val dlistE = prove_goal Dlist.thy
+"[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons[x][xl];x~=UU;xl~=UU|]==>Q|]==>Q"
+ (fn prems =>
+ [
+ (rtac (Exh_dlist RS disjE) 1),
+ (eresolve_tac prems 1),
+ (etac disjE 1),
+ (eresolve_tac prems 1),
+ (etac exE 1),
+ (etac exE 1),
+ (resolve_tac prems 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+(* ------------------------------------------------------------------------*)
+(* Properties of dlist_when *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goalw Dlist.thy [dlist_when_def] "dlist_when[f1][f2][UU]=UU"
+ (fn prems =>
+ [
+ (asm_simp_tac (HOLCF_ss addsimps [dlist_iso_strict]) 1)
+ ]);
+
+val dlist_when = [temp];
+
+val temp = prove_goalw Dlist.thy [dlist_when_def,dnil_def]
+ "dlist_when[f1][f2][dnil]= f1"
+ (fn prems =>
+ [
+ (asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso]) 1)
+ ]);
+
+val dlist_when = temp::dlist_when;
+
+val temp = prove_goalw Dlist.thy [dlist_when_def,dcons_def]
+ "[|x~=UU;xl~=UU|] ==> dlist_when[f1][f2][dcons[x][xl]]= f2[x][xl]"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso,defined_spair]) 1)
+ ]);
+
+val dlist_when = temp::dlist_when;
+
+val dlist_rews = dlist_when @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Rewrites for discriminators and selectors *)
+(* ------------------------------------------------------------------------*)
+
+fun prover defs thm = prove_goalw Dlist.thy defs thm
+ (fn prems =>
+ [
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_discsel = [
+ prover [is_dnil_def] "is_dnil[UU]=UU",
+ prover [is_dcons_def] "is_dcons[UU]=UU",
+ prover [dhd_def] "dhd[UU]=UU",
+ prover [dtl_def] "dtl[UU]=UU"
+ ];
+
+fun prover defs thm = prove_goalw Dlist.thy defs thm
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_discsel = [
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "is_dnil[dnil]=TT",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "[|x~=UU;xl~=UU|] ==> is_dnil[dcons[x][xl]]=FF",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "is_dcons[dnil]=FF",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "[|x~=UU;xl~=UU|] ==> is_dcons[dcons[x][xl]]=TT",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "dhd[dnil]=UU",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "[|x~=UU;xl~=UU|] ==> dhd[dcons[x][xl]]=x",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "dtl[dnil]=UU",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "[|x~=UU;xl~=UU|] ==> dtl[dcons[x][xl]]=xl"] @ dlist_discsel;
+
+val dlist_rews = dlist_discsel @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Definedness and strictness *)
+(* ------------------------------------------------------------------------*)
+
+fun prover contr thm = prove_goal Dlist.thy thm
+ (fn prems =>
+ [
+ (res_inst_tac [("P1",contr)] classical3 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (dtac sym 1),
+ (asm_simp_tac HOLCF_ss 1),
+ (simp_tac (HOLCF_ss addsimps (prems @ dlist_rews)) 1)
+ ]);
+
+
+val dlist_constrdef = [
+prover "is_dnil[UU] ~= UU" "dnil~=UU",
+prover "is_dcons[UU] ~= UU" "[|x~=UU;xl~=UU|] ==> dcons[x][xl]~=UU"
+ ];
+
+
+fun prover defs thm = prove_goalw Dlist.thy defs thm
+ (fn prems =>
+ [
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_constrdef = [
+ prover [dcons_def] "dcons[UU][xl]=UU",
+ prover [dcons_def] "dcons[x][UU]=UU"
+ ] @ dlist_constrdef;
+
+val dlist_rews = dlist_constrdef @ dlist_rews;
+
+
+(* ------------------------------------------------------------------------*)
+(* Distinctness wrt. << and = *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goal Dlist.thy "~dnil << dcons[x][xl]"
+ (fn prems =>
+ [
+ (res_inst_tac [("P1","TT << FF")] classical3 1),
+ (resolve_tac dist_less_tr 1),
+ (dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_dist_less = [temp];
+
+val temp = prove_goal Dlist.thy "[|x~=UU;xl~=UU|]==>~dcons[x][xl] << dnil"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (res_inst_tac [("P1","TT << FF")] classical3 1),
+ (resolve_tac dist_less_tr 1),
+ (dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_dist_less = temp::dlist_dist_less;
+
+val temp = prove_goal Dlist.thy "dnil ~= dcons[x][xl]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("P1","TT = FF")] classical3 1),
+ (resolve_tac dist_eq_tr 1),
+ (dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
+ (etac box_equals 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_dist_eq = [temp,temp RS not_sym];
+
+val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Invertibility *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
+\ dcons[x1][x2] << dcons[y1][y2]|] ==> x1<< y1 & x2 << y2"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac conjI 1),
+ (dres_inst_tac [("fo5","dlist_when[UU][LAM x l.x]")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (dres_inst_tac [("fo5","dlist_when[UU][LAM x l.l]")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
+ ]);
+
+val dlist_invert =[temp];
+
+(* ------------------------------------------------------------------------*)
+(* Injectivity *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
+\ dcons[x1][x2] = dcons[y1][y2]|] ==> x1= y1 & x2 = y2"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac conjI 1),
+ (dres_inst_tac [("f","dlist_when[UU][LAM x l.x]")] cfun_arg_cong 1),
+ (etac box_equals 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (dres_inst_tac [("f","dlist_when[UU][LAM x l.l]")] cfun_arg_cong 1),
+ (etac box_equals 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
+ ]);
+
+val dlist_inject = [temp];
+
+
+(* ------------------------------------------------------------------------*)
+(* definedness for discriminators and selectors *)
+(* ------------------------------------------------------------------------*)
+
+fun prover thm = prove_goal Dlist.thy thm
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac dlistE 1),
+ (contr_tac 1),
+ (REPEAT (asm_simp_tac (HOLCF_ss addsimps dlist_discsel) 1))
+ ]);
+
+val dlist_discsel_def =
+ [
+ prover "l~=UU ==> is_dnil[l]~=UU",
+ prover "l~=UU ==> is_dcons[l]~=UU"
+ ];
+
+val dlist_rews = dlist_discsel_def @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* enhance the simplifier *)
+(* ------------------------------------------------------------------------*)
+
+val dhd2 = prove_goal Dlist.thy "xl~=UU ==> dhd[dcons[x][xl]]=x"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dtl2 = prove_goal Dlist.thy "x~=UU ==> dtl[dcons[x][xl]]=xl"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Properties dlist_take *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take(n)[UU]=UU"
+ (fn prems =>
+ [
+ (res_inst_tac [("n","n")] natE 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac iterate_ss 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_take = [temp];
+
+val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take(0)[xs]=UU"
+ (fn prems =>
+ [
+ (asm_simp_tac iterate_ss 1)
+ ]);
+
+val dlist_take = temp::dlist_take;
+
+val temp = prove_goalw Dlist.thy [dlist_take_def]
+ "dlist_take(Suc(n))[dnil]=dnil"
+ (fn prems =>
+ [
+ (asm_simp_tac iterate_ss 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_take = temp::dlist_take;
+
+val temp = prove_goalw Dlist.thy [dlist_take_def]
+ "dlist_take(Suc(n))[dcons[x][xl]]=dcons[x][dlist_take(n)[xl]]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("n","n")] natE 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_take = temp::dlist_take;
+
+val dlist_rews = dlist_take @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* take lemma for dlists *)
+(* ------------------------------------------------------------------------*)
+
+fun prover reach defs thm = prove_goalw Dlist.thy defs thm
+ (fn prems =>
+ [
+ (res_inst_tac [("t","l1")] (reach RS subst) 1),
+ (res_inst_tac [("t","l2")] (reach RS subst) 1),
+ (rtac (fix_def2 RS ssubst) 1),
+ (rtac (contlub_cfun_fun RS ssubst) 1),
+ (rtac is_chain_iterate 1),
+ (rtac (contlub_cfun_fun RS ssubst) 1),
+ (rtac is_chain_iterate 1),
+ (rtac lub_equal 1),
+ (rtac (is_chain_iterate RS ch2ch_fappL) 1),
+ (rtac (is_chain_iterate RS ch2ch_fappL) 1),
+ (rtac allI 1),
+ (resolve_tac prems 1)
+ ]);
+
+val dlist_take_lemma = prover dlist_reach [dlist_take_def]
+ "(!!n.dlist_take(n)[l1]=dlist_take(n)[l2]) ==> l1=l2";
+
+
+(* ------------------------------------------------------------------------*)
+(* Co -induction for dlists *)
+(* ------------------------------------------------------------------------*)
+
+val dlist_coind_lemma = prove_goalw Dlist.thy [dlist_bisim_def]
+"dlist_bisim(R) ==> ! p q.R(p,q) --> dlist_take(n)[p]=dlist_take(n)[q]"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (strip_tac 1),
+ ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
+ (atac 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (etac disjE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (etac exE 1),
+ (etac exE 1),
+ (etac exE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (REPEAT (etac conjE 1)),
+ (rtac cfun_arg_cong 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+val dlist_coind = prove_goal Dlist.thy "[|dlist_bisim(R);R(p,q)|] ==> p = q"
+ (fn prems =>
+ [
+ (rtac dlist_take_lemma 1),
+ (rtac (dlist_coind_lemma RS spec RS spec RS mp) 1),
+ (resolve_tac prems 1),
+ (resolve_tac prems 1)
+ ]);
+
+(* ------------------------------------------------------------------------*)
+(* structural induction *)
+(* ------------------------------------------------------------------------*)
+
+val dlist_finite_ind = prove_goal Dlist.thy
+"[|P(UU);P(dnil);\
+\ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])\
+\ |] ==> !l.P(dlist_take(n)[l])"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (resolve_tac prems 1),
+ (rtac allI 1),
+ (res_inst_tac [("l","l")] dlistE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","dlist_take(n1)[xl]=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (resolve_tac prems 1),
+ (resolve_tac prems 1),
+ (atac 1),
+ (atac 1),
+ (etac spec 1)
+ ]);
+
+val dlist_all_finite_lemma1 = prove_goal Dlist.thy
+"!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (rtac allI 1),
+ (res_inst_tac [("l","l")] dlistE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (eres_inst_tac [("x","xl")] allE 1),
+ (etac disjE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_all_finite_lemma2 = prove_goal Dlist.thy "? n.dlist_take(n)[l]=l"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","l=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (subgoal_tac "(!n.dlist_take(n)[l]=UU) |(? n.dlist_take(n)[l]=l)" 1),
+ (etac disjE 1),
+ (eres_inst_tac [("P","l=UU")] notE 1),
+ (rtac dlist_take_lemma 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (atac 1),
+ (subgoal_tac "!n.!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l" 1),
+ (fast_tac HOL_cs 1),
+ (rtac allI 1),
+ (rtac dlist_all_finite_lemma1 1)
+ ]);
+
+val dlist_all_finite= prove_goalw Dlist.thy [dlist_finite_def] "dlist_finite(l)"
+ (fn prems =>
+ [
+ (rtac dlist_all_finite_lemma2 1)
+ ]);
+
+val dlist_ind = prove_goal Dlist.thy
+"[|P(UU);P(dnil);\
+\ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])|] ==> P(l)"
+ (fn prems =>
+ [
+ (rtac (dlist_all_finite_lemma2 RS exE) 1),
+ (etac subst 1),
+ (rtac (dlist_finite_ind RS spec) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
+ ]);
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Dlist.thy Thu Mar 24 13:43:45 1994 +0100
@@ -0,0 +1,111 @@
+(* Title: HOLCF/dlist.thy
+
+ Author: Franz Regensburger
+ ID: $ $
+ Copyright 1994 Technische Universitaet Muenchen
+
+Theory for lists
+*)
+
+Dlist = Stream2 +
+
+types dlist 1
+
+(* ----------------------------------------------------------------------- *)
+(* arity axiom is validated by semantic reasoning *)
+(* partial ordering is implicit in the isomorphism axioms and their cont. *)
+
+arities dlist::(pcpo)pcpo
+
+consts
+
+(* ----------------------------------------------------------------------- *)
+(* essential constants *)
+
+dlist_rep :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
+dlist_abs :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
+
+(* ----------------------------------------------------------------------- *)
+(* abstract constants and auxiliary constants *)
+
+dlist_copy :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
+
+dnil :: "'a dlist"
+dcons :: "'a -> 'a dlist -> 'a dlist"
+dlist_when :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
+is_dnil :: "'a dlist -> tr"
+is_dcons :: "'a dlist -> tr"
+dhd :: "'a dlist -> 'a"
+dtl :: "'a dlist -> 'a dlist"
+dlist_take :: "nat => 'a dlist -> 'a dlist"
+dlist_finite :: "'a dlist => bool"
+dlist_bisim :: "('a dlist => 'a dlist => bool) => bool"
+
+rules
+
+(* ----------------------------------------------------------------------- *)
+(* axiomatization of recursive type 'a dlist *)
+(* ----------------------------------------------------------------------- *)
+(* ('a dlist,dlist_abs) is the initial F-algebra where *)
+(* F is the locally continuous functor determined by domain equation *)
+(* X = one ++ 'a ** X *)
+(* ----------------------------------------------------------------------- *)
+(* dlist_abs is an isomorphism with inverse dlist_rep *)
+(* identity is the least endomorphism on 'a dlist *)
+
+dlist_abs_iso "dlist_rep[dlist_abs[x]] = x"
+dlist_rep_iso "dlist_abs[dlist_rep[x]] = x"
+dlist_copy_def "dlist_copy == (LAM f. dlist_abs oo \
+\ (when[sinl][sinr oo (ssplit[LAM x y. x ## f[y]])])\
+\ oo dlist_rep)"
+dlist_reach "(fix[dlist_copy])[x]=x"
+
+(* ----------------------------------------------------------------------- *)
+(* properties of additional constants *)
+(* ----------------------------------------------------------------------- *)
+(* constructors *)
+
+dnil_def "dnil == dlist_abs[sinl[one]]"
+dcons_def "dcons == (LAM x l. dlist_abs[sinr[x##l]])"
+
+(* ----------------------------------------------------------------------- *)
+(* discriminator functional *)
+
+dlist_when_def
+"dlist_when == (LAM f1 f2 l.\
+\ when[LAM x.f1][ssplit[LAM x l.f2[x][l]]][dlist_rep[l]])"
+
+(* ----------------------------------------------------------------------- *)
+(* discriminators and selectors *)
+
+is_dnil_def "is_dnil == dlist_when[TT][LAM x l.FF]"
+is_dcons_def "is_dcons == dlist_when[FF][LAM x l.TT]"
+dhd_def "dhd == dlist_when[UU][LAM x l.x]"
+dtl_def "dtl == dlist_when[UU][LAM x l.l]"
+
+(* ----------------------------------------------------------------------- *)
+(* the taker for dlists *)
+
+dlist_take_def "dlist_take == (%n.iterate(n,dlist_copy,UU))"
+
+(* ----------------------------------------------------------------------- *)
+
+dlist_finite_def "dlist_finite == (%s.? n.dlist_take(n)[s]=s)"
+
+(* ----------------------------------------------------------------------- *)
+(* definition of bisimulation is determined by domain equation *)
+(* simplification and rewriting for abstract constants yields def below *)
+
+dlist_bisim_def "dlist_bisim ==\
+\ ( %R.!l1 l2.\
+\ R(l1,l2) -->\
+\ ((l1=UU & l2=UU) |\
+\ (l1=dnil & l2=dnil) |\
+\ (? x l11 l21. x~=UU & l11~=UU & l21~=UU & \
+\ l1=dcons[x][l11] & l2 = dcons[x][l21] & R(l11,l21))))"
+
+end
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Porder0.thy Thu Mar 24 13:43:45 1994 +0100
@@ -0,0 +1,42 @@
+(* Title: HOLCF/porder0.thy
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Definition of class porder (partial order)
+
+The prototype theory for this class is void.thy
+
+*)
+
+Porder0 = Void +
+
+(* Introduction of new class. The witness is type void. *)
+
+classes po < term
+
+(* default type is still term ! *)
+(* void is the prototype in po *)
+
+arities void :: po
+
+consts "<<" :: "['a,'a::po] => bool" (infixl 55)
+
+rules
+
+(* class axioms: justification is theory Void *)
+
+refl_less "x << x"
+ (* witness refl_less_void *)
+
+antisym_less "[|x<<y ; y<<x |] ==> x = y"
+ (* witness antisym_less_void *)
+
+trans_less "[|x<<y ; y<<z |] ==> x<<z"
+ (* witness trans_less_void *)
+
+(* instance of << for the prototype void *)
+
+inst_void_po "(op <<)::[void,void]=>bool = less_void"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/dlist.ML Thu Mar 24 13:43:45 1994 +0100
@@ -0,0 +1,563 @@
+(* Title: HOLCF/dlist.ML
+ Author: Franz Regensburger
+ ID: $ $
+ Copyright 1994 Technische Universitaet Muenchen
+
+Lemmas for dlist.thy
+*)
+
+open Dlist;
+
+(* ------------------------------------------------------------------------*)
+(* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict *)
+(* ------------------------------------------------------------------------*)
+
+val dlist_iso_strict= dlist_rep_iso RS (dlist_abs_iso RS
+ (allI RSN (2,allI RS iso_strict)));
+
+val dlist_rews = [dlist_iso_strict RS conjunct1,
+ dlist_iso_strict RS conjunct2];
+
+(* ------------------------------------------------------------------------*)
+(* Properties of dlist_copy *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goalw Dlist.thy [dlist_copy_def] "dlist_copy[f][UU]=UU"
+ (fn prems =>
+ [
+ (asm_simp_tac (HOLCF_ss addsimps
+ (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
+ ]);
+
+val dlist_copy = [temp];
+
+
+val temp = prove_goalw Dlist.thy [dlist_copy_def,dnil_def]
+ "dlist_copy[f][dnil]=dnil"
+ (fn prems =>
+ [
+ (asm_simp_tac (HOLCF_ss addsimps
+ (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
+ ]);
+
+val dlist_copy = temp :: dlist_copy;
+
+
+val temp = prove_goalw Dlist.thy [dlist_copy_def,dcons_def]
+ "xl~=UU ==> dlist_copy[f][dcons[x][xl]]= dcons[x][f[xl]]"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps
+ (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps [defined_spair]) 1)
+ ]);
+
+val dlist_copy = temp :: dlist_copy;
+
+val dlist_rews = dlist_copy @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Exhaustion and elimination for dlists *)
+(* ------------------------------------------------------------------------*)
+
+val Exh_dlist = prove_goalw Dlist.thy [dcons_def,dnil_def]
+ "l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons[x][xl])"
+ (fn prems =>
+ [
+ (simp_tac HOLCF_ss 1),
+ (rtac (dlist_rep_iso RS subst) 1),
+ (res_inst_tac [("p","dlist_rep[l]")] ssumE 1),
+ (rtac disjI1 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (rtac disjI2 1),
+ (rtac disjI1 1),
+ (res_inst_tac [("p","x")] oneE 1),
+ (contr_tac 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (rtac disjI2 1),
+ (rtac disjI2 1),
+ (res_inst_tac [("p","y")] sprodE 1),
+ (contr_tac 1),
+ (rtac exI 1),
+ (rtac exI 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+
+val dlistE = prove_goal Dlist.thy
+"[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons[x][xl];x~=UU;xl~=UU|]==>Q|]==>Q"
+ (fn prems =>
+ [
+ (rtac (Exh_dlist RS disjE) 1),
+ (eresolve_tac prems 1),
+ (etac disjE 1),
+ (eresolve_tac prems 1),
+ (etac exE 1),
+ (etac exE 1),
+ (resolve_tac prems 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+(* ------------------------------------------------------------------------*)
+(* Properties of dlist_when *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goalw Dlist.thy [dlist_when_def] "dlist_when[f1][f2][UU]=UU"
+ (fn prems =>
+ [
+ (asm_simp_tac (HOLCF_ss addsimps [dlist_iso_strict]) 1)
+ ]);
+
+val dlist_when = [temp];
+
+val temp = prove_goalw Dlist.thy [dlist_when_def,dnil_def]
+ "dlist_when[f1][f2][dnil]= f1"
+ (fn prems =>
+ [
+ (asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso]) 1)
+ ]);
+
+val dlist_when = temp::dlist_when;
+
+val temp = prove_goalw Dlist.thy [dlist_when_def,dcons_def]
+ "[|x~=UU;xl~=UU|] ==> dlist_when[f1][f2][dcons[x][xl]]= f2[x][xl]"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso,defined_spair]) 1)
+ ]);
+
+val dlist_when = temp::dlist_when;
+
+val dlist_rews = dlist_when @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Rewrites for discriminators and selectors *)
+(* ------------------------------------------------------------------------*)
+
+fun prover defs thm = prove_goalw Dlist.thy defs thm
+ (fn prems =>
+ [
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_discsel = [
+ prover [is_dnil_def] "is_dnil[UU]=UU",
+ prover [is_dcons_def] "is_dcons[UU]=UU",
+ prover [dhd_def] "dhd[UU]=UU",
+ prover [dtl_def] "dtl[UU]=UU"
+ ];
+
+fun prover defs thm = prove_goalw Dlist.thy defs thm
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_discsel = [
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "is_dnil[dnil]=TT",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "[|x~=UU;xl~=UU|] ==> is_dnil[dcons[x][xl]]=FF",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "is_dcons[dnil]=FF",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "[|x~=UU;xl~=UU|] ==> is_dcons[dcons[x][xl]]=TT",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "dhd[dnil]=UU",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "[|x~=UU;xl~=UU|] ==> dhd[dcons[x][xl]]=x",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "dtl[dnil]=UU",
+prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
+ "[|x~=UU;xl~=UU|] ==> dtl[dcons[x][xl]]=xl"] @ dlist_discsel;
+
+val dlist_rews = dlist_discsel @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Definedness and strictness *)
+(* ------------------------------------------------------------------------*)
+
+fun prover contr thm = prove_goal Dlist.thy thm
+ (fn prems =>
+ [
+ (res_inst_tac [("P1",contr)] classical3 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (dtac sym 1),
+ (asm_simp_tac HOLCF_ss 1),
+ (simp_tac (HOLCF_ss addsimps (prems @ dlist_rews)) 1)
+ ]);
+
+
+val dlist_constrdef = [
+prover "is_dnil[UU] ~= UU" "dnil~=UU",
+prover "is_dcons[UU] ~= UU" "[|x~=UU;xl~=UU|] ==> dcons[x][xl]~=UU"
+ ];
+
+
+fun prover defs thm = prove_goalw Dlist.thy defs thm
+ (fn prems =>
+ [
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_constrdef = [
+ prover [dcons_def] "dcons[UU][xl]=UU",
+ prover [dcons_def] "dcons[x][UU]=UU"
+ ] @ dlist_constrdef;
+
+val dlist_rews = dlist_constrdef @ dlist_rews;
+
+
+(* ------------------------------------------------------------------------*)
+(* Distinctness wrt. << and = *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goal Dlist.thy "~dnil << dcons[x][xl]"
+ (fn prems =>
+ [
+ (res_inst_tac [("P1","TT << FF")] classical3 1),
+ (resolve_tac dist_less_tr 1),
+ (dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_dist_less = [temp];
+
+val temp = prove_goal Dlist.thy "[|x~=UU;xl~=UU|]==>~dcons[x][xl] << dnil"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (res_inst_tac [("P1","TT << FF")] classical3 1),
+ (resolve_tac dist_less_tr 1),
+ (dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_dist_less = temp::dlist_dist_less;
+
+val temp = prove_goal Dlist.thy "dnil ~= dcons[x][xl]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("P1","TT = FF")] classical3 1),
+ (resolve_tac dist_eq_tr 1),
+ (dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
+ (etac box_equals 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_dist_eq = [temp,temp RS not_sym];
+
+val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Invertibility *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
+\ dcons[x1][x2] << dcons[y1][y2]|] ==> x1<< y1 & x2 << y2"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac conjI 1),
+ (dres_inst_tac [("fo5","dlist_when[UU][LAM x l.x]")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (dres_inst_tac [("fo5","dlist_when[UU][LAM x l.l]")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
+ ]);
+
+val dlist_invert =[temp];
+
+(* ------------------------------------------------------------------------*)
+(* Injectivity *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
+\ dcons[x1][x2] = dcons[y1][y2]|] ==> x1= y1 & x2 = y2"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac conjI 1),
+ (dres_inst_tac [("f","dlist_when[UU][LAM x l.x]")] cfun_arg_cong 1),
+ (etac box_equals 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (dres_inst_tac [("f","dlist_when[UU][LAM x l.l]")] cfun_arg_cong 1),
+ (etac box_equals 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
+ ]);
+
+val dlist_inject = [temp];
+
+
+(* ------------------------------------------------------------------------*)
+(* definedness for discriminators and selectors *)
+(* ------------------------------------------------------------------------*)
+
+fun prover thm = prove_goal Dlist.thy thm
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac dlistE 1),
+ (contr_tac 1),
+ (REPEAT (asm_simp_tac (HOLCF_ss addsimps dlist_discsel) 1))
+ ]);
+
+val dlist_discsel_def =
+ [
+ prover "l~=UU ==> is_dnil[l]~=UU",
+ prover "l~=UU ==> is_dcons[l]~=UU"
+ ];
+
+val dlist_rews = dlist_discsel_def @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* enhance the simplifier *)
+(* ------------------------------------------------------------------------*)
+
+val dhd2 = prove_goal Dlist.thy "xl~=UU ==> dhd[dcons[x][xl]]=x"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dtl2 = prove_goal Dlist.thy "x~=UU ==> dtl[dcons[x][xl]]=xl"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Properties dlist_take *)
+(* ------------------------------------------------------------------------*)
+
+val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take(n)[UU]=UU"
+ (fn prems =>
+ [
+ (res_inst_tac [("n","n")] natE 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac iterate_ss 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_take = [temp];
+
+val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take(0)[xs]=UU"
+ (fn prems =>
+ [
+ (asm_simp_tac iterate_ss 1)
+ ]);
+
+val dlist_take = temp::dlist_take;
+
+val temp = prove_goalw Dlist.thy [dlist_take_def]
+ "dlist_take(Suc(n))[dnil]=dnil"
+ (fn prems =>
+ [
+ (asm_simp_tac iterate_ss 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_take = temp::dlist_take;
+
+val temp = prove_goalw Dlist.thy [dlist_take_def]
+ "dlist_take(Suc(n))[dcons[x][xl]]=dcons[x][dlist_take(n)[xl]]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("n","n")] natE 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_take = temp::dlist_take;
+
+val dlist_rews = dlist_take @ dlist_rews;
+
+(* ------------------------------------------------------------------------*)
+(* take lemma for dlists *)
+(* ------------------------------------------------------------------------*)
+
+fun prover reach defs thm = prove_goalw Dlist.thy defs thm
+ (fn prems =>
+ [
+ (res_inst_tac [("t","l1")] (reach RS subst) 1),
+ (res_inst_tac [("t","l2")] (reach RS subst) 1),
+ (rtac (fix_def2 RS ssubst) 1),
+ (rtac (contlub_cfun_fun RS ssubst) 1),
+ (rtac is_chain_iterate 1),
+ (rtac (contlub_cfun_fun RS ssubst) 1),
+ (rtac is_chain_iterate 1),
+ (rtac lub_equal 1),
+ (rtac (is_chain_iterate RS ch2ch_fappL) 1),
+ (rtac (is_chain_iterate RS ch2ch_fappL) 1),
+ (rtac allI 1),
+ (resolve_tac prems 1)
+ ]);
+
+val dlist_take_lemma = prover dlist_reach [dlist_take_def]
+ "(!!n.dlist_take(n)[l1]=dlist_take(n)[l2]) ==> l1=l2";
+
+
+(* ------------------------------------------------------------------------*)
+(* Co -induction for dlists *)
+(* ------------------------------------------------------------------------*)
+
+val dlist_coind_lemma = prove_goalw Dlist.thy [dlist_bisim_def]
+"dlist_bisim(R) ==> ! p q.R(p,q) --> dlist_take(n)[p]=dlist_take(n)[q]"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (strip_tac 1),
+ ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
+ (atac 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (etac disjE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (etac exE 1),
+ (etac exE 1),
+ (etac exE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (REPEAT (etac conjE 1)),
+ (rtac cfun_arg_cong 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+val dlist_coind = prove_goal Dlist.thy "[|dlist_bisim(R);R(p,q)|] ==> p = q"
+ (fn prems =>
+ [
+ (rtac dlist_take_lemma 1),
+ (rtac (dlist_coind_lemma RS spec RS spec RS mp) 1),
+ (resolve_tac prems 1),
+ (resolve_tac prems 1)
+ ]);
+
+(* ------------------------------------------------------------------------*)
+(* structural induction *)
+(* ------------------------------------------------------------------------*)
+
+val dlist_finite_ind = prove_goal Dlist.thy
+"[|P(UU);P(dnil);\
+\ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])\
+\ |] ==> !l.P(dlist_take(n)[l])"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (resolve_tac prems 1),
+ (rtac allI 1),
+ (res_inst_tac [("l","l")] dlistE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (res_inst_tac [("Q","dlist_take(n1)[xl]=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (resolve_tac prems 1),
+ (resolve_tac prems 1),
+ (atac 1),
+ (atac 1),
+ (etac spec 1)
+ ]);
+
+val dlist_all_finite_lemma1 = prove_goal Dlist.thy
+"!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (rtac allI 1),
+ (res_inst_tac [("l","l")] dlistE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (eres_inst_tac [("x","xl")] allE 1),
+ (etac disjE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ ]);
+
+val dlist_all_finite_lemma2 = prove_goal Dlist.thy "? n.dlist_take(n)[l]=l"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","l=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (subgoal_tac "(!n.dlist_take(n)[l]=UU) |(? n.dlist_take(n)[l]=l)" 1),
+ (etac disjE 1),
+ (eres_inst_tac [("P","l=UU")] notE 1),
+ (rtac dlist_take_lemma 1),
+ (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (atac 1),
+ (subgoal_tac "!n.!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l" 1),
+ (fast_tac HOL_cs 1),
+ (rtac allI 1),
+ (rtac dlist_all_finite_lemma1 1)
+ ]);
+
+val dlist_all_finite= prove_goalw Dlist.thy [dlist_finite_def] "dlist_finite(l)"
+ (fn prems =>
+ [
+ (rtac dlist_all_finite_lemma2 1)
+ ]);
+
+val dlist_ind = prove_goal Dlist.thy
+"[|P(UU);P(dnil);\
+\ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])|] ==> P(l)"
+ (fn prems =>
+ [
+ (rtac (dlist_all_finite_lemma2 RS exE) 1),
+ (etac subst 1),
+ (rtac (dlist_finite_ind RS spec) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
+ ]);
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/dlist.thy Thu Mar 24 13:43:45 1994 +0100
@@ -0,0 +1,111 @@
+(* Title: HOLCF/dlist.thy
+
+ Author: Franz Regensburger
+ ID: $ $
+ Copyright 1994 Technische Universitaet Muenchen
+
+Theory for lists
+*)
+
+Dlist = Stream2 +
+
+types dlist 1
+
+(* ----------------------------------------------------------------------- *)
+(* arity axiom is validated by semantic reasoning *)
+(* partial ordering is implicit in the isomorphism axioms and their cont. *)
+
+arities dlist::(pcpo)pcpo
+
+consts
+
+(* ----------------------------------------------------------------------- *)
+(* essential constants *)
+
+dlist_rep :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
+dlist_abs :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
+
+(* ----------------------------------------------------------------------- *)
+(* abstract constants and auxiliary constants *)
+
+dlist_copy :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
+
+dnil :: "'a dlist"
+dcons :: "'a -> 'a dlist -> 'a dlist"
+dlist_when :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
+is_dnil :: "'a dlist -> tr"
+is_dcons :: "'a dlist -> tr"
+dhd :: "'a dlist -> 'a"
+dtl :: "'a dlist -> 'a dlist"
+dlist_take :: "nat => 'a dlist -> 'a dlist"
+dlist_finite :: "'a dlist => bool"
+dlist_bisim :: "('a dlist => 'a dlist => bool) => bool"
+
+rules
+
+(* ----------------------------------------------------------------------- *)
+(* axiomatization of recursive type 'a dlist *)
+(* ----------------------------------------------------------------------- *)
+(* ('a dlist,dlist_abs) is the initial F-algebra where *)
+(* F is the locally continuous functor determined by domain equation *)
+(* X = one ++ 'a ** X *)
+(* ----------------------------------------------------------------------- *)
+(* dlist_abs is an isomorphism with inverse dlist_rep *)
+(* identity is the least endomorphism on 'a dlist *)
+
+dlist_abs_iso "dlist_rep[dlist_abs[x]] = x"
+dlist_rep_iso "dlist_abs[dlist_rep[x]] = x"
+dlist_copy_def "dlist_copy == (LAM f. dlist_abs oo \
+\ (when[sinl][sinr oo (ssplit[LAM x y. x ## f[y]])])\
+\ oo dlist_rep)"
+dlist_reach "(fix[dlist_copy])[x]=x"
+
+(* ----------------------------------------------------------------------- *)
+(* properties of additional constants *)
+(* ----------------------------------------------------------------------- *)
+(* constructors *)
+
+dnil_def "dnil == dlist_abs[sinl[one]]"
+dcons_def "dcons == (LAM x l. dlist_abs[sinr[x##l]])"
+
+(* ----------------------------------------------------------------------- *)
+(* discriminator functional *)
+
+dlist_when_def
+"dlist_when == (LAM f1 f2 l.\
+\ when[LAM x.f1][ssplit[LAM x l.f2[x][l]]][dlist_rep[l]])"
+
+(* ----------------------------------------------------------------------- *)
+(* discriminators and selectors *)
+
+is_dnil_def "is_dnil == dlist_when[TT][LAM x l.FF]"
+is_dcons_def "is_dcons == dlist_when[FF][LAM x l.TT]"
+dhd_def "dhd == dlist_when[UU][LAM x l.x]"
+dtl_def "dtl == dlist_when[UU][LAM x l.l]"
+
+(* ----------------------------------------------------------------------- *)
+(* the taker for dlists *)
+
+dlist_take_def "dlist_take == (%n.iterate(n,dlist_copy,UU))"
+
+(* ----------------------------------------------------------------------- *)
+
+dlist_finite_def "dlist_finite == (%s.? n.dlist_take(n)[s]=s)"
+
+(* ----------------------------------------------------------------------- *)
+(* definition of bisimulation is determined by domain equation *)
+(* simplification and rewriting for abstract constants yields def below *)
+
+dlist_bisim_def "dlist_bisim ==\
+\ ( %R.!l1 l2.\
+\ R(l1,l2) -->\
+\ ((l1=UU & l2=UU) |\
+\ (l1=dnil & l2=dnil) |\
+\ (? x l11 l21. x~=UU & l11~=UU & l21~=UU & \
+\ l1=dcons[x][l11] & l2 = dcons[x][l21] & R(l11,l21))))"
+
+end
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/porder0.thy Thu Mar 24 13:43:45 1994 +0100
@@ -0,0 +1,42 @@
+(* Title: HOLCF/porder0.thy
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Definition of class porder (partial order)
+
+The prototype theory for this class is void.thy
+
+*)
+
+Porder0 = Void +
+
+(* Introduction of new class. The witness is type void. *)
+
+classes po < term
+
+(* default type is still term ! *)
+(* void is the prototype in po *)
+
+arities void :: po
+
+consts "<<" :: "['a,'a::po] => bool" (infixl 55)
+
+rules
+
+(* class axioms: justification is theory Void *)
+
+refl_less "x << x"
+ (* witness refl_less_void *)
+
+antisym_less "[|x<<y ; y<<x |] ==> x = y"
+ (* witness antisym_less_void *)
+
+trans_less "[|x<<y ; y<<z |] ==> x<<z"
+ (* witness trans_less_void *)
+
+(* instance of << for the prototype void *)
+
+inst_void_po "(op <<)::[void,void]=>bool = less_void"
+
+end