Theory Arity

theory Arity
imports "HOLCF-Join-Classes" Lifting
begin

typedef Arity = "UNIV :: nat set"
  morphisms Rep_Arity to_Arity by auto

setup_lifting type_definition_Arity

(*
instantiation Arity :: order
begin
lift_definition less_eq_Arity :: "Arity ⇒ Arity ⇒ bool" is "λ x y . x ≤ y".
lift_definition less_Arity :: "Arity ⇒ Arity ⇒ bool" is "λ x y . x < y".
instance
  apply standard
  apply (transfer, fastforce)+
  done
end
*)

instantiation Arity :: po
begin
lift_definition below_Arity :: "Arity ⇒ Arity ⇒ bool" is "λ x y . y ≤ x".

instance
apply standard
apply ((transfer, auto)+)
done
end

instance Arity :: chfin
proof
  fix S  :: "nat ⇒ Arity"
  assume "chain S"
  have "LeastM Rep_Arity (λx. x ∈ range S) ∈ range S"
    by (rule LeastM_natI) auto
  then obtain n where n: "S n = LeastM Rep_Arity (λx. x ∈ range S)" by auto
  have "max_in_chain n S"
  proof(rule max_in_chainI)
    fix j
    assume "n ≤ j" hence "S n ⊑ S j" using `chain S` by (metis chain_mono)
    also
    have "Rep_Arity (S n) ≤ Rep_Arity (S j)"
      unfolding n image_def
      by (metis (lifting, full_types) LeastM_nat_lemma UNIV_I mem_Collect_eq)
    hence "S j ⊑ S n" by transfer
    finally  
    show "S n = S j".
  qed
  thus "∃n. max_in_chain n S"..
qed

instance Arity :: cpo ..

lift_definition inc_Arity :: "Arity ⇒ Arity" is Suc.
lift_definition pred_Arity :: "Arity ⇒ Arity" is "(λ x . x - 1)".

lemma inc_Arity_cont[simp]: "cont inc_Arity"
  apply (rule chfindom_monofun2cont)
  apply (rule monofunI)
  apply (transfer, simp)
  done

lemma pred_Arity_cont[simp]: "cont pred_Arity"
  apply (rule chfindom_monofun2cont)
  apply (rule monofunI)
  apply (transfer, simp)
  done

definition inc :: "Arity → Arity" where
  "inc = (Λ x. inc_Arity x)"

definition pred :: "Arity → Arity" where
  "pred = (Λ x. pred_Arity x)"

lemma inc_inj[simp]: "inc⋅n = inc⋅n' ⟷ n = n'"
  by (simp add: inc_def pred_def, transfer, simp)

lemma pred_inc[simp]: "pred⋅(inc⋅n) = n" 
  by (simp add: inc_def pred_def, transfer, simp)

lemma inc_below_inc[simp]: "inc⋅a ⊑ inc⋅b ⟷ a ⊑ b"
  by (simp add: inc_def pred_def, transfer, simp)

lemma inc_below_below_pred[elim]:
  "inc⋅a ⊑ b ⟹ a ⊑ pred ⋅ b"
  by (simp add: inc_def pred_def, transfer, simp)

lemma Rep_Arity_inc[simp]: "Rep_Arity (inc⋅a') = Suc (Rep_Arity a')"
  by (simp add: inc_def pred_def, transfer, simp)

instantiation Arity :: zero
begin
lift_definition zero_Arity :: Arity is 0.
instance..
end

instantiation Arity :: one
begin
lift_definition one_Arity :: Arity is 1.
instance ..
end

lemma one_is_inc_zero: "1 = inc⋅0"
  by (simp add: inc_def, transfer, simp)

lemma inc_not_0[simp]: "inc⋅n = 0 ⟷ False"
  by (simp add: inc_def pred_def, transfer, simp)
 
lemma pred_0[simp]: "pred⋅0 = 0"
  by (simp add: inc_def pred_def, transfer, simp)
  
lemma Arity_ind:  "P 0 ⟹ (⋀ n. P n ⟹ P (inc⋅n)) ⟹ P n"
  apply (simp add: inc_def)
  apply transfer
  by (rule nat.induct) 
 
lemma Arity_total:   
  fixes x y :: Arity
  shows "x ⊑ y ∨ y ⊑ x"
by transfer auto

instance Arity :: Finite_Join_cpo
proof
  fix x y :: Arity
  show "compatible x y" by (metis Arity_total compatibleI)
qed

lemma Arity_zero_top[simp]: "(x :: Arity) ⊑ 0"
  by transfer simp

lemma Arity_above_top[simp]: "0 ⊑ (a :: Arity) ⟷ a = 0"
  by transfer simp

lemma Arity_zero_join[simp]: "(x :: Arity) ⊔ 0 = 0"
  by transfer simp
lemma Arity_zero_join2[simp]: "0 ⊔ (x :: Arity) = 0"
  by transfer simp

lemma Arity_up_zero_join[simp]: "(x :: Arity⇩⊥) ⊔ up⋅0 = up⋅0"
  by (cases x) auto
lemma Arity_up_zero_join2[simp]: "up⋅0 ⊔ (x :: Arity⇩⊥) = up⋅0"
  by (cases x) auto
lemma up_zero_top[simp]: "x ⊑ up⋅(0::Arity)"
  by (cases x) auto
lemma Arity_above_up_top[simp]: "up⋅0 ⊑ (a :: Arity⇩⊥) ⟷ a = up⋅0"
  by (metis Arity_up_zero_join2 join_self_below(4))


lemma Arity_exhaust: "(y = 0 ⟹ P) ⟹ (⋀x. y = inc ⋅ x ⟹ P) ⟹ P"
  by (metis Abs_cfun_inverse2 Arity.inc_def Rep_Arity_inverse inc_Arity.abs_eq inc_Arity_cont list_decode.cases zero_Arity_def)

end