src/HOL/Lambda/Eta.thy
author wenzelm
Sat Apr 08 22:51:06 2006 +0200 (2006-04-08)
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 19380 b808efaa5828
permissions -rw-r--r--
refined 'abbreviation';
     1 (*  Title:      HOL/Lambda/Eta.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Stefan Berghofer
     4     Copyright   1995, 2005 TU Muenchen
     5 *)
     6 
     7 header {* Eta-reduction *}
     8 
     9 theory Eta imports ParRed begin
    10 
    11 
    12 subsection {* Definition of eta-reduction and relatives *}
    13 
    14 consts
    15   free :: "dB => nat => bool"
    16 primrec
    17   "free (Var j) i = (j = i)"
    18   "free (s \<degree> t) i = (free s i \<or> free t i)"
    19   "free (Abs s) i = free s (i + 1)"
    20 
    21 consts
    22   eta :: "(dB \<times> dB) set"
    23 
    24 abbreviation
    25   eta_red :: "[dB, dB] => bool"   (infixl "-e>" 50)
    26   "s -e> t == (s, t) \<in> eta"
    27   eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50)
    28   "s -e>> t == (s, t) \<in> eta^*"
    29   eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50)
    30   "s -e>= t == (s, t) \<in> eta^="
    31 
    32 inductive eta
    33   intros
    34     eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) -e> s[dummy/0]"
    35     appL [simp, intro]: "s -e> t ==> s \<degree> u -e> t \<degree> u"
    36     appR [simp, intro]: "s -e> t ==> u \<degree> s -e> u \<degree> t"
    37     abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t"
    38 
    39 inductive_cases eta_cases [elim!]:
    40   "Abs s -e> z"
    41   "s \<degree> t -e> u"
    42   "Var i -e> t"
    43 
    44 
    45 subsection "Properties of eta, subst and free"
    46 
    47 lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
    48   by (induct s fixing: i t u) (simp_all add: subst_Var)
    49 
    50 lemma free_lift [simp]:
    51     "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
    52   apply (induct t fixing: i k)
    53     apply (auto cong: conj_cong)
    54   apply arith
    55   done
    56 
    57 lemma free_subst [simp]:
    58     "free (s[t/k]) i =
    59       (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
    60   apply (induct s fixing: i k t)
    61     prefer 2
    62     apply simp
    63     apply blast
    64    prefer 2
    65    apply simp
    66   apply (simp add: diff_Suc subst_Var split: nat.split)
    67   done
    68 
    69 lemma free_eta: "s -e> t ==> free t i = free s i"
    70   by (induct fixing: i set: eta) (simp_all cong: conj_cong)
    71 
    72 lemma not_free_eta:
    73     "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
    74   by (simp add: free_eta)
    75 
    76 lemma eta_subst [simp]:
    77     "s -e> t ==> s[u/i] -e> t[u/i]"
    78   by (induct fixing: u i set: eta) (simp_all add: subst_subst [symmetric])
    79 
    80 theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
    81   by (induct s fixing: i dummy) simp_all
    82 
    83 
    84 subsection "Confluence of eta"
    85 
    86 lemma square_eta: "square eta eta (eta^=) (eta^=)"
    87   apply (unfold square_def id_def)
    88   apply (rule impI [THEN allI [THEN allI]])
    89   apply simp
    90   apply (erule eta.induct)
    91      apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
    92     apply safe
    93        prefer 5
    94        apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
    95       apply blast+
    96   done
    97 
    98 theorem eta_confluent: "confluent eta"
    99   apply (rule square_eta [THEN square_reflcl_confluent])
   100   done
   101 
   102 
   103 subsection "Congruence rules for eta*"
   104 
   105 lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
   106   by (induct set: rtrancl)
   107     (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   108 
   109 lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t"
   110   by (induct set: rtrancl)
   111     (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   112 
   113 lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'"
   114   by (induct set: rtrancl) (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   115 
   116 lemma rtrancl_eta_App:
   117     "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'"
   118   by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
   119 
   120 
   121 subsection "Commutation of beta and eta"
   122 
   123 lemma free_beta:
   124     "s -> t ==> free t i \<Longrightarrow> free s i"
   125   by (induct fixing: i set: beta) auto
   126 
   127 lemma beta_subst [intro]: "s -> t ==> s[u/i] -> t[u/i]"
   128   by (induct fixing: u i set: beta) (simp_all add: subst_subst [symmetric])
   129 
   130 lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
   131   by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
   132 
   133 lemma eta_lift [simp]: "s -e> t ==> lift s i -e> lift t i"
   134   by (induct fixing: i set: eta) simp_all
   135 
   136 lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
   137   apply (induct u fixing: s t i)
   138     apply (simp_all add: subst_Var)
   139     apply blast
   140    apply (blast intro: rtrancl_eta_App)
   141   apply (blast intro!: rtrancl_eta_Abs eta_lift)
   142   done
   143 
   144 lemma square_beta_eta: "square beta eta (eta^*) (beta^=)"
   145   apply (unfold square_def)
   146   apply (rule impI [THEN allI [THEN allI]])
   147   apply (erule beta.induct)
   148      apply (slowsimp intro: rtrancl_eta_subst eta_subst)
   149     apply (blast intro: rtrancl_eta_AppL)
   150    apply (blast intro: rtrancl_eta_AppR)
   151   apply simp;
   152   apply (slowsimp intro: rtrancl_eta_Abs free_beta
   153     iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
   154   done
   155 
   156 lemma confluent_beta_eta: "confluent (beta \<union> eta)"
   157   apply (assumption |
   158     rule square_rtrancl_reflcl_commute confluent_Un
   159       beta_confluent eta_confluent square_beta_eta)+
   160   done
   161 
   162 
   163 subsection "Implicit definition of eta"
   164 
   165 text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *}
   166 
   167 lemma not_free_iff_lifted:
   168     "(\<not> free s i) = (\<exists>t. s = lift t i)"
   169   apply (induct s fixing: i)
   170     apply simp
   171     apply (rule iffI)
   172      apply (erule linorder_neqE)
   173       apply (rule_tac x = "Var nat" in exI)
   174       apply simp
   175      apply (rule_tac x = "Var (nat - 1)" in exI)
   176      apply simp
   177     apply clarify
   178     apply (rule notE)
   179      prefer 2
   180      apply assumption
   181     apply (erule thin_rl)
   182     apply (case_tac t)
   183       apply simp
   184      apply simp
   185     apply simp
   186    apply simp
   187    apply (erule thin_rl)
   188    apply (erule thin_rl)
   189    apply (rule iffI)
   190     apply (elim conjE exE)
   191     apply (rename_tac u1 u2)
   192     apply (rule_tac x = "u1 \<degree> u2" in exI)
   193     apply simp
   194    apply (erule exE)
   195    apply (erule rev_mp)
   196    apply (case_tac t)
   197      apply simp
   198     apply simp
   199     apply blast
   200    apply simp
   201   apply simp
   202   apply (erule thin_rl)
   203   apply (rule iffI)
   204    apply (erule exE)
   205    apply (rule_tac x = "Abs t" in exI)
   206    apply simp
   207   apply (erule exE)
   208   apply (erule rev_mp)
   209   apply (case_tac t)
   210     apply simp
   211    apply simp
   212   apply simp
   213   apply blast
   214   done
   215 
   216 theorem explicit_is_implicit:
   217   "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
   218     (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
   219   by (auto simp add: not_free_iff_lifted)
   220 
   221 
   222 subsection {* Parallel eta-reduction *}
   223 
   224 consts
   225   par_eta :: "(dB \<times> dB) set"
   226 
   227 abbreviation
   228   par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
   229   "s =e> t == (s, t) \<in> par_eta"
   230 
   231 abbreviation (xsymbols)
   232   par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
   233   "op \<Rightarrow>\<^sub>\<eta> == op =e>"
   234 
   235 inductive par_eta
   236 intros
   237   var [simp, intro]: "Var x \<Rightarrow>\<^sub>\<eta> Var x"
   238   eta [simp, intro]: "\<not> free s 0 \<Longrightarrow> s \<Rightarrow>\<^sub>\<eta> s'\<Longrightarrow> Abs (s \<degree> Var 0) \<Rightarrow>\<^sub>\<eta> s'[dummy/0]"
   239   app [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> s' \<Longrightarrow> t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> s \<degree> t \<Rightarrow>\<^sub>\<eta> s' \<degree> t'"
   240   abs [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> Abs s \<Rightarrow>\<^sub>\<eta> Abs t"
   241 
   242 lemma free_par_eta [simp]:
   243   assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   244   shows "free t i = free s i" using eta
   245   by (induct fixing: i) (simp_all cong: conj_cong)
   246 
   247 lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t"
   248   by (induct t) simp_all
   249 
   250 lemma par_eta_lift [simp]:
   251   assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   252   shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
   253   by (induct fixing: i) simp_all
   254 
   255 lemma par_eta_subst [simp]:
   256   assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   257   shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
   258   by (induct fixing: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
   259 
   260 theorem eta_subset_par_eta: "eta \<subseteq> par_eta"
   261   apply (rule subsetI)
   262   apply clarify
   263   apply (erule eta.induct)
   264   apply (blast intro!: par_eta_refl)+
   265   done
   266 
   267 theorem par_eta_subset_eta: "par_eta \<subseteq> eta\<^sup>*"
   268   apply (rule subsetI)
   269   apply clarify
   270   apply (erule par_eta.induct)
   271   apply blast
   272   apply (rule rtrancl_into_rtrancl)
   273   apply (rule rtrancl_eta_Abs)
   274   apply (rule rtrancl_eta_AppL)
   275   apply assumption
   276   apply (rule eta.eta)
   277   apply simp
   278   apply (rule rtrancl_eta_App)
   279   apply assumption+
   280   apply (rule rtrancl_eta_Abs)
   281   apply assumption
   282   done
   283 
   284 
   285 subsection {* n-ary eta-expansion *}
   286 
   287 consts eta_expand :: "nat \<Rightarrow> dB \<Rightarrow> dB"
   288 primrec
   289   eta_expand_0: "eta_expand 0 t = t"
   290   eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 \<degree> Var 0)"
   291 
   292 lemma eta_expand_Suc':
   293   "eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
   294   by (induct n fixing: t) simp_all
   295 
   296 theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)"
   297   by (induct k) (simp_all add: lift_lift)
   298 
   299 theorem eta_expand_beta:
   300   assumes u: "u => u'"
   301   shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
   302 proof (induct k fixing: t t')
   303   case 0 with u show ?case by simp
   304 next
   305   case (Suc k)
   306   hence "Abs (lift t (Suc 0)) \<degree> Var 0 => lift t' (Suc 0)[Var 0/0]"
   307     by (blast intro: par_beta_lift)
   308   with Suc show ?case by (simp del: eta_expand_Suc add: eta_expand_Suc')
   309 qed
   310 
   311 theorem eta_expand_red:
   312   assumes t: "t => t'"
   313   shows "eta_expand k t => eta_expand k t'"
   314   by (induct k) (simp_all add: t)
   315 
   316 theorem eta_expand_eta: "t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
   317 proof (induct k fixing: t t')
   318   case 0
   319   show ?case by simp
   320 next
   321   case (Suc k)
   322   have "Abs (lift (eta_expand k t) 0 \<degree> Var 0) \<Rightarrow>\<^sub>\<eta> lift t' 0[arbitrary/0]"
   323     by (fastsimp intro: par_eta_lift Suc)
   324   thus ?case by simp
   325 qed
   326 
   327 
   328 subsection {* Elimination rules for parallel eta reduction *}
   329 
   330 theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u"
   331   shows "u = u1' \<degree> u2' \<Longrightarrow>
   332     \<exists>u1 u2 k. t = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2'" using eta
   333 proof (induct fixing: u1' u2')
   334   case (app s s' t t')
   335   have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp
   336   with app show ?case by blast
   337 next
   338   case (eta dummy s s')
   339   then obtain u1'' u2'' where s': "s' = u1'' \<degree> u2''"
   340     by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
   341   then have "\<exists>u1 u2 k. s = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1'' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2''" by (rule eta)
   342   then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)"
   343     and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by iprover
   344   from u1 u2 eta s' have "\<not> free u1 0" and "\<not> free u2 0"
   345     by (simp_all del: free_par_eta add: free_par_eta [symmetric])
   346   with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (u1[dummy/0] \<degree> u2[dummy/0])"
   347     by (simp del: lift_subst add: lift_subst_dummy lift_eta_expand)
   348   moreover from u1 par_eta_refl have "u1[dummy/0] \<Rightarrow>\<^sub>\<eta> u1''[dummy/0]"
   349     by (rule par_eta_subst)
   350   moreover from u2 par_eta_refl have "u2[dummy/0] \<Rightarrow>\<^sub>\<eta> u2''[dummy/0]"
   351     by (rule par_eta_subst)
   352   ultimately show ?case using eta s'
   353     by (simp only: subst.simps dB.simps) blast
   354 next
   355   case var thus ?case by simp
   356 next
   357   case abs thus ?case by simp
   358 qed
   359 
   360 theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'"
   361   shows "t' = Abs u' \<Longrightarrow>
   362     \<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta
   363 proof (induct fixing: u')
   364   case (abs s t)
   365   have "Abs s = eta_expand 0 (Abs s)" by simp
   366   with abs show ?case by blast
   367 next
   368   case (eta dummy s s')
   369   then obtain u'' where s': "s' = Abs u''"
   370     by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
   371   then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta)
   372   then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by iprover
   373   from eta u s' have "\<not> free u (Suc 0)"
   374     by (simp del: free_par_eta add: free_par_eta [symmetric])
   375   with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))"
   376     by (simp del: lift_subst add: lift_eta_expand lift_subst_dummy)
   377   moreover from u par_eta_refl have "u[lift dummy 0/Suc 0] \<Rightarrow>\<^sub>\<eta> u''[lift dummy 0/Suc 0]"
   378     by (rule par_eta_subst)
   379   ultimately show ?case using eta s' by fastsimp
   380 next
   381   case var thus ?case by simp
   382 next
   383   case app thus ?case by simp
   384 qed
   385 
   386 
   387 subsection {* Eta-postponement theorem *}
   388 
   389 text {*
   390 Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
   391 *}
   392 
   393 theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
   394 proof (induct t fixing: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule)
   395   case (less t)
   396   from `t => u`
   397   show ?case
   398   proof cases
   399     case (var n)
   400     with less show ?thesis
   401       by (auto intro: par_beta_refl)
   402   next
   403     case (abs r' r'')
   404     with less have "s \<Rightarrow>\<^sub>\<eta> Abs r'" by simp
   405     then obtain r k where s: "s = eta_expand k (Abs r)" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
   406       by (blast dest: par_eta_elim_abs)
   407     from abs have "size r' < size t" by simp
   408     with abs(2) rr obtain t' where rt: "r => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> r''"
   409       by (blast dest: less(1))
   410     with s abs show ?thesis
   411       by (auto intro: eta_expand_red eta_expand_eta)
   412   next
   413     case (app q' q'' r' r'')
   414     with less have "s \<Rightarrow>\<^sub>\<eta> q' \<degree> r'" by simp
   415     then obtain q r k where s: "s = eta_expand k (q \<degree> r)"
   416       and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
   417       by (blast dest: par_eta_elim_app [OF _ refl])
   418     from app have "size q' < size t" and "size r' < size t" by simp_all
   419     with app(2,3) qq rr obtain t' t'' where "q => t'" and
   420       "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
   421       by (blast dest: less(1))
   422     with s app show ?thesis
   423       by (fastsimp intro: eta_expand_red eta_expand_eta)
   424   next
   425     case (beta q' q'' r' r'')
   426     with less have "s \<Rightarrow>\<^sub>\<eta> Abs q' \<degree> r'" by simp
   427     then obtain q r k k' where s: "s = eta_expand k (eta_expand k' (Abs q) \<degree> r)"
   428       and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
   429       by (blast dest: par_eta_elim_app par_eta_elim_abs)
   430     from beta have "size q' < size t" and "size r' < size t" by simp_all
   431     with beta(2,3) qq rr obtain t' t'' where "q => t'" and
   432       "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
   433       by (blast dest: less(1))
   434     with s beta show ?thesis
   435       by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst)
   436   qed
   437 qed
   438 
   439 theorem eta_postponement': assumes eta: "s -e>> t"
   440   shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
   441   using eta [simplified rtrancl_subset
   442     [OF eta_subset_par_eta par_eta_subset_eta, symmetric]]
   443 proof (induct fixing: u)
   444   case 1
   445   thus ?case by blast
   446 next
   447   case (2 s' s'' s''')
   448   from 2 obtain t' where s': "s' => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> s'''"
   449     by (auto dest: par_eta_beta)
   450   from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'" using 2
   451     by blast
   452   from par_eta_subset_eta t' have "t' -e>> s'''" ..
   453   with t'' have "t'' -e>> s'''" by (rule rtrancl_trans)
   454   with s show ?case by iprover
   455 qed
   456 
   457 theorem eta_postponement:
   458   assumes st: "(s, t) \<in> (beta \<union> eta)\<^sup>*"
   459   shows "(s, t) \<in> eta\<^sup>* O beta\<^sup>*" using st
   460 proof induct
   461   case 1
   462   show ?case by blast
   463 next
   464   case (2 s' s'')
   465   from 2(3) obtain t' where s: "s \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and t': "t' -e>> s'" by blast
   466   from 2(2) show ?case
   467   proof
   468     assume "s' -> s''"
   469     with beta_subset_par_beta have "s' => s''" ..
   470     with t' obtain t'' where st: "t' => t''" and tu: "t'' -e>> s''"
   471       by (auto dest: eta_postponement')
   472     from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" ..
   473     with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtrancl_trans)
   474     thus ?thesis using tu ..
   475   next
   476     assume "s' -e> s''"
   477     with t' have "t' -e>> s''" ..
   478     with s show ?thesis ..
   479   qed
   480 qed
   481 
   482 end