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 1236 ca3c69545a78
parent 1234 1240d5eb275d
child 1237 38eb2bd9ad3a
equal deleted inserted replaced
1235:2daa5549579e 1236:ca3c69545a78 
    90      @{thms alphas_eqvt} ctxt)) ctxt)) *}
 
    90      @{thms alphas_eqvt} ctxt)) ctxt)) *}
 
    91 thm alphas_equivp
 
    91 thm alphas_equivp
 
    92 *)
 
    92 *)
 
    93 
    93 
    94 primrec
 
    94 primrec
 
    95     rfv_rkind :: "rkind \<Rightarrow> atom set"
 
    95     fv_rkind :: "rkind \<Rightarrow> atom set"
 
    96 and rfv_rty   :: "rty \<Rightarrow> atom set"
 
    96 and fv_rty   :: "rty \<Rightarrow> atom set"
 
    97 and rfv_rtrm  :: "rtrm \<Rightarrow> atom set"
 
    97 and fv_rtrm  :: "rtrm \<Rightarrow> atom set"
 
    98 where
 
    98 where
 
    99   "rfv_rkind (Type) = {}"
 
    99   "fv_rkind (Type) = {}"
 
   100 | "rfv_rkind (KPi A x K) = (rfv_rty A) \<union> ((rfv_rkind K) - {atom x})"
 
   100 | "fv_rkind (KPi A x K) = (fv_rty A) \<union> ((fv_rkind K) - {atom x})"
 
   101 | "rfv_rty (TConst i) = {atom i}"
 
   101 | "fv_rty (TConst i) = {atom i}"
 
   102 | "rfv_rty (TApp A M) = (rfv_rty A) \<union> (rfv_rtrm M)"
 
   102 | "fv_rty (TApp A M) = (fv_rty A) \<union> (fv_rtrm M)"
 
   103 | "rfv_rty (TPi A x B) = (rfv_rty A) \<union> ((rfv_rty B) - {atom x})"
 
   103 | "fv_rty (TPi A x B) = (fv_rty A) \<union> ((fv_rty B) - {atom x})"
 
   104 | "rfv_rtrm (Const i) = {atom i}"
 
   104 | "fv_rtrm (Const i) = {atom i}"
 
   105 | "rfv_rtrm (Var x) = {atom x}"
 
   105 | "fv_rtrm (Var x) = {atom x}"
 
   106 | "rfv_rtrm (App M N) = (rfv_rtrm M) \<union> (rfv_rtrm N)"
 
   106 | "fv_rtrm (App M N) = (fv_rtrm M) \<union> (fv_rtrm N)"
 
   107 | "rfv_rtrm (Lam A x M) = (rfv_rty A) \<union> ((rfv_rtrm M) - {atom x})"
 
   107 | "fv_rtrm (Lam A x M) = (fv_rty A) \<union> ((fv_rtrm M) - {atom x})"
 
   108 
   108 
   109 inductive
 
   109 inductive
 
   110     arkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
 
   110     arkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
 
   111 and arty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>rty _" [100, 100] 100)
 
   111 and arty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>rty _" [100, 100] 100)
 
   112 and artrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 
   112 and artrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 
   113 where
 
   113 where
 
   114   a1: "(Type) \<approx>ki (Type)"
 
   114   a1: "(Type) \<approx>ki (Type)"
 
   115 | a2: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, K) \<approx>gen arkind rfv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
 
   115 | a2: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, K) \<approx>gen arkind fv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
 
   116 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>rty (TConst j)"
 
   116 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>rty (TConst j)"
 
   117 | a4: "\<lbrakk>A \<approx>rty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>rty (TApp A' M')"
 
   117 | a4: "\<lbrakk>A \<approx>rty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>rty (TApp A' M')"
 
   118 | a5: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, B) \<approx>gen arty rfv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>rty (TPi A' b B')"
 
   118 | a5: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, B) \<approx>gen arty fv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>rty (TPi A' b B')"
 
   119 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 
   119 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 
   120 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 
   120 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 
   121 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
 
   121 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
 
   122 | a9: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, M) \<approx>gen artrm rfv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
   122 | a9: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, M) \<approx>gen artrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
   123 
   123 
   124 lemma arkind_arty_artrm_inj:
 
   124 lemma arkind_arty_artrm_inj:
 
   125   "(Type) \<approx>ki (Type) = True"
 
   125   "(Type) \<approx>ki (Type) = True"
 
   126   "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>rty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen arkind rfv_rkind pi ({atom b}, K')))"
 
   126   "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>rty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen arkind fv_rkind pi ({atom b}, K')))"
 
   127   "(TConst i) \<approx>rty (TConst j) = (i = j)"
 
   127   "(TConst i) \<approx>rty (TConst j) = (i = j)"
 
   128   "(TApp A M) \<approx>rty (TApp A' M') = (A \<approx>rty A' \<and> M \<approx>tr M')"
 
   128   "(TApp A M) \<approx>rty (TApp A' M') = (A \<approx>rty A' \<and> M \<approx>tr M')"
 
   129   "((TPi A a B) \<approx>rty (TPi A' b B')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen arty rfv_rty pi ({atom b}, B'))))"
 
   129   "((TPi A a B) \<approx>rty (TPi A' b B')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen arty fv_rty pi ({atom b}, B'))))"
 
   130   "(Const i) \<approx>tr (Const j) = (i = j)"
 
   130   "(Const i) \<approx>tr (Const j) = (i = j)"
 
   131   "(Var x) \<approx>tr (Var y) = (x = y)"
 
   131   "(Var x) \<approx>tr (Var y) = (x = y)"
 
   132   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
 
   132   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
 
   133   "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen artrm rfv_rtrm pi ({atom b}, M'))))"
 
   133   "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen artrm fv_rtrm pi ({atom b}, M'))))"
 
   134 apply -
 
   134 apply -
 
   135 apply (simp add: arkind_arty_artrm.intros)
 
   135 apply (simp add: arkind_arty_artrm.intros)
 
   136 
   136 
   137 apply rule apply (erule arkind.cases) apply simp apply blast
 
   137 apply rule apply (erule arkind.cases) apply simp apply blast
 
   138 apply (simp only: arkind_arty_artrm.intros)
 
   138 apply (simp only: arkind_arty_artrm.intros)
 
   158 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
 
   158 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
 
   159 apply (simp only: arkind_arty_artrm.intros)
 
   159 apply (simp only: arkind_arty_artrm.intros)
 
   160 done
 
   160 done
 
   161 
   161 
   162 lemma rfv_eqvt[eqvt]:
 
   162 lemma rfv_eqvt[eqvt]:
 
   163   "((pi\<bullet>rfv_rkind t1) = rfv_rkind (pi\<bullet>t1))"
 
   163   "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
 
   164   "((pi\<bullet>rfv_rty t2) = rfv_rty (pi\<bullet>t2))"
 
   164   "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
 
   165   "((pi\<bullet>rfv_rtrm t3) = rfv_rtrm (pi\<bullet>t3))"
 
   165   "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))"
 
   166 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)
 
   166 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)
 
   167 apply(simp_all add:  union_eqvt Diff_eqvt)
 
   167 apply(simp_all add:  union_eqvt Diff_eqvt)
 
   168 apply(simp_all add: permute_set_eq atom_eqvt)
 
   168 apply(simp_all add: permute_set_eq atom_eqvt)
 
   169 done
 
   169 done
 
   170 
   170 
   329 is
 
   329 is
 
   330   "Lam"
 
   330   "Lam"
 
   331 
   331 
   332 (* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *)
 
   332 (* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *)
 
   333 quotient_definition
 
   333 quotient_definition
 
   334    "fv_rkind :: RKIND \<Rightarrow> atom set"
 
   334    "fv_kind :: RKIND \<Rightarrow> atom set"
 
   335 is
 
   335 is
 
   336   "rfv_rkind"
 
   336   "fv_rkind"
 
   337 
   337 
   338 quotient_definition
 
   338 quotient_definition
 
   339    "fv_rty :: RTY \<Rightarrow> atom set"
 
   339    "fv_ty :: RTY \<Rightarrow> atom set"
 
   340 is
 
   340 is
 
   341   "rfv_rty"
 
   341   "fv_rty"
 
   342 
   342 
   343 quotient_definition
 
   343 quotient_definition
 
   344    "fv_rtrm :: RTRM \<Rightarrow> atom set"
 
   344    "fv_trm :: RTRM \<Rightarrow> atom set"
 
   345 is
 
   345 is
 
   346   "rfv_rtrm"
 
   346   "fv_rtrm"
 
   347 
   347 
   348 lemma alpha_rfv:
 
   348 lemma alpha_rfv:
 
   349   shows "(t \<approx>ki s \<longrightarrow> rfv_rkind t = rfv_rkind s) \<and>
 
   349   shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and>
 
   350      (t1 \<approx>rty s1 \<longrightarrow> rfv_rty t1 = rfv_rty s1) \<and>
 
   350      (t1 \<approx>rty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and>
 
   351      (t2 \<approx>tr s2 \<longrightarrow> rfv_rtrm t2 = rfv_rtrm s2)"
 
   351      (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)"
 
   352   apply(rule arkind_arty_artrm.induct)
 
   352   apply(rule arkind_arty_artrm.induct)
 
   353   apply(simp_all add: alpha_gen)
 
   353   apply(simp_all add: alpha_gen)
 
   354   done
 
   354   done
 
   355 
   355 
   356 lemma perm_rsp[quot_respect]:
 
   356 lemma perm_rsp[quot_respect]:
 
   396   apply (rule a9) apply assumption
 
   396   apply (rule a9) apply assumption
 
   397   apply (rule_tac x="0" in exI)
 
   397   apply (rule_tac x="0" in exI)
 
   398   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   398   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   399   done
 
   399   done
 
   400 
   400 
   401 lemma rfv_rty_rsp[quot_respect]: 
   401 lemma fv_rty_rsp[quot_respect]: 
   402   "(arty ===> op =) rfv_rty rfv_rty"
 
   402   "(arty ===> op =) fv_rty fv_rty"
 
   403   by (simp add: alpha_rfv)
 
   403   by (simp add: alpha_rfv)
 
   404 lemma rfv_rkind_rsp[quot_respect]:
 
   404 lemma fv_rkind_rsp[quot_respect]:
 
   405   "(arkind ===> op =) rfv_rkind rfv_rkind"
 
   405   "(arkind ===> op =) fv_rkind fv_rkind"
 
   406   by (simp add: alpha_rfv)
 
   406   by (simp add: alpha_rfv)
 
   407 lemma rfv_rtrm_rsp[quot_respect]:
 
   407 lemma fv_rtrm_rsp[quot_respect]:
 
   408   "(artrm ===> op =) rfv_rtrm rfv_rtrm"
 
   408   "(artrm ===> op =) fv_rtrm fv_rtrm"
 
   409   by (simp add: alpha_rfv)
 
   409   by (simp add: alpha_rfv)
 
   410 
   410 
   411 thm rkind_rty_rtrm.induct
 
   411 thm rkind_rty_rtrm.induct
 
   412 lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted]
 
   412 lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted]
 
   413 
   413 
   456 
   456 
   457 lemmas ARKIND_ARTY_ARTRM_inducts = arkind_arty_artrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
   457 lemmas ARKIND_ARTY_ARTRM_inducts = arkind_arty_artrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
   458 
   458 
   459 lemmas RKIND_RTY_RTRM_INJECT = arkind_arty_artrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
   459 lemmas RKIND_RTY_RTRM_INJECT = arkind_arty_artrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
   460 
   460 
   461 lemmas fv_rkind_rty_rtrm = rfv_rkind_rfv_rty_rfv_rtrm.simps[quot_lifted]
 
   461 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
 
   462 
   462 
   463 lemmas fv_eqvt = rfv_eqvt[quot_lifted]
 
   463 lemmas fv_eqvt = rfv_eqvt[quot_lifted]
 
   464 
   464 
   465 lemma supp_rkind_rty_rtrm_easy:
 
   465 lemma supp_rkind_rty_rtrm_easy:
 
   466  "supp TYP = {}"
 
   466  "supp TYP = {}"
 
   513 apply(default)
 
   513 apply(default)
 
   514 apply(simp_all only: RKIND_RTY_RTRM_fs)
 
   514 apply(simp_all only: RKIND_RTY_RTRM_fs)
 
   515 done
 
   515 done
 
   516 
   516 
   517 lemma supp_fv:
 
   517 lemma supp_fv:
 
   518  "supp t1 = fv_rkind t1"
 
   518  "supp t1 = fv_kind t1"
 
   519  "supp t2 = fv_rty t2"
 
   519  "supp t2 = fv_ty t2"
 
   520  "supp t3 = fv_rtrm t3"
 
   520  "supp t3 = fv_trm t3"
 
   521 apply(induct t1 and t2 and t3 rule: RKIND_RTY_RTRM_inducts)
 
   521 apply(induct t1 and t2 and t3 rule: RKIND_RTY_RTRM_inducts)
 
   522 apply (simp_all add: supp_rkind_rty_rtrm_easy)
 
   522 apply (simp_all add: supp_rkind_rty_rtrm_easy)
 
   523 apply (simp_all add: fv_rkind_rty_rtrm)
 
   523 apply (simp_all add: fv_kind_ty_trm)
 
   524 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")
 
   524 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")
 
   525 apply(simp add: supp_Abs Set.Un_commute)
 
   525 apply(simp add: supp_Abs Set.Un_commute)
 
   526 apply(simp (no_asm) add: supp_def)
 
   526 apply(simp (no_asm) add: supp_def)
 
   527 apply(simp add: RKIND_RTY_RTRM_INJECT)
 
   527 apply(simp add: RKIND_RTY_RTRM_INJECT)
 
   528 apply(simp add: Abs_eq_iff)
 
   528 apply(simp add: Abs_eq_iff)
 
   563  "supp (CONS i) = {atom i}"
 
   563  "supp (CONS i) = {atom i}"
 
   564  "supp (VAR x) = {atom x}"
 
   564  "supp (VAR x) = {atom x}"
 
   565  "supp (APP M N) = supp M \<union> supp N"
 
   565  "supp (APP M N) = supp M \<union> supp N"
 
   566  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
 
   566  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
 
   567 apply (simp_all only: supp_rkind_rty_rtrm_easy)
 
   567 apply (simp_all only: supp_rkind_rty_rtrm_easy)
 
   568 apply (simp_all only: supp_fv fv_rkind_rty_rtrm)
 
   568 apply (simp_all only: supp_fv fv_kind_ty_trm)
 
   569 done
 
   569 done
 
   570 
   570 
   571 end
 
   571 end
 
   572 
   572 
   573 
   573
nominal2