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/Dnat.ML
changeset 243 c22b85994e17
child 297 5ef75ff3baeb 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Dnat.ML	Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,471 @@
+(*  Title: 	HOLCF/dnat.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Lemmas for dnat.thy 
+*)
+
+open Dnat;
+
+(* ------------------------------------------------------------------------*)
+(* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict               *)
+(* ------------------------------------------------------------------------*)
+
+val dnat_iso_strict= dnat_rep_iso RS (dnat_abs_iso RS 
+	(allI  RSN (2,allI RS iso_strict)));
+
+val dnat_rews = [dnat_iso_strict RS conjunct1,
+		dnat_iso_strict RS conjunct2];
+
+(* ------------------------------------------------------------------------*)
+(* Properties of dnat_copy                                                 *)
+(* ------------------------------------------------------------------------*)
+
+fun prover defs thm =  prove_goalw Dnat.thy defs thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps 
+		(dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
+	]);
+
+val dnat_copy = 
+	[
+	prover [dnat_copy_def] "dnat_copy[f][UU]=UU",
+	prover [dnat_copy_def,dzero_def] "dnat_copy[f][dzero]= dzero",
+	prover [dnat_copy_def,dsucc_def] 
+		"n~=UU ==> dnat_copy[f][dsucc[n]] = dsucc[f[n]]"
+	];
+
+val dnat_rews =  dnat_copy @ dnat_rews; 
+
+(* ------------------------------------------------------------------------*)
+(* Exhaustion and elimination for dnat                                     *)
+(* ------------------------------------------------------------------------*)
+
+val Exh_dnat = prove_goalw Dnat.thy [dsucc_def,dzero_def]
+	"n = UU | n = dzero | (? x . x~=UU & n = dsucc[x])"
+ (fn prems =>
+	[
+	(simp_tac HOLCF_ss  1),
+	(rtac (dnat_rep_iso RS subst) 1),
+	(res_inst_tac [("p","dnat_rep[n]")] ssumE 1),
+	(rtac disjI1 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(rtac (disjI1 RS disjI2) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(res_inst_tac [("p","x")] oneE 1),
+	(contr_tac 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(rtac (disjI2 RS disjI2) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+val dnatE = prove_goal Dnat.thy 
+ "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc[x];x~=UU|]==>Q|]==>Q"
+ (fn prems =>
+	[
+	(rtac (Exh_dnat RS disjE) 1),
+	(eresolve_tac prems 1),
+	(etac disjE 1),
+	(eresolve_tac prems 1),
+	(REPEAT (etac exE 1)),
+	(resolve_tac prems 1),
+	(fast_tac HOL_cs 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+(* ------------------------------------------------------------------------*)
+(* Properties of dnat_when                                                 *)
+(* ------------------------------------------------------------------------*)
+
+fun prover defs thm =  prove_goalw Dnat.thy defs thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps 
+		(dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
+	]);
+
+
+val dnat_when = [
+	prover [dnat_when_def] "dnat_when[c][f][UU]=UU",
+	prover [dnat_when_def,dzero_def] "dnat_when[c][f][dzero]=c",
+	prover [dnat_when_def,dsucc_def] 
+		"n~=UU ==> dnat_when[c][f][dsucc[n]]=f[n]"
+	];
+
+val dnat_rews = dnat_when @ dnat_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Rewrites for  discriminators and  selectors                             *)
+(* ------------------------------------------------------------------------*)
+
+fun prover defs thm = prove_goalw Dnat.thy defs thm
+ (fn prems =>
+	[
+	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+	]);
+
+val dnat_discsel = [
+	prover [is_dzero_def] "is_dzero[UU]=UU",
+	prover [is_dsucc_def] "is_dsucc[UU]=UU",
+	prover [dpred_def] "dpred[UU]=UU"
+	];
+
+
+fun prover defs thm = prove_goalw Dnat.thy defs thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+	]);
+
+val dnat_discsel = [
+	prover [is_dzero_def] "is_dzero[dzero]=TT",
+	prover [is_dzero_def] "n~=UU ==>is_dzero[dsucc[n]]=FF",
+	prover [is_dsucc_def] "is_dsucc[dzero]=FF",
+	prover [is_dsucc_def] "n~=UU ==> is_dsucc[dsucc[n]]=TT",
+	prover [dpred_def] "dpred[dzero]=UU",
+	prover [dpred_def] "n~=UU ==> dpred[dsucc[n]]=n"
+	] @ dnat_discsel;
+
+val dnat_rews = dnat_discsel @ dnat_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Definedness and strictness                                              *)
+(* ------------------------------------------------------------------------*)
+
+fun prover contr thm = prove_goal Dnat.thy thm
+ (fn prems =>
+	[
+	(res_inst_tac [("P1",contr)] classical3 1),
+	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(dtac sym 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(simp_tac (HOLCF_ss addsimps (prems @ dnat_rews)) 1)
+	]);
+
+val dnat_constrdef = [
+	prover "is_dzero[UU] ~= UU" "dzero~=UU",
+	prover "is_dsucc[UU] ~= UU" "n~=UU ==> dsucc[n]~=UU"
+	]; 
+
+
+fun prover defs thm = prove_goalw Dnat.thy defs thm
+ (fn prems =>
+	[
+	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+	]);
+
+val dnat_constrdef = [
+	prover [dsucc_def] "dsucc[UU]=UU"
+	] @ dnat_constrdef;
+
+val dnat_rews = dnat_constrdef @ dnat_rews;
+
+
+(* ------------------------------------------------------------------------*)
+(* Distinctness wrt. << and =                                              *)
+(* ------------------------------------------------------------------------*)
+
+fun prover contrfun thm = prove_goal Dnat.thy thm
+ (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",contrfun)] monofun_cfun_arg 1),
+	(etac box_less 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+	]);
+
+val dnat_dist_less = 
+	[
+prover "is_dzero" "n~=UU ==> ~dzero << dsucc[n]",
+prover "is_dsucc" "n~=UU ==> ~dsucc[n] << dzero"
+	];
+
+fun prover contrfun thm = prove_goal Dnat.thy thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(res_inst_tac [("P1","TT = FF")] classical3 1),
+	(resolve_tac dist_eq_tr 1),
+	(dres_inst_tac [("f",contrfun)] cfun_arg_cong 1),
+	(etac box_equals 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+	]);
+
+val dnat_dist_eq = 
+	[
+prover "is_dzero" "n~=UU ==> dzero ~= dsucc[n]",
+prover "is_dsucc" "n~=UU ==> dsucc[n] ~= dzero"
+	];
+
+val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
+
+(* ------------------------------------------------------------------------*)
+(* Invertibility                                                           *)
+(* ------------------------------------------------------------------------*)
+
+val dnat_invert = 
+	[
+prove_goal Dnat.thy 
+"[|x1~=UU; y1~=UU; dsucc[x1] << dsucc[y1] |] ==> x1<< y1"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(dres_inst_tac [("fo5","dnat_when[c][LAM x.x]")] monofun_cfun_arg 1),
+	(etac box_less 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+	])
+	];
+
+(* ------------------------------------------------------------------------*)
+(* Injectivity                                                             *)
+(* ------------------------------------------------------------------------*)
+
+val dnat_inject = 
+	[
+prove_goal Dnat.thy 
+"[|x1~=UU; y1~=UU; dsucc[x1] = dsucc[y1] |] ==> x1= y1"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(dres_inst_tac [("f","dnat_when[c][LAM x.x]")] cfun_arg_cong 1),
+	(etac box_equals 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+	])
+	];
+
+(* ------------------------------------------------------------------------*)
+(* definedness for  discriminators and  selectors                          *)
+(* ------------------------------------------------------------------------*)
+
+
+fun prover thm = prove_goal Dnat.thy thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac dnatE 1),
+	(contr_tac 1),
+	(REPEAT (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1))
+	]);
+
+val dnat_discsel_def = 
+	[
+	prover  "n~=UU ==> is_dzero[n]~=UU",
+	prover  "n~=UU ==> is_dsucc[n]~=UU"
+	];
+
+val dnat_rews = dnat_discsel_def @ dnat_rews;
+
+ 
+(* ------------------------------------------------------------------------*)
+(* Properties dnat_take                                                    *)
+(* ------------------------------------------------------------------------*)
+
+val dnat_take =
+	[
+prove_goalw Dnat.thy [dnat_take_def] "dnat_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 dnat_rews) 1)
+	]),
+prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
+ (fn prems =>
+	[
+	(asm_simp_tac iterate_ss 1)
+	])];
+
+fun prover thm = prove_goalw Dnat.thy [dnat_take_def] thm
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(simp_tac iterate_ss 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+	]);
+
+val dnat_take = [
+prover "dnat_take(Suc(n))[dzero]=dzero",
+prover "xs~=UU ==> dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
+	] @ dnat_take;
+
+
+val dnat_rews = dnat_take @ dnat_rews;
+
+(* ------------------------------------------------------------------------*)
+(* take lemma for dnats                                                  *)
+(* ------------------------------------------------------------------------*)
+
+fun prover reach defs thm  = prove_goalw Dnat.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 dnat_take_lemma = prover dnat_reach  [dnat_take_def]
+	"(!!n.dnat_take(n)[s1]=dnat_take(n)[s2]) ==> s1=s2";
+
+
+(* ------------------------------------------------------------------------*)
+(* Co -induction for dnats                                                 *)
+(* ------------------------------------------------------------------------*)
+
+val dnat_coind_lemma = prove_goalw Dnat.thy [dnat_bisim_def] 
+"dnat_bisim(R) ==> ! p q.R(p,q) --> dnat_take(n)[p]=dnat_take(n)[q]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(nat_ind_tac "n" 1),
+	(simp_tac (HOLCF_ss addsimps dnat_take) 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 dnat_take) 1),
+	(etac disjE 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
+	(etac exE 1),
+	(etac exE 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
+	(REPEAT (etac conjE 1)),
+	(rtac cfun_arg_cong 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+val dnat_coind = prove_goal Dnat.thy "[|dnat_bisim(R);R(p,q)|] ==> p = q"
+ (fn prems =>
+	[
+	(rtac dnat_take_lemma 1),
+	(rtac (dnat_coind_lemma RS spec RS spec RS mp) 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1)
+	]);
+
+
+(* ------------------------------------------------------------------------*)
+(* structural induction for admissible predicates                          *)
+(* ------------------------------------------------------------------------*)
+
+val dnat_ind = prove_goal Dnat.thy
+"[| adm(P);\
+\   P(UU);\
+\   P(dzero);\
+\   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)"
+ (fn prems =>
+	[
+	(rtac (dnat_reach RS subst) 1),
+	(res_inst_tac [("x","s")] spec 1),
+	(rtac fix_ind 1),
+	(rtac adm_all2 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 [("n","xa")] dnatE 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+	(resolve_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+	(resolve_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+	(res_inst_tac [("Q","x[xb]=UU")] classical2 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(resolve_tac prems 1),
+	(eresolve_tac prems 1),
+	(etac spec 1)
+	]);
+
+
+val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)"
+ (fn prems =>
+	[
+	(rtac allI 1),
+	(res_inst_tac [("s","x")] dnat_ind 1),
+	(REPEAT (resolve_tac adm_thms 1)),
+	(contX_tacR 1),
+	(REPEAT (resolve_tac adm_thms 1)),
+	(contX_tacR 1),
+	(REPEAT (resolve_tac adm_thms 1)),
+	(contX_tacR 1),
+	(fast_tac HOL_cs 1),
+	(rtac allI 1),
+	(res_inst_tac [("n","y")] dnatE 1),
+	(fast_tac (HOL_cs addSIs [UU_I]) 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
+	(rtac allI 1),
+	(res_inst_tac [("n","y")] dnatE 1),
+	(fast_tac (HOL_cs addSIs [UU_I]) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(hyp_subst_tac 1),
+	(strip_tac 1),
+	(rtac disjI2 1),
+	(forward_tac dnat_invert 1),
+	(atac 2),
+	(atac 1),
+	(etac allE 1),
+	(dtac mp 1),
+	(atac 1),
+	(etac disjE 1),
+	(contr_tac 1),
+	(asm_simp_tac HOLCF_ss 1)
+	]);
+
+val dnat_ind = prove_goal Dnat.thy
+"[| adm(P);\
+\   P(UU);\
+\   P(dzero);\
+\   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)"
+ (fn prems =>
+	[
+	(rtac (dnat_reach RS subst) 1),
+	(res_inst_tac [("x","s")] spec 1),
+	(rtac fix_ind 1),
+	(rtac adm_all2 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 [("n","xa")] dnatE 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+	(resolve_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+	(resolve_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+	(res_inst_tac [("Q","x[xb]=UU")] classical2 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+	(resolve_tac prems 1),
+	(eresolve_tac prems 1),
+	(etac spec 1)
+	]);
+
+val dnat_ind2 = dnat_flat RS adm_flat RS dnat_ind;
+(*  "[| ?P(UU); ?P(dzero);
+    !!s1. [| s1 ~= UU; ?P(s1) |] ==> ?P(dsucc[s1]) |] ==> ?P(?s)" : thm
+*)
+
isabelle