equal
deleted
inserted
replaced
4 FOCUS streams (with lifted elements). |
4 FOCUS streams (with lifted elements). |
5 |
5 |
6 TODO: integrate Fstreams.thy |
6 TODO: integrate Fstreams.thy |
7 *) |
7 *) |
8 |
8 |
9 section {* FOCUS flat streams *} |
9 section \<open>FOCUS flat streams\<close> |
10 |
10 |
11 theory Fstream |
11 theory Fstream |
12 imports "~~/src/HOL/HOLCF/Library/Stream" |
12 imports "~~/src/HOL/HOLCF/Library/Stream" |
13 begin |
13 begin |
14 |
14 |
150 done |
150 done |
151 |
151 |
152 lemma slen_fscons_eq_rev: |
152 lemma slen_fscons_eq_rev: |
153 "(#x < enat (Suc (Suc n))) = (!a y. x ~= a~> y | #y < enat (Suc n))" |
153 "(#x < enat (Suc (Suc n))) = (!a y. x ~= a~> y | #y < enat (Suc n))" |
154 apply (simp add: fscons_def2 slen_scons_eq_rev) |
154 apply (simp add: fscons_def2 slen_scons_eq_rev) |
155 apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) |
155 apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>) |
156 apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) |
156 apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>) |
157 apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) |
157 apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>) |
158 apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) |
158 apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>) |
159 apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) |
159 apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>) |
160 apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) |
160 apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>) |
161 apply (erule contrapos_np) |
161 apply (erule contrapos_np) |
162 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
162 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
163 done |
163 done |
164 |
164 |
165 lemma slen_fscons_less_eq: |
165 lemma slen_fscons_less_eq: |