theory LFex

imports Nominal "../Quotient_List"

begin

atom_decl name ident

nominal_datatype kind = 

    Type

  | KPi "ty" "name" "kind"

and ty =  

    TConst "ident"

  | TApp "ty" "trm"

  | TPi "ty" "name" "ty"

and trm = 

    Const "ident"

  | Var "name"

  | App "trm" "trm"

  | Lam "ty" "name" "trm" 

function

    fv_kind :: "kind \<Rightarrow> name set"

and fv_ty   :: "ty \<Rightarrow> name set"

and fv_trm  :: "trm \<Rightarrow> name set"

where

  "fv_kind (Type) = {}"

| "fv_kind (KPi A x K) = (fv_ty A) \<union> ((fv_kind K) - {x})"

| "fv_ty (TConst i) = {}"

| "fv_ty (TApp A M) = (fv_ty A) \<union> (fv_trm M)"

| "fv_ty (TPi A x B) = (fv_ty A) \<union> ((fv_ty B) - {x})"

| "fv_trm (Const i) = {}"

| "fv_trm (Var x) = {x}"

| "fv_trm (App M N) = (fv_trm M) \<union> (fv_trm N)"

| "fv_trm (Lam A x M) = (fv_ty A) \<union> ((fv_trm M) - {x})"

sorry

termination fv_kind sorry

inductive

    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)

and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)

and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)

where

  a1:  "(Type) \<approx>ki (Type)"

| a21: "\<lbrakk>A \<approx>ty A'; K \<approx>ki K'\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x K')"

| a22: "\<lbrakk>A \<approx>ty A'; K \<approx>ki ([(x,x')]\<bullet>K'); x \<notin> (fv_ty A'); x \<notin> ((fv_kind K') - {x'})\<rbrakk> 

        \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"

| a3:  "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"

| a4:  "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"

| a51: "\<lbrakk>A \<approx>ty A'; B \<approx>ty B'\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x B')"

| a52: "\<lbrakk>A \<approx>ty A'; B \<approx>ty ([(x,x')]\<bullet>B'); x \<notin> (fv_ty B'); x \<notin> ((fv_ty B') - {x'})\<rbrakk> 

        \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"

| a6:  "i = j \<Longrightarrow> (Const i) \<approx>trm (Const j)"

| a7:  "x = y \<Longrightarrow> (Var x) \<approx>trm (Var y)"

| a8:  "\<lbrakk>M \<approx>trm M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"

| a91: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x M')"

| a92: "\<lbrakk>A \<approx>ty A'; M \<approx>tr ([(x,x')]\<bullet>M'); x \<notin> (fv_ty B'); x \<notin> ((fv_trm M') - {x'})\<rbrakk> 

        \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"

lemma al_refl:

  fixes K::"kind" 

  and   A::"ty"

  and   M::"trm"

  shows "K \<approx>ki K"

  and   "A \<approx>ty A"

  and   "M \<approx>tr M"

  apply(induct K and A and M rule: kind_ty_trm.inducts)

  apply(auto intro: akind_aty_atrm.intros)

  done

lemma alpha_equivps:

  shows "equivp akind"

  and   "equivp aty"

  and   "equivp atrm"

sorry

quotient_type KIND = kind / akind

  by (rule alpha_equivps)

quotient_type 

    TY = ty / aty and   

    TRM = trm / atrm

  by (auto intro: alpha_equivps)

quotient_definition

   "TYP :: KIND"

is

  "Type"

quotient_definition

   "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"

is

  "KPi"

quotient_definition

   "TCONST :: ident \<Rightarrow> TY"

is

  "TConst"

quotient_definition

   "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"

is

  "TApp"

quotient_definition

   "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"

is

  "TPi"

(* FIXME: does not work with CONST *)

quotient_definition

   "CONS :: ident \<Rightarrow> TRM"

is

  "Const"

quotient_definition

   "VAR :: name \<Rightarrow> TRM"

is

  "Var"

quotient_definition

   "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"

is

  "App"

quotient_definition

   "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"

is

  "Lam"

thm TYP_def

thm KPI_def

thm TCONST_def

thm TAPP_def

thm TPI_def

thm VAR_def

thm CONS_def

thm APP_def

thm LAM_def

(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)

quotient_definition

   "FV_kind :: KIND \<Rightarrow> name set"

is

  "fv_kind"

quotient_definition

   "FV_ty :: TY \<Rightarrow> name set"

is

  "fv_ty"

quotient_definition

   "FV_trm :: TRM \<Rightarrow> name set"

is

  "fv_trm"

thm FV_kind_def

thm FV_ty_def

thm FV_trm_def

(* FIXME: does not work yet *)

overloading

    perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"   (unchecked)

    perm_ty   \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"       (unchecked)

    perm_trm  \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"     (unchecked) 

begin

quotient_definition

   "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"

is

  "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"

quotient_definition

   "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"

is

  "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"

quotient_definition

   "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"

is

  "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"

end

(* TODO/FIXME: Think whether these RSP theorems are true. *)

lemma kpi_rsp[quot_respect]: 

  "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry

lemma tconst_rsp[quot_respect]: 

  "(op = ===> aty) TConst TConst" sorry

lemma tapp_rsp[quot_respect]: 

  "(aty ===> atrm ===> aty) TApp TApp" sorry

lemma tpi_rsp[quot_respect]: 

  "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry

lemma var_rsp[quot_respect]: 

  "(op = ===> atrm) Var Var" sorry

lemma app_rsp[quot_respect]: 

  "(atrm ===> atrm ===> atrm) App App" sorry

lemma const_rsp[quot_respect]: 

  "(op = ===> atrm) Const Const" sorry

lemma lam_rsp[quot_respect]: 

  "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry

lemma perm_kind_rsp[quot_respect]: 

  "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry

lemma perm_ty_rsp[quot_respect]: 

  "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry

lemma perm_trm_rsp[quot_respect]: 

  "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry

lemma fv_ty_rsp[quot_respect]: 

  "(aty ===> op =) fv_ty fv_ty" sorry

lemma fv_kind_rsp[quot_respect]: 

  "(akind ===> op =) fv_kind fv_kind" sorry

lemma fv_trm_rsp[quot_respect]: 

  "(atrm ===> op =) fv_trm fv_trm" sorry

thm akind_aty_atrm.induct

thm kind_ty_trm.induct

lemma 

  assumes a0:

  "P1 TYP TYP"

  and a1: 

  "\<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> 

  \<Longrightarrow> P1 (KPI A x K) (KPI A' x K')"

  and a2:    

  "\<And>A A' K K' x x'. \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); 

    x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K')"

  and a3: 

  "\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j)"

  and a4:

  "\<And>A A' M M'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P2 (TAPP A M) (TAPP A' M')"

  and a5:

  "\<And>A A' B B' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x B')"

  and a6:

  "\<And>A A' B x x' B'. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \<bullet> B'); P2 B ([(x, x')] \<bullet> B'); 

  x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B')"

  and a7:

  "\<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j))"

  and a8:

  "\<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y))"

  and a9:

  "\<And>M m M' N N'. \<lbrakk>(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\<rbrakk> \<Longrightarrow> P3 (APP M N) (APP M' N')"

  and a10: 

  "\<And>A A' M M' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x M')"

  and a11:

  "\<And>A A' M x x' M' B'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); 

  x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')"

  shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>

         ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> 

         ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"

using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11

apply(lifting_setup akind_aty_atrm.induct)

defer

apply injection

apply cleaning

apply (simp only: ball_reg_eqv[OF KIND_equivp] ball_reg_eqv[OF TRM_equivp] ball_reg_eqv[OF TY_equivp])

apply (rule ball_reg_right)+

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

defer

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

defer

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

defer

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})

apply simp

apply simp

apply regularize+

done

(* Does not work:

lemma

  assumes a0: "P1 TYP"

  and     a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)"

  and     a2: "\<And>id. P2 (TCONST id)"

  and     a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)"

  and     a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)"

  and     a5: "\<And>id. P3 (CONS id)"

  and     a6: "\<And>name. P3 (VAR name)"

  and     a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)"

  and     a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)"

  shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"

using a0 a1 a2 a3 a4 a5 a6 a7 a8

*)

lemma "\<lbrakk>P TYP;

  \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind);

  \<And>id. Q (TCONST id);

  \<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm);

  \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2);

  \<And>id. R (CONS id); \<And>name. R (VAR name);

  \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);

  \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>

  \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"

apply(lifting kind_ty_trm.induct)

done

end