Quelle  Examples.thy

section ‹Examples of Rensets and Renaming-Based Recursion›

theory Examples
  imports FRBCE_Rensets Rensets 
begin 

subsection ‹Variables and terms as rensets›

text ‹Variables form a renset: ›
interpretation Var: Renset where vsubstA = "vss"  
  unfolding Renset_def vss_def by auto

text ‹Terms form a renset: ›
interpretation Term: Renset where vsubstA = "λt x. vsubst t x"  
  unfolding Renset_def   
 using subst_Vr subst_comp_same  
 using fresh_subst_same subst_chain 
  using subst_commute_diff by auto

text ‹... and a CE renset: ›

interpretation Term: CE_Renset 
  where vsubstA = "λt x. subst t (Vr x)"  
    and VrA = Vr and ApA = Ap and LmA = Lm
  apply standard  
  by (auto simp add: Lm_subst_rename fresh_subst_same)


subsection ‹ Interpretation in semantic domains›

type_synonym 'A I = "(var ==> 'A) ==> 'A"

locale Sem_Int = 
  fixes ap :: "'A ==> 'A ==> 'A" and lm :: "('A ==> 'A) ==> 'A"
begin 

(* The target domain is a CE renset: *)
sublocale CE_Renset 
  where vsubstA = "λs x y ξ. s (ξ (y := ξ x))"
    and VrA = "λx ξ. ξ x" 
    and ApA = "λi1 i2 ξ. ap (i1 ξ) (i2 ξ)"
    and LmA = "λx i ξ. lm (λd. i (ξ(x:=d)))"
  by standard (auto simp: fun_eq_iff fun_upd_twist intro!: arg_cong[of _ _ lm]) 

(* ... hence the desired recursive clauses hold: *)
lemmas sem_f_clauses = f_Vr f_Ap f_Lm f_subst f_unique

end (* context Sem_Int *)


subsection ‹ Closure of rensets under functors ›

text ‹ A functor applied to a renset yields a renset -- actually,
  "local functor", i.e., one that is functorial
 .r.t. functions on the substitutive set's carrier only, suffices. ›


locale Local_Functor = 
  fixes Fmap :: "('A ==> 'A) ==> 'FA ==> 'FA"
  assumes Fmap_id: "Fmap id = id"
    and Fmap_comp: "Fmap (g o f) = Fmap g o Fmap f"
begin

lemma Fmap_comp': "Fmap (g o f) k = Fmap g (Fmap f k)"
  using Fmap_comp by auto

end (* context Local_Functor *)


locale Renset_plus_Local_Functor = 
  Renset vsubstA + Local_Functor Fmap 
  for vsubstA :: "'A ==> var ==> var ==> 'A" 
    and Fmap :: "('A ==> 'A) ==> 'FA ==> 'FA" 
begin

(* The new renset with carrier 'A F: *)
sublocale F: Renset where vsubstA = 
  "λk x y. Fmap (λa. vsubstA a x y) k" 
  apply standard
  subgoal by (metis Fmap_id eq_id_iff vsubstA_id)
  subgoal unfolding Fmap_comp'[symmetric] o_def by simp
  subgoal unfolding Fmap_comp'[symmetric] o_def  
   by (simp add: vsubstA_chain)
  subgoal unfolding Fmap_comp'[symmetric] o_def  
    using vsubstA_commute_diff by force .

end (* context Renset_plus_Local_Functor *)


subsection ‹ The length of a term via renaming-based recursion ›

(* The target domain is a CE substitutive set: *)
interpretation length : CE_Renset
  where vsubstA = "λn x y. n"
    and VrA = "λx. 1" 
    and ApA = "λn1 n2. max n1 n2 + 1" 
    and LmA = "λx n. n + 1"
  apply standard by auto

(* ... hence the desired recursive clauses hold: *)
lemmas length_f_clauses = length.f_Vr length.f_Ap length.f_Lm length.f_subst length.f_unique


subsection ‹ Counting the lambda-abstractions in a term via renaming-based recursion ›

(* The target domain is a CE substitutive set: *)
interpretation clam : CE_Renset
  where vsubstA = "λn x y. n"
    and VrA = "λx. 0" 
    and ApA = "λn1 n2. n1 + n2" 
    and LmA = "λx n. n + 1"
  apply standard by auto

(* ... hence the desired recursive clauses hold: *)
lemmas clam_f_clauses = clam.f_Vr clam.f_Ap clam.f_Lm clam.f_subst clam.f_unique


subsection ‹ Counting free occurences of a variable in a term via renaming-based recursion ›

(* Counting the number of free occurrences of a variable in a term *)
(* The target domain is a CE substitutive set: *)
interpretation cfv : CE_Renset
  where vsubstA = 
    "λf z y. λx. if x ∉ {y,z}
     then f x
     else if x = z ∧ x ≠ y then f x + f y
     else if x = y ∧ x ≠ z then (0::nat)
     else f y"
    and VrA = "λy. λx. if x = y then 1 else 0" 
    and ApA = "λf1 f2. λx. f1 x + f2 x" 
    and LmA = "λy f. λx. if x = y then 0 else f x"
  apply standard by (auto simp: fun_eq_iff)

(* ... hence the desired recursive clauses hold: *)
lemmas cfv_f_clauses = cfv.f_Vr cfv.f_Ap cfv.f_Lm cfv.f_subst cfv.f_unique


subsection ‹ Substitution via renaming-based recursion ›

(* The target domain is a CE substitutive set: *)
locale Subst = 
  fixes s :: trm and x :: var
begin

sublocale ssb : BCE_Renset
  where vsubstA = "vsubst"
    and VrA = "λy. if y = x then s else Vr y" 
    and ApA = "Ap" 
    and LmA = "Lm"
    and X = "FFvars s ∪ {x}"
  apply standard by (auto simp: fun_eq_iff cofinite_fresh Term.LmA_rename) 

(* ... hence the desired recursive clauses hold: *)
lemmas ssb_f_clauses = ssb.f_Vr ssb.f_Ap ssb.f_Lm ssb.f_subst ssb.f_unique

(* We actually already have the substitution operator defined, 
and the one defined above can be proved to be the same as this: *)

lemma subst_eq_ssb: 
  "subst t s x = ssb.f t"
proof-
  have "(λt. subst t s x) = ssb.f" 
    apply(rule ssb.f_unique) by auto
  thus ?thesis unfolding fun_eq_iff by auto
qed

end (* context Subst *)


subsection ‹ Parrallel substitution via renaming-based recursion ›

(* The target domain is a CE substitutive set: *)
locale PSubst = 
  fixes ρ :: fenv
begin

definition X where
  "X = supp ρ ∪ ∪ {FFvars (get ρ x) | x . x ∈ supp ρ}"

lemma finite_Supp: "finite X" 
  unfolding X_def unfolding finite_Un apply safe
  by (auto simp: finite_supp cofinite_fresh)

sublocale canEta' : BCE_Renset
  where vsubstA = "vsubst"
    and VrA = "λy. get ρ y" 
    and ApA = "Ap" 
    and LmA = "Lm"
    and X = "X" 
  apply standard
  by (auto simp: fun_eq_iff cofinite_fresh finite_Supp Term.LmA_rename X_def finite_supp)
    (metis fresh_subst_id mem_Collect_eq subst_Vr supp_get)

(* ... hence the desired recursive clauses hold: *)
lemmas canEta'_f_clauses =  canEta'.f_Vr canEta'.f_Ap canEta'.f_Lm canEta'.f_subst canEta'.f_unique

end (* context PSubst *)


subsection ‹ Counting bound variables via renaming-based recursion ›

(* Counting the number of bound variables *)

(* This is an instance of the semantic-domain interpretation pattern: *)
interpretation cbvs: Sem_Int where ap = "(+)" and lm = "λd. d (1::nat)" .

(* ... hence the desired recursive clauses hold: *)
lemmas cbvs_f_clauses = cbvs.f_Vr cbvs.f_Ap cbvs.f_Lm cbvs.f_subst cbvs.f_unique

definition cbv  :: "trm ==> nat" where 
  "cbv t ≡ cbvs.f t (λ_. 0)"


subsection ‹ Testing eta-reducibility via renaming-based recursion ›

(* This is an instance of the semantic-domain interpretation pattern: *)
interpretation canEta': Sem_Int where ap = "(∧)" and lm = "λd. d True" .

(* ... hence the desired recursive clauses hold: *)
lemmas canEta'_f_clauses = canEta'.f_Vr canEta'.f_Ap canEta'.f_Lm canEta'.f_subst canEta'.f_unique

definition canEta  :: "trm ==> bool" where 
  "canEta t ≡ ∃x s. t = Lm x (Ap s (Vr x)) ∧ canEta'.f s ((λ_. True)(x:=False))"


end