<commit_before>(*  Title:      HOLCF/FunCpo.thy
    ID:         $Id$
    Author:     <NAME>

Definition of the partial ordering for the type of all functions => (fun)

Class instance of  => (fun) for class pcpo.
*)

header {* Class instances for the full function space *}

theory Ffun
imports Pcpo
begin

subsection {* Full function space is a partial order *}

instance "fun"  :: (type, sq_ord) sq_ord ..

defs (overloaded)
  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  

lemma refl_less_fun: "(f::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f"
by (simp add: less_fun_def)

lemma antisym_less_fun:
  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f1\<rbrakk> \<Longrightarrow> f1 = f2"
by (simp add: less_fun_def expand_fun_eq antisym_less)

lemma trans_less_fun:
  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f3\<rbrakk> \<Longrightarrow> f1 \<sqsubseteq> f3"
apply (unfold less_fun_def)
apply clarify
apply (rule trans_less)
apply (erule spec)
apply (erule spec)
done

instance "fun"  :: (type, po) po
by intro_classes
  (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+

text {* make the symbol @{text "<<"} accessible for type fun *}

lemma expand_fun_less: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
by (simp add: less_fun_def)

lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
by (simp add: less_fun_def)

subsection {* Full function space is chain complete *}

text {* chains of functions yield chains in the po range *}

lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
by (simp add: chain_def less_fun_def)

lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
by (simp add: chain_def less_fun_def)


text {* upper bounds of function chains yield upper bound in the po range *}

lemma ub2ub_fun:
  "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
by (auto simp add: is_ub_def less_fun_def)

text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}

lemma lub_fun:
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"<commit_msg>update instance proofs to new style<commit_after>(*  Title:      HOLCF/FunCpo.thy
    ID:         $Id$
    Author:     <NAME>

Definition of the partial ordering for the type of all functions => (fun)

Class instance of  => (fun) for class pcpo.
*)

header {* Class instances for the full function space *}

theory Ffun
imports Pcpo
begin

subsection {* Full function space is a partial order *}

instantiation "fun"  :: (type, sq_ord) sq_ord
begin

definition
  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  

instance ..
end

instance "fun" :: (type, po) po
proof
  fix f :: "'a \<Rightarrow> 'b"
  show "f \<sqsubseteq> f"
    by (simp add: less_fun_def)
next
  fix f g :: "'a \<Rightarrow> 'b"
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
    by (simp add: less_fun_def expand_fun_eq antisym_less)
next
  fix f g h :: "'a \<Rightarrow> 'b"
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
    unfolding less_fun_def by (fast elim: trans_less)
qed

text {* make the symbol @{text "<<"} accessible for type fun *}

lemma expand_fun_less: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
by (simp add: less_fun_def)

lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
by (simp add: less_fun_def)

subsection {* Full function space is chain complete *}

text {* chains of functions yield chains in the po range *}

lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
by (simp add: chain_def less_fun_def)

lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
by (simp add: chain_def less_fun_def)


text {* upper bounds of function chains yield upper bound in the po range *}

lemma ub2ub_fun:
  "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
by (auto simp add: is_ub_def less_fun_def)

text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}

lemma lub_fun:
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
{'fraction_non_alphanumeric': 0.1542565014447655, 'fraction_numerical': 0.004000889086463659, 'mean_word_length': 4.033557046979865, 'pattern_counts': {'":': 0, '<': 93, '<?xml version=': 0, '>': 87, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5351795', 'n_tokens_mistral': 1740, 'n_tokens_neox': 1644, 'n_words': 575}