3 imports "../Nominal/Test" "LaTeXsugar" |
3 imports "../Nominal/Test" "LaTeXsugar" |
4 begin |
4 begin |
5 |
5 |
6 consts |
6 consts |
7 fv :: "'a \<Rightarrow> 'b" |
7 fv :: "'a \<Rightarrow> 'b" |
8 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |
8 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |
|
9 alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
9 |
10 |
10 definition |
11 definition |
11 "equal \<equiv> (op =)" |
12 "equal \<equiv> (op =)" |
12 |
13 |
13 notation (latex output) |
14 notation (latex output) |
26 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
27 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
27 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and |
28 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and |
28 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and |
29 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and |
29 Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and |
30 Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and |
30 Cons ("_::_" [78,77] 73) and |
31 Cons ("_::_" [78,77] 73) and |
31 supp_gen ("aux _" [1000] 10) |
32 supp_gen ("aux _" [1000] 10) and |
|
33 alpha_bn ("_ \<approx>bn _") |
|
34 |
32 (*>*) |
35 (*>*) |
33 |
36 |
34 |
37 |
35 section {* Introduction *} |
38 section {* Introduction *} |
36 |
39 |
1365 *} |
1368 *} |
1366 |
1369 |
1367 section {* The Lifting of Definitions and Properties *} |
1370 section {* The Lifting of Definitions and Properties *} |
1368 |
1371 |
1369 text {* |
1372 text {* |
1370 %%% TODO Fix 'Andrew Pitts' in bibliography |
|
1371 |
|
1372 To define the quotient types we first need to show that the defined |
1373 To define the quotient types we first need to show that the defined |
1373 relations are equivalence relations. |
1374 relations are equivalence relations. |
1374 |
1375 |
1375 \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} |
1376 \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} |
1376 defined as above are equivalence relations and are equivariant. |
1377 defined as above are equivalence relations and are equivariant. |
1434 Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"}, |
1435 Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"}, |
1435 since the @{term "x"} is bound. On the raw level, before the binding is |
1436 since the @{term "x"} is bound. On the raw level, before the binding is |
1436 introduced the term has the support equal to @{text "{x}"}. |
1437 introduced the term has the support equal to @{text "{x}"}. |
1437 |
1438 |
1438 To show the support equations for the lifted types we want to use the |
1439 To show the support equations for the lifted types we want to use the |
1439 Lemma \ref{suppabs}, so we start with showing that they have a finite |
1440 Theorem \ref{suppabs}, so we start with showing that they have a finite |
1440 support. |
1441 support. |
1441 |
1442 |
1442 \begin{lemma} The types @{text "ty\<^isup>\<alpha>\<^isub>1 \<dots> ty\<^isup>\<alpha>\<^isub>n"} have finite support. |
1443 \begin{lemma} The types @{text "ty\<^isup>\<alpha>\<^isub>1 \<dots> ty\<^isup>\<alpha>\<^isub>n"} have finite support. |
1443 \end{lemma} |
1444 \end{lemma} |
1444 \begin{proof} |
1445 \begin{proof} |
1448 support. We also know that atoms and finite atom sets and lists that |
1449 support. We also know that atoms and finite atom sets and lists that |
1449 occur in the constructors have finite support. A union of finite |
1450 occur in the constructors have finite support. A union of finite |
1450 sets is finite thus the support of the constructor is finite. |
1451 sets is finite thus the support of the constructor is finite. |
1451 \end{proof} |
1452 \end{proof} |
1452 |
1453 |
|
1454 % Very vague... |
1453 \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"} |
1455 \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"} |
1454 of this type: |
1456 of this type: |
1455 \begin{center} |
1457 \begin{center} |
1456 @{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}. |
1458 @{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}. |
1457 \end{center} |
1459 \end{center} |
1458 \end{lemma} |
1460 \end{lemma} |
1459 \begin{proof} |
1461 \begin{proof} |
1460 By induction on the lifted types, together with the equations that characterize |
1462 We will show this by induction together with equations that characterize |
1461 @{term "fv_bn"} in terms of @{term "supp"}... |
1463 @{term "fv_bn\<^isup>\<alpha>\<^isub>"} in terms of @{term "alpha_bn\<^isup>\<alpha>"}. For each of @{text "fv_bn\<^isup>\<alpha>"} |
|
1464 functions this equaton is: |
|
1465 \begin{center} |
|
1466 @{term "{a. infinite {b. \<not> alpha_bn\<^isup>\<alpha> ((a \<rightleftharpoons> b) \<bullet> x) x}} = fv_bn\<^isup>\<alpha> x"} |
|
1467 \end{center} |
|
1468 |
|
1469 In the induction we need to show these equations together with the goal |
|
1470 for the appropriate constructors. We first transform the right hand sides. |
|
1471 The free variable functions are applied to theirs respective constructors |
|
1472 so we can apply the lifted free variable defining equations to obtain |
|
1473 free variable functions applied to subterms minus binders. Using the |
|
1474 induction hypothesis we can replace free variable functions applied to |
|
1475 subterms by support. Using Theorem \ref{suppabs} we replace the differences |
|
1476 by supports of appropriate abstractions. |
|
1477 |
|
1478 Unfolding the definition of supports on both sides of the equations we |
|
1479 obtain by simple calculations the equalities. |
1462 \end{proof} |
1480 \end{proof} |
|
1481 |
|
1482 With the above equations we can substitute free variables for support in |
|
1483 the lifted free variable equations, which gives us the support equations |
|
1484 for the term constructors. With this we can show that for each binding in |
|
1485 a constructors the bindings can be renamed. |
|
1486 |
1463 *} |
1487 *} |
1464 |
1488 |
1465 text {* |
1489 text {* |
1466 %%% FIXME: The restricions should have already been described in previous sections? |
1490 %%% FIXME: The restricions should have already been described in previous sections? |
1467 Restrictions |
1491 Restrictions |