2112

1 
structure Thms : Thms_sig =


2 
struct

3191

3 
val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"


4 
val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"


5 
val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"

2112

6 
val CUT_DEF = cut_def


7 


8 
local val _ = goal HOL.thy "!P x. P x > P (Eps P)"


9 
val _ = by (strip_tac 1)


10 
val _ = by (rtac selectI 1)


11 
val _ = by (assume_tac 1)


12 
in val SELECT_AX = result()


13 
end;


14 


15 
(*


16 
* A useful congruence rule


17 
**)


18 
local val [p1,p2] = goal HOL.thy "(M = N) ==> \


19 
\ (!!x. ((x = N) ==> (f x = g x))) ==> \


20 
\ (Let M f = Let N g)";


21 
val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);


22 
val _ = by (rtac p2 1);


23 
val _ = by (rtac refl 1);


24 
in val LET_CONG = result() RS eq_reflection


25 
end;


26 


27 
val COND_CONG = if_cong RS eq_reflection;


28 


29 
fun C f x y = f y x;


30 
fun prover thl = [fast_tac HOL_cs 1];


31 
val P = C (prove_goal HOL.thy) prover;


32 


33 
val eqT = P"(x = True) > x"


34 
val rev_eq_mp = P"(x = y) > y > x"


35 
val simp_thm = P"(x>y) > (x = x') > (x' > y)"


36 


37 
end;
