8 begin |
8 begin |
9 |
9 |
10 print_syntax |
10 print_syntax |
11 |
11 |
12 notation (latex output) |
12 notation (latex output) |
13 rel_conj ("_ OOO _" [53, 53] 52) |
13 rel_conj ("_ OOO _" [53, 53] 52) and |
14 and |
14 "op -->" (infix "\<rightarrow>" 100) and |
15 "op -->" (infix "\<rightarrow>" 100) |
15 "==>" (infix "\<Rightarrow>" 100) and |
16 and |
16 fun_map (infix "\<longrightarrow>" 51) and |
17 "==>" (infix "\<Rightarrow>" 100) |
17 fun_rel (infix "\<Longrightarrow>" 51) and |
18 and |
18 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
19 fun_map (infix "\<longrightarrow>" 51) |
19 fempty ("\<emptyset>\<^isub>f") and |
20 and |
20 funion ("_ \<union>\<^isub>f _") and |
21 fun_rel (infix "\<Longrightarrow>" 51) |
21 Cons ("_::_") |
22 and |
22 |
23 list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *) |
|
24 |
23 |
25 ML {* |
24 ML {* |
26 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
25 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
27 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
26 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
28 let |
27 let |
55 (HOL). This logic consists of a small number of axioms and inference rules |
54 (HOL). This logic consists of a small number of axioms and inference rules |
56 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
55 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
57 very restricted mechanisms for extending the logic: one is the definition of |
56 very restricted mechanisms for extending the logic: one is the definition of |
58 new constants in terms of existing ones; the other is the introduction of |
57 new constants in terms of existing ones; the other is the introduction of |
59 new types by identifying non-empty subsets in existing types. It is well |
58 new types by identifying non-empty subsets in existing types. It is well |
60 understood to use both mechanisms for dealing with quotient constructions in |
59 understood how to use both mechanisms for dealing with quotient constructions in |
61 HOL (see \cite{Homeier05,Paulson06}). For example the integers |
60 HOL (see \cite{Homeier05,Paulson06}). For example the integers |
62 in Isabelle/HOL are constructed by a quotient construction over the type |
61 in Isabelle/HOL are constructed by a quotient construction over the type |
63 @{typ "nat \<times> nat"} and the equivalence relation |
62 @{typ "nat \<times> nat"} and the equivalence relation |
64 |
63 |
65 @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"} |
64 @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"} |
66 |
65 |
67 \noindent |
66 \noindent |
68 This constructions yields the type @{typ int} and definitions for @{text |
67 This constructions yields the new type @{typ int} and definitions for @{text |
69 "0::int"} and @{text "1::int"} in terms of pairs of natural numbers can be |
68 "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of |
70 given (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations such as |
69 natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations |
71 @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in terms of operations on |
70 such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined |
72 pairs of natural numbers (namely @{text "add\<^bsub>nat\<times>nat\<^esub> |
71 in terms of operations on pairs of natural numbers (namely @{text "add\<^bsub>nat\<times>nat\<^esub> |
73 (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \<equiv> (x\<^isub>1 + |
72 (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \<equiv> (x\<^isub>1 + |
74 x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}). Similarly one can construct the |
73 x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}). Similarly one can construct the |
75 type of finite sets by quotienting lists according to the equivalence |
74 type of finite sets by quotienting lists according to the equivalence |
76 relation |
75 relation |
77 |
76 |
78 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
77 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
79 |
78 |
80 \noindent |
79 \noindent |
81 which states that two lists are equivalent if every element in one list is also |
80 which states that two lists are equivalent if every element in one list is also |
82 member in the other (@{text "\<in>"} stands here for membership in lists). |
81 member in the other (@{text "\<in>"} stands here for membership in lists). The |
83 |
82 empty finite set, written @{term "{||}"} can then be defined as the |
84 The problem is that in order to be able to reason about integers and |
83 empty list and union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. |
85 finite sets, one needs to establish a reasoning infrastructure by |
84 |
|
85 Another important area of quotients is reasoning about programming language |
|
86 calculi. A simple example are lambda-terms defined as |
|
87 |
|
88 \begin{center} |
|
89 @{text "t ::= x | t t | \<lambda>x.t"} |
|
90 \end{center} |
|
91 |
|
92 \noindent |
|
93 The difficulty with this definition of lambda-terms arises when, for |
|
94 example, proving formally the substitution lemma ... |
|
95 On the other hand if we reason about alpha-equated lambda-terms, that means |
|
96 terms quotient according to alpha-equivalence, then reasoning infrastructure |
|
97 can be introduced that make the formal proof of the substitution lemma |
|
98 almost trivial. |
|
99 |
|
100 |
|
101 The problem is that in order to be able to reason about integers, finite sets |
|
102 and alpha-equated lambda-terms one needs to establish a reasoning infrastructure by |
86 transferring, or \emph{lifting}, definitions and theorems from the ``raw'' |
103 transferring, or \emph{lifting}, definitions and theorems from the ``raw'' |
87 type @{typ "nat \<times> nat"} to the quotient type @{typ int} (similarly for |
104 type @{typ "nat \<times> nat"} to the quotient type @{typ int} (similarly for |
88 @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}). This lifting usually |
105 @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}, and also for raw lambda-terms |
|
106 and alpha-equated lambda-terms). This lifting usually |
89 requires a \emph{lot} of tedious reasoning effort. The purpose of a \emph{quotient |
107 requires a \emph{lot} of tedious reasoning effort. The purpose of a \emph{quotient |
90 package} is to ease the lifting and automate the reasoning as much as |
108 package} is to ease the lifting and automate the reasoning as much as |
91 possible. While for integers and finite sets teh tedious reasoning needs |
109 possible. While for integers and finite sets teh tedious reasoning needs |
92 to be done only once, Nominal Isabelle providing a reasoning infrastructure |
110 to be done only once, Nominal Isabelle providing a reasoning infrastructure |
93 for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over |
111 for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over |