Simplified the calling sequence of CONTEXT_REWRITE_RULE
authorpaulson
Fri May 30 15:55:27 1997 +0200 (1997-05-30)
changeset 33797091ffa99c93
parent 3378 11f4884a071a
child 3380 2986e3b1f86a
Simplified the calling sequence of CONTEXT_REWRITE_RULE
Eliminated get_rhs, which was calling dest_Trueprop too many times
TFL/rules.new.sml
TFL/rules.sig
TFL/tfl.sml
     1.1 --- a/TFL/rules.new.sml	Fri May 30 15:30:52 1997 +0200
     1.2 +++ b/TFL/rules.new.sml	Fri May 30 15:55:27 1997 +0200
     1.3 @@ -442,13 +442,11 @@
     1.4  
     1.5     
     1.6  fun dest_equal(Const ("==",_) $ 
     1.7 -              (Const ("Trueprop",_) $ lhs) 
     1.8 -            $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
     1.9 +	       (Const ("Trueprop",_) $ lhs) 
    1.10 +	       $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
    1.11    | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
    1.12    | dest_equal tm = S.dest_eq tm;
    1.13  
    1.14 -
    1.15 -fun get_rhs tm = #rhs(dest_equal (HOLogic.dest_Trueprop tm));
    1.16  fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
    1.17  
    1.18  fun variants FV vlist =
    1.19 @@ -654,7 +652,7 @@
    1.20  val restricted = U.can(S.find_term
    1.21                         (U.holds(fn c => (#Name(S.dest_const c)="cut"))))
    1.22  
    1.23 -fun CONTEXT_REWRITE_RULE(func,R){thms=[cut_lemma],congs,th} =
    1.24 +fun CONTEXT_REWRITE_RULE(func,R){cut_lemma, congs, th} =
    1.25   let val tc_list = ref[]: term list ref
    1.26       val dummy = term_ref := []
    1.27       val dummy = thm_ref  := []
    1.28 @@ -690,7 +688,6 @@
    1.29                    val dummy = assert (forall (op aconv)
    1.30                                        (ListPair.zip (vlist, args)))
    1.31                                 "assertion failed in CONTEXT_REWRITE_RULE"
    1.32 -(*                val fbvs1 = variants (S.free_vars imp) fbvs *)
    1.33                    val imp_body1 = subst_free (ListPair.zip (args, vstrl))
    1.34                                               imp_body
    1.35                    val tych = cterm_of sign
    1.36 @@ -702,7 +699,7 @@
    1.37                    val mss' = add_prems(mss, map ASSUME ants1)
    1.38                    val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1
    1.39                                  handle _ => reflexive Q1
    1.40 -                  val Q2 = get_rhs(HOLogic.dest_Trueprop(#prop(rep_thm Q1eeqQ2)))
    1.41 +                  val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
    1.42                    val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
    1.43                    val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)
    1.44                    val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
    1.45 @@ -775,14 +772,16 @@
    1.46                           | _   => [S.list_mk_conj(map cncl rcontext)]
    1.47                val TC = genl(S.list_mk_imp(antl, A))
    1.48                val dummy = print_cterms "func:\n" [cterm_of sign func]
    1.49 -              val dummy = print_cterms "TC:\n" [cterm_of sign (HOLogic.mk_Trueprop TC)]
    1.50 +              val dummy = print_cterms "TC:\n" 
    1.51 +		              [cterm_of sign (HOLogic.mk_Trueprop TC)]
    1.52                val dummy = tc_list := (TC :: !tc_list)
    1.53                val nestedp = nested TC
    1.54 -              val dummy = if nestedp then say "nested\n" else say "not_nested\n"
    1.55 +              val dummy = if nestedp then say"nested\n" else say"not_nested\n"
    1.56                val dummy = term_ref := ([func,TC]@(!term_ref))
    1.57                val th' = if nestedp then raise RULES_ERR{func = "solver", 
    1.58                                                        mesg = "nested function"}
    1.59 -                        else let val cTC = cterm_of sign (HOLogic.mk_Trueprop TC)
    1.60 +                        else let val cTC = cterm_of sign 
    1.61 +			                      (HOLogic.mk_Trueprop TC)
    1.62                               in case rcontext of
    1.63                                  [] => SPEC_ALL(ASSUME cTC)
    1.64                                 | _ => MP (SPEC_ALL (ASSUME cTC)) 
     2.1 --- a/TFL/rules.sig	Fri May 30 15:30:52 1997 +0200
     2.2 +++ b/TFL/rules.sig	Fri May 30 15:55:27 1997 +0200
     2.3 @@ -50,14 +50,12 @@
     2.4    val simpl_conv : thm list -> cterm -> thm
     2.5  
     2.6  (* For debugging my isabelle solver in the conditional rewriter *)
     2.7 -(*
     2.8    val term_ref : term list ref
     2.9    val thm_ref : thm list ref
    2.10    val mss_ref : meta_simpset list ref
    2.11    val tracing :bool ref
    2.12 -*)
    2.13    val CONTEXT_REWRITE_RULE : term * term
    2.14 -                             -> {thms:thm list,congs: thm list, th:thm} 
    2.15 +                             -> {cut_lemma:thm, congs: thm list, th:thm} 
    2.16                               -> thm * term list
    2.17    val RIGHT_ASSOC : thm -> thm 
    2.18  
     3.1 --- a/TFL/tfl.sml	Fri May 30 15:30:52 1997 +0200
     3.2 +++ b/TFL/tfl.sml	Fri May 30 15:55:27 1997 +0200
     3.3 @@ -426,9 +426,9 @@
     3.4       val (case_rewrites,context_congs) = extraction_thms theory
     3.5       val corollaries' = map(R.simplify case_rewrites) corollaries
     3.6       fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
     3.7 -                         {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA],
     3.8 -                         congs = context_congs,
     3.9 -                            th = th}
    3.10 +                         {cut_lemma = R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
    3.11 +			  congs = context_congs,
    3.12 +			  th = th}
    3.13       val (rules, TCs) = ListPair.unzip (map xtract corollaries')
    3.14       val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
    3.15       val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
    3.16 @@ -464,9 +464,9 @@
    3.17       val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
    3.18       val corollaries' = map (R.simplify case_rewrites) corollaries
    3.19       fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
    3.20 -                        {thms = [(R.ISPECL o map tych)[f,R1] Thms.CUT_LEMMA], 
    3.21 -                        congs = context_congs,
    3.22 -                          th  = th}
    3.23 +                        {cut_lemma = R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
    3.24 +			 congs = context_congs,
    3.25 +			 th  = th}
    3.26   in {proto_def=proto_def, 
    3.27       WFR=WFR, 
    3.28       pats=pats,