equal
deleted
inserted
replaced
62 *} |
62 *} |
63 |
63 |
64 text {* |
64 text {* |
65 the subst method |
65 the subst method |
66 |
66 |
67 @{thm[display] mult_commute} |
67 @{thm[display] mult.commute} |
68 \rulename{mult_commute} |
68 \rulename{mult.commute} |
69 |
69 |
70 this would fail: |
70 this would fail: |
71 apply (simp add: mult_commute) |
71 apply (simp add: mult.commute) |
72 *} |
72 *} |
73 |
73 |
74 |
74 |
75 lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y" |
75 lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y" |
76 txt{* |
76 txt{* |
77 @{subgoals[display,indent=0,margin=65]} |
77 @{subgoals[display,indent=0,margin=65]} |
78 *} |
78 *} |
79 apply (subst mult_commute) |
79 apply (subst mult.commute) |
80 txt{* |
80 txt{* |
81 @{subgoals[display,indent=0,margin=65]} |
81 @{subgoals[display,indent=0,margin=65]} |
82 *} |
82 *} |
83 oops |
83 oops |
84 |
84 |
85 (*exercise involving THEN*) |
85 (*exercise involving THEN*) |
86 lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y" |
86 lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y" |
87 apply (rule mult_commute [THEN ssubst]) |
87 apply (rule mult.commute [THEN ssubst]) |
88 oops |
88 oops |
89 |
89 |
90 |
90 |
91 lemma "\<lbrakk>x = f x; triple (f x) (f x) x\<rbrakk> \<Longrightarrow> triple x x x" |
91 lemma "\<lbrakk>x = f x; triple (f x) (f x) x\<rbrakk> \<Longrightarrow> triple x x x" |
92 apply (erule ssubst) |
92 apply (erule ssubst) |