2295   The remaining difficulty is when a deep binder contains atoms that are bound, but

  2295   The remaining difficulty is when a deep binder contains atoms that are

  2296   also that are free.

  2296   bound, but also atoms that are free. An example is @{text "Let\<^sup>\<alpha>"} in \eqref{}.

  2297 

  2297   Then @{text "(\<pi> \<bullet> x\<^isub>1)

  2298 

  2298   \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. In such

  2299   to the whole term @{text "Let_pat x\<^isub>1 x\<^isub>2 x\<^isub>3"},

  2299   cases, however, we only want to rename binders that will become bound, which

  2300   because @{text p} might contain names bound by @{text bn}, but also some that are 

  2300   does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. The problem is that the

  2301   free. To solve this problem we have to introduce a permutation function that only

  2301   permutation operation @{text "\<bullet>"} permutes all of them. The remedy is to

  2302   permutes names bound by @{text bn} and leaves the other names unchanged. We do this again

  2302   introduce an auxiliary permutation operation, written @{text "_

  2303   by lifting. For a

  2303   \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permute bound atoms and

  2304   clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 

  2304   leaves the other atoms unchanged. Like the @{text

  2305 

  2305   "fa_bn"}$_{1..m}$-functions, we can define this operation over raw terms

  2306 

  2306   analysing how the @{text "bn"}$_{1..m}$-functions are defined and then lift

  2307   {\bf NOT DONE YET}

  2307   them to alpha-equivalent terms. Assuming the user specified a clause

  2308 

  2308 

  2309   {\it 

  2309   \[  

  2310   

  2310   @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}

  2311   The only remaining difficulty is that in order to derive the stronger induction

  2311   \]\smallskip

  2312   principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that

  2312 

  2313   in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and 

  2313   \noindent

  2314   \emph{all} @{text Let}-terms. 

  2314   we define @{text "\<pi> \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} with @{text "y\<^isub>i"} determined as follows:

  2315   What we need instead is a cases lemma where we only have to consider terms that have 

  2315 

  2316   binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications

  2316   \[\mbox{

  2317 

  2318   

  2319   

  2320   \begin{center}

  2321   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}  with

  2322   $\begin{cases}

  2323   \text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\

  2324   \text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\

  2325   \text{@{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise}  

  2326   \end{cases}$

  2327   \end{center}

  2328   

  2329   \noindent

  2330   with @{text "y\<^isub>i"} determined as follows:

  2331   

  2332   \begin{center}

  2335   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\

  2319   $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\

  2336   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise

  2320   $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet> x\<^isub>i"} otherwise

  2337   \end{tabular}

  2321   \end{tabular}}

  2338   \end{center}

  2322   \]\smallskip

  2339   

  2323 

  2340   \noindent

  2324   \noindent

  2341   Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that

  2325   Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} functions to 

  2342   @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}

  2326   alpha-equated terms. Moreover we can prove the following two properties

  2343   is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. 

  2344   These facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This

  2345   completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction

  2346   principle.

  2347   

  2348 

  2349   Given a binding function @{text "bn"} we define an auxiliary permutation 

  2350   operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.

  2351   Assuming a clause of @{text bn} is given as 

  2352   

  2353   \begin{center}

  2354   @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, 

  2355   \end{center}

  2356 

  2357   \noindent 

  2358   then we define 

  2359   

  2360   \begin{center}

  2361   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 

  2362   \end{center}

  2363   

  2364   \noindent

  2365   with @{text "y\<^isub>i"} determined as follows:

  2366   

  2367   \begin{center}

  2368   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}

  2369   $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\

  2370   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\

  2371   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise

  2372   \end{tabular}

  2373   \end{center}

  2374   

  2375   \noindent

  2376   Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 

  2377   alpha-equated terms. We can then prove the following two facts

  2380   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}

  2329   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text "\<pi>"}\\

  2381   {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}

  2330   {\it (i)} @{text "\<pi> \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and\\ 

  2382     @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.

  2331   {\it (ii)} @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x) \<approx>\<AL>\<^bsub>bn\<^esub> x"}.

  2386   By induction on @{text x}. The equations follow by simple unfolding 

  2335   By induction on @{text x}. The properties follow by simple unfolding 

  2393   atoms. The second amounts to the fact that permuting the binders has no 

  2342   atoms. The main point of the auxiliary permutation

  2394   effect on the free-atom function. The main point of this permutation

  2343   functions is that it allows us to rename just the binders in a term,  

  2395   function, however, is that if we have a permutation that is fresh 

  2344   without changing anything else. 

  2396   for the support of an object @{text x}, then we can use this permutation 

  2345   

  2397   to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the 

  2346   Having the auxiliary permutation function in place, we can now solve all remaining cases. 

  2398   @{text "Let"} term-constructor from the example shown 

  2347   For @{text "Let\<^sup>\<alpha>"} term-constructor, for example, we can by Property \ref{avoiding} 

  2399   in \eqref{letpat} this means for a permutation @{text "r"}

  2348   obtain a @{text "\<pi>"} such that 

  2400   

  2349 

  2401   \begin{equation}\label{renaming}

  2350   \[

  2402   \begin{array}{l}

  2351   @{text "(\<pi> \<bullet> (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c"} \hspace{10mm}

  2403   \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 

  2352   @{text "\<pi> \<bullet> [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2 = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"} 

  2404   \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}

  2353   \]\smallskip

  2405   \end{array}

  2354 

  2406   \end{equation}

  2355   \noindent

  2407 

  2356   hold. Using Lemma \ref{permutebn}{\it (i)} we can simplify this

  2408   \noindent

  2357   to @{text "set (bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and 

  2409   This fact will be crucial when establishing the strong induction principles below.

  2358   @{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since

  2410 

  2359   @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by Lemma \ref{permutebn}{\it (ii)}

  2411  

  2360   we can infer that

  2361 

  2362   \[

  2363   @{text "Let\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}  

  2364   \]\smallskip

  2365 

  2366   \noindent

  2367   are alpha-equivalent. This allows us to use the implication from the strong cases

  2368   lemma and we can discharge all proof-obligations to do with having covered all

  2369   cases.

  2414   the strong induction principles. 

  2372   the strong induction principles. We have automated the reasoning for all

  2415   }

  2373   term-calculi the user might specify. The feature of the function package

  2374   by Krauss \cite{Krauss09} that allows us to establish an induction principle

  2375   by just finding decreasing measures and showing that the induction principle

  2376   covers all cases, tremendously helped us in implementing the automation.