clarified order of rules for match_tac/resolve_tac;
authorwenzelm
Sat Aug 16 16:18:39 2014 +0200 (2014-08-16)
changeset 57954c52223cd1003
parent 57953 69728243a614
child 57955 f28337c2c0a8
clarified order of rules for match_tac/resolve_tac;
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/Tools/fixrec.ML
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Sat Aug 16 14:42:35 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sat Aug 16 16:18:39 2014 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4        val tr = instantiate' [SOME T, SOME U] [SOME f]
     1.5            (mk_meta_eq @{thm Abs_cfun_inverse2});
     1.6        val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
     1.7 -      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
     1.8 +      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)));
     1.9      in SOME (perhaps (SINGLE (tac 1)) tr) end
    1.10  *}
    1.11  
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 14:42:35 2014 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 16:18:39 2014 +0200
     2.3 @@ -151,7 +151,7 @@
     2.4        let
     2.5          val prop = mk_trp (mk_cont functional)
     2.6          val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
     2.7 -        val tac = REPEAT_ALL_NEW (match_tac rules) 1
     2.8 +        val tac = REPEAT_ALL_NEW (match_tac (rev rules)) 1
     2.9        in
    2.10          Goal.prove_global thy [] [] prop (K tac)
    2.11        end
    2.12 @@ -189,7 +189,7 @@
    2.13    let
    2.14      val defl_simps =
    2.15        Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
    2.16 -    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps
    2.17 +    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) (rev defl_simps)
    2.18      val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2
    2.19      fun proc1 t =
    2.20        (case dest_DEFL t of
    2.21 @@ -632,7 +632,7 @@
    2.22             simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,
    2.23             simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1,
    2.24             REPEAT (etac @{thm conjE} 1),
    2.25 -           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
    2.26 +           REPEAT (resolve_tac (rev isodefl_rules @ prems) 1 ORELSE atac 1)])
    2.27        end
    2.28      val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
    2.29      fun conjuncts [] _ = []
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Aug 16 14:42:35 2014 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Aug 16 16:18:39 2014 +0200
     3.3 @@ -131,11 +131,11 @@
     3.4  
     3.5  val get_rec_tab = Rec_Data.get
     3.6  fun get_deflation_thms thy =
     3.7 -  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation}
     3.8 +  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation})
     3.9  
    3.10  val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID}
    3.11  fun get_map_ID_thms thy =
    3.12 -  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID}
    3.13 +  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID})
    3.14  
    3.15  
    3.16  (******************************************************************************)
     4.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sat Aug 16 14:42:35 2014 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Aug 16 16:18:39 2014 +0200
     4.3 @@ -131,7 +131,7 @@
     4.4            "The error occurred for the goal statement:\n" ^
     4.5            Syntax.string_of_term lthy prop)
     4.6          val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
     4.7 -        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules))
     4.8 +        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)))
     4.9          val slow_tac = SOLVED' (simp_tac lthy)
    4.10          val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
    4.11        in