Theory Higher_Order_Terms.Term_to_Nterm
chapter ‹Converting between ‹term›s and ‹nterm›s›
theory Term_to_Nterm
imports
Fresh_Class
Find_First
Term
Nterm
begin
section ‹‹α›-equivalence›
inductive alpha_equiv :: "(name, name) fmap ⇒ nterm ⇒ nterm ⇒ bool" where
const: "alpha_equiv env (Nconst x) (Nconst x)" |
var1: "x |∉| fmdom env ⟹ x |∉| fmran env ⟹ alpha_equiv env (Nvar x) (Nvar x)" |
var2: "fmlookup env x = Some y ⟹ alpha_equiv env (Nvar x) (Nvar y)" |
abs: "alpha_equiv (fmupd x y env) n1 n2 ⟹ alpha_equiv env (Λ⇩n x. n1) (Λ⇩n y. n2)" |
app: "alpha_equiv env n1 n2 ⟹ alpha_equiv env m1 m2 ⟹ alpha_equiv env (n1 $⇩n m1) (n2 $⇩n m2)"
code_pred alpha_equiv .
abbreviation alpha_eq :: "nterm ⇒ nterm ⇒ bool" (infixl ‹≈⇩α› 50) where
"alpha_eq n1 n2 ≡ alpha_equiv fmempty n1 n2"
lemma alpha_equiv_refl[intro?]:
assumes "fmpred (=) Γ"
shows "alpha_equiv Γ t t"
using assms proof (induction t arbitrary: Γ)
case Napp
show ?case
apply (rule alpha_equiv.app; rule Napp)
using Napp.prems unfolding fdisjnt_alt_def by auto
qed (auto simp: fdisjnt_alt_def intro: alpha_equiv.intros)
corollary alpha_eq_refl: "alpha_eq t t"
by (auto intro: alpha_equiv_refl)
section ‹From @{typ term} to @{typ nterm}›
fun term_to_nterm :: "name list ⇒ term ⇒ (name, nterm) state" where
"term_to_nterm _ (Const name) = State_Monad.return (Nconst name)" |
"term_to_nterm _ (Free name) = State_Monad.return (Nvar name)" |
"term_to_nterm Γ (Bound n) = State_Monad.return (Nvar (Γ ! n))" |
"term_to_nterm Γ (Λ t) = do {
n ← fresh_create;
e ← term_to_nterm (n # Γ) t;
State_Monad.return (Λ⇩n n. e)
}" |
"term_to_nterm Γ (t⇩1 $ t⇩2) = do {
e⇩1 ← term_to_nterm Γ t⇩1;
e⇩2 ← term_to_nterm Γ t⇩2;
State_Monad.return (e⇩1 $⇩n e⇩2)
}"
lemmas term_to_nterm_induct = term_to_nterm.induct[case_names const free bound abs app]
lemma term_to_nterm:
assumes "no_abs t"
shows "fst (run_state (term_to_nterm Γ t) x) = convert_term t"
using assms
apply (induction arbitrary: x)
apply auto
by (auto simp: free_term_def free_nterm_def const_term_def const_nterm_def app_term_def app_nterm_def split_beta split: prod.splits)
definition term_to_nterm' :: "term ⇒ nterm" where
"term_to_nterm' t = frun_fresh (term_to_nterm [] t) (frees t)"
lemma term_to_nterm_mono: "mono_state (term_to_nterm Γ x)"
by (induction Γ x rule: term_to_nterm.induct) (auto intro: bind_mono_strong)
lemma term_to_nterm_vars0:
assumes "wellformed' (length Γ) t"
shows "frees (fst (run_state (term_to_nterm Γ t) s)) |⊆| frees t |∪| fset_of_list Γ"
using assms proof (induction Γ t arbitrary: s rule: term_to_nterm_induct)
case (bound Γ i)
hence "Γ ! i |∈| fset_of_list Γ"
including fset.lifting by transfer auto
thus ?case
by (auto simp: State_Monad.return_def)
next
case (abs Γ t)
let ?x = "next s"
from abs have "frees (fst (run_state (term_to_nterm (?x # Γ) t) ?x)) |⊆| frees t |∪| {|?x|} |∪| fset_of_list Γ"
by simp
thus ?case
by (auto simp: create_alt_def split_beta)
qed (auto simp: split_beta)
corollary term_to_nterm_vars:
assumes "wellformed t"
shows "frees (fresh_frun (term_to_nterm [] t) F) |⊆| frees t"
proof -
let ?Γ = "[]"
from assms have "wellformed' (length ?Γ) t"
by simp
hence "frees (fst (run_state (term_to_nterm ?Γ t) (fNext F))) |⊆| (frees t |∪| fset_of_list ?Γ)"
by (rule term_to_nterm_vars0)
thus ?thesis
by (simp add: fresh_fNext_def fresh_frun_def)
qed
corollary term_to_nterm_closed: "closed t ⟹ wellformed t ⟹ closed (term_to_nterm' t)"
using term_to_nterm_vars[where F = "frees t" and t = t, simplified]
unfolding closed_except_def term_to_nterm'_def
by (simp add: fresh_frun_def)
lemma term_to_nterm_consts: "pred_state (λt'. consts t' = consts t) (term_to_nterm Γ t)"
apply (rule pred_stateI)
apply (induction t arbitrary: Γ)
apply (auto split: prod.splits)
done
section ‹From @{typ nterm} to @{typ term}›
fun nterm_to_term :: "name list ⇒ nterm ⇒ term" where
"nterm_to_term Γ (Nconst name) = Const name" |
"nterm_to_term Γ (Nvar name) = (case find_first name Γ of Some n ⇒ Bound n | None ⇒ Free name)" |
"nterm_to_term Γ (t $⇩n u) = nterm_to_term Γ t $ nterm_to_term Γ u" |
"nterm_to_term Γ (Λ⇩n x. t) = Λ nterm_to_term (x # Γ) t"
lemma nterm_to_term:
assumes "no_abs t" "fdisjnt (fset_of_list Γ) (frees t)"
shows "nterm_to_term Γ t = convert_term t"
using assms proof (induction arbitrary: Γ)
case (free name)
then show ?case
apply simp
apply (auto simp: free_nterm_def free_term_def fdisjnt_alt_def split: option.splits)
apply (rule find_first_none)
by (metis fset_of_list_elem)
next
case (const name)
show ?case
apply simp
by (simp add: const_nterm_def const_term_def)
next
case (app t⇩1 t⇩2)
then have "nterm_to_term Γ t⇩1 = convert_term t⇩1" "nterm_to_term Γ t⇩2 = convert_term t⇩2"
by (auto simp: fdisjnt_alt_def finter_funion_distrib)
then show ?case
apply simp
by (simp add: app_nterm_def app_term_def)
qed
abbreviation "nterm_to_term' ≡ nterm_to_term []"
lemma nterm_to_term': "no_abs t ⟹ nterm_to_term' t = convert_term t"
by (auto simp: fdisjnt_alt_def nterm_to_term)
lemma nterm_to_term_frees[simp]: "frees (nterm_to_term Γ t) = frees t - fset_of_list Γ"
proof (induction t arbitrary: Γ)
case (Nvar name)
show ?case
proof (cases "find_first name Γ")
case None
hence "name |∉| fset_of_list Γ"
including fset.lifting
by transfer (metis find_first_some option.distinct(1))
with None show ?thesis
by auto
next
case (Some u)
hence "name |∈| fset_of_list Γ"
including fset.lifting
by transfer (metis find_first_none option.distinct(1))
with Some show ?thesis
by auto
qed
qed (auto split: option.splits)
section ‹Correctness›
text ‹Some proofs in this section have been contributed by Yu Zhang.›
lemma term_to_nterm_nterm_to_term0:
assumes "wellformed' (length Γ) t" "fdisjnt (fset_of_list Γ) (frees t)" "distinct Γ"
assumes "fBall (frees t |∪| fset_of_list Γ) (λx. x ≤ s)"
shows "nterm_to_term Γ (fst (run_state (term_to_nterm Γ t) s)) = t"
using assms proof (induction Γ t arbitrary: s rule: term_to_nterm_induct)
case (free Γ name)
hence "fdisjnt (fset_of_list Γ) {|name|}"
by simp
hence "name ∉ set Γ"
including fset.lifting by transfer' (simp add: disjnt_def)
hence "find_first name Γ = None"
by (rule find_first_none)
thus ?case
by (simp add: State_Monad.return_def)
next
case (bound Γ i)
thus ?case
by (simp add: State_Monad.return_def find_first_some_index)
next
case (app Γ t⇩1 t⇩2)
have "fdisjnt (fset_of_list Γ) (frees t⇩1)"
apply (rule fdisjnt_subset_right[where N = "frees t⇩1 |∪| frees t⇩2"])
using app by auto
have "fdisjnt (fset_of_list Γ) (frees t⇩2)"
apply (rule fdisjnt_subset_right[where N = "frees t⇩1 |∪| frees t⇩2"])
using app by auto
have s: "s ≤ snd (run_state (term_to_nterm Γ t⇩1) s)"
apply (rule state_io_relD[OF term_to_nterm_mono])
apply (rule surjective_pairing)
done
show ?case
apply (auto simp: split_beta)
subgoal
apply (rule app)
subgoal using app by simp
subgoal by fact
subgoal by fact
using app by auto
subgoal
apply (rule app)
subgoal using app by simp
subgoal by fact
subgoal by fact
using app s by force+
done
next
case (abs Γ t)
have "next s |∉| frees t |∪| fset_of_list Γ"
using abs(5) next_ge_fall by auto
have "nterm_to_term (next s # Γ) (fst (run_state (term_to_nterm (next s # Γ) t) (next s))) = t"
proof (subst abs)
show "wellformed' (length (next s # Γ)) t"
using abs by auto
show "fdisjnt (fset_of_list (next s # Γ)) (frees t)"
apply simp
apply (rule fdisjnt_insert)
using ‹next s |∉| frees t |∪| fset_of_list Γ› abs by auto
show "distinct (next s # Γ)"
apply simp
apply rule
using ‹next s |∉| frees t |∪| fset_of_list Γ› apply (simp add: fset_of_list_elem)
apply fact
done
have "fBall (frees t |∪| fset_of_list Γ) (λx. x ≤ next s)"
proof (rule fBall_pred_weaken)
show "fBall (frees t |∪| fset_of_list Γ) (λx. x ≤ s)"
using abs(5) by simp
next
show "⋀x. x |∈| frees t |∪| fset_of_list Γ ⟹ x ≤ s ⟹ x ≤ next s"
by (metis Fresh_Class.next_ge dual_order.strict_trans less_eq_name_def)
qed
thus "fBall (frees t |∪| fset_of_list (next s # Γ)) (λx. x ≤ next s)"
by simp
qed auto
thus ?case
by (auto simp: split_beta create_alt_def)
qed (auto simp: State_Monad.return_def)
lemma term_to_nterm_nterm_to_term:
assumes "wellformed t" "frees t |⊆| S"
shows "nterm_to_term' (frun_fresh (term_to_nterm [] t) (S |∪| Q)) = t"
proof (rule term_to_nterm_nterm_to_term0)
show "wellformed' (length []) t"
using assms by simp
next
show "fdisjnt (fset_of_list []) (frees t)"
unfolding fdisjnt_alt_def by simp
next
have "fBall (S |∪| Q) (λx. x < fresh.fNext next default (S |∪| Q))"
by (metis fNext_geq_not_member fresh_fNext_def le_less_linear fBallI)
hence "fBall (S |∪| Q) (λx. x ≤ fresh.fNext next default (S |∪| Q))"
by (meson fBall_pred_weaken less_eq_name_def)
thus "fBall (frees t |∪| fset_of_list []) (λx. x ≤ fresh.fNext next default (S |∪| Q))"
using ‹frees t |⊆| S›
by auto
qed simp
corollary term_to_nterm_nterm_to_term_simple:
assumes "wellformed t"
shows "nterm_to_term' (term_to_nterm' t) = t"
unfolding term_to_nterm'_def using assms
by (metis order_refl sup.idem term_to_nterm_nterm_to_term)
lemma nterm_to_term_eq:
assumes "frees u |⊆| fset_of_list (common_prefix Γ Γ')"
shows "nterm_to_term Γ u = nterm_to_term Γ' u"
using assms
proof (induction u arbitrary: Γ Γ')
case (Nvar name)
hence "name ∈ set (common_prefix Γ Γ')"
unfolding frees_nterm.simps
including fset.lifting
by transfer' simp
thus ?case
by (auto simp: common_prefix_find)
next
case (Nabs x t)
hence *: "frees t - {|x|} |⊆| fset_of_list (common_prefix Γ Γ')"
by simp
show ?case
apply simp
apply (rule Nabs)
using * Nabs by auto
qed auto
corollary nterm_to_term_eq_closed: "closed t ⟹ nterm_to_term Γ t = nterm_to_term Γ' t"
by (rule nterm_to_term_eq) (auto simp: closed_except_def)
lemma nterm_to_term_wellformed: "wellformed' (length Γ) (nterm_to_term Γ t)"
proof (induction t arbitrary: Γ)
case (Nabs x t)
hence "wellformed' (Suc (length Γ)) (nterm_to_term (x # Γ) t)"
by (metis length_Cons)
thus ?case
by auto
qed (auto simp: find_first_correct split: option.splits)
corollary nterm_to_term_closed_wellformed: "closed t ⟹ wellformed (nterm_to_term Γ t)"
by (metis Ex_list_of_length nterm_to_term_eq_closed nterm_to_term_wellformed)
lemma nterm_to_term_term_to_nterm:
assumes "frees t |⊆| fset_of_list Γ" "length Γ = length Γ'"
shows "alpha_equiv (fmap_of_list (zip Γ Γ')) t (fst (run_state (term_to_nterm Γ' (nterm_to_term Γ t)) s))"
using assms proof (induction Γ t arbitrary: s Γ' rule:nterm_to_term.induct)
case (4 Γ x t)
show ?case
apply (simp add: split_beta)
apply (rule alpha_equiv.abs)
using "4.IH"[where Γ' = "next s # Γ'"] "4.prems"
by (fastforce simp: create_alt_def intro: alpha_equiv.intros)
qed
(force split: option.splits intro: find_first_some intro!: alpha_equiv.intros
simp: fset_of_list_elem find_first_in_map split_beta fdisjnt_alt_def)+
corollary nterm_to_term_term_to_nterm': "closed t ⟹ t ≈⇩α term_to_nterm' (nterm_to_term' t)"
unfolding term_to_nterm'_def closed_except_def
apply (rule nterm_to_term_term_to_nterm[where Γ = "[]" and Γ' = "[]", simplified])
by auto
context begin
private lemma term_to_nterm_alpha_equiv0:
"length Γ1 = length Γ2 ⟹ distinct Γ1 ⟹ distinct Γ2 ⟹ wellformed' (length Γ1) t1 ⟹
fresh_fin (frees t1 |∪| fset_of_list Γ1) s1 ⟹ fdisjnt (fset_of_list Γ1) (frees t1) ⟹
fresh_fin (frees t1 |∪| fset_of_list Γ2) s2 ⟹ fdisjnt (fset_of_list Γ2) (frees t1) ⟹
alpha_equiv (fmap_of_list (zip Γ1 Γ2)) (fst( run_state (term_to_nterm Γ1 t1) s1)) (fst ( run_state (term_to_nterm Γ2 t1) s2))"
proof (induction Γ1 t1 arbitrary: Γ2 s1 s2 rule:term_to_nterm_induct)
case (free Γ1 name)
then have "name |∉| fmdom (fmap_of_list (zip Γ1 Γ2))"
unfolding fdisjnt_alt_def
by force
moreover have "name |∉| fmran (fmap_of_list (zip Γ1 Γ2))"
apply rule
apply (subst (asm) fmran_of_list)
apply (subst (asm) fset_of_list_map[symmetric])
apply (subst (asm) distinct_clearjunk_id)
subgoal
apply (subst map_fst_zip)
apply fact
apply fact
done
apply (subst (asm) map_snd_zip)
apply fact
using free unfolding fdisjnt_alt_def
by fastforce
ultimately show ?case
by (force intro:alpha_equiv.intros)
next
case (abs Γ t)
have *: "next s1 > s1" "next s2 > s2"
using next_ge by force+
from abs.prems(5,7) have "next s1 ∉ set Γ" "next s2 ∉ set Γ2"
unfolding fBall_funion
by (metis fset_of_list_elem next_ge_fall)+
moreover have "fresh_fin (frees t |∪| fset_of_list Γ) (next s1)"
"fresh_fin (frees t |∪| fset_of_list Γ2) (next s2)"
using * abs
by (smt dual_order.trans fBall_pred_weaken frees_term.simps(3) less_imp_le)+
moreover have "fdisjnt (finsert (next s1) (fset_of_list Γ)) (frees t)"
"fdisjnt (finsert (next s2) (fset_of_list Γ2)) (frees t)"
unfolding fdisjnt_alt_def using abs frees_term.simps
by (metis fdisjnt_alt_def finter_finsert_right funionCI inf_commute next_ge_fall)+
moreover have "wellformed' (Suc (length Γ2)) t"
using wellformed'.simps abs
by (metis Suc_eq_plus1)
ultimately show ?case
using abs.prems(1,2,3)
by (auto simp: split_beta create_alt_def
intro: alpha_equiv.abs abs.IH[of _ "next s2 # Γ2", simplified])
next
case (app Γ1 t⇩1 t⇩2)
hence "wellformed' (length Γ1) t⇩1" "wellformed' (length Γ1) t⇩2"
and "fresh_fin (frees t⇩1 |∪| fset_of_list Γ1) s1" "fresh_fin (frees t⇩1 |∪| fset_of_list Γ2) s2"
and "fdisjnt (fset_of_list Γ1) (frees t⇩1)" "fdisjnt (fset_of_list Γ2) (frees t⇩1)"
and "fdisjnt (fset_of_list Γ1) (frees t⇩2)" "fdisjnt (fset_of_list Γ2) (frees t⇩2)"
using app
unfolding fdisjnt_alt_def
by (auto simp: inf_sup_distrib1)
have "s1 ≤ snd (run_state (term_to_nterm Γ1 t⇩1) s1)" "s2 ≤ snd (run_state (term_to_nterm Γ2 t⇩1) s2)"
using term_to_nterm_mono
by (simp add: state_io_rel_def)+
hence "fresh_fin (frees t⇩2 |∪| fset_of_list Γ1) (snd (run_state (term_to_nterm Γ1 t⇩1) s1))"
using ‹fresh_fin (frees (t⇩1 $ t⇩2) |∪| fset_of_list Γ1) s1›
by force
have "fresh_fin (frees t⇩2 |∪| fset_of_list Γ2) (snd (run_state (term_to_nterm Γ2 t⇩1) s2))"
apply rule
using app frees_term.simps ‹s2 ≤ _› dual_order.trans
by (metis funion_iff)
show ?case
apply (auto simp: split_beta create_alt_def)
apply (rule alpha_equiv.app)
subgoal
using app.IH
using ‹fBall (frees t⇩1 |∪| fset_of_list Γ1) (λy. y ≤ s1)›
‹fBall (frees t⇩1 |∪| fset_of_list Γ2) (λy. y ≤ s2)›
‹fdisjnt (fset_of_list Γ1) (frees t⇩1)›
‹fdisjnt (fset_of_list Γ2) (frees t⇩1)› ‹wellformed' (length Γ1) t⇩1›
app.prems(1) app.prems(2) app.prems(3) by blast
subgoal
using app.IH
using ‹fBall (frees t⇩2 |∪| fset_of_list Γ1) (λy. y ≤ snd (run_state (term_to_nterm Γ1 t⇩1) s1))›
‹fBall (frees t⇩2 |∪| fset_of_list Γ2) (λy. y ≤ snd (run_state (term_to_nterm Γ2 t⇩1) s2))›
‹fdisjnt (fset_of_list Γ1) (frees t⇩2)›
‹fdisjnt (fset_of_list Γ2) (frees t⇩2)›
‹wellformed' (length Γ1) t⇩2›
app.prems(1) app.prems(2) app.prems(3) by blast
done
qed (force intro: alpha_equiv.intros simp: fmlookup_of_list in_set_zip)+
lemma term_to_nterm_alpha_equiv:
assumes "length Γ1 = length Γ2" "distinct Γ1" "distinct Γ2" "closed t"
assumes "wellformed' (length Γ1) t"
assumes "fresh_fin (fset_of_list Γ1) s1" "fresh_fin (fset_of_list Γ2) s2"
shows "alpha_equiv (fmap_of_list (zip Γ1 Γ2)) (fst (run_state (term_to_nterm Γ1 t) s1)) (fst (run_state (term_to_nterm Γ2 t) s2))"
using assms
by (simp add: fdisjnt_alt_def closed_except_def term_to_nterm_alpha_equiv0)
end
global_interpretation nrelated: term_struct_rel_strong "(λt n. t = nterm_to_term Γ n)" for Γ
proof (standard, goal_cases)
case (5 name t)
then show ?case by (cases t) (auto simp: const_term_def const_nterm_def split: option.splits)
next
case (6 u⇩1 u⇩2 t)
then show ?case by (cases t) (auto simp: app_term_def app_nterm_def split: option.splits)
qed (auto simp: const_term_def const_nterm_def app_term_def app_nterm_def)
lemma env_nrelated_closed:
assumes "nrelated.P_env Γ env nenv" "closed_env nenv"
shows "nrelated.P_env Γ' env nenv"
proof
fix x
from assms have "rel_option (λt n. t = nterm_to_term Γ n) (fmlookup env x) (fmlookup nenv x)"
by auto
thus "rel_option (λt n. t = nterm_to_term Γ' n) (fmlookup env x) (fmlookup nenv x)"
using assms
by (cases rule: option.rel_cases) (auto dest: fmdomI simp: nterm_to_term_eq_closed)
qed
lemma nrelated_subst:
assumes "nrelated.P_env Γ env nenv" "closed_env nenv" "fdisjnt (fset_of_list Γ) (fmdom nenv)"
shows "subst (nterm_to_term Γ t) env = nterm_to_term Γ (subst t nenv)"
using assms
proof (induction t arbitrary: Γ env nenv)
case (Nvar name)
thus ?case
proof (cases rule: fmrel_cases[where x = name])
case (some t⇩1 t⇩2)
with Nvar have "name |∉| fset_of_list Γ"
unfolding fdisjnt_alt_def by (auto dest: fmdomI)
hence "find_first name Γ = None"
including fset.lifting by transfer' (simp add: find_first_none)
with some show ?thesis
by auto
qed (auto split: option.splits)
next
case (Nabs x t)
show ?case
apply simp
apply (subst subst_drop[symmetric, where x = x])
subgoal by simp
apply (rule Nabs)
using Nabs unfolding fdisjnt_alt_def
by (auto intro: env_nrelated_closed)
qed auto
lemma nterm_to_term_insert_dupl:
assumes "y ∈ set (take n Γ)" "n ≤ length Γ"
shows "nterm_to_term Γ t = incr_bounds (- 1) (Suc n) (nterm_to_term (insert_nth n y Γ) t)"
using assms
proof (induction t arbitrary: n Γ)
case (Nvar name)
show ?case
proof (cases "y = name")
case True
with Nvar obtain i where "find_first name Γ = Some i" "i < n"
by (auto elim: find_first_some_strong)
hence "find_first name (take n Γ) = Some i"
by (rule find_first_prefix)
show ?thesis
apply simp
apply (subst ‹find_first name Γ = Some i›)
apply simp
apply (subst find_first_append)
apply (subst ‹find_first name (take n Γ) = Some i›)
apply simp
using ‹i < n› by simp
next
case False
show ?thesis
apply (simp del: insert_nth_take_drop)
apply (subst find_first_insert_nth_neq)
subgoal using False by simp
by (cases "find_first name Γ") auto
qed
next
case (Nabs x t)
show ?case
apply simp
apply (subst Nabs(1)[where n = "Suc n"])
using Nabs by auto
qed auto
lemma nterm_to_term_bounds_dupl:
assumes "i < length Γ" "j < length Γ" "i < j"
assumes "Γ ! i = Γ ! j"
shows "j |∉| bounds (nterm_to_term Γ t)"
using assms
proof (induction t arbitrary: Γ i j)
case (Nvar name)
show ?case
proof (cases "find_first name Γ")
case (Some k)
show ?thesis
proof
assume "j |∈| bounds (nterm_to_term Γ (Nvar name))"
with Some have "find_first name Γ = Some j"
by simp
moreover have "find_first name Γ ≠ Some j"
proof (rule find_first_later)
show "i < length Γ" "j < length Γ" "i < j"
by fact+
next
show "Γ ! j = name"
by (rule find_first_correct) fact
thus "Γ ! i = name"
using Nvar by simp
qed
ultimately show False
by blast
qed
qed simp
next
case (Nabs x t)
show ?case
proof
assume "j |∈| bounds (nterm_to_term Γ (Λ⇩n x. t))"
then obtain j' where "j' |∈| bounds (nterm_to_term (x # Γ) t)" "j' > 0" "j = j' - 1"
by auto
hence "Suc j |∈| bounds (nterm_to_term (x # Γ) t)"
by simp
moreover have "Suc j |∉| bounds (nterm_to_term (x # Γ) t)"
proof (rule Nabs)
show "Suc i < length (x # Γ)" "Suc j < length (x # Γ)" "Suc i < Suc j" "(x # Γ) ! Suc i = (x # Γ) ! Suc j"
using Nabs by simp+
qed
ultimately show False
by blast
qed
qed auto
fun subst_single :: "nterm ⇒ name ⇒ nterm ⇒ nterm" where
"subst_single (Nvar s) s' t' = (if s = s' then t' else Nvar s)" |
"subst_single (t⇩1 $⇩n t⇩2) s' t' = subst_single t⇩1 s' t' $⇩n subst_single t⇩2 s' t'" |
"subst_single (Λ⇩n x. t) s' t' = (Λ⇩n x. (if x = s' then t else subst_single t s' t'))" |
"subst_single t _ _ = t"
lemma subst_single_eq: "subst_single t s t' = subst t (fmap_of_list [(s, t')])"
proof (induction t)
case (Nabs x t)
then show ?case
by (cases "x = s") (simp add: fmfilter_alt_defs)+
qed auto
lemma nterm_to_term_subst_replace_bound:
assumes "closed u'" "n ≤ length Γ" "x ∉ set (take n Γ)"
shows "nterm_to_term Γ (subst_single u x u') = replace_bound n (nterm_to_term (insert_nth n x Γ) u) (nterm_to_term Γ u')"
using assms
proof (induction u arbitrary: n Γ)
case (Nvar name)
note insert_nth_take_drop[simp del]
show ?case
proof (cases "name = x")
case True
thus ?thesis
using Nvar
apply (simp add: find_first_insert_nth_eq)
apply (subst incr_bounds_eq[where k = 0])
subgoal by simp
apply (rule nterm_to_term_closed_wellformed)
by auto
next
case False
thus ?thesis
apply auto
apply (subst find_first_insert_nth_neq)
subgoal by simp
by (cases "find_first name Γ") auto
qed
next
case (Nabs y t)
note insert_nth_take_drop[simp del]
show ?case
proof (cases "x = y")
case True
have "nterm_to_term (y # Γ) t = replace_bound (Suc n) (nterm_to_term (y # insert_nth n y Γ) t) (nterm_to_term Γ u')"
proof (subst replace_bound_eq)
show "Suc n |∉| bounds (nterm_to_term (y # insert_nth n y Γ) t)"
apply (rule nterm_to_term_bounds_dupl[where i = 0])
subgoal by simp
subgoal using Nabs(3) by (simp add: insert_nth_take_drop)
subgoal by simp
apply simp
apply (subst nth_insert_nth_index_eq)
using Nabs by auto
show "nterm_to_term (y # Γ) t = incr_bounds (- 1) (Suc n + 1) (nterm_to_term (y # insert_nth n y Γ) t)"
apply (subst nterm_to_term_insert_dupl[where Γ = "y # Γ" and y = y and n = "Suc n"])
using Nabs by auto
qed
with True show ?thesis
by auto
next
case False
have "nterm_to_term (y # Γ) (subst_single t x u') = replace_bound (Suc n) (nterm_to_term (y # insert_nth n x Γ) t) (nterm_to_term Γ u')"
apply (subst Nabs(1)[of "Suc n"])
subgoal by fact
subgoal using Nabs by simp
subgoal using False Nabs by simp
apply (subst nterm_to_term_eq_closed[where t = u'])
using Nabs by auto
with False show ?thesis
by auto
qed
qed auto
corollary nterm_to_term_subst_β:
assumes "closed u'"
shows "nterm_to_term Γ (subst u (fmap_of_list [(x, u')])) = nterm_to_term (x # Γ) u [nterm_to_term Γ u']⇩β"
using assms
by (rule nterm_to_term_subst_replace_bound[where n = 0, simplified, unfolded subst_single_eq])
end