equal
deleted
inserted
replaced
799 that of @{term x} the property @{term "P y"} holds. *} |
799 that of @{term x} the property @{term "P y"} holds. *} |
800 |
800 |
801 lemma |
801 lemma |
802 shows trans: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" |
802 shows trans: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" |
803 and narrow: "(\<Delta>@[(X,Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>)\<turnstile>M<:N" |
803 and narrow: "(\<Delta>@[(X,Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>)\<turnstile>M<:N" |
804 proof (induct Q fixing: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule) |
804 proof (induct Q arbitrary: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule) |
805 case (less Q) |
805 case (less Q) |
806 --{* \begin{minipage}[t]{0.9\textwidth} |
806 --{* \begin{minipage}[t]{0.9\textwidth} |
807 First we mention the induction hypotheses of the outer induction for later |
807 First we mention the induction hypotheses of the outer induction for later |
808 reference:\end{minipage}*} |
808 reference:\end{minipage}*} |
809 have IH_trans: |
809 have IH_trans: |