src/HOL/Partial_Function.thy
changeset 59647 c6f413b660cf
parent 59517 22c9e6cf5572
child 60062 4c5de5a860ee
     1.1 --- a/src/HOL/Partial_Function.thy	Sat Mar 07 15:40:36 2015 +0100
     1.2 +++ b/src/HOL/Partial_Function.thy	Sat Mar 07 21:32:31 2015 +0100
     1.3 @@ -168,21 +168,23 @@
     1.4  text {* Fixpoint induction rule *}
     1.5  
     1.6  lemma fixp_induct_uc:
     1.7 -  fixes F :: "'c \<Rightarrow> 'c" and
     1.8 -    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
     1.9 -    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
    1.10 -    P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
    1.11 +  fixes F :: "'c \<Rightarrow> 'c"
    1.12 +    and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"
    1.13 +    and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
    1.14 +    and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
    1.15    assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
    1.16 -  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
    1.17 -  assumes inverse: "\<And>f. U (C f) = f"
    1.18 -  assumes adm: "ccpo.admissible lub_fun le_fun P"
    1.19 -  and bot: "P (\<lambda>_. lub {})"
    1.20 -  assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
    1.21 +    and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
    1.22 +    and inverse: "\<And>f. U (C f) = f"
    1.23 +    and adm: "ccpo.admissible lub_fun le_fun P"
    1.24 +    and bot: "P (\<lambda>_. lub {})"
    1.25 +    and step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
    1.26    shows "P (U f)"
    1.27  unfolding eq inverse
    1.28  apply (rule ccpo.fixp_induct[OF ccpo adm])
    1.29  apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
    1.30 -by (rule_tac f="C x" in step, simp add: inverse)
    1.31 +apply (rule_tac f5="C x" in step)
    1.32 +apply (simp add: inverse)
    1.33 +done
    1.34  
    1.35  
    1.36  text {* Rules for @{term mono_body}: *}