# Theory Weakening

theory Weakening
imports Nominal
theory Weakening
imports
begin

text

atom_decl name

text

nominal_datatype lam =
Var
| App
| Lam  ( [100,100] 100)

nominal_datatype ty =
TVar
| TArr   ( [100,100] 100)

lemma ty_fresh:
fixes x::
and   T::
shows
by (nominal_induct T rule: ty.strong_induct)

text

inductive
valid ::
where
v1[intro]:
| v2[intro]:

equivariance valid

text

inductive
typing ::  ( [60,60,60] 60)
where
t_Var[intro]:
| t_App[intro]:
| t_Lam[intro]:

text

equivariance typing
nominal_inductive typing

text

abbreviation
::  ( [60,60] 60)
where

text

text

lemma weakening_version1:
fixes Γ1 Γ2::
assumes a:
and     b:
and     c:
shows
using a b c
by (nominal_induct Γ1 t T avoiding: Γ2 rule: typing.strong_induct)
(auto | atomize)+

text

lemma weakening_version2:
fixes Γ1 Γ2::
and   t ::
and   τ ::
assumes a:
and     b:
and     c:
shows
using a b c
proof (nominal_induct Γ1 t T avoiding: Γ2 rule: typing.strong_induct)
case (t_Var Γ1 x T)
have  by fact
moreover
have  by fact
moreover
have  by fact
ultimately show  by auto
next
case (t_Lam x Γ1 T1 t T2)
have vc:  by fact
have ih:  by fact
have  by fact
then have  by simp
moreover
have  by fact
then have  using vc by (simp add: v2)
ultimately have  using ih by simp
with vc show  by auto
qed (auto)

text

lemma weakening_not_straigh_forward:
fixes Γ1 Γ2::
assumes a:
and     b:
and     c:
shows
using a b c
proof (induct arbitrary: Γ2)
case (t_Var Γ1 x T)
have  by fact
moreover
have  by fact
moreover
have  by fact
ultimately show  by auto
next
case (t_Lam x Γ1 T1 t T2)

have a0:  by fact
have a1:  by fact
have a2:  by fact
have a3:  by fact
have ih:  by fact
have  using a2 by simp
moreover
have  using v2
oops

text

lemma weakening_with_explicit_renaming:
fixes Γ1 Γ2::
assumes a:
and     b:
and     c:
shows
using a b c
proof (induct arbitrary: Γ2)
case (t_Lam x Γ1 T1 t T2)
have fc0:  by fact
have ih:  by fact
obtain c:: where fc1:
by (rule exists_fresh) (auto simp add: fs_name1)
have  using fc1
by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
moreover
have
proof -

have
proof -
have  by fact
then have  using fc0 fc1
by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
then show  by (rule perm_boolE)
qed
moreover
have
proof -
have  by fact
then show  using fc1
by (auto intro!: v2 simp add: fresh_left calc_atm eqvts)
qed

ultimately have  using ih by simp

then have  by (rule perm_boolI)
then have  using fc1
by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
then show  using fc1 by auto
qed
ultimately show  by simp
qed (auto)

text

end