Quelle Pattern.thy Sprache: Isabelle

section \<open>Simply-typed lambda-calculus with let and tuple patterns\<close>

theory Pattern
imports "HOL-Nominal.Nominal"
begin

atom_decl name

nominal_datatype ty =
    Atom nat
  | Arrow ty ty  (infixr \<open>\<rightarrow>\<close> 200)
  | TupleT ty ty  (infixr \<open>\<otimes>\<close> 210)

lemma fresh_type [simp]: "(a::name) \ (T::ty)"
  by (induct T rule: ty.induct) (simp_all add: fresh_nat)

lemma supp_type [simp]: "supp (T::ty) = ({} :: name set)"
  by (induct T rule: ty.induct) (simp_all add: ty.supp supp_nat)

lemma perm_type: "(pi::name prm) \ (T::ty) = T"
  by (induct T rule: ty.induct) (simp_all add: perm_nat_def)

nominal_datatype trm =
    Var name
  | Tuple trm trm  (\<open>(1'\<langle>_,/ _'\<rangle>)\<close>)
  | Abs ty "\name\trm"
  | App trm trm  (infixl \<open>\<cdot>\<close> 200)
  | Let ty trm btrm
and btrm =
    Base trm
  | Bind ty "\name\btrm"

abbreviation
  Abs_syn :: "name \ ty \ trm \ trm" (\(3\_:_./ _)\ [0, 0, 10] 10)
where
  "\x:T. t \ Abs T x t"

datatype pat =
    PVar name ty
  | PTuple pat pat  (\<open>(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)\<close>)

(* FIXME: The following should be done automatically by the nominal package *)
overloading pat_perm \<equiv> "perm :: name prm \<Rightarrow> pat \<Rightarrow> pat" (unchecked)
begin

primrec pat_perm
where
  "pat_perm pi (PVar x ty) = PVar (pi \ x) (pi \ ty)"
| "pat_perm pi \\p, q\\ = \\pat_perm pi p, pat_perm pi q\\"

end

declare pat_perm.simps [eqvt]

lemma supp_PVar [simp]: "((supp (PVar x T))::name set) = supp x"
  by (simp add: supp_def perm_fresh_fresh)

lemma supp_PTuple [simp]: "((supp \\p, q\\)::name set) = supp p \ supp q"
  by (simp add: supp_def Collect_disj_eq del: disj_not1)

instance pat :: pt_name
proof
  fix x :: pat
  show "([]::(name \ _) list) \ x = x"
    by (induct x) simp_all
  fix pi1 pi2 :: "(name \ name) list"
  show "(pi1 @ pi2) \ x = pi1 \ pi2 \ x"
    by (induct x) (simp_all add: pt_name2)
  assume "pi1 \ pi2"
  then show "pi1 \ x = pi2 \ x"
    by (induct x) (simp_all add: pt_name3)
qed

instance pat :: fs_name
proof
  fix x :: pat
  show "finite (supp x::name set)"
    by (induct x) (simp_all add: fin_supp)
qed

(* the following function cannot be defined using nominal_primrec, *)
(* since variable parameters are currently not allowed.            *)
primrec abs_pat :: "pat \ btrm \ btrm" (\(3\[_]./ _)\ [0, 10] 10)
where
  "(\[PVar x T]. t) = Bind T x t"
| "(\[\\p, q\\]. t) = (\[p]. \[q]. t)"

lemma abs_pat_eqvt [eqvt]:
  "(pi :: name prm) \ (\[p]. t) = (\[pi \ p]. (pi \ t))"
  by (induct p arbitrary: t) simp_all

lemma abs_pat_fresh [simp]:
  "(x::name) \ (\[p]. t) = (x \ supp p \ x \ t)"
  by (induct p arbitrary: t) (simp_all add: abs_fresh supp_atm)

lemma abs_pat_alpha:
  assumes fresh: "((pi::name prm) \ supp p::name set) \* t"
  and pi: "set pi \ supp p \ pi \ supp p"
  shows "(\[p]. t) = (\[pi \ p]. pi \ t)"
proof -
  note pt_name_inst at_name_inst pi
  moreover have "(supp p::name set) \* (\[p]. t)"
    by (simp add: fresh_star_def)
  moreover from fresh
  have "(pi \ supp p::name set) \* (\[p]. t)"
    by (simp add: fresh_star_def)
  ultimately have "pi \ (\[p]. t) = (\[p]. t)"
    by (rule pt_freshs_freshs)
  then show ?thesis by (simp add: eqvts)
qed

primrec pat_vars :: "pat \ name list"
where
  "pat_vars (PVar x T) = [x]"
| "pat_vars \\p, q\\ = pat_vars q @ pat_vars p"

lemma pat_vars_eqvt [eqvt]:
  "(pi :: name prm) \ (pat_vars p) = pat_vars (pi \ p)"
  by (induct p rule: pat.induct) (simp_all add: eqvts)

lemma set_pat_vars_supp: "set (pat_vars p) = supp p"
  by (induct p) (auto simp add: supp_atm)

lemma distinct_eqvt [eqvt]:
  "(pi :: name prm) \ (distinct (xs::name list)) = distinct (pi \ xs)"
  by (induct xs) (simp_all add: eqvts)

primrec pat_type :: "pat \ ty"
where
  "pat_type (PVar x T) = T"
| "pat_type \\p, q\\ = pat_type p \ pat_type q"

lemma pat_type_eqvt [eqvt]:
  "(pi :: name prm) \ (pat_type p) = pat_type (pi \ p)"
  by (induct p) simp_all

lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \ p) = pat_type p"
  by (induct p) (simp_all add: perm_type)

type_synonym ctx = "(name \ ty) list"

inductive
  ptyping :: "pat \ ty \ ctx \ bool" (\\ _ : _ \ _\ [60, 60, 60] 60)
where
  PVar: "\ PVar x T : T \ [(x, T)]"
| PTuple: "\ p : T \ \\<^sub>1 \ \ q : U \ \\<^sub>2 \ \ \\p, q\\ : T \ U \ \\<^sub>2 @ \\<^sub>1"

lemma pat_vars_ptyping:
  assumes "\ p : T \ \"
  shows "pat_vars p = map fst \" using assms
  by induct simp_all

inductive
  valid :: "ctx \ bool"
where
  Nil [intro!]: "valid []"
| Cons [intro!]: "valid \ \ x \ \ \ valid ((x, T) # \)"

inductive_cases validE[elim!]: "valid ((x, T) # \)"

lemma fresh_ctxt_set_eq: "((x::name) \ (\::ctx)) = (x \ fst ` set \)"
  by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm)

lemma valid_distinct: "valid \ = distinct (map fst \)"
  by (induct \<Gamma>) (auto simp add: fresh_ctxt_set_eq [symmetric])

abbreviation
  "sub_ctx" :: "ctx \ ctx \ bool" (\_ \ _\)
where
  "\\<^sub>1 \ \\<^sub>2 \ \x. x \ set \\<^sub>1 \ x \ set \\<^sub>2"

abbreviation
  Let_syn :: "pat \ trm \ trm \ trm" (\(LET (_ =/ _)/ IN (_))\ 10)
where
  "LET p = t IN u \ Let (pat_type p) t (\[p]. Base u)"

inductive typing :: "ctx \ trm \ ty \ bool" (\_ \ _ : _\ [60, 60, 60] 60)
where
  Var [intro]: "valid \ \ (x, T) \ set \ \ \ \ Var x : T"
| Tuple [intro]: "\ \ t : T \ \ \ u : U \ \ \ \t, u\ : T \ U"
| Abs [intro]: "(x, T) # \ \ t : U \ \ \ (\x:T. t) : T \ U"
| App [intro]: "\ \ t : T \ U \ \ \ u : T \ \ \ t \ u : U"
| Let: "((supp p)::name set) \* t \
    \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow>
    \<Gamma> \<turnstile> (LET p = t IN u) : U"

equivariance ptyping

equivariance valid

equivariance typing

lemma valid_typing:
  assumes "\ \ t : T"
  shows "valid \" using assms
  by induct auto

lemma pat_var:
  assumes "\ p : T \ \"
  shows "(supp p::name set) = supp \" using assms
  by induct (auto simp add: supp_list_nil supp_list_cons supp_prod supp_list_append)

lemma valid_app_fresh:
  assumes "valid (\ @ \)" and "(x::name) \ supp \"
  shows "x \ \" using assms
  by (induct \<Delta>)
    (auto simp add: supp_list_nil supp_list_cons supp_prod supp_atm fresh_list_append)

lemma pat_freshs:
  assumes "\ p : T \ \"
  shows "(supp p::name set) \* c = (supp \::name set) \* c" using assms
  by (auto simp add: fresh_star_def pat_var)

lemma valid_app_mono:
  assumes "valid (\ @ \\<^sub>1)" and "(supp \::name set) \* \\<^sub>2" and "valid \\<^sub>2" and "\\<^sub>1 \ \\<^sub>2"
  shows "valid (\ @ \\<^sub>2)" using assms
  by (induct \<Delta>)
    (auto simp add: supp_list_cons fresh_star_Un_elim supp_prod
       fresh_list_append supp_atm fresh_star_insert_elim fresh_star_empty_elim)

nominal_inductive2 typing
avoids
  Abs: "{x}"
| Let: "(supp p)::name set"
  by (auto simp add: fresh_star_def abs_fresh fin_supp pat_var
    dest!: valid_typing valid_app_fresh)

lemma better_T_Let [intro]:
  assumes t: "\ \ t : T" and p: "\ p : T \ \" and u: "\ @ \ \ u : U"
  shows "\ \ (LET p = t IN u) : U"
proof -
  obtain pi::"name prm" where pi: "(pi \ (supp p::name set)) \* (t, Base u, \)"
    and pi': "set pi \ supp p \ (pi \ supp p)"
    by (rule at_set_avoiding [OF at_name_inst fin_supp fin_supp])
  from p u have p_fresh: "(supp p::name set) \* \"
    by (auto simp add: fresh_star_def pat_var dest!: valid_typing valid_app_fresh)
  from pi have p_fresh': "(pi \ (supp p::name set)) \* \"
    by (simp add: fresh_star_prod_elim)
  from pi have p_fresh'': "(pi \ (supp p::name set)) \* Base u"
    by (simp add: fresh_star_prod_elim)
  from pi have "(supp (pi \ p)::name set) \* t"
    by (simp add: fresh_star_prod_elim eqvts)
  moreover note t
  moreover from p have "pi \ (\ p : T \ \)" by (rule perm_boolI)
  then have "\ (pi \ p) : T \ (pi \ \)" by (simp add: eqvts perm_type)
  moreover from u have "pi \ (\ @ \ \ u : U)" by (rule perm_boolI)
  with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' p_fresh p_fresh']
  have "(pi \ \) @ \ \ (pi \ u) : U" by (simp add: eqvts perm_type)
  ultimately have "\ \ (LET (pi \ p) = t IN (pi \ u)) : U"
    by (rule Let)
  then show ?thesis by (simp add: abs_pat_alpha [OF p_fresh'' pi'] pat_type_perm_eq)
qed

lemma weakening:
  assumes "\\<^sub>1 \ t : T" and "valid \\<^sub>2" and "\\<^sub>1 \ \\<^sub>2"
  shows "\\<^sub>2 \ t : T" using assms
proof (nominal_induct \<Gamma>\<^sub>1 t T avoiding: \<Gamma>\<^sub>2 rule: typing.strong_induct)
  case (Abs x T \<Gamma> t U)
  then show ?case
    by (simp add: typing.Abs valid.Cons)
next
  case (Let p t \<Gamma> T \<Delta> u U)
  then show ?case
    by (smt (verit, ccfv_threshold) Un_iff pat_freshs set_append typing.simps valid_app_mono valid_typing)
qed auto

inductive
  match :: "pat \ trm \ (name \ trm) list \ bool" (\\ _ \ _ \ _\ [50, 50, 50] 50)
where
  PVar: "\ PVar x T \ t \ [(x, t)]"
| PProd: "\ p \ t \ \ \ \ q \ u \ \' \ \ \\p, q\\ \ \t, u\ \ \ @ \'"

fun
  lookup :: "(name \ trm) list \ name \ trm"
where
  "lookup [] x = Var x"
| "lookup ((y, e) # \) x = (if x = y then e else lookup \ x)"

lemma lookup_eqvt[eqvt]:
  fixes pi :: "name prm"
  and   \<theta> :: "(name \<times> trm) list"
  and   X :: "name"
  shows "pi \ (lookup \ X) = lookup (pi \ \) (pi \ X)"
  by (induct \<theta>) (auto simp add: eqvts)

nominal_primrec
  psubst :: "(name \ trm) list \ trm \ trm" (\_\_\\ [95,0] 210)
  and psubstb :: "(name \ trm) list \ btrm \ btrm" (\_\_\\<^sub>b\ [95,0] 210)
where
  "\\Var x\ = (lookup \ x)"
| "\\t \ u\ = \\t\ \ \\u\"
| "\\\t, u\\ = \\\t\, \\u\\"
| "\\Let T t u\ = Let T (\\t\) (\\u\\<^sub>b)"
| "x \ \ \ \\\x:T. t\ = (\x:T. \\t\)"
| "\\Base t\\<^sub>b = Base (\\t\)"
| "x \ \ \ \\Bind T x t\\<^sub>b = Bind T x (\\t\\<^sub>b)"
  by (finite_guess | simp add: abs_fresh | fresh_guess)+

lemma lookup_fresh:
  "x = y \ x \ set (map fst \) \ \(y, t)\set \. x \ t \ x \ lookup \ y"
  by (induct \<theta>) (use fresh_atm in force)+

lemma psubst_fresh:
  assumes "x \ set (map fst \)" and "\(y, t)\set \. x \ t"
  shows "x \ \\t\" and "x \ \\t'\\<^sub>b" using assms
proof (nominal_induct t and t' avoiding: \ rule: trm_btrm.strong_inducts)
  case (Var name)
  then show ?case
    by (metis lookup_fresh simps(1))
qed (auto simp: abs_fresh)

lemma psubst_eqvt[eqvt]:
  fixes pi :: "name prm"
  shows "pi \ (\\t\) = (pi \ \)\pi \ t\"
  and "pi \ (\\t'\\<^sub>b) = (pi \ \)\pi \ t'\\<^sub>b"
  by (nominal_induct t and t' avoiding: \ rule: trm_btrm.strong_inducts)
    (simp_all add: eqvts fresh_bij)

abbreviation
  subst :: "trm \ name \ trm \ trm" (\_[_\_]\ [100,0,0] 100)
where
  "t[x\t'] \ [(x,t')]\t\"

abbreviation
  substb :: "btrm \ name \ trm \ btrm" (\_[_\_]\<^sub>b\ [100,0,0] 100)
where
  "t[x\t']\<^sub>b \ [(x,t')]\t\\<^sub>b"

lemma lookup_forget:
  "(supp (map fst \)::name set) \* x \ lookup \ x = Var x"
  by (induct \<theta>) (auto simp add: split_paired_all fresh_star_def fresh_atm supp_list_cons supp_atm)

lemma supp_fst: "(x::name) \ supp (map fst (\::(name \ trm) list)) \ x \ supp \"
  by (induct \<theta>) (auto simp add: supp_list_nil supp_list_cons supp_prod)

lemma psubst_forget:
  "(supp (map fst \)::name set) \* t \ \\t\ = t"
  "(supp (map fst \)::name set) \* t' \ \\t'\\<^sub>b = t'"
proof (nominal_induct t and t' avoiding: \ rule: trm_btrm.strong_inducts)
  case (Var name)
  then show ?case
    by (simp add: fresh_star_set lookup_forget)
next
  case (Abs ty name trm)
  then show ?case
    apply (simp add: fresh_def)
    by (metis abs_fresh(1) fresh_star_set supp_fst trm.fresh(3))
next
  case (Bind ty name btrm)
  then show ?case
    apply (simp add: fresh_def)
    by (metis abs_fresh(1) btrm.fresh(2) fresh_star_set supp_fst)
qed (auto simp: fresh_star_set)

lemma psubst_nil[simp]: "[]\t\ = t" "[]\t'\\<^sub>b = t'"
  by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil)

lemma psubst_cons:
  assumes "(supp (map fst \)::name set) \* u"
  shows "((x, u) # \)\t\ = \\t[x\u]\" and "((x, u) # \)\t'\\<^sub>b = \\t'[x\u]\<^sub>b\\<^sub>b"
  using assms
  by (nominal_induct t and t' avoiding: x u \ rule: trm_btrm.strong_inducts)
    (simp_all add: fresh_list_nil fresh_list_cons psubst_forget)

lemma psubst_append:
  "(supp (map fst (\\<^sub>1 @ \\<^sub>2))::name set) \* map snd (\\<^sub>1 @ \\<^sub>2) \ (\\<^sub>1 @ \\<^sub>2)\t\ = \\<^sub>2\\\<^sub>1\t\\"
proof (induct \<theta>\<^sub>1 arbitrary: t)
  case Nil
  then show ?case
    by (auto simp: psubst_nil)
next
  case (Cons a \<theta>\<^sub>1)
  then show ?case
  proof (cases a)
    case (Pair a b)
    with Cons show ?thesis
      apply (simp add: supp_list_cons fresh_star_set fresh_list_cons)
      by (metis Un_iff fresh_star_set map_append psubst_cons(1) supp_list_append)
  qed
qed

lemma abs_pat_psubst [simp]:
  "(supp p::name set) \* \ \ \\\[p]. t\\<^sub>b = (\[p]. \\t\\<^sub>b)"
  by (induct p arbitrary: t) (auto simp add: fresh_star_def supp_atm)

lemma valid_insert:
  assumes "valid (\ @ [(x, T)] @ \)"
  shows "valid (\ @ \)" using assms
  by (induct \<Delta>)
    (auto simp add: fresh_list_append fresh_list_cons)

lemma fresh_set:
  shows "y \ xs = (\x\set xs. y \ x)"
  by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)

lemma context_unique:
  assumes "valid \"
  and "(x, T) \ set \"
  and "(x, U) \ set \"
  shows "T = U" using assms
  by induct (auto simp add: fresh_set fresh_prod fresh_atm)

lemma subst_type_aux:
  assumes a: "\ @ [(x, U)] @ \ \ t : T"
  and b: "\ \ u : U"
  shows "\ @ \ \ t[x\u] : T" using a b
proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct)
  case (Var y T x u \<Delta>)
  from \<open>valid (\<Delta> @ [(x, U)] @ \<Gamma>)\<close>
  have valid: "valid (\ @ \)" by (rule valid_insert)
  show "\ @ \ \ Var y[x\u] : T"
  proof cases
    assume eq: "x = y"
    from Var eq have "T = U" by (auto intro: context_unique)
    with Var eq valid show "\ @ \ \ Var y[x\u] : T" by (auto intro: weakening)
  next
    assume ineq: "x \ y"
    from Var ineq have "(y, T) \ set (\ @ \)" by simp
    then show "\ @ \ \ Var y[x\u] : T" using ineq valid by auto
  qed
next
  case (Tuple t\<^sub>1 T\<^sub>1 t\<^sub>2 T\<^sub>2)
  from refl \<open>\<Gamma> \<turnstile> u : U\<close>
  have "\ @ \ \ t\<^sub>1[x\u] : T\<^sub>1" by (rule Tuple)
  moreover from refl \<open>\<Gamma> \<turnstile> u : U\<close>
  have "\ @ \ \ t\<^sub>2[x\u] : T\<^sub>2" by (rule Tuple)
  ultimately have "\ @ \ \ \t\<^sub>1[x\u], t\<^sub>2[x\u]\ : T\<^sub>1 \ T\<^sub>2" ..
  then show ?case by simp
next
  case (Let p t T \<Delta>' s S)
  from refl \<open>\<Gamma> \<turnstile> u : U\<close>
  have "\ @ \ \ t[x\u] : T" by (rule Let)
  moreover note \<open>\<turnstile> p : T \<Rightarrow> \<Delta>'\<close>
  moreover have "\' @ (\ @ [(x, U)] @ \) = (\' @ \) @ [(x, U)] @ \" by simp
  then have "(\' @ \) @ \ \ s[x\u] : S" using \\ \ u : U\ by (rule Let)
  then have "\' @ \ @ \ \ s[x\u] : S" by simp
  ultimately have "\ @ \ \ (LET p = t[x\u] IN s[x\u]) : S"
    by (rule better_T_Let)
  moreover from Let have "(supp p::name set) \* [(x, u)]"
    by (simp add: fresh_star_def fresh_list_nil fresh_list_cons)
  ultimately show ?case by simp
next
  case (Abs y T t S)
  have "(y, T) # \ @ [(x, U)] @ \ = ((y, T) # \) @ [(x, U)] @ \"
    by simp
  then have "((y, T) # \) @ \ \ t[x\u] : S" using \\ \ u : U\ by (rule Abs)
  then have "(y, T) # \ @ \ \ t[x\u] : S" by simp
  then have "\ @ \ \ (\y:T. t[x\u]) : T \ S"
    by (rule typing.Abs)
  moreover from Abs have "y \ [(x, u)]"
    by (simp add: fresh_list_nil fresh_list_cons)
  ultimately show ?case by simp
next
  case (App t\<^sub>1 T S t\<^sub>2)
  from refl \<open>\<Gamma> \<turnstile> u : U\<close>
  have "\ @ \ \ t\<^sub>1[x\u] : T \ S" by (rule App)
  moreover from refl \<open>\<Gamma> \<turnstile> u : U\<close>
  have "\ @ \ \ t\<^sub>2[x\u] : T" by (rule App)
  ultimately have "\ @ \ \ (t\<^sub>1[x\u]) \ (t\<^sub>2[x\u]) : S"
    by (rule typing.App)
  then show ?case by simp
qed

lemmas subst_type = subst_type_aux [of "[]", simplified]

lemma match_supp_fst:
  assumes "\ p \ u \ \" shows "(supp (map fst \)::name set) = supp p" using assms
  by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append)

lemma match_supp_snd:
  assumes "\ p \ u \ \" shows "(supp (map snd \)::name set) = supp u" using assms
  by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append trm.supp)

lemma match_fresh: "\ p \ u \ \ \ (supp p::name set) \* u \
  (supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>"
  by (simp add: fresh_star_def fresh_def match_supp_fst match_supp_snd)

lemma match_type_aux:
  assumes "\ p : U \ \"
  and "\\<^sub>2 \ u : U"
  and "\\<^sub>1 @ \ @ \\<^sub>2 \ t : T"
  and "\ p \ u \ \"
  and "(supp p::name set) \* u"
  shows "\\<^sub>1 @ \\<^sub>2 \ \\t\ : T" using assms
proof (induct arbitrary: \<Gamma>\<^sub>1 \<Gamma>\<^sub>2 t u T \<theta>)
  case (PVar x U)
  from \<open>\<Gamma>\<^sub>1 @ [(x, U)] @ \<Gamma>\<^sub>2 \<turnstile> t : T\<close> \<open>\<Gamma>\<^sub>2 \<turnstile> u : U\<close>
  have "\\<^sub>1 @ \\<^sub>2 \ t[x\u] : T" by (rule subst_type_aux)
  moreover from \<open>\<turnstile> PVar x U \<rhd> u \<Rightarrow> \<theta>\<close> have "\<theta> = [(x, u)]"
    by cases simp_all
  ultimately show ?case by simp
next
  case (PTuple p S \<Delta>\<^sub>1 q U \<Delta>\<^sub>2)
  from \<open>\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>\<close> obtain u\<^sub>1 u\<^sub>2 \<theta>\<^sub>1 \<theta>\<^sub>2
    where u: "u = \u\<^sub>1, u\<^sub>2\" and \: "\ = \\<^sub>1 @ \\<^sub>2"
    and p: "\ p \ u\<^sub>1 \ \\<^sub>1" and q: "\ q \ u\<^sub>2 \ \\<^sub>2"
    by cases simp_all
  with PTuple have "\\<^sub>2 \ \u\<^sub>1, u\<^sub>2\ : S \ U" by simp
  then obtain u\<^sub>1: "\<Gamma>\<^sub>2 \<turnstile> u\<^sub>1 : S" and u\<^sub>2: "\<Gamma>\<^sub>2 \<turnstile> u\<^sub>2 : U"
    by cases (simp_all add: ty.inject trm.inject)
  note u\<^sub>1
  moreover from \<open>\<Gamma>\<^sub>1 @ (\<Delta>\<^sub>2 @ \<Delta>\<^sub>1) @ \<Gamma>\<^sub>2 \<turnstile> t : T\<close>
  have "(\\<^sub>1 @ \\<^sub>2) @ \\<^sub>1 @ \\<^sub>2 \ t : T" by simp
  moreover note p
  moreover from \<open>supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u\<close> and u
  have "(supp p::name set) \* u\<^sub>1" by (simp add: fresh_star_def)
  ultimately have \<theta>\<^sub>1: "(\<Gamma>\<^sub>1 @ \<Delta>\<^sub>2) @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<^sub>1\<lparr>t\<rparr> : T"
    by (rule PTuple)
  note u\<^sub>2
  moreover from \<theta>\<^sub>1
  have "\\<^sub>1 @ \\<^sub>2 @ \\<^sub>2 \ \\<^sub>1\t\ : T" by simp
  moreover note q
  moreover from \<open>supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u\<close> and u
  have "(supp q::name set) \* u\<^sub>2" by (simp add: fresh_star_def)
  ultimately have "\\<^sub>1 @ \\<^sub>2 \ \\<^sub>2\\\<^sub>1\t\\ : T"
    by (rule PTuple)
  moreover from \<open>\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>\<close> \<open>supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u\<close>
  have "(supp (map fst \)::name set) \* map snd \"
    by (rule match_fresh)
  ultimately show ?case using \<theta> by (simp add: psubst_append)
qed

lemmas match_type = match_type_aux [where \<Gamma>\<^sub>1="[]", simplified]

inductive eval :: "trm \ trm \ bool" (\_ \ _\ [60,60] 60)
where
  TupleL: "t \ t' \ \t, u\ \ \t', u\"
| TupleR: "u \ u' \ \t, u\ \ \t, u'\"
| Abs: "t \ t' \ (\x:T. t) \ (\x:T. t')"
| AppL: "t \ t' \ t \ u \ t' \ u"
| AppR: "u \ u' \ t \ u \ t \ u'"
| Beta: "x \ u \ (\x:T. t) \ u \ t[x\u]"
| Let: "((supp p)::name set) \* t \ distinct (pat_vars p) \
    \<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> (LET p = t IN u) \<longmapsto> \<theta>\<lparr>u\<rparr>"

equivariance match

equivariance eval

lemma match_vars:
  assumes "\ p \ t \ \" and "x \ supp p"
  shows "x \ set (map fst \)" using assms
  by induct (auto simp add: supp_atm)

lemma match_fresh_mono:
  assumes "\ p \ t \ \" and "(x::name) \ t"
  shows "\(y, t)\set \. x \ t" using assms
  by induct auto

nominal_inductive2 eval
avoids
  Abs: "{x}"
| Beta: "{x}"
| Let: "(supp p)::name set"
proof (simp_all add: fresh_star_def abs_fresh fin_supp)
  show "x \ t[x\u]" if "x \ u" for x t u
    by (simp add: \<open>x \<sharp> u\<close> psubst_fresh(1))
next
  show "\x\supp p. (x::name) \ \\u\"
    if "\x\supp p. (x::name) \ t" and "\ p \ t \ \"
    for p t \<theta> u
    by (meson that match_fresh_mono match_vars psubst_fresh(1))
qed

lemma typing_case_Abs:
  assumes ty: "\ \ (\x:T. t) : S"
  and fresh: "x \ \"
  and R: "\U. S = T \ U \ (x, T) # \ \ t : U \ P"
  shows P using ty
proof cases
  case (Abs x' T' t' U)
  obtain y::name where y: "y \ (x, \, \x':T'. t')"
    by (rule exists_fresh) (auto intro: fin_supp)
  from \<open>(\<lambda>x:T. t) = (\<lambda>x':T'. t')\<close> [symmetric]
  have x: "x \ (\x':T'. t')" by (simp add: abs_fresh)
  have x': "x' \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
  from \<open>(x', T') # \<Gamma> \<turnstile> t' : U\<close> have x'': "x' \<sharp> \<Gamma>"
    by (auto dest: valid_typing)
  have "(\x:T. t) = (\x':T'. t')" by fact
  also from x x' y have "\ = [(x, y)] \ [(x', y)] \ (\x':T'. t')"
    by (simp only: perm_fresh_fresh fresh_prod)
  also have "\ = (\x:T'. [(x, y)] \ [(x', y)] \ t')"
    by (simp add: swap_simps perm_fresh_fresh)
  finally have "(\x:T. t) = (\x:T'. [(x, y)] \ [(x', y)] \ t')" .
  then have T: "T = T'" and t: "[(x, y)] \ [(x', y)] \ t' = t"
    by (simp_all add: trm.inject alpha)
  from Abs T have "S = T \ U" by simp
  moreover from \<open>(x', T') # \<Gamma> \<turnstile> t' : U\<close>
  have "[(x, y)] \ [(x', y)] \ ((x', T') # \ \ t' : U)"
    by (simp add: perm_bool)
  with T t y x'' fresh have "(x, T) # \ \ t : U"
    by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod)
  ultimately show ?thesis by (rule R)
qed simp_all

nominal_primrec ty_size :: "ty \ nat"
where
  "ty_size (Atom n) = 0"
| "ty_size (T \ U) = ty_size T + ty_size U + 1"
| "ty_size (T \ U) = ty_size T + ty_size U + 1"
  by (rule TrueI)+

lemma bind_tuple_ineq:
  "ty_size (pat_type p) < ty_size U \ Bind U x t \ (\[p]. u)"
  by (induct p arbitrary: U x t u) (auto simp add: btrm.inject)

lemma valid_appD: assumes "valid (\ @ \)"
  shows "valid \" "valid \" using assms
  by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>)
    (auto simp add: Cons_eq_append_conv fresh_list_append)

lemma valid_app_freshs: assumes "valid (\ @ \)"
  shows "(supp \::name set) \* \" "(supp \::name set) \* \" using assms
  by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>)
    (auto simp add: Cons_eq_append_conv fresh_star_def
     fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append
     supp_prod fresh_prod supp_atm fresh_atm
     dest: notE [OF iffD1 [OF fresh_def]])

lemma perm_mem_left: "(x::name) \ ((pi::name prm) \ A) \ (rev pi \ x) \ A"
  by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp)

lemma perm_mem_right: "(rev (pi::name prm) \ (x::name)) \ A \ x \ (pi \ A)"
  by (drule perm_boolI [of _ pi]) (simp add: eqvts perm_pi_simp)

lemma perm_cases:
  assumes pi: "set pi \ A \ A"
  shows "((pi::name prm) \ B) \ A \ B"
proof
  fix x assume "x \ pi \ B"
  then show "x \ A \ B" using pi
  proof (induct pi arbitrary: x B rule: rev_induct)
    case Nil
    then show ?case
      by simp
  next
    case (snoc y xs)
    then show ?case
      apply simp
      by (metis SigmaE perm_mem_left perm_pi_simp(2) pt_name2 swap_simps(3))
  qed
qed

lemma abs_pat_alpha':
  assumes eq: "(\[p]. t) = (\[q]. u)"
  and ty: "pat_type p = pat_type q"
  and pv: "distinct (pat_vars p)"
  and qv: "distinct (pat_vars q)"
  shows "\pi::name prm. p = pi \ q \ t = pi \ u \
    set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)"
  using assms
proof (induct p arbitrary: q t u)
  case (PVar x T)
  note PVar' = this
  show ?case
  proof (cases q)
    case (PVar x' T')
    with \<open>(\<lambda>[PVar x T]. t) = (\<lambda>[q]. u)\<close>
    have "x = x' \ t = u \ x \ x' \ t = [(x, x')] \ u \ x \ u"
      by (simp add: btrm.inject alpha)
    then show ?thesis
    proof
      assume "x = x' \ t = u"
      with PVar PVar' have "PVar x T = ([]::name prm) \ q \
        t = ([]::name prm) \<bullet> u \<and>
        set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
          (supp (PVar x T) \<union> supp q)" by simp
      then show ?thesis ..
    next
      assume "x \ x' \ t = [(x, x')] \ u \ x \ u"
      with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and>
        t = [(x, x')] \ u \
        set [(x, x')] \ (supp (PVar x T) \ supp q) \
          (supp (PVar x T) \<union> supp q)"
        by (simp add: perm_swap swap_simps supp_atm perm_type)
      then show ?thesis ..
    qed
  next
    case (PTuple p\<^sub>1 p\<^sub>2)
    with PVar have "ty_size (pat_type p\<^sub>1) < ty_size T" by simp
    then have "Bind T x t \ (\[p\<^sub>1]. \[p\<^sub>2]. u)"
      by (rule bind_tuple_ineq)
    moreover from PTuple PVar
    have "Bind T x t = (\[p\<^sub>1]. \[p\<^sub>2]. u)" by simp
    ultimately show ?thesis ..
  qed
next
  case (PTuple p\<^sub>1 p\<^sub>2)
  note PTuple' = this
  show ?case
  proof (cases q)
    case (PVar x T)
    with PTuple have "ty_size (pat_type p\<^sub>1) < ty_size T" by auto
    then have "Bind T x u \ (\[p\<^sub>1]. \[p\<^sub>2]. t)"
      by (rule bind_tuple_ineq)
    moreover from PTuple PVar
    have "Bind T x u = (\[p\<^sub>1]. \[p\<^sub>2]. t)" by simp
    ultimately show ?thesis ..
  next
    case (PTuple p\<^sub>1' p\<^sub>2')
    with PTuple' have "(\[p\<^sub>1]. \[p\<^sub>2]. t) = (\[p\<^sub>1']. \[p\<^sub>2']. u)" by simp
    moreover from PTuple PTuple' have "pat_type p\<^sub>1 = pat_type p\<^sub>1'"
      by (simp add: ty.inject)
    moreover from PTuple' have "distinct (pat_vars p\<^sub>1)" by simp
    moreover from PTuple PTuple' have "distinct (pat_vars p\<^sub>1')" by simp
    ultimately have "\pi::name prm. p\<^sub>1 = pi \ p\<^sub>1' \
      (\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u) \<and>
      set pi \<subseteq> (supp p\<^sub>1 \<union> supp p\<^sub>1') \<times> (supp p\<^sub>1 \<union> supp p\<^sub>1')"
      by (rule PTuple')
    then obtain pi::"name prm" where
      "p\<^sub>1 = pi \ p\<^sub>1'" "(\[p\<^sub>2]. t) = pi \ (\[p\<^sub>2']. u)" and
      pi: "set pi \ (supp p\<^sub>1 \ supp p\<^sub>1') \ (supp p\<^sub>1 \ supp p\<^sub>1')" by auto
    from \<open>(\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u)\<close>
    have "(\[p\<^sub>2]. t) = (\[pi \ p\<^sub>2']. pi \ u)"
      by (simp add: eqvts)
    moreover from PTuple PTuple' have "pat_type p\<^sub>2 = pat_type (pi \ p\<^sub>2')"
      by (simp add: ty.inject pat_type_perm_eq)
    moreover from PTuple' have "distinct (pat_vars p\<^sub>2)" by simp
    moreover from PTuple PTuple' have "distinct (pat_vars (pi \ p\<^sub>2'))"
      by (simp add: pat_vars_eqvt [symmetric] distinct_eqvt [symmetric])
    ultimately have "\pi'::name prm. p\<^sub>2 = pi' \ pi \ p\<^sub>2' \
      t = pi' \ pi \ u \
      set pi' \ (supp p\<^sub>2 \ supp (pi \ p\<^sub>2')) \ (supp p\<^sub>2 \ supp (pi \ p\<^sub>2'))"
      by (rule PTuple')
    then obtain pi'::"name prm" where
      "p\<^sub>2 = pi' \ pi \ p\<^sub>2'" "t = pi' \ pi \ u" and
      pi': "set pi' \<subseteq> (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2')) \<times>
        (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2'))" by auto
    from PTuple PTuple' have "pi \ distinct (pat_vars \\p\<^sub>1', p\<^sub>2'\\)" by simp
    then have "distinct (pat_vars \\pi \ p\<^sub>1', pi \ p\<^sub>2'\\)" by (simp only: eqvts)
    with \<open>p\<^sub>1 = pi \<bullet> p\<^sub>1'\<close> PTuple'
    have fresh: "(supp p\<^sub>2 \ supp (pi \ p\<^sub>2') :: name set) \* p\<^sub>1"
      by (auto simp add: set_pat_vars_supp fresh_star_def fresh_def eqvts)
    from \<open>p\<^sub>1 = pi \<bullet> p\<^sub>1'\<close> have "pi' \<bullet> (p\<^sub>1 = pi \<bullet> p\<^sub>1')" by (rule perm_boolI)
    with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' fresh fresh]
    have "p\<^sub>1 = pi' \ pi \ p\<^sub>1'" by (simp add: eqvts)
    with \<open>p\<^sub>2 = pi' \<bullet> pi \<bullet> p\<^sub>2'\<close> have "\<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>"
      by (simp add: pt_name2)
    moreover
    have "((supp p\<^sub>2 \ (pi \ supp p\<^sub>2')) \ (supp p\<^sub>2 \ (pi \ supp p\<^sub>2'))::(name \ name) set) \
      (supp p\<^sub>2 \<union> (supp p\<^sub>1 \<union> supp p\<^sub>1' \<union> supp p\<^sub>2')) \<times> (supp p\<^sub>2 \<union> (supp p\<^sub>1 \<union> supp p\<^sub>1' \<union> supp p\<^sub>2'))"
      by (rule subset_refl Sigma_mono Un_mono perm_cases [OF pi])+
    with pi' have "set pi' \<subseteq> \<dots>" by (simp add: supp_eqvt [symmetric])
    with pi have "set (pi' @ pi) \ (supp \\p\<^sub>1, p\<^sub>2\\ \ supp \\p\<^sub>1', p\<^sub>2'\\) \
      (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>)"
      by (simp add: Sigma_Un_distrib1 Sigma_Un_distrib2 Un_ac) blast
    moreover note \<open>t = pi' \<bullet> pi \<bullet> u\<close>
    ultimately have "\\p\<^sub>1, p\<^sub>2\\ = (pi' @ pi) \ q \ t = (pi' @ pi) \ u \
      set (pi' @ pi) \ (supp \\p\<^sub>1, p\<^sub>2\\ \ supp q) \
        (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp q)" using PTuple
      by (simp add: pt_name2)
    then show ?thesis ..
  qed
qed

lemma typing_case_Let:
  assumes ty: "\ \ (LET p = t IN u) : U"
  and fresh: "(supp p::name set) \* \"
  and distinct: "distinct (pat_vars p)"
  and R: "\T \. \ \ t : T \ \ p : T \ \ \ \ @ \ \ u : U \ P"
  shows P using ty
proof cases
  case (Let p' t' T \<Delta> u')
  then have "(supp \::name set) \* \"
    by (auto intro: valid_typing valid_app_freshs)
  with Let have "(supp p'::name set) \* \"
    by (simp add: pat_var)
  with fresh have fresh': "(supp p \ supp p' :: name set) \* \"
    by (auto simp add: fresh_star_def)
  from Let have "(\[p]. Base u) = (\[p']. Base u')"
    by (simp add: trm.inject)
  moreover from Let have "pat_type p = pat_type p'"
    by (simp add: trm.inject)
  moreover note distinct
  moreover from \<open>\<Delta> @ \<Gamma> \<turnstile> u' : U\<close> have "valid (\<Delta> @ \<Gamma>)"
    by (rule valid_typing)
  then have "valid \" by (rule valid_appD)
  with \<open>\<turnstile> p' : T \<Rightarrow> \<Delta>\<close> have "distinct (pat_vars p')"
    by (simp add: valid_distinct pat_vars_ptyping)
  ultimately have "\pi::name prm. p = pi \ p' \ Base u = pi \ Base u' \
    set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')"
    by (rule abs_pat_alpha')
  then obtain pi::"name prm" where pi: "p = pi \ p'" "u = pi \ u'"
    and pi': "set pi \ (supp p \ supp p') \ (supp p \ supp p')"
    by (auto simp add: btrm.inject)
  from Let have "\ \ t : T" by (simp add: trm.inject)
  moreover from \<open>\<turnstile> p' : T \<Rightarrow> \<Delta>\<close> have "\<turnstile> (pi \<bullet> p') : (pi \<bullet> T) \<Rightarrow> (pi \<bullet> \<Delta>)"
    by (simp add: ptyping.eqvt)
  with pi have "\ p : T \ (pi \ \)" by (simp add: perm_type)
  moreover from Let
  have "(pi \ \) @ (pi \ \) \ (pi \ u') : (pi \ U)"
    by (simp add: append_eqvt [symmetric] typing.eqvt)
  with pi have "(pi \ \) @ \ \ u : U"
    by (simp add: perm_type pt_freshs_freshs
      [OF pt_name_inst at_name_inst pi' fresh' fresh'])
  ultimately show ?thesis by (rule R)
qed simp_all

lemma preservation:
  assumes "t \ t'" and "\ \ t : T"
  shows "\ \ t' : T" using assms
proof (nominal_induct avoiding: \<Gamma> T rule: eval.strong_induct)
  case (TupleL t t' u)
  from \<open>\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T\<close> obtain T\<^sub>1 T\<^sub>2
    where "T = T\<^sub>1 \ T\<^sub>2" "\ \ t : T\<^sub>1" "\ \ u : T\<^sub>2"
    by cases (simp_all add: trm.inject)
  from \<open>\<Gamma> \<turnstile> t : T\<^sub>1\<close> have "\<Gamma> \<turnstile> t' : T\<^sub>1" by (rule TupleL)
  then have "\ \ \t', u\ : T\<^sub>1 \ T\<^sub>2" using \\ \ u : T\<^sub>2\
    by (rule Tuple)
  with \<open>T = T\<^sub>1 \<otimes> T\<^sub>2\<close> show ?case by simp
next
  case (TupleR u u' t)
  from \<open>\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T\<close> obtain T\<^sub>1 T\<^sub>2
    where "T = T\<^sub>1 \ T\<^sub>2" "\ \ t : T\<^sub>1" "\ \ u : T\<^sub>2"
    by cases (simp_all add: trm.inject)
  from \<open>\<Gamma> \<turnstile> u : T\<^sub>2\<close> have "\<Gamma> \<turnstile> u' : T\<^sub>2" by (rule TupleR)
  with \<open>\<Gamma> \<turnstile> t : T\<^sub>1\<close> have "\<Gamma> \<turnstile> \<langle>t, u'\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2"
    by (rule Tuple)
  with \<open>T = T\<^sub>1 \<otimes> T\<^sub>2\<close> show ?case by simp
next
  case (Abs t t' x S)
  from \<open>\<Gamma> \<turnstile> (\<lambda>x:S. t) : T\<close> \<open>x \<sharp> \<Gamma>\<close> obtain U where
    T: "T = S \ U" and U: "(x, S) # \ \ t : U"
    by (rule typing_case_Abs)
  from U have "(x, S) # \ \ t' : U" by (rule Abs)
  then have "\ \ (\x:S. t') : S \ U"
    by (rule typing.Abs)
  with T show ?case by simp
next
  case (Beta x u S t)
  from \<open>\<Gamma> \<turnstile> (\<lambda>x:S. t) \<cdot> u : T\<close> \<open>x \<sharp> \<Gamma>\<close>
  obtain "(x, S) # \ \ t : T" and "\ \ u : S"
    by cases (auto simp add: trm.inject ty.inject elim: typing_case_Abs)
  then show ?case by (rule subst_type)
next
  case (Let p t \<theta> u)
  from \<open>\<Gamma> \<turnstile> (LET p = t IN u) : T\<close> \<open>supp p \<sharp>* \<Gamma>\<close> \<open>distinct (pat_vars p)\<close>
  obtain U \<Delta> where "\<turnstile> p : U \<Rightarrow> \<Delta>" "\<Gamma> \<turnstile> t : U" "\<Delta> @ \<Gamma> \<turnstile> u : T"
    by (rule typing_case_Let)
  then show ?case using \<open>\<turnstile> p \<rhd> t \<Rightarrow> \<theta>\<close> \<open>supp p \<sharp>* t\<close>
    by (rule match_type)
next
  case (AppL t t' u)
  from \<open>\<Gamma> \<turnstile> t \<cdot> u : T\<close> obtain U where
    t: "\ \ t : U \ T" and u: "\ \ u : U"
    by cases (auto simp add: trm.inject)
  from t have "\ \ t' : U \ T" by (rule AppL)
  then show ?case using u by (rule typing.App)
next
  case (AppR u u' t)
  from \<open>\<Gamma> \<turnstile> t \<cdot> u : T\<close> obtain U where
    t: "\ \ t : U \ T" and u: "\ \ u : U"
    by cases (auto simp add: trm.inject)
  from u have "\ \ u' : U" by (rule AppR)
  with t show ?case by (rule typing.App)
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.27 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.