equal
deleted
inserted
replaced
1 theory Examples2 |
1 theory Examples2 |
2 imports Examples |
2 imports Examples |
3 begin |
3 begin |
4 text {* \vspace{-5ex} *} |
4 text {* \vspace{-5ex} *} |
5 interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" |
5 interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" |
6 where "partial_order.less op \<le> (x::nat) y = (x < y)" |
6 where "partial_order.less op \<le> (x::int) y = (x < y)" |
7 proof - |
7 proof - |
8 txt {* \normalsize The goals are @{subgoals [display]} |
8 txt {* \normalsize The goals are @{subgoals [display]} |
9 The proof that @{text \<le>} is a partial order is as above. *} |
9 The proof that @{text \<le>} is a partial order is as above. *} |
10 show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)" |
10 show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" |
11 by unfold_locales auto |
11 by unfold_locales auto |
12 txt {* \normalsize The second goal is shown by unfolding the |
12 txt {* \normalsize The second goal is shown by unfolding the |
13 definition of @{term "partial_order.less"}. *} |
13 definition of @{term "partial_order.less"}. *} |
14 show "partial_order.less op \<le> (x::nat) y = (x < y)" |
14 show "partial_order.less op \<le> (x::int) y = (x < y)" |
15 unfolding partial_order.less_def [OF `partial_order op \<le>`] |
15 unfolding partial_order.less_def [OF `partial_order op \<le>`] |
16 by auto |
16 by auto |
17 qed |
17 qed |
18 |
18 |
19 text {* Note that the above proof is not in the context of the |
19 text {* Note that the above proof is not in the context of the |