equal
deleted
inserted
replaced
63 \end{isabelle} |
63 \end{isabelle} |
64 Intuitively, this theorem says that |
64 Intuitively, this theorem says that |
65 enlarging the set of function symbols enlarges the set of ground |
65 enlarging the set of function symbols enlarges the set of ground |
66 terms. The proof is a trivial rule induction. |
66 terms. The proof is a trivial rule induction. |
67 First we use the \isa{clarify} method to assume the existence of an element of |
67 First we use the \isa{clarify} method to assume the existence of an element of |
68 \isa{terms~F}. (We could have used \isa{intro subsetI}.) We then |
68 \isa{gterms~F}. (We could have used \isa{intro subsetI}.) We then |
69 apply rule induction. Here is the resulting subgoal: |
69 apply rule induction. Here is the resulting subgoal: |
70 \begin{isabelle} |
70 \begin{isabelle} |
71 \ 1.\ \isasymAnd x\ args\ f.\isanewline |
71 \ 1.\ \isasymAnd x\ args\ f.\isanewline |
72 \ \ \ \ \ \ \ \isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline |
72 \ \ \ \ \ \ \ \isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline |
73 \ \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G% |
73 \ \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G% |
94 inversion is done in Isabelle. |
94 inversion is done in Isabelle. |
95 |
95 |
96 Recall that \isa{even} is the minimal set closed under these two rules: |
96 Recall that \isa{even} is the minimal set closed under these two rules: |
97 \begin{isabelle} |
97 \begin{isabelle} |
98 0\ \isasymin \ even\isanewline |
98 0\ \isasymin \ even\isanewline |
99 n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin |
99 n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin |
100 \ even |
100 \ even |
101 \end{isabelle} |
101 \end{isabelle} |
102 Minimality means that \isa{even} contains only the elements that these |
102 Minimality means that \isa{even} contains only the elements that these |
103 rules force it to contain. If we are told that \isa{a} |
103 rules force it to contain. If we are told that \isa{a} |
104 belongs to |
104 belongs to |
105 \isa{even} then there are only two possibilities. Either \isa{a} is \isa{0} |
105 \isa{even} then there are only two possibilities. Either \isa{a} is \isa{0} |
106 or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n} |
106 or else \isa{a} has the form \isa{Suc(Suc~n)}, for some suitable \isa{n} |
107 that belongs to |
107 that belongs to |
108 \isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves |
108 \isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves |
109 for us when it accepts an inductive definition: |
109 for us when it accepts an inductive definition: |
110 \begin{isabelle} |
110 \begin{isabelle} |
111 \isasymlbrakk a\ \isasymin \ even;\isanewline |
111 \isasymlbrakk a\ \isasymin \ even;\isanewline |