theory LamFun+ −
imports "../Nominal2" Quotient_Option+ −
begin+ −
+ −
atom_decl name+ −
declare [[STEPS = 100]]+ −
+ −
nominal_datatype lam =+ −
Var "name"+ −
| App "lam" "lam"+ −
| Lam x::"name" l::"lam" bind x in l+ −
+ −
thm lam.distinct+ −
thm lam.induct+ −
thm lam.exhaust+ −
thm lam.fv_defs+ −
thm lam.bn_defs+ −
thm lam.perm_simps+ −
thm lam.eq_iff+ −
thm lam.fv_bn_eqvt+ −
thm lam.size_eqvt+ −
thm lam.size+ −
thm lam_raw.size+ −
thm lam.fresh+ −
+ −
primrec match_Var_raw where+ −
"match_Var_raw (Var_raw x) = Some x"+ −
| "match_Var_raw (App_raw x y) = None"+ −
| "match_Var_raw (Lam_raw n t) = None"+ −
+ −
quotient_definition+ −
"match_Var :: lam \<Rightarrow> name option"+ −
is match_Var_raw+ −
+ −
lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw"+ −
by (rule, induct_tac a b rule: alpha_lam_raw.induct, simp_all)+ −
+ −
lemmas match_Var_simps = match_Var_raw.simps[quot_lifted]+ −
+ −
primrec match_App_raw where+ −
"match_App_raw (Var_raw x) = None"+ −
| "match_App_raw (App_raw x y) = Some (x, y)"+ −
| "match_App_raw (Lam_raw n t) = None"+ −
+ −
quotient_definition+ −
"match_App :: lam \<Rightarrow> (lam \<times> lam) option"+ −
is match_App_raw+ −
+ −
lemma [quot_respect]:+ −
"(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw"+ −
by (intro fun_relI, induct_tac a b rule: alpha_lam_raw.induct, simp_all)+ −
+ −
lemmas match_App_simps = match_App_raw.simps[quot_lifted]+ −
+ −
definition next_name where+ −
"next_name (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)"+ −
+ −
lemma lam_eq: "Lam a t = Lam b s \<longleftrightarrow> (a \<leftrightarrow> b) \<bullet> t = s"+ −
apply (simp add: lam.eq_iff Abs_eq_iff alphas)+ −
sorry+ −
+ −
lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)"+ −
by (auto simp add: lam_eq)+ −
+ −
definition+ −
"match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then+ −
(let z = next_name (S, t) in Some (z, THE s. t = Lam z s)) else None)"+ −
+ −
lemma match_Lam_simps:+ −
"match_Lam S (Var n) = None"+ −
"match_Lam S (App l r) = None"+ −
"match_Lam S (Lam z s) = (let n = next_name (S, (Lam z s)) in Some (n, (z \<leftrightarrow> n) \<bullet> s))"+ −
apply (simp_all add: match_Lam_def lam.distinct)+ −
apply (auto simp add: lam_eq)+ −
done+ −
+ −
lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"+ −
by (induct x rule: lam.induct) (simp_all add: match_App_simps)+ −
+ −
+ −
lemma lam_some: "match_Lam S x = Some (n, t) \<Longrightarrow> x = Lam n t"+ −
apply (induct x rule: lam.induct)+ −
apply (simp add: match_Lam_simps)+ −
apply (simp add: match_Lam_simps)+ −
apply (simp add: match_Lam_simps Let_def lam_eq)+ −
apply clarify+ −
done+ −
+ −
function subst where+ −
"subst v s t = (+ −
case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow>+ −
case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow>+ −
case match_Lam (v, s) t of Some (n, s') \<Rightarrow> Lam n (subst v s s') | None \<Rightarrow> undefined)"+ −
print_theorems+ −
thm subst_rel.intros[no_vars]+ −
by pat_completeness auto+ −
+ −
termination apply (relation "measure (\<lambda>(_, _, t). size t)")+ −
apply auto[1]+ −
apply (case_tac a) apply simp+ −
apply (frule lam_some) apply (simp add: lam.size)+ −
apply (case_tac a) apply simp+ −
apply (frule app_some) apply (simp add: lam.size)+ −
apply (case_tac a) apply simp+ −
apply (frule app_some) apply (simp add: lam.size)+ −
done+ −
+ −
lemma subst_eqs:+ −
"subst y s (Var x) = (if x = y then s else (Var x))"+ −
"subst y s (App l r) = App (subst y s l) (subst y s r)"+ −
"subst y s (Lam x t) =+ −
(let n = next_name ((y, s), Lam x t) in Lam n (subst y s ((x \<leftrightarrow> n) \<bullet> t)))"+ −
apply (subst subst.simps)+ −
apply (simp only: match_Var_simps option.simps)+ −
apply (subst subst.simps)+ −
apply (simp only: match_App_simps option.simps prod.simps match_Var_simps)+ −
apply (subst subst.simps)+ −
apply (simp only: match_App_simps option.simps prod.simps match_Var_simps match_Lam_simps Let_def)+ −
done+ −
+ −
lemma subst_eqvt:+ −
"p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)"+ −
proof (induct v s t rule: subst.induct)+ −
case (1 v s t)+ −
show ?case proof (cases t rule: lam.exhaust)+ −
fix n+ −
assume "t = Var n"+ −
then show ?thesis by (simp add: match_Var_simps)+ −
next+ −
fix l r+ −
assume "t = App l r"+ −
then show ?thesis+ −
apply (simp only: subst_eqs lam.perm_simps)+ −
apply (subst 1(2)[of "(l, r)" "l" "r"])+ −
apply (simp add: match_Var_simps)+ −
apply (simp add: match_App_simps)+ −
apply (rule refl)+ −
apply (subst 1(3)[of "(l, r)" "l" "r"])+ −
apply (simp add: match_Var_simps)+ −
apply (simp add: match_App_simps)+ −
apply (rule refl)+ −
apply (rule refl)+ −
done+ −
next+ −
fix n t'+ −
assume "t = Lam n t'"+ −
then show ?thesis+ −
apply (simp only: subst_eqs lam.perm_simps Let_def)+ −
apply (subst 1(1))+ −
apply (simp add: match_Var_simps)+ −
apply (simp add: match_App_simps)+ −
apply (simp add: match_Lam_simps Let_def)+ −
apply (rule refl)+ −
(* next_name is not equivariant :( *)+ −
apply (simp only: lam_eq)+ −
sorry+ −
qed+ −
qed+ −
+ −
lemma subst_eqvt':+ −
"p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)"+ −
apply (induct t arbitrary: v s rule: lam.induct)+ −
apply (simp only: subst_eqs lam.perm_simps eqvts)+ −
apply (simp only: subst_eqs lam.perm_simps)+ −
apply (simp only: subst_eqs lam.perm_simps Let_def)+ −
apply (simp only: lam_eq)+ −
sorry+ −
+ −
lemma subst_eq3:+ −
"atom x \<sharp> (y, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)"+ −
apply (simp only: subst_eqs Let_def)+ −
apply (simp only: lam_eq)+ −
(* p # y p # s subst_eqvt *)+ −
(* p \<bullet> -p \<bullet> (subst y s t) = subst y s t *)+ −
sorry+ −
+ −
end+ −
+ −
+ −
+ −