src/CCL/Fix.thy

 (*  Title:      CCL/Fix.thy
     Author:     Martin Coen
     Copyright   1993  University of Cambridge
 *)
 
-section {* Tentative attempt at including fixed point induction; justified by Smith *}
+section \<open>Tentative attempt at including fixed point induction; justified by Smith\<close>
 
 theory Fix
 imports Type
 begin
 

   INCL_def: "INCL(\<lambda>x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) \<longrightarrow> P(fix(f)))" and
   po_INCL: "INCL(\<lambda>x. a(x) [= b(x))" and
   INCL_subst: "INCL(P) \<Longrightarrow> INCL(\<lambda>x. P((g::i\<Rightarrow>i)(x)))"
 
 
-subsection {* Fixed Point Induction *}
+subsection \<open>Fixed Point Induction\<close>
 
 lemma fix_ind:
   assumes base: "P(bot)"
     and step: "\<And>x. P(x) \<Longrightarrow> P(f(x))"
     and incl: "INCL(P)"

    apply (rule base)
   apply (erule step)
   done
 
 
-subsection {* Inclusive Predicates *}
+subsection \<open>Inclusive Predicates\<close>
 
 lemma inclXH: "INCL(P) \<longleftrightarrow> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) \<longrightarrow> P(fix(f)))"
   by (simp add: INCL_def)
 
 lemma inclI: "\<lbrakk>\<And>f. ALL n:Nat. P(f^n`bot) \<Longrightarrow> P(fix(f))\<rbrakk> \<Longrightarrow> INCL(\<lambda>x. P(x))"

 
 lemma inclE: "\<lbrakk>INCL(P); (ALL n:Nat. P(f^n`bot)) \<longrightarrow> P(fix(f)) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   by (blast dest: inclD)
 
 
-subsection {* Lemmas for Inclusive Predicates *}
+subsection \<open>Lemmas for Inclusive Predicates\<close>
 
 lemma npo_INCL: "INCL(\<lambda>x. \<not> a(x) [= t)"
   apply (rule inclI)
   apply (drule bspec)
    apply (rule zeroT)

   apply (simp add: eq_iff)
   apply (rule conj_INCL po_INCL)+
   done
 
 
-subsection {* Derivation of Reachability Condition *}
+subsection \<open>Derivation of Reachability Condition\<close>
 
 (* Fixed points of idgen *)
 
 lemma fix_idgenfp: "idgen(fix(idgen)) = fix(idgen)"
   apply (rule fixB [symmetric])