491 text \<open>

   491 text \<open>

   492   The function @{ML all_elims} takes a list of (certified) terms and instantiates

   492   The function @{ML all_elims} takes a list of (certified) terms and instantiates

   493   theorems of the form @{thm [source] all_elims_test}. For example we can instantiate

   493   theorems of the form @{thm [source] all_elims_test}. For example we can instantiate

   494   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:

   494   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:

   495 

   495 

   497 \<open>let

   497 \<open>let

   498   val ctrms = [@{cterm "a::nat"}, @{cterm "b::nat"}, @{cterm "c::nat"}]

   498   val ctrms = [@{cterm "a::nat"}, @{cterm "b::nat"}, @{cterm "c::nat"}]

   499   val new_thm = all_elims ctrms @{thm all_elims_test}

   499   val new_thm = all_elims ctrms @{thm all_elims_test}

   500 in

   500 in

   501   pwriteln (pretty_thm_no_vars @{context} new_thm)

   501   pwriteln (pretty_thm_no_vars @{context} new_thm)

   508 

   508 

   509   Similarly, the function @{ML imp_elims} eliminates preconditions from implications. 

   509   Similarly, the function @{ML imp_elims} eliminates preconditions from implications. 

   510   For example we can eliminate the preconditions \<open>A\<close> and \<open>B\<close> from

   510   For example we can eliminate the preconditions \<open>A\<close> and \<open>B\<close> from

   511   @{thm [source] imp_elims_test}:

   511   @{thm [source] imp_elims_test}:

   512 

   512 

   514 \<open>let

   514 \<open>let

   515   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}

   515   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}

   516 in

   516 in

   517   pwriteln (pretty_thm_no_vars @{context} res)

   517   pwriteln (pretty_thm_no_vars @{context} res)

   518 end\<close>

   518 end\<close>

   520 

   520 

   521   Now we set up the proof for the introduction rule as follows:

   521   Now we set up the proof for the introduction rule as follows:

   522 \<close>

   522 \<close>

   523 

   523 

   524 lemma fresh_Lam:

   524 lemma fresh_Lam: