subsection‹Constructive Functions›
theory Constructive imports Main
begin
notation
bot ("⊥") and
top ("⊤") and
inf (infixl "⊓" 70)
and sup (infixl "⊔" 65)
class order_bot_max = order_bot +
fixes maximal :: "'a ⇒ bool"
assumes maximal_def: "maximal x = (∀ y . ¬ x < y)"
assumes [simp]: "¬ maximal ⊥"
begin
lemma ex_not_le_bot[simp]: "∃ a. ¬ a ≤ ⊥"
apply (subgoal_tac "¬ maximal ⊥")
apply (subst (asm) maximal_def, simp_all add: less_le, auto)
apply (rule_tac x = x in exI, auto)
apply (subgoal_tac "x = ⊥", simp)
by (rule antisym, simp_all)
end
instantiation "option" :: (type) order_bot_max
begin
definition bot_option_def: "(⊥::'a option) = None"
definition le_option_def: "((x::'a option) ≤ y) = (x = None ∨ x = y)"
definition less_option_def: "((x::'a option) < y) = (x ≤ y ∧ ¬ (y ≤ x))"
definition maximal_option_def: "maximal (x::'a option) = (∀ y . ¬ x < y)"
instance
proof
qed (auto simp add: le_option_def less_option_def maximal_option_def bot_option_def)
lemma [simp]: "None ≤ x"
by (subst bot_option_def [THEN sym], simp)
end
context order_bot
begin
definition "is_lfp f x = ((f x = x) ∧ (∀ y . f y = y ⟶ x ≤ y))"
definition "emono f = (∀ x y. x ≤ y ⟶ f x ≤ f y)"
definition "Lfp f = Eps (is_lfp f)"
lemma lfp_unique: "is_lfp f x ⟹ is_lfp f y ⟹ x = y"
apply (simp add: is_lfp_def)
by (simp add: local.antisym)
lemma lfp_exists: "is_lfp f x ⟹ Lfp f = x"
apply (rule lfp_unique, simp_all)
by (simp add: Lfp_def someI)
lemma emono_a: "emono f ⟹ x ≤ y ⟹ f x ≤ f y"
by (simp add: emono_def)
lemma emono_fix: "emono f ⟹ f y = y ⟹ (f ^^ n) ⊥ ≤ y"
apply (induction n)
apply (simp_all)
apply (drule emono_a, simp_all)
by simp
lemma emono_is_lfp: "emono (f::'a ⇒ 'a) ⟹ (f ^^ (n + 1)) ⊥ = (f ^^ n) ⊥ ⟹ is_lfp f ((f ^^ n) ⊥)"
apply (simp add: is_lfp_def, safe)
by (rule emono_fix, simp_all)
lemma emono_lfp_bot: "emono (f::'a ⇒ 'a) ⟹ (f ^^ (n + 1)) ⊥ = (f ^^ n) ⊥ ⟹ Lfp f = ((f ^^ n) ⊥)"
apply (drule emono_is_lfp, simp_all)
by (simp add: lfp_exists)
lemma emono_up: "emono f ⟹ (f ^^ n) ⊥ ≤ (f ^^ (Suc n)) ⊥"
apply (induction n)
apply (simp_all)
by (drule emono_a, simp_all)
end
context order
begin
definition "min_set A = (SOME n . n ∈ A ∧ (∀ x ∈ A . n ≤ x))"
end
lemma min_nonempty_nat_set_aux: "∀ A . (n::nat) ∈ A ⟶ (∃ k ∈ A . (∀ x ∈ A . k ≤ x))"
apply (induction n, safe)
apply (rule_tac x = 0 in bexI, simp_all)
apply (case_tac "0 ∈ A")
apply (rule_tac x = 0 in bexI, simp_all)
apply (drule_tac x = "{n . Suc n ∈ A}" in spec)
apply safe
apply (rule_tac x = "Suc k" in bexI, simp_all, safe)
apply (drule_tac x = "x - 1" in spec)
by (case_tac x, simp_all)
lemma min_nonempty_nat_set: "(n::nat) ∈ A ⟹ (∃ k . k ∈ A ∧ (∀ x ∈ A . k ≤ x))"
by (cut_tac min_nonempty_nat_set_aux, auto)
thm someI_ex
lemma min_set_nat_aux: "(n::nat) ∈ A ⟹ min_set A ∈ A ∧ (∀ x ∈ A . min_set A ≤ x)"
apply (simp add: min_set_def)
apply (drule min_nonempty_nat_set)
by (rule someI_ex, simp_all)
lemma "(n::nat) ∈ A ⟹ min_set A ∈ A ∧ min_set A ≤ n"
by (simp add: min_set_nat_aux)
lemma min_set_in: "(n::nat) ∈ A ⟹ min_set A ∈ A"
by (simp add: min_set_nat_aux)
lemma min_set_less: "(n::nat) ∈ A ⟹ min_set A ≤ n"
by (simp add: min_set_nat_aux)
definition "mono_a f = (∀ a b a' b'. (a::'a::order) ≤ a' ∧ (b::'b::order) ≤ b' ⟶ f a b ≤ f a' b')"
class fin_cpo = order_bot_max +
assumes fin_up_chain: "(∀ i:: nat . a i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
begin
lemma emono_ex_lfp: "emono f ⟹ ∃ n . is_lfp f ((f ^^ n) ⊥)"
apply (cut_tac a = "λ i . (f ^^ i) ⊥" in fin_up_chain)
apply (safe, rule emono_up, simp)
apply (rule_tac x= n in exI)
apply (rule emono_is_lfp, simp)
by (drule_tac x = "n + 1" in spec, simp)
lemma emono_lfp: "emono f ⟹ ∃ n . Lfp f = (f ^^ n) ⊥"
apply (drule emono_ex_lfp, safe)
apply (rule_tac x = n in exI)
by (rule lfp_exists, simp)
lemma emono_is_lfp: "emono f ⟹ is_lfp f (Lfp f)"
apply (drule emono_ex_lfp, safe)
by (frule lfp_exists, simp)
definition "lfp_index (f::'a ⇒ 'a) = min_set {n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}"
lemma lfp_index_aux: "emono f ⟹ (∀ i < (lfp_index f) . (f ^^ i) ⊥ < (f ^^ (i + 1)) ⊥) ∧ (f ^^ (lfp_index f)) ⊥ = (f ^^ ((lfp_index f) + 1)) ⊥"
apply (simp add: lfp_index_def)
apply safe
apply (simp add: less_le_not_le, safe)
apply (cut_tac n = i in emono_up, simp_all)
apply (cut_tac n = i and A = "{n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}" in min_set_less, simp)
apply (rule antisym, simp_all)
apply (cut_tac n = i in emono_up, simp_all)
apply (cut_tac a = "λ i . (f ^^ i) ⊥" in fin_up_chain, simp, safe)
apply (drule emono_up, simp)
apply (cut_tac n = "n" and A = "{n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}" in min_set_in)
apply (drule_tac x = "Suc n" in spec, simp)
by simp
lemma [simp]: "emono f ⟹ i < lfp_index f ⟹ (f ^^ i) ⊥ < f ((f ^^ i) ⊥)"
by (drule lfp_index_aux, simp)
lemma [simp]: "emono f ⟹ f ((f ^^ (lfp_index f)) ⊥) = (f ^^ (lfp_index f)) ⊥"
by (drule lfp_index_aux, simp)
lemma "emono f ⟹ Lfp f = (f ^^ lfp_index f) ⊥"
by (rule emono_lfp_bot, simp_all)
lemma AA_aux: "emono f ⟹ (⋀ b . b ≤ a ⟹ f b ≤ a) ⟹ (f ^^ n) ⊥ ≤ a"
by (induction n, simp_all)
lemma AA: "emono f ⟹ (⋀ b . b ≤ a ⟹ f b ≤ a) ⟹ Lfp f ≤ a"
apply (cut_tac f = f in emono_lfp, simp_all, safe, simp)
by (simp add: AA_aux)
lemma BB: "emono f ⟹ f (Lfp f) = Lfp f"
using local.emono_is_lfp local.is_lfp_def by blast
lemma Lfp_mono: "emono f ⟹ emono g ⟹ (⋀ a . f a ≤ g a) ⟹ Lfp f ≤ Lfp g"
by (metis AA BB local.emono_def local.order_trans)
end
declare [[show_types]]
lemma [simp]: "mono_a f ⟹ emono (f a)"
by (simp add: emono_def mono_a_def)
lemma [simp]: "mono_a f ⟹ emono (λ a . f a b)"
by (simp add: emono_def mono_a_def)
lemma mono_aD: "mono_a f ⟹ a ≤ a' ⟹ b ≤ b' ⟹ f a b ≤ f a' b'"
by (simp add: mono_a_def)
lemma [simp]: "mono_a (f::'a::fin_cpo ⇒ 'b::fin_cpo ⇒ 'b) ⟹ mono_a g ⟹ emono (λb. f (Lfp (g b)) b)"
apply (simp add: emono_def, safe)
apply (rule_tac f = f in mono_aD, simp_all)
by (rule Lfp_mono, simp_all add: mono_a_def)
lemma CCC: "mono_a (f::'a::fin_cpo ⇒ 'b::fin_cpo ⇒ 'b) ⟹ mono_a g ⟹ Lfp (λa. g (Lfp (f a)) a) ≤ Lfp (g (Lfp (λb. f (Lfp (g b)) b)))"
apply (rule AA, simp_all)
apply (subst (2) BB [THEN sym], simp_all)
apply (rule_tac f = g in mono_aD, simp_all)
apply (rule AA, simp_all)
apply (subst BB [THEN sym], simp_all)
by (rule_tac f = f in mono_aD, simp_all)
lemma Lfp_commute: "mono_a (f::'a::fin_cpo ⇒ 'b::fin_cpo ⇒ 'b::fin_cpo) ⟹ mono_a g ⟹ Lfp (λ b . f (Lfp (λ a . (g (Lfp (f a))) a)) b) = Lfp (λ b . f (Lfp (g b)) b)"
apply (rule antisym)
apply (rule AA, simp_all)
apply (subst (3) BB [THEN sym], simp_all)
apply (rule_tac f = f in mono_aD)
apply simp_all
by (simp_all add: CCC)
instantiation "option" :: (type) fin_cpo
begin
lemma fin_up_non_bot: "(∀ i . (a::nat ⇒ 'a option) i ≤ a (Suc i)) ⟹ a n ≠ ⊥ ⟹ n ≤ i ⟹ a i = a n"
apply (induction i, simp_all)
apply (case_tac "n ≤ i", simp_all)
apply (drule_tac x = i in spec)
apply (simp add: le_option_def bot_option_def, safe, simp_all)
using le_Suc_eq by blast
lemma fin_up_chain_option: "(∀ i:: nat . (a::nat ⇒ 'a option) i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
apply (case_tac "∃ n . a n ≠ ⊥", safe, simp_all)
apply (rule_tac x = n in exI, safe)
by (rule fin_up_non_bot, simp_all)
instance
proof
qed (simp add: fin_up_chain_option)
end
instantiation "prod" :: (order_bot_max, order_bot_max) order_bot_max
begin
definition bot_prod_def: "(⊥ :: 'a × 'b) = (⊥, ⊥)"
definition le_prod_def: "(x ≤ y) = (fst x ≤ fst y ∧ snd x ≤ snd y)"
definition less_prod_def: "((x::'a×'b) < y) = (x ≤ y ∧ ¬ (y ≤ x))"
definition maximal_prod_def: "maximal (x::'a × 'b) = (∀ y . ¬ x < y)"
instance proof
qed (auto simp add: le_prod_def less_prod_def bot_prod_def maximal_prod_def)
end
instantiation "prod" :: (fin_cpo, fin_cpo) fin_cpo
begin
lemma fin_up_chain_prod: "(∀ i:: nat . (a::nat ⇒ 'a × 'b) i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
apply (cut_tac a = "fst o a" in fin_up_chain)
apply (simp add: le_prod_def)
apply (cut_tac a = "snd o a" in fin_up_chain)
apply (simp add: le_prod_def)
apply safe
apply (rule_tac x = "max n na" in exI)
by (metis (no_types, hide_lams) comp_apply max.bounded_iff max.cobounded1 max.cobounded2 prod.collapse)
instance proof
qed (auto simp add: fin_up_chain_prod)
end
end