author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 48985  5386df44a037 
child 57607  5ff0cf3f5f6f 
permissions  rwrr 
27063  1 
theory Examples2 
2 
imports Examples 

3 
begin 

32981  4 
text {* \vspace{5ex} *} 
32982  5 
interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" 
43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
32983
diff
changeset

6 
where "int.less x y = (x < y)" 
32981  7 
proof  
32983  8 
txt {* \normalsize The goals are now: 
9 
@{subgoals [display]} 

10 
The proof that~@{text \<le>} is a partial order is as above. *} 

32982  11 
show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" 
32981  12 
by unfold_locales auto 
13 
txt {* \normalsize The second goal is shown by unfolding the 

14 
definition of @{term "partial_order.less"}. *} 

43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
32983
diff
changeset

15 
show "partial_order.less op \<le> x y = (x < y)" 
32981  16 
unfolding partial_order.less_def [OF `partial_order op \<le>`] 
17 
by auto 

18 
qed 

27063  19 

32981  20 
text {* Note that the above proof is not in the context of the 
32983  21 
interpreted locale. Hence, the premise of @{text 
22 
"partial_order.less_def"} is discharged manually with @{text OF}. 

27063  23 
*} 
24 
end 