signature REWRITE_TOOLS =

 signature REWRITE_TOOLS =

 sig

 sig

   type deriv

   type deriv

   val contains_rule : rule -> rls -> bool

   val contains_rule : rule -> rls -> bool

   val thy_containing_rls : theory' -> rls' -> string * theory'

   val thy_containing_rls : theory' -> rls' -> string * theory'

   val thy_containing_cal : theory' -> prog_calcID -> string * string

   val thy_containing_cal : theory' -> prog_calcID -> string * string

   datatype contthy

   datatype contthy

   = ContNOrew of {applto: term, thm_rls: guh, thyID: thyID}

   = ContNOrew of {applto: term, thm_rls: guh, thyID: thyID}

      | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: guh, thminst: term, thyID: thyID}

      | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: guh, thminst: term, thyID: thyID}

   val sym_drop : thmID -> thmID val sym_rls : rls -> rls

   val sym_drop : thmID -> thmID val sym_rls : rls -> rls

   val sym_rule : rule -> rule

   val sym_rule : rule -> rule

   val thms_of_rls : rls -> rule list

   val thms_of_rls : rls -> rule list

   val theID2filename : theID -> filename

   val theID2filename : theID -> filename

   val no_thycontext : guh -> bool

   val no_thycontext : guh -> bool

   val distinct_Thm : rule list -> rule list

   val distinct_Thm : rule list -> rule list

   val eq_Thms : string list -> rule -> bool

   val eq_Thms : string list -> rule -> bool

   val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->

   val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->

     term option -> term -> deriv

     term option -> term -> deriv

   val reverse_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->

   val reverse_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->

     term option -> term -> (rule * (term * term list)) list

     term option -> term -> (rule * (term * term list)) list

   val thy_containing_thm : string -> string * string val thypart2filename : theID -> filename

   val thy_containing_thm : string -> string * string val thypart2filename : theID -> filename

   val guh2theID : guh -> theID

   val guh2theID : guh -> theID

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   val trtas2str : (term * rule * (term * term list)) list -> string

   val trtas2str : (term * rule * (term * term list)) list -> string

   val eq_Thm : rule * rule -> bool

   val eq_Thm : rule * rule -> bool

      applto  : term	      (*rewrite this formula               .*)

      applto  : term	      (*rewrite this formula               .*)

    	}						 

    	}						 

 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718

 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718

    pass other tacs unchanged.*)

    pass other tacs unchanged.*)

 (* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)

 (* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)

 fun deriv_of_thm'' ((thmID, _) : thm'') =

 fun deriv_of_thm'' ((thmID, _) : thm'') =

   thmID |> Global_Theory.get_thm (Isac ()) |> Thm.get_name_hint

   thmID |> Global_Theory.get_thm (Isac ()) |> Thm.get_name_hint

 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)

 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)

     let val thm_deriv = deriv_of_thm'' thm''

     let val thm_deriv = deriv_of_thm'' thm''

     in

     in

     (case Applicable.applicable_in pos pt tac of

     (case Applicable.applicable_in pos pt tac of

         ContThm

         ContThm

          {thyID = theory'2thyID thy',

          {thyID = theory'2thyID thy',

           thm = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

           thm = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

           applto = f, applat  = e_term, reword  = ord',

           applto = f, applat  = e_term, reword  = ord',

           asms = [](*asms ~~ asms'*), lhs = (e_term, e_term)(*(lhs, lhs')*), rhs = (e_term, e_term)(*(rhs, rhs')*),

           asms = [](*asms ~~ asms'*), lhs = (e_term, e_term)(*(lhs, lhs')*), rhs = (e_term, e_term)(*(rhs, rhs')*),

           result = res, resasms = asm, asmrls  = id_rls erls}

           result = res, resasms = asm, asmrls  = id_rls erls}

      | Chead.Notappl _ =>

      | Chead.Notappl _ =>

          let

          let

            val f = case p_ of

            val f = case p_ of

          in

          in

            ContNOrew

            ContNOrew

             {thyID   = theory'2thyID thy',

             {thyID   = theory'2thyID thy',

              thm_rls = 

              thm_rls = 

                thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

                thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

              applto  = f}

              applto  = f}

 		     end

 		     end

      | _ => error "context_thy..Rewrite: uncovered case 2")

      | _ => error "context_thy..Rewrite: uncovered case 2")

     end

     end

     let val thm = Global_Theory.get_thm (Isac ()) thmID

     let val thm = Global_Theory.get_thm (Isac ()) thmID

     in

     in

 	  (case Applicable.applicable_in pos pt tac of

 	  (case Applicable.applicable_in pos pt tac of

 	       let

 	       let

            val thm_deriv = Thm.get_name_hint thm

            val thm_deriv = Thm.get_name_hint thm

            val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)

            val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)

 	       in

 	       in

 	         ContThmInst

 	         ContThmInst

 	       end

 	       end

      | Chead.Notappl _ =>

      | Chead.Notappl _ =>

          let

          let

            val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID

            val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID

            val thm_deriv = Thm.get_name_hint thm

            val thm_deriv = Thm.get_name_hint thm

            val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)

            val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)

            val f = case p_ of

            val f = case p_ of

          in

          in

            ContNOrewInst

            ContNOrewInst

             {thyID = theory'2thyID thy',

             {thyID = theory'2thyID thy',

              thm_rls = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

              thm_rls = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

              bdvs = subst, thminst = thminst, applto = f}

              bdvs = subst, thminst = thminst, applto = f}

          end

          end

       | _ => error "context_thy..Rewrite_Inst: uncovered case 4")

       | _ => error "context_thy..Rewrite_Inst: uncovered case 4")

     end

     end

     (case Applicable.applicable_in p pt tac of

     (case Applicable.applicable_in p pt tac of

          ContRls

          ContRls

           {thyID = theory'2thyID thy',

           {thyID = theory'2thyID thy',

            rls = rls2guh (thy_containing_rls thy' rls') rls',

            rls = rls2guh (thy_containing_rls thy' rls') rls',

            applto = f, result = res, asms = asm}

            applto = f, result = res, asms = asm}

      | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))

      | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))

     (case Applicable.applicable_in p pt tac of

     (case Applicable.applicable_in p pt tac of

          ContRlsInst

          ContRlsInst

           {thyID = theory'2thyID thy',

           {thyID = theory'2thyID thy',

            rls = rls2guh (thy_containing_rls thy' rls') rls',

            rls = rls2guh (thy_containing_rls thy' rls') rls',

            bdvs = subst, applto = f, result = res, asms = asm}

            bdvs = subst, applto = f, result = res, asms = asm}

      | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))

      | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))

   | context_thy (_, p) tac =

   | context_thy (_, p) tac =

 (* get all theorems in a rule set (recursivley containing rule sets) *)

 (* get all theorems in a rule set (recursivley containing rule sets) *)

 fun thm_of_rule Erule = []

 fun thm_of_rule Erule = []

   | thm_of_rule (thm as Thm _) = [thm]

   | thm_of_rule (thm as Thm _) = [thm]

   | thm_of_rule (Calc _) = []

   | thm_of_rule (Calc _) = []

 (* try if a rewrite-rule is applicable to a given formula; 

 (* try if a rewrite-rule is applicable to a given formula; 

    in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 

    in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 

 fun try_rew thy ((_, ro) : rew_ord) erls (subst : subst) f (thm' as Thm (_, thm)) =

 fun try_rew thy ((_, ro) : rew_ord) erls (subst : subst) f (thm' as Thm (_, thm)) =

     if contains_bdv thm

     if contains_bdv thm

     then case rewrite_inst_ thy ro erls false subst thm f of

     then case rewrite_inst_ thy ro erls false subst thm f of

 	  | NONE => []

 	  | NONE => []

     else (case rewrite_ thy ro erls false thm f of

     else (case rewrite_ thy ro erls false thm f of

 	  | NONE => [])

 	  | NONE => [])

   | try_rew thy _ _ _ f (cal as Calc c) = 

   | try_rew thy _ _ _ f (cal as Calc c) = 

     (case adhoc_thm thy c f of

     (case adhoc_thm thy c f of

     | NONE => [])

     | NONE => [])

   | try_rew thy _ _ _ f (cal as Cal1 c) = 

   | try_rew thy _ _ _ f (cal as Cal1 c) = 

     (case adhoc_thm thy c f of

     (case adhoc_thm thy c f of

       | NONE => [])

       | NONE => [])

   | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls

   | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls

   | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"

   | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"

 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules, ...}) = 

 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules, ...}) = 

   | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) = 

   | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) = 

   | filter_appl_rews _ _ _ (Rrls _) = []

   | filter_appl_rews _ _ _ (Rrls _) = []

   | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"

   | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"

 (* decide if a tactic is applicable to a given formula; 

 (* decide if a tactic is applicable to a given formula; 

    in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)

    in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)

     try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))

     try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))

     try_rew thy (ro, assoc_rew_ord ro) erls [] f (Thm thm'')

     try_rew thy (ro, assoc_rew_ord ro) erls [] f (Thm thm'')

     filter_appl_rews thy [] f (assoc_rls rls')

     filter_appl_rews thy [] f (assoc_rls rls')

   | atomic_appl_tacs _ _ _ _ tac = 

   | atomic_appl_tacs _ _ _ _ tac = 

 (* filenames not only for thydata, but also for thy's etc *)

 (* filenames not only for thydata, but also for thy's etc *)

 fun theID2filename (theID : theID) = theID2guh theID ^ ".xml" : filename

 fun theID2filename (theID : theID) = theID2guh theID ^ ".xml" : filename

 fun guh2theID (guh : guh) =

 fun guh2theID (guh : guh) =

 	    end	

 	    end	

     end

     end

 fun guh2filename (guh : guh) = guh ^ ".xml" : filename;

 fun guh2filename (guh : guh) = guh ^ ".xml" : filename;

     let

     let

       val (_, thy, sect, xstr) = case guh2theID guh of

       val (_, thy, sect, xstr) = case guh2theID guh of

         [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

         [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

       | _ => error "guh2rewtac: uncovered case"

       | _ => error "guh2rewtac: uncovered case"

     in case sect of

     in case sect of

     | _ => error ("guh2rewtac: not impl. for '"^xstr^"'") 

     | _ => error ("guh2rewtac: not impl. for '"^xstr^"'") 

     end

     end

   | guh2rewtac guh subs =

   | guh2rewtac guh subs =

     let

     let

       val (_, thy, sect, xstr) = case guh2theID guh of

       val (_, thy, sect, xstr) = case guh2theID guh of

         [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

         [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

       | _ => error "guh2rewtac: uncovered case"

       | _ => error "guh2rewtac: uncovered case"

     in case sect of

     in case sect of

       "Theorems" => 

       "Theorems" => 

     | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'") 

     | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'") 

     end

     end

 (* the front-end may request a context for any element of the hierarchy *)

 (* the front-end may request a context for any element of the hierarchy *)

 fun no_thycontext (guh : guh) = (guh2theID guh; false)

 fun no_thycontext (guh : guh) = (guh2theID guh; false)

    # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst

    # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst

    # instantiate this subs with the istates env to [(bdv, x),..]

    # instantiate this subs with the istates env to [(bdv, x),..]

    # otherwise []

    # otherwise []

    WN060617 hack assuming that all scripts use only one bound variable

    WN060617 hack assuming that all scripts use only one bound variable

    and use 'v_' as the formal argument for this bound variable*)

    and use 'v_' as the formal argument for this bound variable*)

     let

     let

       val (_, _, thyID, sect, xstr) = case guh2theID guh of

       val (_, _, thyID, sect, xstr) = case guh2theID guh of

         theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)

         theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)

       | _ => error "subs_from: uncovered case"

       | _ => error "subs_from: uncovered case"

     in

     in

             if contains_bdv thm

             if contains_bdv thm

             then

             then

               let

               let

                 val formal_arg = str2term "v_"

                 val formal_arg = str2term "v_"

                 val value = subst_atomic env formal_arg

                 val value = subst_atomic env formal_arg

             else []

             else []

 	        end

 	        end

   	  | "Rulesets" => 

   	  | "Rulesets" => 

         let

         let

           val rules = (get_rules o assoc_rls) xstr

           val rules = (get_rules o assoc_rls) xstr

           if contain_bdv rules

           if contain_bdv rules

           then

           then

             let

             let

               val formal_arg = str2term "v_"

               val formal_arg = str2term "v_"

               val value = subst_atomic env formal_arg

               val value = subst_atomic env formal_arg

           else []

           else []

         end

         end

       | str => error ("subs_from: uncovered case with " ^ str)

       | str => error ("subs_from: uncovered case with " ^ str)

     end

     end

   | subs_from _ _ (guh : guh) = error ("subs_from: uncovered case with " ^ guh)

   | subs_from _ _ (guh : guh) = error ("subs_from: uncovered case with " ^ guh)

         if is_bdv_subst t then SOME t else NONE

         if is_bdv_subst t then SOME t else NONE

       | scan (Abs (_, _, body)) = scan body

       | scan (Abs (_, _, body)) = scan body

       | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst

       | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst

   in

   in

     case scan prog of

     case scan prog of

     | SOME tm =>

     | SOME tm =>

         let val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair

         let val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair

           (* "[(bdv,v_v)]": term

           (* "[(bdv,v_v)]": term

                           |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list

                           |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list

                                                          |> [("bdv","x")]: (term * term) list *)

                                                          |> [("bdv","x")]: (term * term) list *)

           (*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)

           (*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)

   end

   end

 end

 end