src/HOL/Transitive_Closure.thy
changeset 32215 87806301a813
parent 31970 ccaadfcf6941
child 32235 8f9b8d14fc9f
     1.1 --- a/src/HOL/Transitive_Closure.thy	Sun Jul 26 22:24:13 2009 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Sun Jul 26 22:28:31 2009 +0200
     1.3 @@ -811,16 +811,16 @@
     1.4  
     1.5  ML {*
     1.6  
     1.7 -structure Trancl_Tac = Trancl_Tac_Fun (
     1.8 -  struct
     1.9 -    val r_into_trancl = @{thm trancl.r_into_trancl};
    1.10 -    val trancl_trans  = @{thm trancl_trans};
    1.11 -    val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
    1.12 -    val r_into_rtrancl = @{thm r_into_rtrancl};
    1.13 -    val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
    1.14 -    val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
    1.15 -    val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
    1.16 -    val rtrancl_trans = @{thm rtrancl_trans};
    1.17 +structure Trancl_Tac = Trancl_Tac
    1.18 +(
    1.19 +  val r_into_trancl = @{thm trancl.r_into_trancl};
    1.20 +  val trancl_trans  = @{thm trancl_trans};
    1.21 +  val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
    1.22 +  val r_into_rtrancl = @{thm r_into_rtrancl};
    1.23 +  val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
    1.24 +  val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
    1.25 +  val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
    1.26 +  val rtrancl_trans = @{thm rtrancl_trans};
    1.27  
    1.28    fun decomp (@{const Trueprop} $ t) =
    1.29      let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
    1.30 @@ -832,19 +832,18 @@
    1.31        | dec _ =  NONE
    1.32      in dec t end
    1.33      | decomp _ = NONE;
    1.34 -
    1.35 -  end);
    1.36 +);
    1.37  
    1.38 -structure Tranclp_Tac = Trancl_Tac_Fun (
    1.39 -  struct
    1.40 -    val r_into_trancl = @{thm tranclp.r_into_trancl};
    1.41 -    val trancl_trans  = @{thm tranclp_trans};
    1.42 -    val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
    1.43 -    val r_into_rtrancl = @{thm r_into_rtranclp};
    1.44 -    val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
    1.45 -    val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
    1.46 -    val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
    1.47 -    val rtrancl_trans = @{thm rtranclp_trans};
    1.48 +structure Tranclp_Tac = Trancl_Tac
    1.49 +(
    1.50 +  val r_into_trancl = @{thm tranclp.r_into_trancl};
    1.51 +  val trancl_trans  = @{thm tranclp_trans};
    1.52 +  val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
    1.53 +  val r_into_rtrancl = @{thm r_into_rtranclp};
    1.54 +  val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
    1.55 +  val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
    1.56 +  val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
    1.57 +  val rtrancl_trans = @{thm rtranclp_trans};
    1.58  
    1.59    fun decomp (@{const Trueprop} $ t) =
    1.60      let fun dec (rel $ a $ b) =
    1.61 @@ -856,31 +855,31 @@
    1.62        | dec _ =  NONE
    1.63      in dec t end
    1.64      | decomp _ = NONE;
    1.65 -
    1.66 -  end);
    1.67 +);
    1.68  *}
    1.69  
    1.70  declaration {* fn _ =>
    1.71    Simplifier.map_ss (fn ss => ss
    1.72 -    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    1.73 -    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
    1.74 -    addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
    1.75 -    addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)))
    1.76 +    addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
    1.77 +    addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
    1.78 +    addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
    1.79 +    addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
    1.80  *}
    1.81  
    1.82 -(* Optional methods *)
    1.83 +
    1.84 +text {* Optional methods. *}
    1.85  
    1.86  method_setup trancl =
    1.87 -  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
    1.88 +  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac) *}
    1.89    {* simple transitivity reasoner *}
    1.90  method_setup rtrancl =
    1.91 -  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
    1.92 +  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac) *}
    1.93    {* simple transitivity reasoner *}
    1.94  method_setup tranclp =
    1.95 -  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
    1.96 +  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac) *}
    1.97    {* simple transitivity reasoner (predicate version) *}
    1.98  method_setup rtranclp =
    1.99 -  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
   1.100 +  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac) *}
   1.101    {* simple transitivity reasoner (predicate version) *}
   1.102  
   1.103  end