177 

   177 

   178 quotient_def 

   178 quotient_def 

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

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

   180 where

   180 where

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

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

   182 

   184 

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

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

   184 lemma kpi_rsp[quotient_rsp]: 

   186 lemma kpi_rsp[quotient_rsp]: 

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

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

   186 lemma tconst_rsp[quotient_rsp]: 

   188 lemma tconst_rsp[quotient_rsp]: 

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

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

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

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

   299 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})

   301 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})

   300 done

   302 done

   301 

   303 

   304 end

   304 end

   305 

   305 

   306 

   306 

   307 

   307