src/HOL/Induct/PropLog.thy
changeset 27034 5257bc7e0c06
parent 24824 b7866aea0815
child 36862 952b2b102a0a
equal deleted inserted replaced
27033:6ef5134fc631 27034:5257bc7e0c06
   132 
   132 
   133 subsubsection {* Towards the completeness proof *}
   133 subsubsection {* Towards the completeness proof *}
   134 
   134 
   135 lemma false_imp: "H |- p->false ==> H |- p->q"
   135 lemma false_imp: "H |- p->false ==> H |- p->q"
   136 apply (rule deduction)
   136 apply (rule deduction)
   137 apply (erule weaken_left_insert [THEN thms_notE])
   137 apply (metis H insert_iff weaken_left_insert thms_notE)
   138 apply blast
       
   139 done
   138 done
   140 
   139 
   141 lemma imp_false:
   140 lemma imp_false:
   142     "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false"
   141     "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false"
   143 apply (rule deduction)
   142 apply (rule deduction)
   144 apply (blast intro: weaken_left_insert thms.MP thms.H)
   143 apply (metis H MP insert_iff weaken_left_insert)
   145 done
   144 done
   146 
   145 
   147 lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
   146 lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
   148   -- {* Typical example of strengthening the induction statement. *}
   147   -- {* Typical example of strengthening the induction statement. *}
   149 apply simp
   148 apply simp