Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/stream.ML
changeset 243 c22b85994e17
child 297 5ef75ff3baeb 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/stream.ML	Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,405 @@
+(*  Title: 	HOLCF/stream.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Lemmas for stream.thy
+*)
+
+open Stream;
+
+(* ------------------------------------------------------------------------*)
+(* The isomorphisms stream_rep_iso and stream_abs_iso are strict           *)
+(* ------------------------------------------------------------------------*)
+
+val stream_iso_strict= stream_rep_iso RS (stream_abs_iso RS 
+	(allI  RSN (2,allI RS iso_strict)));
+
+val stream_rews = [stream_iso_strict RS conjunct1,
+		stream_iso_strict RS conjunct2];
+
+(* ------------------------------------------------------------------------*)
+(* Properties of stream_copy                                               *)
+(* ------------------------------------------------------------------------*)
+
+fun prover defs thm =  prove_goalw Stream.thy defs thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps 
+		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
+	]);
+
+val stream_copy = 
+	[
+	prover [stream_copy_def] "stream_copy[f][UU]=UU",
+	prover [stream_copy_def,scons_def] 
+	"x~=UU ==> stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
+	];
+
+val stream_rews =  stream_copy @ stream_rews; 
+
+(* ------------------------------------------------------------------------*)
+(* Exhaustion and elimination for streams                                  *)
+(* ------------------------------------------------------------------------*)
+
+val Exh_stream = prove_goalw Stream.thy [scons_def]
+	"s = UU | (? x xs. x~=UU & s = scons[x][xs])"
+ (fn prems =>
+	[
+	(simp_tac HOLCF_ss  1),
+	(rtac (stream_rep_iso RS subst) 1),
+	(res_inst_tac [("p","stream_rep[s]")] sprodE 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(res_inst_tac [("p","y")] liftE1 1),
+	(contr_tac 1),
+	(rtac disjI2 1),
+	(rtac exI 1),
+	(rtac exI 1),
+	(etac conjI 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+val streamE = prove_goal Stream.thy 
+	"[| s=UU ==> Q; !!x xs.[|s=scons[x][xs];x~=UU|]==>Q|]==>Q"
+ (fn prems =>
+	[
+	(rtac (Exh_stream RS 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)
+	]);
+
+(* ------------------------------------------------------------------------*)
+(* Properties of stream_when                                               *)
+(* ------------------------------------------------------------------------*)
+
+fun prover defs thm =  prove_goalw Stream.thy defs thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps 
+		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
+	]);
+
+
+val stream_when = [
+	prover [stream_when_def] "stream_when[f][UU]=UU",
+	prover [stream_when_def,scons_def] 
+		"x~=UU ==> stream_when[f][scons[x][xs]]= f[x][xs]"
+	];
+
+val stream_rews = stream_when @ stream_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Rewrites for  discriminators and  selectors                             *)
+(* ------------------------------------------------------------------------*)
+
+fun prover defs thm = prove_goalw Stream.thy defs thm
+ (fn prems =>
+	[
+	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
+	]);
+
+val stream_discsel = [
+	prover [is_scons_def] "is_scons[UU]=UU",
+	prover [shd_def] "shd[UU]=UU",
+	prover [stl_def] "stl[UU]=UU"
+	];
+
+fun prover defs thm = prove_goalw Stream.thy defs thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+	]);
+
+val stream_discsel = [
+prover [is_scons_def,shd_def,stl_def] "x~=UU ==> is_scons[scons[x][xs]]=TT",
+prover [is_scons_def,shd_def,stl_def] "x~=UU ==> shd[scons[x][xs]]=x",
+prover [is_scons_def,shd_def,stl_def] "x~=UU ==> stl[scons[x][xs]]=xs"
+	] @ stream_discsel;
+
+val stream_rews = stream_discsel @ stream_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Definedness and strictness                                              *)
+(* ------------------------------------------------------------------------*)
+
+fun prover contr thm = prove_goal Stream.thy thm
+ (fn prems =>
+	[
+	(res_inst_tac [("P1",contr)] classical3 1),
+	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(dtac sym 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1)
+	]);
+
+val stream_constrdef = [
+	prover "is_scons[UU] ~= UU" "x~=UU ==> scons[x][xs]~=UU"
+	]; 
+
+fun prover defs thm = prove_goalw Stream.thy defs thm
+ (fn prems =>
+	[
+	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
+	]);
+
+val stream_constrdef = [
+	prover [scons_def] "scons[UU][xs]=UU"
+	] @ stream_constrdef;
+
+val stream_rews = stream_constrdef @ stream_rews;
+
+
+(* ------------------------------------------------------------------------*)
+(* Distinctness wrt. << and =                                              *)
+(* ------------------------------------------------------------------------*)
+
+
+(* ------------------------------------------------------------------------*)
+(* Invertibility                                                           *)
+(* ------------------------------------------------------------------------*)
+
+val stream_invert =
+	[
+prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
+\ scons[x1][x2] << scons[y1][y2]|] ==> x1<< y1 & x2 << y2"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac conjI 1),
+	(dres_inst_tac [("fo5","stream_when[LAM x l.x]")] monofun_cfun_arg 1),
+	(etac box_less 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
+	(dres_inst_tac [("fo5","stream_when[LAM x l.l]")] monofun_cfun_arg 1),
+	(etac box_less 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
+	])
+	];
+
+(* ------------------------------------------------------------------------*)
+(* Injectivity                                                             *)
+(* ------------------------------------------------------------------------*)
+
+val stream_inject = 
+	[
+prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
+\ scons[x1][x2] = scons[y1][y2]|] ==> x1= y1 & x2 = y2"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac conjI 1),
+	(dres_inst_tac [("f","stream_when[LAM x l.x]")] cfun_arg_cong 1),
+	(etac box_equals 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
+	(dres_inst_tac [("f","stream_when[LAM x l.l]")] cfun_arg_cong 1),
+	(etac box_equals 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
+	])
+	];
+
+(* ------------------------------------------------------------------------*)
+(* definedness for  discriminators and  selectors                          *)
+(* ------------------------------------------------------------------------*)
+
+fun prover thm = prove_goal Stream.thy thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac streamE 1),
+	(contr_tac 1),
+	(REPEAT (asm_simp_tac (HOLCF_ss addsimps stream_discsel) 1))
+	]);
+
+val stream_discsel_def = 
+	[
+	prover "s~=UU ==> is_scons[s]~=UU", 
+	prover "s~=UU ==> shd[s]~=UU" 
+	];
+
+val stream_rews = stream_discsel_def @ stream_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Properties stream_take                                                  *)
+(* ------------------------------------------------------------------------*)
+
+val stream_take =
+	[
+prove_goalw Stream.thy [stream_take_def] "stream_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 stream_rews) 1)
+	]),
+prove_goalw Stream.thy [stream_take_def] "stream_take(0)[xs]=UU"
+ (fn prems =>
+	[
+	(asm_simp_tac iterate_ss 1)
+	])];
+
+fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(simp_tac iterate_ss 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+	]);
+
+val stream_take = [
+prover 
+  "x~=UU ==> stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
+	] @ stream_take;
+
+val stream_rews = stream_take @ stream_rews;
+
+(* ------------------------------------------------------------------------*)
+(* take lemma for streams                                                  *)
+(* ------------------------------------------------------------------------*)
+
+fun prover reach defs thm  = prove_goalw Stream.thy defs thm
+ (fn prems =>
+	[
+	(res_inst_tac [("t","s1")] (reach RS subst) 1),
+	(res_inst_tac [("t","s2")] (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 stream_take_lemma = prover stream_reach  [stream_take_def]
+	"(!!n.stream_take(n)[s1]=stream_take(n)[s2]) ==> s1=s2";
+
+
+(* ------------------------------------------------------------------------*)
+(* Co -induction for streams                                               *)
+(* ------------------------------------------------------------------------*)
+
+val stream_coind_lemma = prove_goalw Stream.thy [stream_bisim_def] 
+"stream_bisim(R) ==> ! p q.R(p,q) --> stream_take(n)[p]=stream_take(n)[q]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(nat_ind_tac "n" 1),
+	(simp_tac (HOLCF_ss addsimps stream_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 stream_rews) 1),
+	(etac exE 1),
+	(etac exE 1),
+	(etac exE 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(REPEAT (etac conjE 1)),
+	(rtac cfun_arg_cong 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+val stream_coind = prove_goal Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
+ (fn prems =>
+	[
+	(rtac stream_take_lemma 1),
+	(rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1)
+	]);
+
+(* ------------------------------------------------------------------------*)
+(* structural induction for admissible predicates                          *)
+(* ------------------------------------------------------------------------*)
+
+val stream_ind = prove_goal Stream.thy
+"[| adm(P);\
+\  P(UU);\
+\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
+\  |] ==> P(s)"
+ (fn prems =>
+	[
+	(rtac (stream_reach RS subst) 1),
+	(res_inst_tac [("x","s")] spec 1),
+	(rtac fix_ind 1),
+	(rtac (allI RS adm_all) 1),
+	(rtac adm_subst 1),
+	(contX_tacR 1),
+	(resolve_tac prems 1),
+	(simp_tac HOLCF_ss 1),
+	(resolve_tac prems 1),
+	(strip_tac 1),
+	(res_inst_tac [("s","xa")] streamE 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(resolve_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(resolve_tac prems 1),
+	(atac 1),
+	(etac spec 1)
+	]);
+
+
+(* ------------------------------------------------------------------------*)
+(* simplify use of Co-induction                                            *)
+(* ------------------------------------------------------------------------*)
+
+val surjectiv_scons = prove_goal Stream.thy "scons[shd[s]][stl[s]]=s"
+ (fn prems =>
+	[
+	(res_inst_tac [("s","s")] streamE 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+	]);
+
+
+val stream_coind_lemma2 = prove_goalw Stream.thy [stream_bisim_def]
+"!s1 s2. R(s1, s2)-->shd[s1]=shd[s2] & R(stl[s1],stl[s2]) ==>stream_bisim(R)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(strip_tac 1),
+	(etac allE 1),
+	(etac allE 1),
+	(dtac mp 1),
+	(atac 1),
+	(etac conjE 1),
+	(res_inst_tac [("Q","s1 = UU & s2 = UU")] classical2 1),
+	(rtac disjI1 1),
+	(fast_tac HOL_cs 1),
+	(rtac disjI2 1),
+	(rtac disjE 1),
+	(etac (de_morgan2 RS ssubst) 1),
+	(res_inst_tac [("x","shd[s1]")] exI 1),
+	(res_inst_tac [("x","stl[s1]")] exI 1),
+	(res_inst_tac [("x","stl[s2]")] exI 1),
+	(rtac conjI 1),
+	(eresolve_tac stream_discsel_def 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
+	(eres_inst_tac [("s","shd[s1]"),("t","shd[s2]")] subst 1),
+	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
+	(res_inst_tac [("x","shd[s2]")] exI 1),
+	(res_inst_tac [("x","stl[s1]")] exI 1),
+	(res_inst_tac [("x","stl[s2]")] exI 1),
+	(rtac conjI 1),
+	(eresolve_tac stream_discsel_def 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
+	(res_inst_tac [("s","shd[s1]"),("t","shd[s2]")] ssubst 1),
+	(etac sym 1),
+	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1)
+	]);
+
+
isabelle