equal
deleted
inserted
replaced
87 lemma test_theorem: |
87 lemma test_theorem: |
88 fixes x :: nat |
88 fixes x :: nat |
89 shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y" |
89 shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y" |
90 by (rule Orderings.order_antisym) |
90 by (rule Orderings.order_antisym) |
91 |
91 |
|
92 (* Premises of the conditional rule yield new subgoals. The |
|
93 assumptions of the goal are propagated into these subgoals |
|
94 *) |
92 lemma |
95 lemma |
93 fixes f :: "nat \<Rightarrow> nat" |
96 fixes f :: "nat \<Rightarrow> nat" |
94 assumes "f x \<le> 0" "f x \<ge> 0" |
97 shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0" |
95 shows "f x = 0" |
|
96 apply (rewrite at "f x" to "0" test_theorem) |
98 apply (rewrite at "f x" to "0" test_theorem) |
97 apply fact |
99 apply assumption |
98 apply fact |
100 apply assumption |
99 apply (rule refl) |
101 apply (rule refl) |
100 done |
102 done |
101 |
103 |
102 (* |
104 (* |
103 Instantiation. |
105 Instantiation. |
104 |
106 |
105 Since all rewriting is now done via conversions, |
107 Since all rewriting is now done via conversions, |