theory De_Bruijn
imports Syntax "List-Index.List_Index"
begin
datatype db =
dbUnit |
dbVar nat |
dbLam db |
dbRec db |
dbInj1 db |
dbInj2 db |
dbPair db db |
dbRoll db |
dbLet db db |
dbApp db db |
dbCase db db db |
dbPrj1 db |
dbPrj2 db |
dbUnroll db |
dbAuth db |
dbUnauth db |
dbHash hash |
dbHashed hash db
consts hash_db :: "db ⇒ hash"
instantiation db :: pure begin
definition permute_db :: "perm ⇒ db ⇒ db" where
"permute_db π x = x"
instance
proof (standard)
qed (simp_all add: permute_db_def)
end
lemma fresh_imp_notin_env: "atom x ♯ e ⟹ x ∉ set e"
by (metis List.finite_set fresh_finite_set_at_base fresh_set)
lemma index_eqvt[eqvt]: "π ∙ index xs x = index (π ∙ xs) (π ∙ x)"
by (induct xs) (auto simp: permute_pure)
nominal_function db_of' :: "var list ⇒ term ⇒ db" where
"db_of' vs Unit = dbUnit" |
"db_of' vs (Var x) = dbVar (index vs x)" |
"atom x ♯ vs ⟹ db_of' vs (Lam x t) = dbLam (db_of' (x # vs) t)" |
"atom x ♯ vs ⟹ db_of' vs (Rec x t) = dbRec (db_of' (x # vs) t)" |
"db_of' vs (Inj1 t) = dbInj1 (db_of' vs t)" |
"db_of' vs (Inj2 t) = dbInj2 (db_of' vs t)" |
"db_of' vs (Pair t u) = dbPair (db_of' vs t) (db_of' vs u)" |
"db_of' vs (Roll t) = dbRoll (db_of' vs t)" |
"atom x ♯ vs ⟹ db_of' vs (Let t x u) = dbLet (db_of' vs t) (db_of' (x # vs) u)" |
"db_of' vs (Case c t u) = dbCase (db_of' vs c) (db_of' vs t) (db_of' vs u)" |
"db_of' vs (App t u) = dbApp (db_of' vs t) (db_of' vs u)" |
"db_of' vs (Prj1 t) = dbPrj1 (db_of' vs t)" |
"db_of' vs (Prj2 t) = dbPrj2 (db_of' vs t)" |
"db_of' vs (Unroll t) = dbUnroll (db_of' vs t)" |
"db_of' vs (Auth t) = dbAuth (db_of' vs t)" |
"db_of' vs (Unauth t) = dbUnauth (db_of' vs t)" |
"db_of' vs (Hashed h t) = dbHashed h (db_of' vs t)" |
"db_of' vs (Hash h) = dbHash h"
using [[simproc del: alpha_lst]]
subgoal by (simp add: eqvt_def db_of'_graph_aux_def map_prod_def)
subgoal by (erule db_of'_graph.induct) (auto simp: fresh_star_def fresh_at_base map_prod_def split: prod.splits)
apply clarify
subgoal for P a b
by (rule term.strong_exhaust[of b P a]) (auto simp: fresh_star_def)
apply (simp_all add: fresh_at_base)
subgoal
apply (erule conjE)+
apply (erule Abs_lst1_fcb2')
apply (simp_all add: eqvt_at_def map_prod_def split: prod.splits)
apply (simp_all add: perm_supp_eq)
done
subgoal
apply (erule conjE)+
apply (erule Abs_lst1_fcb2')
apply (simp_all add: eqvt_at_def map_prod_def split: prod.splits)
apply (simp_all add: perm_supp_eq)
done
subgoal for x vs t u x' vs' t' u'
apply (erule conjE)+
apply (erule Abs_lst1_fcb2')
apply (simp_all add: eqvt_at_def map_prod_def split: prod.splits)
apply (simp_all add: perm_supp_eq)
done
done
nominal_termination (eqvt)
by lexicographic_order
definition db_of where
"db_of = db_of' []"
definition hash :: "term ⇒ hash" where
"hash = hash_db o db_of"
lemma hash_eqvt[eqvt]: "π ∙ hash x = hash (π ∙ x)"
unfolding hash_def db_of_def o_apply by auto
definition pick_fresh :: "var list ⇒ var" where
"pick_fresh xs = (SOME x :: var. atom x ♯ xs)"
lemma pick_fresh[simp]: "atom (pick_fresh xs) ♯ xs"
unfolding pick_fresh_def by (rule someI_ex, rule obtain_fresh, rule exI)
primrec term_of' :: "var list ⇒ db ⇒ term" where
"term_of' vs dbUnit = Unit" |
"term_of' vs (dbVar x) = Var (nth vs x)" |
"term_of' vs (dbLam t) = (let x = pick_fresh vs in Lam x (term_of' (x # vs) t))" |
"term_of' vs (dbRec t) = (let x = pick_fresh vs in Rec x (term_of' (x # vs) t))" |
"term_of' vs (dbInj1 t) = Inj1 (term_of' vs t)" |
"term_of' vs (dbInj2 t) = Inj2 (term_of' vs t)" |
"term_of' vs (dbPair t u) = Pair (term_of' vs t) (term_of' vs u)" |
"term_of' vs (dbRoll t) = Roll (term_of' vs t)" |
"term_of' vs (dbLet t u) = (let x = pick_fresh vs in Let (term_of' vs t) x (term_of' (x # vs) u))" |
"term_of' vs (dbCase c t u) = Case (term_of' vs c) (term_of' vs t) (term_of' vs u)" |
"term_of' vs (dbApp t u) = App (term_of' vs t) (term_of' vs u)" |
"term_of' vs (dbPrj1 t) = Prj1 (term_of' vs t)" |
"term_of' vs (dbPrj2 t) = Prj2 (term_of' vs t)" |
"term_of' vs (dbUnroll t) = Unroll (term_of' vs t)" |
"term_of' vs (dbAuth t) = Auth (term_of' vs t)" |
"term_of' vs (dbUnauth t) = Unauth (term_of' vs t)" |
"term_of' vs (dbHashed h t) = Hashed h (term_of' vs t)" |
"term_of' vs (dbHash h) = Hash h"
primrec ok_db :: "nat ⇒ db ⇒ bool" where
"ok_db n dbUnit = True" |
"ok_db n (dbVar x) = (x < n)" |
"ok_db n (dbLam t) = ok_db (n + 1) t" |
"ok_db n (dbRec t) = ok_db (n + 1) t" |
"ok_db n (dbInj1 t) = ok_db n t" |
"ok_db n (dbInj2 t) = ok_db n t" |
"ok_db n (dbPair t u) = (ok_db n t ∧ ok_db n u)" |
"ok_db n (dbRoll t) = ok_db n t" |
"ok_db n (dbLet t u) = (ok_db n t ∧ ok_db (n + 1) u)" |
"ok_db n (dbCase c t u) = (ok_db n c ∧ ok_db n t ∧ ok_db n u)" |
"ok_db n (dbApp t u) = (ok_db n t ∧ ok_db n u)" |
"ok_db n (dbPrj1 t) = ok_db n t" |
"ok_db n (dbPrj2 t) = ok_db n t" |
"ok_db n (dbUnroll t) = ok_db n t" |
"ok_db n (dbAuth t) = ok_db n t" |
"ok_db n (dbUnauth t) = ok_db n t" |
"ok_db n (dbHashed h t) = ok_db n t" |
"ok_db n (dbHash h) = True"
lemma permute_list_alt: "π ∙ xs = map (λx. π ∙ x) xs"
by (induct xs) auto
lemma fresh_term_of': "ok_db (length vs) t ⟹ atom x ♯ vs ⟹ atom x ♯ term_of' vs t"
by (induct t arbitrary: vs)
(auto simp: fresh_set_fresh_forall HOL.Let_def)
lemma permute_term_of': "ok_db (length vs) t ⟹ π ∙ term_of' vs t = term_of' (π ∙ vs) t"
proof (induct t arbitrary: vs π)
case (dbLam t)
show ?case
proof (cases "π ∙ pick_fresh vs = pick_fresh (π ∙ vs)")
case True
with dbLam show ?thesis by (auto simp: HOL.Let_def)
next
case False
show ?thesis
unfolding term_of'.simps HOL.Let_def term.eq_iff term.perm_simps
apply (rule trans[OF Abs_lst_eq_flipI, of "pick_fresh (π ∙ vs)"])
using dbLam(2) False
apply
(auto intro!: fresh_term_of' simp: fresh_at_base fresh_Cons perm_supp_eq flip_fresh_fresh dbLam(1))
apply (metis length_eqvt permute_pure)
apply (subst dbLam(1))
apply (auto simp: flip_fresh_fresh)
apply (metis length_eqvt permute_pure)
done
qed
next
case (dbRec t)
show ?case
proof (cases "π ∙ pick_fresh vs = pick_fresh (π ∙ vs)")
case True
with dbRec show ?thesis by (auto simp: HOL.Let_def)
next
case False
show ?thesis
unfolding term_of'.simps HOL.Let_def term.eq_iff term.perm_simps
apply (rule trans[OF Abs_lst_eq_flipI, of "pick_fresh (π ∙ vs)"])
using dbRec(2) False
apply
(auto intro!: fresh_term_of' simp: fresh_at_base fresh_Cons perm_supp_eq flip_fresh_fresh dbRec(1))
apply (metis length_eqvt permute_pure)
apply (subst dbRec(1))
apply (auto simp: flip_fresh_fresh)
apply (metis length_eqvt permute_pure)
done
qed
next
case (dbLet t1 t2)
show ?case
proof (cases "π ∙ pick_fresh vs = pick_fresh (π ∙ vs)")
case True
with dbLet show ?thesis by (auto simp: HOL.Let_def)
next
case False
show ?thesis
unfolding term_of'.simps HOL.Let_def term.eq_iff term.perm_simps
apply (rule conjI, rule trans[OF Abs_lst_eq_flipI, of "pick_fresh (π ∙ vs)"])
using dbLet(3) False
apply
(auto intro!: fresh_term_of' simp: fresh_at_base fresh_Cons perm_supp_eq flip_fresh_fresh dbLet(1,2))
apply (metis length_eqvt permute_pure)
apply (subst dbLet(2))
apply (auto simp: flip_fresh_fresh)
apply (metis length_eqvt permute_pure)
done
qed
qed (auto simp: permute_list_alt permute_pure)
lemma ok_db_db_of': "(⋀x. x ∉ set vs ⟹ atom x ♯ t) ⟹ n = length vs ⟹ ok_db n (db_of' vs t)"
by (hypsubst_thin, nominal_induct t avoiding: vs rule: term.strong_induct)
(auto simp: index_less_size_conv fresh_at_base, (metis length_Cons list.set_intros)+)
lemma term_of'_db_of': "(⋀x. x ∉ set vs ⟹ atom x ♯ t) ⟹ term_of' vs (db_of' vs t) = t"
proof (nominal_induct t avoiding: vs rule: term.strong_induct)
case (Lam x t)
show ?case
proof (cases "x = pick_fresh vs")
case True
with Lam(3) show ?thesis
unfolding db_of'.simps(3)[OF Lam(1)] term_of'.simps HOL.Let_def term.eq_iff
by (force intro!: Lam(2))
next
case False
show ?thesis
unfolding db_of'.simps(3)[OF Lam(1)] term_of'.simps HOL.Let_def term.eq_iff
by (rule trans[OF Abs_lst_eq_flipI, of x])
(auto intro!: fresh_term_of' ok_db_db_of' trans[OF permute_term_of'] Lam(2)
dest!: Lam(3) simp: False fresh_at_base fresh_Cons Lam(1) perm_supp_eq)
qed
next
case (Rec x t)
then show ?case
proof (cases "x = pick_fresh vs")
case True
with Rec(3) show ?thesis
unfolding db_of'.simps(4)[OF Rec(1)] term_of'.simps HOL.Let_def term.eq_iff
by (force intro!: Rec(2))
next
case False
show ?thesis
unfolding db_of'.simps(4)[OF Rec(1)] term_of'.simps HOL.Let_def term.eq_iff
by (rule trans[OF Abs_lst_eq_flipI, of x])
(auto intro!: fresh_term_of' ok_db_db_of' trans[OF permute_term_of'] Rec(2)
dest!: Rec(3) simp: False fresh_at_base fresh_Cons Rec(1) perm_supp_eq)
qed
next
case (Let t' x t)
then show ?case
proof (cases "x = pick_fresh vs")
case True
with Let(4) show ?thesis
unfolding db_of'.simps(9)[OF Let(1)] term_of'.simps HOL.Let_def term.eq_iff
by (force intro!: Let(2,3))
next
case False
show ?thesis
unfolding db_of'.simps(9)[OF Let(1)] term_of'.simps HOL.Let_def term.eq_iff
by (rule conjI, rule trans[OF Abs_lst_eq_flipI, of x])
(auto intro!: fresh_term_of' ok_db_db_of' trans[OF permute_term_of'] Let(2,3)
dest!: Let(4) simp: False fresh_at_base fresh_Cons Let(1) perm_supp_eq)
qed
qed (auto simp: fresh_at_base intro!: nth_index)
lemma db_of'_inj:
assumes "⋀x. x ∉ set vs ⟹ atom x ♯ (t, u)"
shows "db_of' vs t = db_of' vs u ⟹ t = u"
using term_of'_db_of'[of vs] assms unfolding fresh_Pair
by metis
lemma db_of'_inj_closed:
"closed t ⟹ closed u ⟹ db_of' [] t = db_of' [] u ⟹ t = u"
by (rule db_of'_inj; auto)
lemma db_of_inj_closed:
"closed t ⟹ closed u ⟹ db_of t = db_of u ⟹ t = u"
by (simp add: db_of_def db_of'_inj_closed)
end