Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: yab.xml Sprache: Isabelle

Original von: Isabelle^©

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

theory Pattern
imports "HOL-Nominal.Nominal"
begin

no_syntax
  "_Map" :: "maplets => 'a \ 'b" ("(1[_])")

atom_decl name

nominal_datatype ty =
    Atom nat
  | Arrow ty ty  (infixr "\" 200)
  | TupleT ty ty  (infixr "\" 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  ("(1'\_,/ _'\)")
  | Abs ty "\name\trm"
  | App trm trm  (infixl "\" 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  ("(1'\\_,/ _'\\)")

(* 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 (standard, goal_cases)
  case (1 x)
  show ?case by (induct x) simp_all
next
  case (2 _ _ x)
  show ?case by (induct x) (simp_all add: pt_name2)
next
  case (3 _ _ x)
  then show ?case by (induct x) (simp_all add: pt_name3)
qed

instance pat :: fs_name
proof (standard, goal_cases)
  case (1 x)
  show ?case 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
  apply (nominal_induct \<Gamma>\<^sub>1 t T avoiding: \<Gamma>\<^sub>2 rule: typing.strong_induct)
  apply auto
  apply (drule_tac x="(x, T) # \\<^sub>2" in meta_spec)
  apply (auto intro: valid_typing)
  apply (drule_tac x="\\<^sub>2" in meta_spec)
  apply (drule_tac x="\ @ \\<^sub>2" in meta_spec)
  apply (auto intro: valid_typing)
  apply (rule typing.Let)
  apply assumption+
  apply (drule meta_mp)
  apply (rule valid_app_mono)
  apply (rule valid_typing)
  apply assumption
  apply (auto simp add: pat_freshs)
  done

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)"
  apply finite_guess+
  apply (simp add: abs_fresh | fresh_guess)+
  done

lemma lookup_fresh:
  "x = y \ x \ set (map fst \) \ \(y, t)\set \. x \ t \ x \ lookup \ y"
  apply (induct \<theta>)
  apply (simp_all add: split_paired_all fresh_atm)
  apply (case_tac "x = y")
  apply (auto simp add: fresh_atm)
  done

lemma psubst_fresh:
  assumes "x \ set (map fst \)" and "\(y, t)\set \. x \ t"
  shows "x \ \\t\" and "x \ \\t'\\<^sub>b" using assms
  apply (nominal_induct t and t' avoiding: \ rule: trm_btrm.strong_inducts)
  apply simp
  apply (rule lookup_fresh)
  apply (rule impI)
  apply (simp_all add: abs_fresh)
  done

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'"
  apply (nominal_induct t and t' avoiding: \ rule: trm_btrm.strong_inducts)
  apply (auto simp add: fresh_star_def lookup_forget abs_fresh)
  apply (drule_tac x=\<theta> in meta_spec)
  apply (drule meta_mp)
  apply (rule ballI)
  apply (drule_tac x=x in bspec)
  apply assumption
  apply (drule supp_fst)
  apply (auto simp add: fresh_def)
  apply (drule_tac x=\<theta> in meta_spec)
  apply (drule meta_mp)
  apply (rule ballI)
  apply (drule_tac x=x in bspec)
  apply assumption
  apply (drule supp_fst)
  apply (auto simp add: fresh_def)
  done

lemma psubst_nil: "[]\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\\"
  by (induct \<theta>\<^sub>1 arbitrary: t)
    (simp_all add: psubst_nil split_paired_all supp_list_cons psubst_cons fresh_star_def
      fresh_list_cons fresh_list_append supp_list_append)

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"
  apply (simp_all add: fresh_star_def abs_fresh fin_supp)
  apply (rule psubst_fresh)
  apply simp
  apply simp
  apply (rule ballI)
  apply (rule psubst_fresh)
  apply (rule match_vars)
  apply assumption+
  apply (rule match_fresh_mono)
  apply auto
  done

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
    apply (induct pi arbitrary: x B rule: rev_induct)
    apply simp
    apply (simp add: split_paired_all supp_eqvt)
    apply (drule perm_mem_left)
    apply (simp add: calc_atm split: if_split_asm)
    apply (auto dest: perm_mem_right)
    done
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

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: yab.xml Sprache: Isabelle

Original von: Isabelle^©

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: yab.xml Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©