2112

1 
structure Thms : Thms_sig =


2 
struct


3 
type Thm = Thm.thm


4 


5 
val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec"


6 
val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct"


7 
val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply"


8 
val CUT_DEF = cut_def


9 


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


11 
val _ = by (strip_tac 1)


12 
val _ = by (rtac selectI 1)


13 
val _ = by (assume_tac 1)


14 
in val SELECT_AX = result()


15 
end;


16 


17 
(*


18 
* A useful congruence rule


19 
**)


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


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


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


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


24 
val _ = by (rtac p2 1);


25 
val _ = by (rtac refl 1);


26 
in val LET_CONG = result() RS eq_reflection


27 
end;


28 


29 
val COND_CONG = if_cong RS eq_reflection;


30 


31 
fun C f x y = f y x;


32 
fun prover thl = [fast_tac HOL_cs 1];


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


34 


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


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


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


38 


39 
end;
