34 differ, which can affect proofs. If you want to avoid this complication, |
34 differ, which can affect proofs. If you want to avoid this complication, |
35 stick to @{term fst} and @{term snd} and write @{term"%p. fst p + snd p"} |
35 stick to @{term fst} and @{term snd} and write @{term"%p. fst p + snd p"} |
36 instead of @{text"\<lambda>(x,y). x+y"}. These terms are distinct even though they |
36 instead of @{text"\<lambda>(x,y). x+y"}. These terms are distinct even though they |
37 denote the same function. |
37 denote the same function. |
38 |
38 |
39 Internally, @{term"%(x,y). t"} becomes @{text"split (\<lambda>x y. t)"}, where |
39 Internally, @{term"%(x,y). t"} becomes @{text"case_prod (\<lambda>x y. t)"}, where |
40 \cdx{split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b |
40 \cdx{split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b |
41 \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as |
41 \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as |
42 \begin{center} |
42 \begin{center} |
43 @{thm split_def} |
43 @{thm split_def} |
44 \hfill(@{thm[source]split_def}) |
44 \hfill(@{thm[source]split_def}) |
69 p} by some pair @{term"(a,b)"}. Then both sides of the |
69 p} by some pair @{term"(a,b)"}. Then both sides of the |
70 equation would simplify to @{term a} by the simplification rules |
70 equation would simplify to @{term a} by the simplification rules |
71 @{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}. |
71 @{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}. |
72 To reason about tuple patterns requires some way of |
72 To reason about tuple patterns requires some way of |
73 converting a variable of product type into a pair. |
73 converting a variable of product type into a pair. |
74 In case of a subterm of the form @{term"split f p"} this is easy: the split |
74 In case of a subterm of the form @{term"case_prod f p"} this is easy: the split |
75 rule @{thm[source]split_split} replaces @{term p} by a pair:% |
75 rule @{thm[source]prod.split} replaces @{term p} by a pair:% |
76 \index{*split (method)} |
76 \index{*split (method)} |
77 *} |
77 *} |
78 |
78 |
79 lemma "(\<lambda>(x,y).y) p = snd p" |
79 lemma "(\<lambda>(x,y).y) p = snd p" |
80 apply(split split_split) |
80 apply(split prod.split) |
81 |
81 |
82 txt{* |
82 txt{* |
83 @{subgoals[display,indent=0]} |
83 @{subgoals[display,indent=0]} |
84 This subgoal is easily proved by simplification. Thus we could have combined |
84 This subgoal is easily proved by simplification. Thus we could have combined |
85 simplification and splitting in one command that proves the goal outright: |
85 simplification and splitting in one command that proves the goal outright: |
86 *} |
86 *} |
87 (*<*) |
87 (*<*) |
88 by simp |
88 by simp |
89 lemma "(\<lambda>(x,y).y) p = snd p"(*>*) |
89 lemma "(\<lambda>(x,y).y) p = snd p"(*>*) |
90 by(simp split: split_split) |
90 by(simp split: prod.split) |
91 |
91 |
92 text{* |
92 text{* |
93 Let us look at a second example: |
93 Let us look at a second example: |
94 *} |
94 *} |
95 |
95 |
100 @{subgoals[display,indent=0]} |
100 @{subgoals[display,indent=0]} |
101 A paired @{text let} reduces to a paired $\lambda$-abstraction, which |
101 A paired @{text let} reduces to a paired $\lambda$-abstraction, which |
102 can be split as above. The same is true for paired set comprehension: |
102 can be split as above. The same is true for paired set comprehension: |
103 *} |
103 *} |
104 |
104 |
105 (*<*)by(simp split: split_split)(*>*) |
105 (*<*)by(simp split: prod.split)(*>*) |
106 lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p" |
106 lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p" |
107 apply simp |
107 apply simp |
108 |
108 |
109 txt{* |
109 txt{* |
110 @{subgoals[display,indent=0]} |
110 @{subgoals[display,indent=0]} |
111 Again, simplification produces a term suitable for @{thm[source]split_split} |
111 Again, simplification produces a term suitable for @{thm[source]prod.split} |
112 as above. If you are worried about the strange form of the premise: |
112 as above. If you are worried about the strange form of the premise: |
113 @{text"split (op =)"} is short for @{term"\<lambda>(x,y). x=y"}. |
113 @{text"case_prod (op =)"} is short for @{term"\<lambda>(x,y). x=y"}. |
114 The same proof procedure works for |
114 The same proof procedure works for |
115 *} |
115 *} |
116 |
116 |
117 (*<*)by(simp split: split_split)(*>*) |
117 (*<*)by(simp split: prod.split)(*>*) |
118 lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p" |
118 lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p" |
119 |
119 |
120 txt{*\noindent |
120 txt{*\noindent |
121 except that we now have to use @{thm[source]split_split_asm}, because |
121 except that we now have to use @{thm[source]prod.split_asm}, because |
122 @{term split} occurs in the assumptions. |
122 @{term split} occurs in the assumptions. |
123 |
123 |
124 However, splitting @{term split} is not always a solution, as no @{term split} |
124 However, splitting @{term split} is not always a solution, as no @{term split} |
125 may be present in the goal. Consider the following function: |
125 may be present in the goal. Consider the following function: |
126 *} |
126 *} |
127 |
127 |
128 (*<*)by(simp split: split_split_asm)(*>*) |
128 (*<*)by(simp split: prod.split_asm)(*>*) |
129 primrec swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" where "swap (x,y) = (y,x)" |
129 primrec swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" where "swap (x,y) = (y,x)" |
130 |
130 |
131 text{*\noindent |
131 text{*\noindent |
132 Note that the above \isacommand{primrec} definition is admissible |
132 Note that the above \isacommand{primrec} definition is admissible |
133 because @{text"\<times>"} is a datatype. When we now try to prove |
133 because @{text"\<times>"} is a datatype. When we now try to prove |