src/HOL/HOLCF/Fun_Cpo.thy
changeset 41032 75b4ff66781c
parent 41030 ff7d177128ef
child 41430 1aa23e9f2c87
equal deleted inserted replaced
41031:9883d1417ce1 41032:75b4ff66781c
    77 by (rule is_lub_fun [THEN lub_eqI])
    77 by (rule is_lub_fun [THEN lub_eqI])
    78 
    78 
    79 instance "fun"  :: (type, cpo) cpo
    79 instance "fun"  :: (type, cpo) cpo
    80 by intro_classes (rule exI, erule is_lub_fun)
    80 by intro_classes (rule exI, erule is_lub_fun)
    81 
    81 
    82 subsection {* Chain-finiteness of function space *}
       
    83 
       
    84 lemma maxinch2maxinch_lambda:
       
    85   "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
       
    86 unfolding max_in_chain_def fun_eq_iff by simp
       
    87 
       
    88 lemma maxinch_mono:
       
    89   "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
       
    90 unfolding max_in_chain_def
       
    91 proof (intro allI impI)
       
    92   fix k
       
    93   assume Y: "\<forall>n\<ge>i. Y i = Y n"
       
    94   assume ij: "i \<le> j"
       
    95   assume jk: "j \<le> k"
       
    96   from ij jk have ik: "i \<le> k" by simp
       
    97   from Y ij have Yij: "Y i = Y j" by simp
       
    98   from Y ik have Yik: "Y i = Y k" by simp
       
    99   from Yij Yik show "Y j = Y k" by auto
       
   100 qed
       
   101 
       
   102 instance "fun" :: (type, discrete_cpo) discrete_cpo
    82 instance "fun" :: (type, discrete_cpo) discrete_cpo
   103 proof
    83 proof
   104   fix f g :: "'a \<Rightarrow> 'b"
    84   fix f g :: "'a \<Rightarrow> 'b"
   105   show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
    85   show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
   106     unfolding fun_below_iff fun_eq_iff
    86     unfolding fun_below_iff fun_eq_iff