theory LFex

imports Nominal QuotMain

begin

atom_decl name id

nominal_datatype kind = 

    Type

  | KPi "ty" "name" "kind"

and ty =  

    TConst "id"

  | TApp "ty" "trm"

  | TPi "ty" "name" "ty"

and trm = 

    Const "id"

  | 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_EQUIVs:

  shows "EQUIV akind"

  and   "EQUIV aty"

  and   "EQUIV atrm"

sorry

quotient KIND = kind / akind

  by (rule alpha_EQUIVs)

quotient TY = ty / aty

   and   TRM = trm / atrm

  by (auto intro: alpha_EQUIVs)

print_quotients

quotient_def 

  TYP :: "KIND"

where

  "TYP \<equiv> Type"

quotient_def 

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

where

  "KPI \<equiv> KPi"

quotient_def 

  TCONST :: "id \<Rightarrow> TY"

where

  "TCONST \<equiv> TConst"

quotient_def 

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

where

  "TAPP \<equiv> TApp"

quotient_def 

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

where

  "TPI \<equiv> TPi"

(* FIXME: does not work with CONST *)

quotient_def 

  CONS :: "id \<Rightarrow> TRM"

where

  "CONS \<equiv> Const"

quotient_def 

  VAR :: "name \<Rightarrow> TRM"

where

  "VAR \<equiv> Var"

quotient_def 

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

where

  "APP \<equiv> App"

quotient_def 

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

where

  "LAM \<equiv> 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_def 

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

where

  "FV_kind \<equiv> fv_kind"

quotient_def 

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

where

  "FV_ty \<equiv> fv_ty"

quotient_def 

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

where

  "FV_trm \<equiv> 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_def 

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

where

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

quotient_def 

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

where

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

quotient_def 

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

where

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

ML {* val defs =

  @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def

    FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}

*}

ML {* val consts = lookup_quot_consts defs *}

thm akind_aty_atrm.induct

ML {*

fun regularize_monos_tac lthy eqvs =

  let 

    val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) eqvs

    val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) eqvs

  in

    REPEAT_ALL_NEW (FIRST' [

      (rtac @{thm impI} THEN' atac),

      (rtac @{thm my_equiv_res_forallR}),

      (rtac @{thm my_equiv_res_forallL}),

      (rtac @{thm Set.imp_mono}),

      (resolve_tac (Inductive.get_monos lthy)),

      (EqSubst.eqsubst_tac lthy [0] (subs1 @ subs2))

    ])

  end

*}

ML {*

  val subs1 = map (fn x => @{thm eq_reflection} OF [@{thm equiv_res_forall} OF [x]]) @{thms alpha_EQUIVs}

*}

ML {*

fun regularize_tac ctxt rel_eqvs rel_refls =

  let 

    val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs

    val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs

  in

  (ObjectLogic.full_atomize_tac) THEN'

  REPEAT_ALL_NEW (FIRST' [

    FIRST' (map rtac rel_refls),

    atac,

    rtac @{thm universal_twice},

    rtac @{thm impI} THEN' atac,

    rtac @{thm implication_twice},

    EqSubst.eqsubst_tac ctxt [0] (subs1 @ subs2),

    (* For a = b \<longrightarrow> a \<approx> b *)

    (rtac @{thm RIGHT_RES_FORALL_REGULAR})

  ])

  end

*}

thm RIGHT_RES_FORALL_REGULAR

thm my_equiv_res_forallR

(*

lemma "\<And>i j xb\<Colon>trm \<Rightarrow> trm \<Rightarrow> bool. Respects (atrm ===> atrm ===> op =) xb \<Longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm\<in>Respects (atrm ===> atrm). xb (Const i) (m (Const j))) \<longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm. xb (Const i) (m (Const j)))"

apply (simp add: Ball_def IN_RESPECTS Respects_def)

apply (metis COMBK_def al_refl(3))

*)

lemma move_quant: "((\<forall>y. \<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>y. \<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"

by auto

lemma "\<lbrakk>P1 TYP TYP; \<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>A A' K x x' K'.

    \<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>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);

 \<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>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>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>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j)); \<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y));

 \<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>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>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')\<rbrakk>

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

   ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"

apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})

apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *})

apply(atomize (full))

apply(rule RIGHT_RES_FORALL_REGULAR)

apply(rule RIGHT_RES_FORALL_REGULAR)

apply(rule RIGHT_RES_FORALL_REGULAR)

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(rule impI) apply(assumption)

apply(rule Set.imp_mono)

apply(rule impI) apply(assumption)

apply(rule Set.imp_mono)

apply(rule impI) apply(assumption)

apply(rule Set.imp_mono)

apply(rule impI) apply(assumption)

apply(rule Set.imp_mono)

apply(rule impI) apply(assumption)

apply(rule Set.imp_mono)

apply(rule impI) apply(assumption)

apply(rule Set.imp_mono)

apply(rule impI) apply(assumption)

apply(rule Set.imp_mono)

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

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

apply (simp add: Ball_def IN_RESPECTS Respects_def)

apply (metis COMBK_def al_refl(3))

apply(rule Set.imp_mono)

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

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

apply (simp add: Ball_def IN_RESPECTS Respects_def)

apply (metis COMBK_def al_refl(3))

apply(rule Set.imp_mono)

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

apply(rule move_quant)

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

apply(rule move_quant)

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

apply(rule move_quant)

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

apply (simp add: Ball_def IN_RESPECTS Respects_def)

apply (metis COMBK_def al_refl(3))

apply(rule impI) apply(assumption)

ML {*

val rty_qty_rel =

  [(@{typ kind}, (@{typ KIND}, @{term akind})),

   (@{typ ty}, (@{typ TY}, @{term aty})),

   (@{typ trm}, (@{typ TRM}, @{term atrm}))]

*}

print_quotients

ML {* val rty = [@{typ }] *}

ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}

ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *}

prove {* build_regularize_goal t_a rty rel @{context}

end