# HG changeset patch # User nipkow # Date 764513025 -3600 # Node ID 3a0485439396c4730ee99b86bfe76770357079e0 # Parent 5ef75ff3baeb943719758274193c27dc47348a27 structural induction for strict lists diff -r 5ef75ff3baeb -r 3a0485439396 src/HOLCF/Dlist.ML --- /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)) + ]); + + + + diff -r 5ef75ff3baeb -r 3a0485439396 src/HOLCF/Dlist.thy --- /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 + + + + diff -r 5ef75ff3baeb -r 3a0485439396 src/HOLCF/Porder0.thy --- /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< x = y" + (* witness antisym_less_void *) + +trans_less "[|x< x<bool = less_void" + +end diff -r 5ef75ff3baeb -r 3a0485439396 src/HOLCF/dlist.ML --- /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)) + ]); + + + + diff -r 5ef75ff3baeb -r 3a0485439396 src/HOLCF/dlist.thy --- /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 + + + + diff -r 5ef75ff3baeb -r 3a0485439396 src/HOLCF/porder0.thy --- /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< x = y" + (* witness antisym_less_void *) + +trans_less "[|x< x<bool = less_void" + +end