# HG changeset patch
# User huffman
# Date 1213302600 -7200
# Node ID 0407630909eff96549a71a2fecf404188319b322
# Parent  b1483d423512074ca07eca7c8a4a5356a376a166
change orientation of fix_eqI and convert to rule_format;
add lemma fix_ind2

diff -r b1483d423512 -r 0407630909ef src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Thu Jun 12 22:29:51 2008 +0200
+++ b/src/HOLCF/Fix.thy	Thu Jun 12 22:30:00 2008 +0200
@@ -106,10 +106,12 @@
 lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
 by (rule fix_least_less, simp)
 
-lemma fix_eqI: "\<lbrakk>F\<cdot>x = x; \<forall>z. F\<cdot>z = z \<longrightarrow> x \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x = fix\<cdot>F"
+lemma fix_eqI:
+  assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
+  shows "fix\<cdot>F = x"
 apply (rule antisym_less)
-apply (simp add: fix_eq [symmetric])
-apply (erule fix_least)
+apply (rule fix_least [OF fixed])
+apply (rule least [OF fix_eq [symmetric]])
 done
 
 lemma fix_eq2: "f \<equiv> fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
@@ -152,16 +154,32 @@
 subsection {* Fixed point induction *}
 
 lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
-apply (subst fix_def2)
+unfolding fix_def2
 apply (erule admD)
 apply (rule chain_iterate)
-apply (induct_tac "i", simp_all)
+apply (rule nat_induct, simp_all)
 done
 
 lemma def_fix_ind:
   "\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
 by (simp add: fix_ind)
 
+lemma fix_ind2:
+  assumes adm: "adm P"
+  assumes 0: "P \<bottom>" and 1: "P (F\<cdot>\<bottom>)"
+  assumes step: "\<And>x. \<lbrakk>P x; P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (F\<cdot>(F\<cdot>x))"
+  shows "P (fix\<cdot>F)"
+unfolding fix_def2
+apply (rule admD [OF adm chain_iterate])
+apply (rule nat_less_induct)
+apply (case_tac n)
+apply (simp add: 0)
+apply (case_tac nat)
+apply (simp add: 1)
+apply (frule_tac x=nat in spec)
+apply (simp add: step)
+done
+
 subsection {* Recursive let bindings *}
 
 definition
@@ -198,7 +216,7 @@
    \<langle>\<mu> x. cfst\<cdot>(F\<cdot>\<langle>x, \<mu> y. csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)\<rangle>),
     \<mu> y. csnd\<cdot>(F\<cdot>\<langle>\<mu> x. cfst\<cdot>(F\<cdot>\<langle>x, \<mu> y. csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)\<rangle>), y\<rangle>)\<rangle>"
   (is "fix\<cdot>F = \<langle>?x, ?y\<rangle>")
-proof (rule fix_eqI [rule_format, symmetric])
+proof (rule fix_eqI)
   have 1: "cfst\<cdot>(F\<cdot>\<langle>?x, ?y\<rangle>) = ?x"
     by (rule trans [symmetric, OF fix_eq], simp)
   have 2: "csnd\<cdot>(F\<cdot>\<langle>?x, ?y\<rangle>) = ?y"
diff -r b1483d423512 -r 0407630909ef src/HOLCF/ex/Focus_ex.thy
--- a/src/HOLCF/ex/Focus_ex.thy	Thu Jun 12 22:29:51 2008 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy	Thu Jun 12 22:30:00 2008 +0200
@@ -224,17 +224,17 @@
 apply (subgoal_tac "fix$ (LAM k. csnd$ (f$<x, k>)) = z")
  apply simp
 apply (subgoal_tac "! w y. f$<x, w> = <y, w> --> z << w")
-apply (rule sym)
 apply (rule fix_eqI)
 apply simp
-apply (rule allI)
-apply (tactic "simp_tac HOLCF_ss 1")
-apply (intro strip)
+(*apply (rule allI)*)
+(*apply (tactic "simp_tac HOLCF_ss 1")*)
+(*apply (intro strip)*)
 apply (subgoal_tac "f$<x, za> = <cfst$ (f$<x,za>) ,za>")
 apply fast
 apply (rule trans)
 apply (rule surjective_pairing_Cprod2 [symmetric])
-apply (erule cfun_arg_cong)
+apply (rule cfun_arg_cong)
+apply simp
 apply (intro strip)
 apply (erule allE)+
 apply (erule mp)