src/HOL/Transitive_Closure.thy
changeset 15076 4b3d280ef06a
parent 14565 c6dc17aab88a
child 15096 be1d3b8cfbd5
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jul 22 19:33:12 2004 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jul 26 15:48:50 2004 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  header {* Reflexive and Transitive closure of a relation *}
     1.6  
     1.7 -theory Transitive_Closure = Inductive:
     1.8 +theory Transitive_Closure = Inductive
     1.9 +
    1.10 +files ("../Provers/trancl.ML"):
    1.11  
    1.12  text {*
    1.13    @{text rtrancl} is reflexive/transitive closure,
    1.14 @@ -444,4 +446,62 @@
    1.15  declare rtranclE [cases set: rtrancl]
    1.16  declare tranclE [cases set: trancl]
    1.17  
    1.18 +subsection {* Setup of transitivity reasoner *}
    1.19 +
    1.20 +use "../Provers/trancl.ML";
    1.21 +
    1.22 +ML_setup {*
    1.23 +
    1.24 +structure Trancl_Tac = Trancl_Tac_Fun (
    1.25 +  struct
    1.26 +    val r_into_trancl = thm "r_into_trancl";
    1.27 +    val trancl_trans  = thm "trancl_trans";
    1.28 +    val rtrancl_refl = thm "rtrancl_refl";
    1.29 +    val r_into_rtrancl = thm "r_into_rtrancl";
    1.30 +    val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    1.31 +    val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
    1.32 +    val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
    1.33 +    val rtrancl_trans = thm "rtrancl_trans";
    1.34 +(*
    1.35 +  fun decomp (Trueprop $ t) = 
    1.36 +    let fun dec (Const ("op :", _) $ t1 $ t2 ) = 
    1.37 +	let fun dec1  (Const ("Pair", _) $ a $ b) =  (a,b);
    1.38 +	    fun dec2 (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
    1.39 +	      | dec2 (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
    1.40 +	      | dec2 r = (r,"r");
    1.41 +	    val (a,b) = dec1 t1;
    1.42 +	    val (rel,r) = dec2 t2;
    1.43 +	in Some (a,b,rel,r) end
    1.44 +      | dec _ =  None 
    1.45 +    in dec t end;
    1.46 +*)
    1.47 +  fun decomp (Trueprop $ t) = 
    1.48 +    let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = 
    1.49 +	let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
    1.50 +	      | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
    1.51 +	      | decr r = (r,"r");
    1.52 +	    val (rel,r) = decr rel;
    1.53 +	in Some (a,b,rel,r) end
    1.54 +      | dec _ =  None 
    1.55 +    in dec t end;
    1.56 +  
    1.57 +  end); (* struct *)
    1.58 +
    1.59 +simpset_ref() := simpset ()
    1.60 +    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    1.61 +    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac));
    1.62 +
    1.63 +*}
    1.64 +
    1.65 +(* Optional methods
    1.66 +
    1.67 +method_setup trancl =
    1.68 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
    1.69 +  {* simple transitivity reasoner *}	    
    1.70 +method_setup rtrancl =
    1.71 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
    1.72 +  {* simple transitivity reasoner *}
    1.73 +
    1.74 +*)
    1.75 +
    1.76  end