src/HOLCF/FOCUS/Fstream.ML
author oheimb
Tue, 07 Sep 2004 16:02:42 +0200
changeset 15188 9d57263faf9e
parent 14981 e73f8140af78
child 17293 ecf182ccc3ca
permissions -rw-r--r--
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     1
(*  Title: 	HOLCF/FOCUS/Fstream.ML
11355
wenzelm
parents: 11350
diff changeset
     2
    ID:         $Id$
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     3
    Author: 	David von Oheimb, TU Muenchen
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     4
*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     5
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
     6
Addsimps[eq_UU_iff RS sym];
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
     7
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     8
Goal "a = Def d \\<Longrightarrow> a\\<sqsubseteq>b \\<Longrightarrow> b = Def d";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     9
by (rtac (flat_eq RS iffD1 RS sym) 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    10
by (rtac Def_not_UU 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    11
by (dtac antisym_less_inverse 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    12
by (eatac (conjunct2 RS trans_less) 1 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    13
qed "Def_maximal";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    14
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    15
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    16
section "fscons";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    17
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    18
Goalw [fscons_def] "a~>s = Def a && s";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    19
by (Simp_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    20
qed "fscons_def2";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    21
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    22
qed_goal "fstream_exhaust" thy "x = UU |  (? a y. x = a~> y)" (fn _ => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    23
	simp_tac (simpset() addsimps [fscons_def2]) 1,
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    24
	cut_facts_tac [thm "stream.exhaust"] 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    25
	fast_tac (claset() addDs [not_Undef_is_Def RS iffD1]) 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    26
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    27
qed_goal "fstream_cases" thy "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P" 
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    28
 (fn prems => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    29
	cut_facts_tac [fstream_exhaust] 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    30
	etac disjE 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    31
	 eresolve_tac prems 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    32
	REPEAT(etac exE 1),
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    33
	eresolve_tac prems 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    34
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    35
fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    36
			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    37
11655
923e4d0d36d5 tuned parentheses in relational expressions;
wenzelm
parents: 11355
diff changeset
    38
qed_goal "fstream_exhaust_eq" thy "(x ~= UU) = (? a y. x = a~> y)" (fn _ => [
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    39
	simp_tac(simpset() addsimps [fscons_def2,thm "stream_exhaust_eq"]) 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    40
	fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    41
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    42
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    43
qed_goal "fscons_not_empty" thy "a~> s ~= <>" (fn _ => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    44
	stac fscons_def2 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    45
        Simp_tac 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    46
Addsimps[fscons_not_empty];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    47
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    48
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    49
qed_goal "fscons_inject" thy "(a~> s = b~> t) = (a = b &  s = t)" (fn _ => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    50
	simp_tac (HOL_ss addsimps [fscons_def2]) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    51
	stac (hd lift.inject RS sym) 1, (*2*back();*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    52
        Simp_tac 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    53
Addsimps[fscons_inject];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    54
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    55
qed_goal "fstream_prefix" thy "a~> s << t ==> ? tt. t = a~> tt &  s << tt" (fn prems =>[
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    56
	cut_facts_tac prems 1,
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    57
	res_inst_tac [("x","t")] (thm "stream.casedist") 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    58
	 cut_facts_tac [fscons_not_empty] 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    59
	 fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2]) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    60
	asm_full_simp_tac (HOL_ss addsimps [fscons_def2]) 1,
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    61
	dtac (thm "stream_flat_prefix") 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    62
	rtac Def_not_UU 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    63
	fast_tac HOL_cs 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    64
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    65
qed_goal "fstream_prefix'" thy
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    66
	"x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))" (fn _ => [
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    67
	simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "stream_prefix'"])1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    68
	Step_tac 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    69
	 ALLGOALS(etac swap),
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    70
	 fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    71
	rtac Lift_cases 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    72
	 contr_tac 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    73
	Step_tac 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    74
	dtac (Def_inject_less_eq RS iffD1) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    75
	Fast_tac 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    76
Addsimps[fstream_prefix'];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    77
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    78
(* ------------------------------------------------------------------------- *)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    79
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    80
section "ft & rt";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    81
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    82
bind_thm("ft_empty",hd (thms "stream.sel_rews"));
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    83
qed_goalw "ft_fscons" thy [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    84
	(Simp_tac 1)]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    85
Addsimps[ft_fscons];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    86
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    87
bind_thm("rt_empty",hd (tl (thms "stream.sel_rews")));
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    88
qed_goalw "rt_fscons" thy [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    89
	(Simp_tac 1)]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    90
Addsimps[rt_fscons];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    91
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    92
qed_goalw "ft_eq" thy [fscons_def] "(ft\\<cdot>s = Def a) = (? t. s = a~> t)" (K [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    93
	Simp_tac 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    94
	Safe_tac,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    95
	 etac subst 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    96
	 rtac exI 1,
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    97
	 rtac (thm "surjectiv_scons" RS sym) 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    98
	Simp_tac 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    99
Addsimps[ft_eq];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   100
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   101
Goal "(d\\<leadsto>y = x) = (ft\\<cdot>x = Def d & rt\\<cdot>x = y)";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   102
by Auto_tac;
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   103
qed "surjective_fscons_lemma";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   104
Goal "ft\\<cdot>x = Def d \\<Longrightarrow> d\\<leadsto>rt\\<cdot>x = x";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   105
by (asm_simp_tac (simpset() addsimps [surjective_fscons_lemma]) 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   106
qed "surjective_fscons";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   107
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   108
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   109
(* ------------------------------------------------------------------------- *)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   110
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   111
section "take";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   112
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   113
qed_goalw "fstream_take_Suc" thy [fscons_def]
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   114
	"stream_take (Suc n)\\<cdot>(a~> s) = a~> stream_take n\\<cdot>s" (K [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   115
	Simp_tac 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   116
Addsimps[fstream_take_Suc];
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   117
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   118
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   119
(* ------------------------------------------------------------------------- *)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   120
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   121
section "slen";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   122
	
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   123
(*bind_thm("slen_empty", slen_empty);*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   124
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   125
qed_goalw "slen_fscons" thy [fscons_def] "#(m~> s) = iSuc (#s)" (fn _ => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   126
	(Simp_tac 1)]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   127
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   128
qed_goal "slen_fscons_eq" thy 
11655
923e4d0d36d5 tuned parentheses in relational expressions;
wenzelm
parents: 11355
diff changeset
   129
	"(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   130
	simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq"]) 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   131
	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   132
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   133
qed_goal "slen_fscons_eq_rev" thy 
11655
923e4d0d36d5 tuned parentheses in relational expressions;
wenzelm
parents: 11355
diff changeset
   134
	"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   135
	simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq_rev"]) 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   136
	step_tac (HOL_cs addSEs [DefE]) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   137
	step_tac (HOL_cs addSEs [DefE]) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   138
	step_tac (HOL_cs addSEs [DefE]) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   139
	step_tac (HOL_cs addSEs [DefE]) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   140
	step_tac (HOL_cs addSEs [DefE]) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   141
	step_tac (HOL_cs addSEs [DefE]) 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   142
	etac swap 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   143
	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   144
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   145
qed_goal "slen_fscons_less_eq" thy 
11655
923e4d0d36d5 tuned parentheses in relational expressions;
wenzelm
parents: 11355
diff changeset
   146
	"(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))" (fn _ => [
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   147
	stac slen_fscons_eq_rev 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   148
	fast_tac (HOL_cs addSDs [fscons_inject RS iffD1]) 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   149
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   150
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   151
(* ------------------------------------------------------------------------- *)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   152
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   153
section "induction";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   154
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   155
qed_goal "fstream_ind" thy 
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   156
	"[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" (fn prems => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   157
	cut_facts_tac prems 1,
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   158
	etac (thm "stream.ind") 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   159
	 atac 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   160
	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] 
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   161
			 addEs (tl (tl prems) RL [fscons_def2 RS subst])) 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   162
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   163
qed_goal "fstream_ind2" thy 
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   164
  "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" (fn prems => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   165
	cut_facts_tac prems 1,
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   166
	etac (thm "stream_ind2") 1,
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   167
	  atac 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   168
	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] 
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   169
			 addIs ([hd(tl(tl prems))]RL[fscons_def2 RS subst]))1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   170
	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] 
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   171
			 addEs [hd(tl(tl(tl prems))RL[fscons_def2 RS subst]
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   172
						 RL[fscons_def2 RS subst])])1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   173
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   174
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   175
(* ------------------------------------------------------------------------- *)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   176
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   177
section "fsfilter";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   178
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   179
qed_goalw "fsfilter_empty" thy [fsfilter_def] "A(C)UU = UU" (fn _ => [
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   180
	rtac (thm "sfilter_empty") 1]);
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   181
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   182
qed_goalw "fsfilter_fscons" thy [fsfilter_def] 
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   183
	"A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" (fn _ => [
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   184
	simp_tac (simpset() addsimps [fscons_def2,thm "sfilter_scons",If_and_if]) 1]);
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   185
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   186
qed_goal "fsfilter_emptys" thy "{}(C)x = UU" (fn _ => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   187
	res_inst_tac [("x","x")] fstream_ind 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   188
	  resolve_tac adm_lemmas 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   189
	   cont_tacR 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   190
	 rtac fsfilter_empty 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   191
	asm_simp_tac (simpset()addsimps [fsfilter_fscons]) 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   192
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   193
qed_goal "fsfilter_insert" thy "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" (fn _=> [
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   194
	simp_tac (simpset() addsimps [thm "fsfilter_fscons"]) 1]);
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   195
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   196
qed_goal "fsfilter_single_in" thy "{a}(C)a~> x = a~> ({a}(C)x)" (fn _=> [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   197
	rtac fsfilter_insert 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   198
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   199
qed_goal "fsfilter_single_out" thy "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" (fn prems => [
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   200
	cut_facts_tac prems 1,
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   201
	asm_simp_tac (simpset() addsimps[fsfilter_fscons]) 1]);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   202
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   203
Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> \\<exists>j t. Y j = a\\<leadsto>t";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   204
by (case_tac "max_in_chain i Y" 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   205
by  (datac (lub_finch1 RS thelubI RS sym) 1 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   206
by  (Force_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   207
by (rewtac max_in_chain_def);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   208
by Auto_tac;
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   209
by (fatac chain_mono3 1 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   210
by (res_inst_tac [("x","Y j")] fstream_cases 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   211
by  (Force_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   212
by (dres_inst_tac [("x","j")] is_ub_thelub 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   213
by (Force_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   214
qed "fstream_lub_lemma1";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   215
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   216
Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> (\\<exists>j t. Y j = a\\<leadsto>t) & (\\<exists>X. chain X & (!i. ? j. Y j = a\\<leadsto>X i) & lub (range X) = s)";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   217
by (fatac fstream_lub_lemma1 1 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   218
by (Clarsimp_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   219
by (res_inst_tac [("x","%i. rt\\<cdot>(Y(i+j))")] exI 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   220
by (rtac conjI 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   221
by  (etac (chain_shift RS chain_monofun) 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   222
by Safe_tac;
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   223
by  (dres_inst_tac [("x","j"),("y","i+j")] chain_mono3 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   224
by   (Simp_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   225
by  (Asm_full_simp_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   226
by  (res_inst_tac [("x","i+j")] exI 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   227
by  (dtac fstream_prefix 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   228
by  (Clarsimp_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   229
by  (stac (contlub_cfun RS sym) 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   230
by   (rtac chainI 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   231
by   (Fast_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   232
by  (etac chain_shift 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   233
by (stac (lub_const RS thelubI) 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   234
by (stac lub_range_shift 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   235
by  (atac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   236
by (Asm_simp_tac 1);
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   237
qed "fstream_lub_lemma";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   238
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   239