Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/LFex.thy
changeset 992 74e9a580448c
parent 991 928e80edf138
child 993 5c0d9a507bcb
equal deleted inserted replaced
991:928e80edf138 992:74e9a580448c 
     1 theory LFex
 
     1 theory LFex
 
     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"
 
     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"  "Abs"
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 atom_decl name
 
     5 atom_decl name
 
     6 atom_decl ident
 
     6 atom_decl ident
 
     7 
     7 
     8 datatype kind = 
     8 datatype kind =
 
     9     Type
 
     9     Type
 
    10   | KPi "ty" "name" "kind"
 
    10   | KPi "ty" "name" "kind"
 
    11 and ty =  
    11 and ty =
 
    12     TConst "ident"
 
    12     TConst "ident"
 
    13   | TApp "ty" "trm"
 
    13   | TApp "ty" "trm"
 
    14   | TPi "ty" "name" "ty"
 
    14   | TPi "ty" "name" "ty"
 
    15 and trm = 
    15 and trm =
 
    16     Const "ident"
 
    16     Const "ident"
 
    17   | Var "name"
 
    17   | Var "name"
 
    18   | App "trm" "trm"
 
    18   | App "trm" "trm"
 
    19   | Lam "ty" "name" "trm" 
    19   | Lam "ty" "name" "trm"
 
    20 
    20 print_theorems
 
    21 fun
 
    21 
       
    22 primrec
 
    22     rfv_kind :: "kind \<Rightarrow> atom set"
 
    23     rfv_kind :: "kind \<Rightarrow> atom set"
 
    23 and rfv_ty   :: "ty \<Rightarrow> atom set"
 
    24 and rfv_ty   :: "ty \<Rightarrow> atom set"
 
    24 and rfv_trm  :: "trm \<Rightarrow> atom set"
 
    25 and rfv_trm  :: "trm \<Rightarrow> atom set"
 
    25 where
 
    26 where
 
    26   "rfv_kind (Type) = {}"
 
    27   "rfv_kind (Type) = {}"
 
    56 apply(simp_all)
 
    57 apply(simp_all)
 
    57 done
 
    58 done
 
    58 instance
 
    59 instance
 
    59 apply default
 
    60 apply default
 
    60 apply (simp_all only:rperm_zero_ok)
 
    61 apply (simp_all only:rperm_zero_ok)
 
    61 apply(induct_tac [!] x)
 
    62 apply(induct_tac[!] x)
 
    62 apply(simp_all)
 
    63 apply(simp_all)
 
    63 apply(induct_tac ty)
 
    64 apply(induct_tac ty)
 
    64 apply(simp_all)
 
    65 apply(simp_all)
 
    65 apply(induct_tac trm)
 
    66 apply(induct_tac trm)
 
    66 apply(simp_all)
 
    67 apply(simp_all)
 
   107 apply simp_all
 
   108 apply simp_all
 
   108 done
 
   109 done
 
   109 termination
 
   110 termination
 
   110 by (size_change)
 
   111 by (size_change)
 
   111 *)
 
   112 *)
 
       
   113 
       
   114 lemma akind_aty_artm_inj:
 
       
   115   "(Type) \<approx>ki (Type) = True"
 
       
   116   "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<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')))"
 
       
   117   "(TConst i) \<approx>ty (TConst j) = (i = j)"
 
       
   118   "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
 
       
   119   "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<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'))"
 
       
   120   "(Const i) \<approx>tr (Const j) = (i = j)"
 
       
   121   "(Var x) \<approx>tr (Var y) = (x = y)"
 
       
   122   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
 
       
   123   "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<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'))"
 
       
   124 apply -
 
       
   125 apply (simp add: akind_aty_atrm.intros)
 
       
   126 
       
   127 apply rule apply (erule akind.cases) apply simp apply blast
 
       
   128 apply (simp only: akind_aty_atrm.intros)
 
       
   129 
       
   130 apply rule apply (erule aty.cases) apply simp apply simp apply simp
 
       
   131 apply (simp only: akind_aty_atrm.intros)
 
       
   132 
       
   133 apply rule apply (erule aty.cases) apply simp apply simp apply simp
 
       
   134 apply (simp only: akind_aty_atrm.intros)
 
       
   135 
       
   136 apply rule apply (erule aty.cases) apply simp apply simp apply blast
 
       
   137 apply (simp only: akind_aty_atrm.intros)
 
       
   138 
       
   139 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
 
       
   140 apply (simp only: akind_aty_atrm.intros)
 
       
   141 
       
   142 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
 
       
   143 apply (simp only: akind_aty_atrm.intros)
 
       
   144 
       
   145 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
 
       
   146 apply (simp only: akind_aty_atrm.intros)
 
       
   147 
       
   148 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
 
       
   149 apply (simp only: akind_aty_atrm.intros)
 
       
   150 done
 
       
   151 
       
   152 (* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *)
 
       
   153 lemma rfv_eqvt_tmp:
 
       
   154   "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1)) \<and>
 
       
   155   ((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2)) \<and>
 
       
   156   ((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
 
       
   157 thm kind_ty_trm.induct
 
       
   158 (*apply(induct t1 t2 t3 rule: kind_ty_trm.inducts)*)
 
       
   159 apply(rule kind_ty_trm.induct[of
 
       
   160   "\<lambda>t1. ((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
 
       
   161   "\<lambda>t2. ((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
 
       
   162   "\<lambda>t3. ((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"])
 
       
   163 apply(simp_all add:  union_eqvt Diff_eqvt)
 
       
   164 apply(simp_all add: permute_set_eq atom_eqvt)
 
       
   165 done
 
       
   166 
       
   167 lemma rfv_eqvt[eqvt]:
 
       
   168   "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
 
       
   169   "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
 
       
   170   "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
 
       
   171 (*apply(induct t1 t2 t3 rule: kind_ty_trm.inducts)*)
 
       
   172 apply(simp_all only: rfv_eqvt_tmp)
 
       
   173 done
 
       
   174 
       
   175 lemma alpha_eqvt:
 
       
   176   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
 
       
   177   "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
 
       
   178   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
 
       
   179 apply(induct rule: akind_aty_atrm.inducts)
 
       
   180 apply (simp_all add: akind_aty_atrm.intros)
 
       
   181 apply(rule a2)
 
       
   182 apply simp
 
       
   183 apply(erule conjE)
 
       
   184 apply(erule exE)
 
       
   185 apply(erule conjE)
 
       
   186 apply(rule_tac x="pi \<bullet> pia" in exI)
 
       
   187 apply(rule conjI)
 
       
   188 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
 
       
   189 apply(simp add: eqvts atom_eqvt)
 
       
   190 apply(rule conjI)
 
       
   191 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
 
       
   192 apply(simp add: eqvts atom_eqvt)
 
       
   193 apply(simp add: permute_eqvt[symmetric])
 
       
   194 apply(rule a5)
 
       
   195 apply simp
 
       
   196 apply(erule conjE)
 
       
   197 apply(erule exE)
 
       
   198 apply(erule conjE)
 
       
   199 apply(rule_tac x="pi \<bullet> pia" in exI)
 
       
   200 apply(rule conjI)
 
       
   201 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
 
       
   202 apply(simp add: eqvts atom_eqvt)
 
       
   203 apply(rule conjI)
 
       
   204 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
 
       
   205 apply(simp add: eqvts atom_eqvt)
 
       
   206 apply(simp add: permute_eqvt[symmetric])
 
       
   207 apply(rule a9)
 
       
   208 apply simp
 
       
   209 apply(erule conjE)
 
       
   210 apply(erule exE)
 
       
   211 apply(erule conjE)
 
       
   212 apply(rule_tac x="pi \<bullet> pia" in exI)
 
       
   213 apply(rule conjI)
 
       
   214 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
 
       
   215 apply(simp add: eqvts atom_eqvt)
 
       
   216 apply(rule conjI)
 
       
   217 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
 
       
   218 apply(simp add: eqvts atom_eqvt)
 
       
   219 apply(simp add: permute_eqvt[symmetric])
 
       
   220 done
 
   112 
   221 
   113 lemma al_refl:
 
   222 lemma al_refl:
 
   114   fixes K::"kind" 
   223   fixes K::"kind" 
   115   and   A::"ty"
 
   224   and   A::"ty"
 
   116   and   M::"trm"
 
   225   and   M::"trm"
 
   207 quotient_definition
 
   316 quotient_definition
 
   208    "fv_trm :: TRM \<Rightarrow> atom set"
 
   317    "fv_trm :: TRM \<Rightarrow> atom set"
 
   209 as
 
   318 as
 
   210   "rfv_trm"
 
   319   "rfv_trm"
 
   211 
   320 
   212 thm akind_aty_atrm.induct
 
       
   213 lemma alpha_rfv:
 
   321 lemma alpha_rfv:
 
   214   shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
 
   322   shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
 
   215      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
 
   323      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
 
   216      (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
 
   324      (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
 
   217   apply(rule akind_aty_atrm.induct)
 
   325   apply(rule akind_aty_atrm.induct)
 
   220 
   328 
   221 lemma perm_rsp[quot_respect]:
 
   329 lemma perm_rsp[quot_respect]:
 
   222   "(op = ===> akind ===> akind) permute permute"
 
   330   "(op = ===> akind ===> akind) permute permute"
 
   223   "(op = ===> aty ===> aty) permute permute"
 
   331   "(op = ===> aty ===> aty) permute permute"
 
   224   "(op = ===> atrm ===> atrm) permute permute"
 
   332   "(op = ===> atrm ===> atrm) permute permute"
 
   225 apply simp_all
 
   333   by (simp_all add:alpha_eqvt)
 
   226 sorry (* by eqvt *)
 
   334 
   227 
       
   228 lemma kpi_rsp[quot_respect]: 
       
   229   "(aty ===> op = ===> akind ===> akind) KPi KPi"
 
       
   230   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 
       
   231 lemma tconst_rsp[quot_respect]: 
   335 lemma tconst_rsp[quot_respect]: 
   232   "(op = ===> aty) TConst TConst"
 
   336   "(op = ===> aty) TConst TConst"
 
   233   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   337   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   234 lemma tapp_rsp[quot_respect]: 
   338 lemma tapp_rsp[quot_respect]: 
   235   "(aty ===> atrm ===> aty) TApp TApp" 
   339   "(aty ===> atrm ===> aty) TApp TApp" 
   236   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   340   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   237 lemma tpi_rsp[quot_respect]: 
       
   238   "(aty ===> op = ===> aty ===> aty) TPi TPi"
 
       
   239   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 
       
   240 lemma var_rsp[quot_respect]: 
   341 lemma var_rsp[quot_respect]: 
   241   "(op = ===> atrm) Var Var"
 
   342   "(op = ===> atrm) Var Var"
 
   242   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   343   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   243 lemma app_rsp[quot_respect]: 
   344 lemma app_rsp[quot_respect]: 
   244   "(atrm ===> atrm ===> atrm) App App"
 
   345   "(atrm ===> atrm ===> atrm) App App"
 
   245   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   346   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   246 lemma const_rsp[quot_respect]: 
   347 lemma const_rsp[quot_respect]: 
   247   "(op = ===> atrm) Const Const"
 
   348   "(op = ===> atrm) Const Const"
 
   248   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   349   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
       
   350 
       
   351 lemma kpi_rsp[quot_respect]: 
       
   352   "(aty ===> op = ===> akind ===> akind) KPi KPi"
 
       
   353   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 
       
   354 lemma tpi_rsp[quot_respect]: 
       
   355   "(aty ===> op = ===> aty ===> aty) TPi TPi"
 
       
   356   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 
   249 lemma lam_rsp[quot_respect]: 
   357 lemma lam_rsp[quot_respect]: 
   250   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
 
   358   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
 
   251   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 
   359   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 
       
   360 
   252 lemma rfv_ty_rsp[quot_respect]: 
   361 lemma rfv_ty_rsp[quot_respect]: 
   253   "(aty ===> op =) rfv_ty rfv_ty"
 
   362   "(aty ===> op =) rfv_ty rfv_ty"
 
   254   by (simp add: alpha_rfv)
 
   363   by (simp add: alpha_rfv)
 
   255 lemma rfv_kind_rsp[quot_respect]:
 
   364 lemma rfv_kind_rsp[quot_respect]:
 
   256   "(akind ===> op =) rfv_kind rfv_kind"
 
   365   "(akind ===> op =) rfv_kind rfv_kind"
 
   257   by (simp add: alpha_rfv)
 
   366   by (simp add: alpha_rfv)
 
   258 lemma rfv_trm_rsp[quot_respect]:
 
   367 lemma rfv_trm_rsp[quot_respect]:
 
   259   "(atrm ===> op =) rfv_trm rfv_trm"
 
   368   "(atrm ===> op =) rfv_trm rfv_trm"
 
   260   by (simp add: alpha_rfv)
 
   369   by (simp add: alpha_rfv)
 
   261 
       
   262 thm akind_aty_atrm.induct
 
       
   263 thm kind_ty_trm.induct
 
       
   264 
   370 
   265 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);
 
   371 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);
 
   266  \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
 
   372  \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
 
   267  \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
 
   373  \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
 
   268  \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
 
   374  \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
nominal2