1 theory LFex

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"

     3 begin

     4 

     5 atom_decl name

     6 atom_decl ident

     7 

     8 datatype kind = 

     9     Type

    10   | KPi "ty" "name" "kind"

    11 and ty =  

    12     TConst "ident"

    13   | TApp "ty" "trm"

    14   | TPi "ty" "name" "ty"

    15 and trm = 

    16     Const "ident"

    17   | Var "name"

    18   | App "trm" "trm"

    19   | Lam "ty" "name" "trm" 

    20 

    21 fun

    22     rfv_kind :: "kind \<Rightarrow> atom set"

    23 and rfv_ty   :: "ty \<Rightarrow> atom set"

    24 and rfv_trm  :: "trm \<Rightarrow> atom set"

    25 where

    26   "rfv_kind (Type) = {}"

    27 | "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"

    28 | "rfv_ty (TConst i) = {}"

    29 | "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"

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

    31 | "rfv_trm (Const i) = {}"

    32 | "rfv_trm (Var x) = {atom x}"

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

    34 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"

    35 

    36 instantiation kind and ty and trm :: pt

    37 begin

    38 

    39 primrec

    40     permute_kind

    41 and permute_ty

    42 and permute_trm

    43 where

    44   "permute_kind pi Type = Type"

    45 | "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)"

    46 | "permute_ty pi (TConst i) = TConst (pi \<bullet> i)"

    47 | "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)"

    48 | "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)"

    49 | "permute_trm pi (Const i) = Const (pi \<bullet> i)"

    50 | "permute_trm pi (Var x) = Var (pi \<bullet> x)"

    51 | "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"

    52 | "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"

    53 

    54 lemma rperm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z"

    55 apply(induct_tac rule: kind_ty_trm.induct)

    56 apply(simp_all)

    57 done

    58 instance

    59 apply default

    60 apply (simp_all only:rperm_zero_ok)

    61 apply(induct_tac [!] x)

    62 apply(simp_all)

    63 apply(induct_tac ty)

    64 apply(simp_all)

    65 apply(induct_tac trm)

    66 apply(simp_all)

    67 apply(induct_tac trm)

    68 apply(simp_all)

    69 done

    70 

    71 end

    72 

    73 inductive

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

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

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

    77 where

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

    79 | a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"

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

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

    82 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"

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

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

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

    86 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"

    87 

    88 lemma al_refl:

    89   fixes K::"kind" 

    90   and   A::"ty"

    91   and   M::"trm"

    92   shows "K \<approx>ki K"

    93   and   "A \<approx>ty A"

    94   and   "M \<approx>tr M"

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

    96   apply(auto intro: akind_aty_atrm.intros)

    97   apply (rule a2)

    98   apply auto

    99   apply(rule_tac x="0" in exI)

   100   apply(simp_all add: fresh_star_def fresh_zero_perm)

   101   apply (rule a5)

   102   apply auto

   103   apply(rule_tac x="0" in exI)

   104   apply(simp_all add: fresh_star_def fresh_zero_perm)

   105   apply (rule a9)

   106   apply auto

   107   apply(rule_tac x="0" in exI)

   108   apply(simp_all add: fresh_star_def fresh_zero_perm)

   109   done

   110 

   111 lemma alpha_equivps:

   112   shows "equivp akind"

   113   and   "equivp aty"

   114   and   "equivp atrm"

   115 sorry

   116 

   117 quotient_type KIND = kind / akind

   118   by (rule alpha_equivps)

   119 

   120 quotient_type

   121     TY = ty / aty and

   122     TRM = trm / atrm

   123   by (auto intro: alpha_equivps)

   124 

   125 quotient_definition

   126    "TYP :: KIND"

   127 as

   128   "Type"

   129 

   130 quotient_definition

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

   132 as

   133   "KPi"

   134 

   135 quotient_definition

   136    "TCONST :: ident \<Rightarrow> TY"

   137 as

   138   "TConst"

   139 

   140 quotient_definition

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

   142 as

   143   "TApp"

   144 

   145 quotient_definition

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

   147 as

   148   "TPi"

   149 

   150 (* FIXME: does not work with CONST *)

   151 quotient_definition

   152    "CONS :: ident \<Rightarrow> TRM"

   153 as

   154   "Const"

   155 

   156 quotient_definition

   157    "VAR :: name \<Rightarrow> TRM"

   158 as

   159   "Var"

   160 

   161 quotient_definition

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

   163 as

   164   "App"

   165 

   166 quotient_definition

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

   168 as

   169   "Lam"

   170 

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

   172 quotient_definition

   173    "fv_kind :: KIND \<Rightarrow> atom set"

   174 as

   175   "rfv_kind"

   176 

   177 quotient_definition

   178    "fv_ty :: TY \<Rightarrow> atom set"

   179 as

   180   "rfv_ty"

   181 

   182 quotient_definition

   183    "fv_trm :: TRM \<Rightarrow> atom set"

   184 as

   185   "rfv_trm"

   186 

   187 thm akind_aty_atrm.induct

   188 lemma alpha_rfv:

   189   shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>

   190      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>

   191      (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"

   192   apply(rule akind_aty_atrm.induct)

   193   apply(simp_all)

   194   done

   195 

   196 lemma perm_rsp[quot_respect]:

   197   "(op = ===> akind ===> akind) permute permute"

   198   "(op = ===> aty ===> aty) permute permute"

   199   "(op = ===> atrm ===> atrm) permute permute"

   200 apply simp_all

   201 sorry (* by eqvt *)

   202 

   203 lemma kpi_rsp[quot_respect]: 

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

   205   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry

   206 lemma tconst_rsp[quot_respect]: 

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

   208   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   209 lemma tapp_rsp[quot_respect]: 

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

   211   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   212 lemma tpi_rsp[quot_respect]: 

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

   214   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry

   215 lemma var_rsp[quot_respect]: 

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

   217   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   218 lemma app_rsp[quot_respect]: 

   219   "(atrm ===> atrm ===> atrm) App App"

   220   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   221 lemma const_rsp[quot_respect]: 

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

   223   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   224 lemma lam_rsp[quot_respect]: 

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

   226   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry

   227 lemma rfv_ty_rsp[quot_respect]: 

   228   "(aty ===> op =) rfv_ty rfv_ty"

   229   by (simp add: alpha_rfv)

   230 lemma rfv_kind_rsp[quot_respect]:

   231   "(akind ===> op =) rfv_kind rfv_kind"

   232   by (simp add: alpha_rfv)

   233 lemma rfv_trm_rsp[quot_respect]:

   234   "(atrm ===> op =) rfv_trm rfv_trm"

   235   by (simp add: alpha_rfv)

   236 

   237 thm akind_aty_atrm.induct

   238 thm kind_ty_trm.induct

   239 

   240 lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);

   241  \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);

   242  \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);

   243  \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);

   244  \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>

   245 \<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"

   246 by (lifting kind_ty_trm.induct)

   247 

   248 instantiation KIND and TY and TRM :: pt

   249 begin

   250 

   251 quotient_definition

   252   "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"

   253 as

   254   "permute :: perm \<Rightarrow> kind \<Rightarrow> kind"

   255 

   256 quotient_definition

   257   "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"

   258 as

   259   "permute :: perm \<Rightarrow> ty \<Rightarrow> ty"

   260 

   261 quotient_definition

   262   "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"

   263 as

   264   "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"

   265 

   266 term "permute_TRM"

   267 thm permute_kind_permute_ty_permute_trm.simps

   268 lemma [simp]:

   269 shows "pi \<bullet> TYP = TYP"

   270 and   "pi \<bullet> (KPI t n k) = KPI (pi \<bullet> t) (pi \<bullet> n) (pi \<bullet> k)"

   271 and   "pi \<bullet> (TCONST i) = TCONST (pi \<bullet> i)"

   272 and   "pi \<bullet> (TAPP A M) = TAPP (pi \<bullet> A) (pi \<bullet> M)"

   273 and   "pi \<bullet> (TPI A x B) = TPI (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> B)"

   274 and   "pi \<bullet> (CONS i) = CONS (pi \<bullet> i)"

   275 and   "pi \<bullet> (VAR x) = VAR (pi \<bullet> x)"

   276 and   "pi \<bullet> (APP M N) = APP (pi \<bullet> M) (pi \<bullet> N)"

   277 and   "pi \<bullet> (LAM A x M) = LAM (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> M)"

   278 apply (lifting permute_kind_permute_ty_permute_trm.simps)

   279 done

   280 

   281 lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"

   282 apply (induct rule: KIND_TY_TRM_induct)

   283 apply simp_all

   284 done

   285 

   286 lemma perm_add_ok: "((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> (x1 :: KIND))) \<and> ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2) \<and> ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"

   287 apply(induct_tac [!] rule: KIND_TY_TRM_induct)

   288 apply (simp_all)

   289 (* Sth went wrong... *)

   290 sorry

   291 

   292 instance

   293 apply default

   294 apply (simp_all add: perm_zero_ok perm_add_ok)

   295 done

   296 

   297 end

   298 

   299 lemma "\<lbrakk>P10 TYP TYP;

   300  \<And>A A' K x K' x'.

   301     \<lbrakk>(A :: TY) = A'; P20 A A';

   302      \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>

   303           (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>

   304     \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');

   305  \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);

   306  \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');

   307  \<And>A A' B x B' x'.

   308     \<lbrakk>A = A'; P20 A A';

   309      \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>

   310           (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>

   311     \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');

   312  \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);

   313  \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');

   314  \<And>A A' M x M' x'.

   315     \<lbrakk>A = A'; P20 A A';

   316      \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>

   317           (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>

   318     \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>

   319 \<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and>

   320    (x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)"

   321 apply (lifting akind_aty_atrm.induct)

   322 done

   323 

   324 end

   325 

   326 

   327 

   328