# HG changeset patch
# User nipkow
# Date 772106596 -7200
# Node ID 89e1986125fe77a03c8646a31f57f8ea4cdaf025
# Parent  888bbb4119f849258a9d6b243fc7acb48078bc15
Franz Regensburger's changes.

diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Cfun1.thy	Mon Jun 20 12:03:16 1994 +0200
@@ -18,7 +18,7 @@
 
 consts  
 	Cfun	:: "('a => 'b)set"
-	fapp	:: "('a -> 'b)=>('a => 'b)"	("(_[_])" [11,0] 1000)
+	fapp	:: "('a -> 'b)=>('a => 'b)"	("(_[_])" [1000,0] 1000)
 						(* usually Rep_Cfun *)
 						(* application      *)
 
diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Fix.ML	Mon Jun 20 12:03:16 1994 +0200
@@ -1072,6 +1072,27 @@
 	(atac 1)
 	]);
 
+
+val adm_disj_lemma11 = prove_goal Fix.thy
+"[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac adm_disj_lemma2 1),
+	(etac adm_disj_lemma10 1),
+	(atac 1)
+	]);
+
+val adm_disj_lemma12 = prove_goal Fix.thy
+"[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac adm_disj_lemma2 1),
+	(etac adm_disj_lemma6 1),
+	(atac 1)
+	]);
+
 val adm_disj = prove_goal  Fix.thy  
 	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
  (fn prems =>
@@ -1083,19 +1104,16 @@
 	(atac 1),
 	(atac 1),
 	(rtac disjI2 1),
-	(rtac adm_disj_lemma2 1),
-	(atac 1),
-	(rtac adm_disj_lemma6 1),
+	(etac adm_disj_lemma12 1),
 	(atac 1),
 	(atac 1),
 	(rtac disjI1 1),
-	(rtac adm_disj_lemma2 1),
-	(atac 1),
-	(rtac adm_disj_lemma10 1),
+	(etac adm_disj_lemma11 1),
 	(atac 1),
 	(atac 1)
 	]);
 
+
 val adm_impl = prove_goal  Fix.thy  
 	"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
  (fn prems =>
diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/HOLCF.ML
--- a/src/HOLCF/HOLCF.ML	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/HOLCF.ML	Mon Jun 20 12:03:16 1994 +0200
@@ -15,6 +15,7 @@
 		addsimps tr_when
 		addsimps andalso_thms
 		addsimps orelse_thms
+                addsimps neg_thms
 		addsimps ifte_thms;
 
 
diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/Stream.ML
--- a/src/HOLCF/Stream.ML	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Stream.ML	Mon Jun 20 12:03:16 1994 +0200
@@ -330,6 +330,17 @@
 	"(!!n.stream_take(n)[s1]=stream_take(n)[s2]) ==> s1=s2";
 
 
+val stream_reach2 = prove_goal Stream.thy  "lub(range(%i.stream_take(i)[s]))=s"
+ (fn prems =>
+	[
+	(res_inst_tac [("t","s")] (stream_reach RS subst) 1),
+	(rtac (fix_def2 RS ssubst) 1),
+	(rewrite_goals_tac [stream_take_def]),
+	(rtac (contlub_cfun_fun RS ssubst) 1),
+	(rtac is_chain_iterate 1),
+	(rtac refl 1)
+	]);
+
 (* ------------------------------------------------------------------------*)
 (* Co -induction for streams                                               *)
 (* ------------------------------------------------------------------------*)
@@ -429,7 +440,6 @@
 	(REPEAT (atac 1))
 	]);
 
-
 (* ------------------------------------------------------------------------*)
 (* simplify use of Co-induction                                            *)
 (* ------------------------------------------------------------------------*)
@@ -643,6 +653,20 @@
 	]);
 
 
+val stream_take_lemma8 = prove_goal Stream.thy
+"[|adm(P); !n. ? m. n < m & P(stream_take(m)[s])|] ==> P(s)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (stream_reach2 RS subst) 1),
+	(rtac adm_disj_lemma11 1),
+	(atac 1),
+	(atac 2),
+	(rewrite_goals_tac [stream_take_def]),
+	(rtac ch2ch_fappL 1),
+	(rtac is_chain_iterate 1)
+	]);
+
 (* ----------------------------------------------------------------------- *)
 (* lemmas stream_finite                                                    *)
 (* ----------------------------------------------------------------------- *)
diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/Tr1.ML
--- a/src/HOLCF/Tr1.ML	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Tr1.ML	Mon Jun 20 12:03:16 1994 +0200
@@ -123,20 +123,22 @@
 (* type tr is flat                                                          *) 
 (* ------------------------------------------------------------------------ *)
 
-val prems = goalw Tr1.thy [flat_def] "flat(TT)";
-by (rtac allI 1);
-by (rtac allI 1);
-by (res_inst_tac [("p","x")] trE 1);
-by (asm_simp_tac ccc1_ss 1);
-by (res_inst_tac [("p","y")] trE 1);
-by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
-by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
-by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
-by (res_inst_tac [("p","y")] trE 1);
-by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
-by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
-by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
-val flat_tr = result();
+val flat_tr = prove_goalw Tr1.thy [flat_def] "flat(TT)"
+ (fn prems =>
+	[
+	(rtac allI 1),
+	(rtac allI 1),
+	(res_inst_tac [("p","x")] trE 1),
+	(asm_simp_tac ccc1_ss 1),
+	(res_inst_tac [("p","y")] trE 1),
+	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
+	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
+	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
+	(res_inst_tac [("p","y")] trE 1),
+	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
+	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
+	(asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1)
+	]);
 
 
 (* ------------------------------------------------------------------------ *) 
diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/Tr2.ML
--- a/src/HOLCF/Tr2.ML	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Tr2.ML	Mon Jun 20 12:03:16 1994 +0200
@@ -19,13 +19,13 @@
 	]);
 
 val andalso_thms = map prover [
-			"TT andalso y = y",
-			"FF andalso y = FF",
-			"UU andalso y = UU"
+			"(TT andalso y) = y",
+			"(FF andalso y) = FF",
+			"(UU andalso y) = UU"
 			];
 
 val andalso_thms = andalso_thms @ 
- [prove_goalw Tr2.thy [andalso_def] "x andalso TT =  x"
+ [prove_goalw Tr2.thy [andalso_def] "(x andalso TT) =  x"
  (fn prems =>
 	[
 	(res_inst_tac [("p","x")] trE 1),
@@ -45,13 +45,13 @@
 	]);
 
 val orelse_thms = map prover [
-			"TT orelse y  = TT",
-			"FF orelse y =  y",
-			"UU orelse y = UU"
+			"(TT orelse y)  = TT",
+			"(FF orelse y) =  y",
+			"(UU orelse y) = UU"
 			];
 
 val orelse_thms = orelse_thms @ 
- [prove_goalw Tr2.thy [orelse_def] "x orelse FF =  x"
+ [prove_goalw Tr2.thy [orelse_def] "(x orelse FF) =  x"
  (fn prems =>
 	[
 	(res_inst_tac [("p","x")] trE 1),
@@ -62,6 +62,22 @@
 
 
 (* ------------------------------------------------------------------------ *) 
+(* lemmas about neg                                                         *) 
+(* ------------------------------------------------------------------------ *)
+
+fun prover s =  prove_goalw Tr2.thy [neg_def] s
+ (fn prems =>
+	[
+	(simp_tac (ccc1_ss addsimps tr_when) 1)
+	]);
+
+val neg_thms = map prover [
+			"neg[TT] = FF",
+			"neg[FF] = TT",
+			"neg[UU] = UU"
+			];
+
+(* ------------------------------------------------------------------------ *) 
 (* lemmas about If_then_else_fi                                             *) 
 (* ------------------------------------------------------------------------ *)
 
diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/Tr2.thy
--- a/src/HOLCF/Tr2.thy	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Tr2.thy	Mon Jun 20 12:03:16 1994 +0200
@@ -10,21 +10,22 @@
 
 consts
 	"@cifte"	:: "tr=>'c=>'c=>'c"
-                             ("(3If _/ (then _/ else _) fi)" [60,60,60] 60)
+                             ("(3If _/ (then _/ else _) fi)" 60)
 	"Icifte"        :: "tr->'c->'c->'c"
 
-	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [61,60] 60)
+	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [36,35] 35)
 	"cop @andalso"	:: "tr -> tr -> tr" ("trand")
-	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [61,60] 60)
+	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
 	"cop @orelse"	:: "tr -> tr -> tr" ("tror")
 
+        "neg"           :: "tr -> tr"
 
 rules
 
   ifte_def    "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
   andalso_def "trand == (LAM t1 t2.tr_when[t2][FF][t1])"
   orelse_def  "tror  == (LAM t1 t2.tr_when[TT][t2][t1])"
-
+  neg_def     "neg == (LAM t. tr_when[FF][TT][t])"
 
 end