author  blanchet 
Mon, 20 Dec 2010 14:17:49 +0100  
changeset 41317  fc48faccd77b 
parent 27208  5fe899199f85 
child 58889  5b7a9633cfa8 
permissions  rwrr 
4905  1 

17248  2 
header {* Prefixpoints *} 
4905  3 

17248  4 
theory Ex4 
5 
imports LCF 

6 
begin 

7 

19755  8 
lemma example: 
9 
assumes asms: "f(p) << p" "!!q. f(q) << q ==> p << q" 

10 
shows "FIX(f)=p" 

11 
apply (unfold eq_def) 

12 
apply (rule conjI) 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
19755
diff
changeset

13 
apply (tactic {* induct_tac @{context} "f" 1 *}) 
19755  14 
apply (rule minimal) 
15 
apply (intro strip) 

16 
apply (rule less_trans) 

17 
prefer 2 

18 
apply (rule asms) 

19 
apply (erule less_ap_term) 

20 
apply (rule asms) 

21 
apply (rule FIX_eq [THEN eq_imp_less1]) 

22 
done 

23 

17248  24 
end 