src/HOLCF/ex/Coind.ML
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/ex/Coind.ML	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,126 +0,0 @@
     1.4 -(*  Title: 	FOCUS/ex/coind.ML
     1.5 -    ID:         $ $
     1.6 -    Author: 	Franz Regensburger
     1.7 -    Copyright   1993, 1995 Technische Universitaet Muenchen
     1.8 -*)
     1.9 -
    1.10 -open Coind;
    1.11 -
    1.12 -(* ------------------------------------------------------------------------- *)
    1.13 -(* expand fixed point properties                                             *)
    1.14 -(* ------------------------------------------------------------------------- *)
    1.15 -
    1.16 -
    1.17 -val nats_def2 = fix_prover2 Coind.thy nats_def 
    1.18 -	"nats = dzero&&(smap`dsucc`nats)";
    1.19 -
    1.20 -val from_def2 = fix_prover2 Coind.thy from_def 
    1.21 -	"from = (n.n&&(from`(dsucc`n)))";
    1.22 -
    1.23 -
    1.24 -
    1.25 -(* ------------------------------------------------------------------------- *)
    1.26 -(* recursive  properties                                                     *)
    1.27 -(* ------------------------------------------------------------------------- *)
    1.28 -
    1.29 -
    1.30 -val from = prove_goal Coind.thy "from`n = n&&(from`(dsucc`n))"
    1.31 - (fn prems =>
    1.32 -	[
    1.33 -	(rtac trans 1),
    1.34 -	(rtac (from_def2 RS ssubst) 1),
    1.35 -	(simp_tac HOLCF_ss  1),
    1.36 -	(rtac refl 1)
    1.37 -	]);
    1.38 -
    1.39 -
    1.40 -val from1 = prove_goal Coind.thy "from` = "
    1.41 - (fn prems =>
    1.42 -	[
    1.43 -	(rtac trans 1),
    1.44 -	(rtac (from RS ssubst) 1),
    1.45 -	(resolve_tac  stream.con_rews 1),
    1.46 -	(rtac refl 1)
    1.47 -	]);
    1.48 -
    1.49 -val coind_rews = 
    1.50 -	[iterator1, iterator2, iterator3, smap1, smap2,from1];
    1.51 -
    1.52 -(* ------------------------------------------------------------------------- *)
    1.53 -(* the example                                                               *)
    1.54 -(* prove:        nats = from`dzero                                           *)
    1.55 -(* ------------------------------------------------------------------------- *)
    1.56 -
    1.57 -val prems = goal Coind.thy "iterator`n`(smap`dsucc)`nats =\
    1.58 -\		 n&&(iterator`(dsucc`n)`(smap`dsucc)`nats)";
    1.59 -by (res_inst_tac [("x","n")] dnat.ind 1);
    1.60 -by (simp_tac (HOLCF_ss addsimps (coind_rews @ stream.rews)) 1);
    1.61 -by (simp_tac (HOLCF_ss addsimps (coind_rews @ stream.rews)) 1);
    1.62 -by (rtac trans 1);
    1.63 -by (rtac nats_def2 1);
    1.64 -by (simp_tac (HOLCF_ss addsimps (coind_rews @ dnat.rews)) 1);
    1.65 -by (rtac trans 1);
    1.66 -by (etac iterator3 1);
    1.67 -by (rtac trans 1);
    1.68 -by (asm_simp_tac HOLCF_ss 1);
    1.69 -by (rtac trans 1);
    1.70 -by (etac smap2 1);
    1.71 -by (rtac cfun_arg_cong 1);
    1.72 -by (asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat.rews)) 1);
    1.73 -val coind_lemma1 = result();
    1.74 -
    1.75 -val prems = goal Coind.thy "nats = from`dzero";
    1.76 -by (res_inst_tac [("R","% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream.coind 1);
    1.77 -by (res_inst_tac [("x","dzero")] exI 2);
    1.78 -by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 2);
    1.79 -by (rewrite_goals_tac [stream.bisim_def]);
    1.80 -by (strip_tac 1);
    1.81 -by (etac exE 1);
    1.82 -by (etac conjE 1);
    1.83 -by (case_tac "n=" 1);
    1.84 -by (rtac disjI1 1);
    1.85 -by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
    1.86 -by (rtac disjI2 1);
    1.87 -by (hyp_subst_tac 1);
    1.88 -by (res_inst_tac [("x","n")] exI 1);
    1.89 -by (res_inst_tac [("x","iterator`(dsucc`n)`(smap`dsucc)`nats")] exI 1);
    1.90 -by (res_inst_tac [("x","from`(dsucc`n)")] exI 1);
    1.91 -by (etac conjI 1);
    1.92 -by (rtac conjI 1);
    1.93 -by (res_inst_tac [("x","dsucc`n")] exI 1);
    1.94 -by (fast_tac HOL_cs 1);
    1.95 -by (rtac conjI 1);
    1.96 -by (rtac coind_lemma1 1);
    1.97 -by (rtac from 1);
    1.98 -val nats_eq_from = result();
    1.99 -
   1.100 -(* another proof using stream_coind_lemma2 *)
   1.101 -
   1.102 -val prems = goal Coind.thy "nats = from`dzero";
   1.103 -by (res_inst_tac [("R","% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream.coind 1);
   1.104 -by (rtac stream_coind_lemma2 1);
   1.105 -by (strip_tac 1);
   1.106 -by (etac exE 1);
   1.107 -by (case_tac "n=" 1);
   1.108 -by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
   1.109 -by (res_inst_tac [("x","::dnat")] exI 1);
   1.110 -by (simp_tac (HOLCF_ss addsimps coind_rews addsimps stream.rews) 1);
   1.111 -by (etac conjE 1);
   1.112 -by (hyp_subst_tac 1);
   1.113 -by (rtac conjI 1);
   1.114 -by (rtac (coind_lemma1 RS ssubst) 1);
   1.115 -by (rtac (from RS ssubst) 1);
   1.116 -by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
   1.117 -by (res_inst_tac [("x","dsucc`n")] exI 1);
   1.118 -by (rtac conjI 1);
   1.119 -by (rtac trans 1);
   1.120 -by (rtac (coind_lemma1 RS ssubst) 1);
   1.121 -by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
   1.122 -by (rtac refl 1);
   1.123 -by (rtac trans 1);
   1.124 -by (rtac (from RS ssubst) 1);
   1.125 -by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
   1.126 -by (rtac refl 1);
   1.127 -by (res_inst_tac [("x","dzero")] exI 1);
   1.128 -by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
   1.129 -val nats_eq_from = result();