TFL/rules.new.sml
changeset 4713 bea2ab2e360b
parent 3629 8e95bd329fff
child 5081 7274f7d101ee
equal deleted inserted replaced
4712:facfbbca7242 4713:bea2ab2e360b
   388  *---------------------------------------------------------------------------*)
   388  *---------------------------------------------------------------------------*)
   389 
   389 
   390 fun SUBS thl = 
   390 fun SUBS thl = 
   391    rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
   391    rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
   392 
   392 
   393 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
   393 local fun rew_conv mss = rewrite_cterm (true,false,false) mss (K(K None))
   394 in
   394 in
   395 fun simpl_conv ss thl ctm = 
   395 fun simpl_conv ss thl ctm = 
   396  rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
   396  rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
   397  RS meta_eq_to_obj_eq
   397  RS meta_eq_to_obj_eq
   398 end;
   398 end;
   652                      val dummy = print_cterms "To eliminate:\n" [tych imp]
   652                      val dummy = print_cterms "To eliminate:\n" [tych imp]
   653                      val ants = map tych (Logic.strip_imp_prems imp)
   653                      val ants = map tych (Logic.strip_imp_prems imp)
   654                      val eq = Logic.strip_imp_concl imp
   654                      val eq = Logic.strip_imp_concl imp
   655                      val lhs = tych(get_lhs eq)
   655                      val lhs = tych(get_lhs eq)
   656                      val mss' = add_prems(mss, map ASSUME ants)
   656                      val mss' = add_prems(mss, map ASSUME ants)
   657                      val lhs_eq_lhs1 = rewrite_cterm(false,true)mss' prover lhs
   657                      val lhs_eq_lhs1 = rewrite_cterm(false,true,false)mss' prover lhs
   658                        handle _ => reflexive lhs
   658                        handle _ => reflexive lhs
   659                      val dummy = print_thms "proven:\n" [lhs_eq_lhs1]
   659                      val dummy = print_thms "proven:\n" [lhs_eq_lhs1]
   660                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   660                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   661                      val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
   661                      val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
   662                   in
   662                   in
   674                   val eq1 = Logic.strip_imp_concl imp_body1
   674                   val eq1 = Logic.strip_imp_concl imp_body1
   675                   val Q = get_lhs eq1
   675                   val Q = get_lhs eq1
   676                   val QeqQ1 = pbeta_reduce (tych Q)
   676                   val QeqQ1 = pbeta_reduce (tych Q)
   677                   val Q1 = #2(D.dest_eq(cconcl QeqQ1))
   677                   val Q1 = #2(D.dest_eq(cconcl QeqQ1))
   678                   val mss' = add_prems(mss, map ASSUME ants1)
   678                   val mss' = add_prems(mss, map ASSUME ants1)
   679                   val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1
   679                   val Q1eeqQ2 = rewrite_cterm (false,true,false) mss' prover Q1
   680                                 handle _ => reflexive Q1
   680                                 handle _ => reflexive Q1
   681                   val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
   681                   val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
   682                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   682                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   683                   val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)
   683                   val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)
   684                   val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
   684                   val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
   699                  then pq_eliminate (thm,sign,vlist,imp_body,Q)
   699                  then pq_eliminate (thm,sign,vlist,imp_body,Q)
   700                  else 
   700                  else 
   701                  let val tych = cterm_of sign
   701                  let val tych = cterm_of sign
   702                      val ants1 = map tych ants
   702                      val ants1 = map tych ants
   703                      val mss' = add_prems(mss, map ASSUME ants1)
   703                      val mss' = add_prems(mss, map ASSUME ants1)
   704                      val Q_eeq_Q1 = rewrite_cterm(false,true) mss' 
   704                      val Q_eeq_Q1 = rewrite_cterm(false,true,false) mss' 
   705                                                      prover (tych Q)
   705                                                      prover (tych Q)
   706                       handle _ => reflexive (tych Q)
   706                       handle _ => reflexive (tych Q)
   707                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   707                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   708                      val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
   708                      val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
   709                      val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
   709                      val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
   769           end handle _ => None
   769           end handle _ => None
   770     in
   770     in
   771     (if (is_cong thm) then cong_prover else restrict_prover) mss thm
   771     (if (is_cong thm) then cong_prover else restrict_prover) mss thm
   772     end
   772     end
   773     val ctm = cprop_of th
   773     val ctm = cprop_of th
   774     val th1 = rewrite_cterm(false,true) (add_congs(mss_of [cut_lemma'], congs))
   774     val th1 = rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs))
   775                             prover ctm
   775                             prover ctm
   776     val th2 = equal_elim th1 th
   776     val th2 = equal_elim th1 th
   777  in
   777  in
   778  (th2, filter (not o restricted) (!tc_list))
   778  (th2, filter (not o restricted) (!tc_list))
   779  end;
   779  end;