--- a/src/HOL/HOLCF/ex/Focus_ex.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy Mon Jul 25 21:50:04 2016 +0200
@@ -107,46 +107,43 @@
instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity)
axiomatization
- Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
+ Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) \<Rightarrow> bool"
definition
- is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" where
- "is_f f = (!i1 i2 o1 o2. f$(i1,i2) = (o1,o2) --> Rf(i1,i2,o1,o2))"
+ is_f :: "('b stream * ('b,'c) tc stream \<rightarrow> 'c stream * ('b,'c) tc stream) \<Rightarrow> bool" where
+ "is_f f \<longleftrightarrow> (\<forall>i1 i2 o1 o2. f\<cdot>(i1, i2) = (o1, o2) \<longrightarrow> Rf (i1, i2, o1, o2))"
definition
- is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
- 'b stream => 'c stream => bool" where
- "is_net_g f x y == (? z.
- (y,z) = f$(x,z) &
- (!oy hz. (oy,hz) = f$(x,hz) --> z << hz))"
+ is_net_g :: "('b stream * ('b,'c) tc stream \<rightarrow> 'c stream * ('b,'c) tc stream) \<Rightarrow>
+ 'b stream \<Rightarrow> 'c stream \<Rightarrow> bool" where
+ "is_net_g f x y \<equiv> (\<exists>z.
+ (y, z) = f\<cdot>(x,z) \<and>
+ (\<forall>oy hz. (oy, hz) = f\<cdot>(x, hz) \<longrightarrow> z << hz))"
definition
- is_g :: "('b stream -> 'c stream) => bool" where
- "is_g g == (? f. is_f f & (!x y. g$x = y --> is_net_g f x y))"
+ is_g :: "('b stream \<rightarrow> 'c stream) \<Rightarrow> bool" where
+ "is_g g \<equiv> (\<exists>f. is_f f \<and> (\<forall>x y. g\<cdot>x = y \<longrightarrow> is_net_g f x y))"
definition
- def_g :: "('b stream -> 'c stream) => bool" where
- "def_g g == (? f. is_f f & g = (LAM x. fst (f$(x,fix$(LAM k. snd (f$(x,k)))))))"
+ def_g :: "('b stream \<rightarrow> 'c stream) => bool" where
+ "def_g g \<equiv> (\<exists>f. is_f f \<and> g = (LAM x. fst (f\<cdot>(x, fix\<cdot>(LAM k. snd (f\<cdot>(x, k)))))))"
(* first some logical trading *)
lemma lemma1:
-"is_g(g) =
- (? f. is_f(f) & (!x.(? z. (g$x,z) = f$(x,z) &
- (! w y. (y,w) = f$(x,w) --> z << w))))"
+ "is_g g \<longleftrightarrow>
+ (\<exists>f. is_f(f) \<and> (\<forall>x.(\<exists>z. (g\<cdot>x,z) = f\<cdot>(x,z) \<and> (\<forall>w y. (y, w) = f\<cdot>(x, w) \<longrightarrow> z << w))))"
apply (simp add: is_g_def is_net_g_def)
apply fast
done
lemma lemma2:
-"(? f. is_f(f) & (!x. (? z. (g$x,z) = f$(x,z) &
- (!w y. (y,w) = f$(x,w) --> z << w))))
- =
- (? f. is_f(f) & (!x. ? z.
- g$x = fst (f$(x,z)) &
- z = snd (f$(x,z)) &
- (! w y. (y,w) = f$(x,w) --> z << w)))"
+ "(\<exists>f. is_f f \<and> (\<forall>x. (\<exists>z. (g\<cdot>x, z) = f\<cdot>(x, z) \<and> (\<forall>w y. (y, w) = f\<cdot>(x,w) \<longrightarrow> z << w)))) \<longleftrightarrow>
+ (\<exists>f. is_f f \<and> (\<forall>x. \<exists>z.
+ g\<cdot>x = fst (f\<cdot>(x, z)) \<and>
+ z = snd (f\<cdot>(x, z)) \<and>
+ (\<forall>w y. (y, w) = f\<cdot>(x, w) \<longrightarrow> z << w)))"
apply (rule iffI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
@@ -180,7 +177,7 @@
apply simp
done
-lemma lemma3: "def_g(g) --> is_g(g)"
+lemma lemma3: "def_g g \<longrightarrow> is_g g"
apply (tactic \<open>simp_tac (put_simpset HOL_ss @{context}
addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1\<close>)
apply (rule impI)
@@ -189,7 +186,7 @@
apply (erule conjE)+
apply (erule conjI)
apply (intro strip)
-apply (rule_tac x = "fix$ (LAM k. snd (f$(x,k)))" in exI)
+apply (rule_tac x = "fix\<cdot>(LAM k. snd (f\<cdot>(x, k)))" in exI)
apply (rule conjI)
apply (simp)
apply (rule prod_eqI, simp, simp)
@@ -205,7 +202,7 @@
apply simp
done
-lemma lemma4: "is_g(g) --> def_g(g)"
+lemma lemma4: "is_g g \<longrightarrow> def_g g"
apply (tactic \<open>simp_tac (put_simpset HOL_ss @{context}
delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1\<close>)
@@ -218,12 +215,12 @@
apply (erule_tac x = "x" in allE)
apply (erule exE)
apply (erule conjE)+
-apply (subgoal_tac "fix$ (LAM k. snd (f$(x, k))) = z")
+apply (subgoal_tac "fix\<cdot>(LAM k. snd (f\<cdot>(x, k))) = z")
apply simp
-apply (subgoal_tac "! w y. f$(x, w) = (y, w) --> z << w")
+apply (subgoal_tac "\<forall>w y. f\<cdot>(x, w) = (y, w) \<longrightarrow> z << w")
apply (rule fix_eqI)
apply simp
-apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)")
+apply (subgoal_tac "f\<cdot>(x, za) = (fst (f\<cdot>(x, za)), za)")
apply fast
apply (rule prod_eqI, simp, simp)
apply (intro strip)
@@ -242,18 +239,14 @@
done
lemma L2:
-"(? f.
- is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
- -->
- (? g. def_g(g::'b stream -> 'c stream ))"
+ "(\<exists>f. is_f (f::'b stream * ('b,'c) tc stream \<rightarrow> 'c stream * ('b,'c) tc stream)) \<longrightarrow>
+ (\<exists>g. def_g (g::'b stream \<rightarrow> 'c stream))"
apply (simp add: def_g_def)
done
theorem conservative_loopback:
-"(? f.
- is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
- -->
- (? g. is_g(g::'b stream -> 'c stream ))"
+ "(\<exists>f. is_f (f::'b stream * ('b,'c) tc stream \<rightarrow> 'c stream * ('b,'c) tc stream)) \<longrightarrow>
+ (\<exists>g. is_g (g::'b stream \<rightarrow> 'c stream))"
apply (rule loopback_eq [THEN subst])
apply (rule L2)
done