src/Tools/isac/ME/rewtools.sml
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 19 Aug 2010 15:02:06 +0200
branchisac-update-Isa09-2
changeset 37930 f2b8d1b3fcc2
parent 37926 e6fc98fbcb85
child 37935 27d365c3dd31
permissions -rw-r--r--
infix mem union --> member union op = ...

\\ --> subtract op = [4,5,6,7] [1,2,3,4,5] -> [1, 2, 3]
missed due to problem with grep '\\'
neuper@37906
     1
(* tools for rewriting, reverse rewriting, context to thy concerning rewriting
neuper@37906
     2
   authors: Walther Neuper 2002, 2006
neuper@37906
     3
  (c) due to copyright terms
neuper@37906
     4
neuper@37906
     5
use"ME/rewtools.sml";
neuper@37906
     6
use"rewtools.sml";
neuper@37906
     7
*)
neuper@37906
     8
neuper@37906
     9
neuper@37906
    10
neuper@37906
    11
(***.reverse rewriting.***)
neuper@37906
    12
neuper@37906
    13
(*.derivation for insertin one level of nodes into the calctree.*)
neuper@37906
    14
type deriv  = (term * rule * (term *term list)) list;
neuper@37906
    15
neuper@37906
    16
fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str' r)^", ("^
neuper@37906
    17
			    (term2str t')^", "^(terms2str a)^"))";
neuper@37906
    18
fun trtas2str trtas = (strs2str o (map trta2str)) trtas;
neuper@37906
    19
val deriv2str = trtas2str;
neuper@37906
    20
fun rta2str (r,(t,a)) = "\n("^(rule2str' r)^", ("^
neuper@37906
    21
			    (term2str t)^", "^(terms2str a)^"))";
neuper@37906
    22
fun rtas2str rtas = (strs2str o (map rta2str)) rtas;
neuper@37906
    23
val deri2str = rtas2str;
neuper@37906
    24
neuper@37906
    25
neuper@37906
    26
(*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*)
neuper@37906
    27
fun sym_thm thm =
neuper@37906
    28
  let 
neuper@37906
    29
    val {sign_ref = sign_ref, der = der, maxidx = maxidx,
neuper@37906
    30
	    shyps = shyps, hyps = hyps, (*tpairs = tpairs,*) prop = prop} = 
neuper@37906
    31
	rep_thm_G thm;
neuper@37906
    32
    val (lhs,rhs) = (dest_equals' o strip_trueprop 
neuper@37906
    33
		     o Logic.strip_imp_concl) prop;
neuper@37906
    34
    val prop' = case strip_imp_prems' prop of
neuper@37926
    35
		   NONE => Trueprop $ (mk_equality (rhs, lhs))
neuper@37926
    36
		 | SOME cs => 
neuper@37906
    37
		   ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
neuper@37906
    38
  in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;
neuper@37906
    39
(*
neuper@37906
    40
  (sym RS real_mult_div_cancel1) handle e => print_exn e;
neuper@37906
    41
Exception THM 1 raised:
neuper@37906
    42
RSN: no unifiers
neuper@37906
    43
"?s = ?t ==> ?t = ?s"
neuper@37906
    44
"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"
neuper@37906
    45
neuper@37906
    46
  val thm = real_mult_div_cancel1;
neuper@37906
    47
  val prop = (#prop o rep_thm) thm;
neuper@37906
    48
  atomt prop;
neuper@37906
    49
  val ppp = Logic.strip_imp_concl prop;
neuper@37906
    50
  atomt ppp;
neuper@37906
    51
  ((#prop o rep_thm o sym_thm o sym_thm) thm) = (#prop o rep_thm) thm;
neuper@37906
    52
val it = true : bool
neuper@37906
    53
  ((sym_thm o sym_thm) thm) = thm;
neuper@37906
    54
val it = true : bool
neuper@37906
    55
neuper@37906
    56
  val thm = real_le_anti_sym;
neuper@37906
    57
  ((sym_thm o sym_thm) thm) = thm;
neuper@37906
    58
val it = true : bool
neuper@37906
    59
neuper@37906
    60
  val thm = real_minus_zero;
neuper@37906
    61
  ((sym_thm o sym_thm) thm) = thm;
neuper@37906
    62
val it = true : bool
neuper@37906
    63
*)
neuper@37906
    64
neuper@37906
    65
neuper@37906
    66
neuper@37926
    67
(*.derive normalform of a rls, or derive until SOME goal,
neuper@37906
    68
   and record rules applied and rewrites.
neuper@37906
    69
val it = fn
neuper@37906
    70
  : theory
neuper@37906
    71
    -> rls
neuper@37906
    72
    -> rule list
neuper@37906
    73
    -> rew_ord       : the order of this rls, which 1 theorem of is used 
neuper@37906
    74
                       for rewriting 1 single step (?14.4.03)
neuper@37906
    75
    -> term option   : 040214 ??? nonsense ??? 
neuper@37906
    76
    -> term 
neuper@37906
    77
    -> (term *       : to this term ...
neuper@37906
    78
        rule * 	     : ... this rule is applied yielding ...
neuper@37906
    79
        (term *      : ... this term ...
neuper@37906
    80
         term list)) : ... under these assumptions.
neuper@37906
    81
       list          :
neuper@37906
    82
returns empty list for a normal form
neuper@37906
    83
FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
neuper@37906
    84
neuper@37906
    85
WN060825 too complicated for the intended use by cancel_, common_nominator_
neuper@37906
    86
and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
neuper@37906
    87
 -- replaced below*)
neuper@37906
    88
(* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);
neuper@37926
    89
   val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, NONE, tt);
neuper@37906
    90
   *)
neuper@37906
    91
fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt = 
neuper@37906
    92
    let datatype switch = Appl | Noap
neuper@37906
    93
	fun rew_once lim rts t Noap [] = 
neuper@37906
    94
	    (case goal of 
neuper@37926
    95
		 NONE => rts
neuper@37926
    96
	       | SOME g => 
neuper@37906
    97
		 raise error ("make_deriv: no derivation for "^(term2str t)))
neuper@37906
    98
	  | rew_once lim rts t Appl [] = 
neuper@37906
    99
	    (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
neuper@37906
   100
	  (*| Seq _ => rts) FIXXXXXME 14.3.03*)
neuper@37906
   101
	  | rew_once lim rts t apno rs' =
neuper@37906
   102
	    (case goal of 
neuper@37926
   103
		 NONE => rew_or_calc lim rts t apno rs'
neuper@37926
   104
	       | SOME g =>
neuper@37906
   105
		 if g = t then rts
neuper@37906
   106
		 else rew_or_calc lim rts t apno rs')
neuper@37906
   107
	and rew_or_calc lim rts t apno (rrs' as (r::rs')) =
neuper@37906
   108
	    if lim < 0 
neuper@37906
   109
	    then (writeln ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
neuper@37906
   110
			   "with deriv =\n"); writeln (deriv2str rts); rts)
neuper@37906
   111
	    else
neuper@37906
   112
	    case r of
neuper@37906
   113
		Thm (thmid, tm) =>
neuper@37906
   114
		(if not (!trace_rewrite) then () else
neuper@37906
   115
		 writeln ("### trying thm '" ^ thmid ^ "'");
neuper@37906
   116
		 case rewrite_ thy ro erls true tm t of
neuper@37926
   117
		     NONE => rew_once lim rts t apno rs'
neuper@37926
   118
		   | SOME (t',a') =>
neuper@37906
   119
		     (if ! trace_rewrite 
neuper@37906
   120
		      then writeln ("### rewrites to: "^(term2str t')) else();
neuper@37906
   121
		      rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))
neuper@37906
   122
	      | Calc (c as (op_,_)) => 
neuper@37906
   123
		let val _ = if not (!trace_rewrite) then () else
neuper@37906
   124
			    writeln ("### trying calc. '" ^ op_ ^ "'")
neuper@37906
   125
		    val t = uminus_to_string t
neuper@37906
   126
		in case get_calculation_ thy c t of
neuper@37926
   127
		       NONE => rew_once lim rts t apno rs'
neuper@37926
   128
		     | SOME (thmid, tm) => 
neuper@37926
   129
		       (let val SOME (t',a') = rewrite_ thy ro erls true tm t
neuper@37906
   130
			    val _ = if not (!trace_rewrite) then () else
neuper@37906
   131
				    writeln("### calc. to: " ^ (term2str t'))
neuper@37906
   132
			    val r' = Thm (thmid, tm)
neuper@37906
   133
			in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
neuper@37906
   134
			end) 
neuper@37906
   135
		       handle _ => raise error "derive_norm, Calc: no rewrite"
neuper@37906
   136
		end
neuper@37906
   137
(* TODO.WN080222: see rewrite__set_
neuper@37906
   138
   @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
neuper@37906
   139
      | Cal1 (cc as (op_,_)) => 
neuper@37906
   140
	  (let val _= if !trace_rewrite andalso i < ! depth then
neuper@37906
   141
		      writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
neuper@37906
   142
	     val ct = uminus_to_string ct
neuper@37906
   143
	   in case get_calculation_ thy cc ct of
neuper@37926
   144
	     NONE => (ct, asm)
neuper@37926
   145
	   | SOME (thmid, thm') =>
neuper@37906
   146
	       let 
neuper@37906
   147
		 val pairopt = 
neuper@37906
   148
		   rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
neuper@37906
   149
		   ((#erls o rep_rls) rls) put_asm thm' ct;
neuper@37926
   150
		 val _ = if pairopt <> NONE then () 
neuper@37906
   151
			 else raise error("rewrite_set_, rewrite_ \""^
neuper@37926
   152
			 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
neuper@37906
   153
		 val _ = if ! trace_rewrite andalso i < ! depth 
neuper@37906
   154
			   then writeln((idt"="(i+1))^" cal1. to: "^
neuper@37906
   155
					(term2str ((fst o the) pairopt)))
neuper@37906
   156
			 else()
neuper@37906
   157
	       in the pairopt end
neuper@37906
   158
	   end)
neuper@37906
   159
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
neuper@37906
   160
	      | Rls_ rls => 
neuper@37906
   161
		(case rewrite_set_ thy true rls t of
neuper@37926
   162
		     NONE => rew_once lim rts t apno rs'
neuper@37926
   163
		   | SOME (t',a') =>
neuper@37906
   164
		     rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');
neuper@37906
   165
(*WN060829    | Rls_ rls => 
neuper@37906
   166
		(case rewrite_set_ thy true rls t of
neuper@37926
   167
		     NONE => rew_once lim rts t apno rs'
neuper@37926
   168
		   | SOME (t',a') =>
neuper@37906
   169
		     if ro [] (t, t') then rew_once lim rts t apno rs'
neuper@37906
   170
		     else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs');
neuper@37906
   171
...lead to deriv = [] with make_polynomial.
neuper@37906
   172
THERE IS SOMETHING DIFFERENT beetween rewriting with the code above
neuper@37906
   173
and between rewriting with rewrite_set: with rules from make_polynomial and 
neuper@37906
   174
t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code
neuper@37906
   175
leads to cycling  Rls_ order_mult_rls_..Rls_ discard_parentheses_..Rls_ order..
neuper@37906
   176
*)
neuper@37906
   177
    in rew_once (!lim_deriv) [] tt Noap rs end;
neuper@37906
   178
neuper@37906
   179
neuper@37906
   180
(*.toggles the marker for 'fun sym_thm'.*)
neuper@37906
   181
fun sym_thmID (thmID : thmID) =
neuper@37906
   182
    case explode thmID of
neuper@37906
   183
	"s"::"y"::"m"::"_"::id => implode id : thmID
neuper@37906
   184
      | id => "sym_"^thmID;
neuper@37906
   185
(* 
neuper@37906
   186
> val thmID = "sym_real_mult_2";
neuper@37906
   187
> sym_thmID thmID;
neuper@37906
   188
val it = "real_mult_2" : string
neuper@37906
   189
> val thmID = "real_num_collect";
neuper@37906
   190
> sym_thmID thmID;
neuper@37906
   191
val it = "sym_real_num_collect" : string*)
neuper@37906
   192
fun sym_drop (thmID : thmID) =
neuper@37906
   193
    case explode thmID of
neuper@37906
   194
	"s"::"y"::"m"::"_"::id => implode id : thmID
neuper@37906
   195
      | id => thmID;
neuper@37906
   196
fun is_sym (thmID : thmID) =
neuper@37906
   197
    case explode thmID of
neuper@37906
   198
	"s"::"y"::"m"::"_"::id => true
neuper@37906
   199
      | id => false;
neuper@37906
   200
neuper@37906
   201
neuper@37906
   202
(*FIXXXXME.040219: detail has to handle Rls id="sym_..." 
neuper@37906
   203
  by applying make_deriv, rev_deriv'; see concat_deriv*)
neuper@37906
   204
fun sym_rls Erls = Erls
neuper@37906
   205
  | sym_rls (Rls {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =
neuper@37906
   206
    Rls {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls, 
neuper@37906
   207
	 rules=rules, rew_ord=rew_ord, preconds=preconds}
neuper@37906
   208
  | sym_rls (Seq {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =
neuper@37906
   209
    Seq {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls, 
neuper@37906
   210
	 rules=rules, rew_ord=rew_ord, preconds=preconds}
neuper@37906
   211
  | sym_rls (Rrls {id, scr, calc, erls, prepat, rew_ord}) = 
neuper@37906
   212
    Rrls {id="sym_"^id, scr=scr, calc=calc, erls=erls, prepat=prepat, 
neuper@37906
   213
	  rew_ord=rew_ord};
neuper@37906
   214
neuper@37906
   215
fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
neuper@37906
   216
  | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
neuper@37906
   217
  | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
neuper@37906
   218
(*
neuper@37906
   219
  val th =  Thm ("real_one_collect",num_str real_one_collect);
neuper@37906
   220
  sym_Thm th;
neuper@37906
   221
val th =
neuper@37906
   222
  Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")
neuper@37906
   223
  : rule
neuper@37906
   224
ML> val it =
neuper@37906
   225
  Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)
neuper@37906
   226
neuper@37906
   227
neuper@37906
   228
(*version for reverse rewrite used before 040214*)
neuper@37906
   229
fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
neuper@37926
   230
(* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t');
neuper@37906
   231
   *)
neuper@37906
   232
fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
neuper@37906
   233
    (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);
neuper@37906
   234
(*
neuper@37906
   235
  val rev_rew = reverse_deriv thy e_rls ; 
neuper@37906
   236
  writeln(rtas2str rev_rew);
neuper@37906
   237
*)
neuper@37906
   238
neuper@37906
   239
fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2
neuper@37906
   240
  | eq_Thm (Thm (id1,_), _) = false
neuper@37906
   241
  | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2
neuper@37906
   242
  | eq_Thm (Rls_ r1, _) = false
neuper@37906
   243
  | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^
neuper@37906
   244
				(rule2str r1)^"' '"^(rule2str r2)^"'");
neuper@37906
   245
fun distinct_Thm r = gen_distinct eq_Thm r;
neuper@37906
   246
neuper@37930
   247
fun eq_Thms thmIDs thm = (member op = (id_of_thm thm) thmIDs)
neuper@37906
   248
    handle _ => false;
neuper@37906
   249
neuper@37906
   250
neuper@37906
   251
(***. context to thy concerning rewriting .***)
neuper@37906
   252
neuper@37906
   253
(*.create the unique handles and filenames for the theory-data.*)
neuper@37906
   254
fun part2guh ([str]:theID) =
neuper@37906
   255
    (case str of
neuper@37906
   256
	"Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
neuper@37906
   257
      | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
neuper@37906
   258
      | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
neuper@37906
   259
      | str => raise error ("thy2guh: called with '"^str^"'"))
neuper@37906
   260
  | part2guh theID = raise error ("part2guh called with theID = "
neuper@37906
   261
				  ^ theID2str theID);
neuper@37906
   262
fun part2filename str = part2guh str ^ ".xml" : filename;
neuper@37906
   263
neuper@37906
   264
neuper@37906
   265
fun thy2guh ([part, thyID]:theID) =
neuper@37906
   266
    (case part of
neuper@37906
   267
	"Isabelle" => "thy_isab_" ^ thyID : guh
neuper@37906
   268
      | "IsacScripts" => "thy_scri_" ^ thyID
neuper@37906
   269
      | "IsacKnowledge" => "thy_isac_" ^ thyID
neuper@37906
   270
      | str => raise error ("thy2guh: called with '"^str^"'"))
neuper@37906
   271
  | thy2guh theID = raise error ("thy2guh called with '"^strs2str' theID^"'");
neuper@37906
   272
fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;
neuper@37906
   273
fun thypart2guh ([part, thyID, thypart]:theID) = 
neuper@37906
   274
    case part of
neuper@37906
   275
	"Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
neuper@37906
   276
      | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
neuper@37906
   277
      | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
neuper@37906
   278
      | str => raise error ("thypart2guh: called with '"^str^"'");
neuper@37906
   279
fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;
neuper@37906
   280
neuper@37906
   281
(*.convert the data got via contextToThy to a globally unique handle
neuper@37906
   282
   there is another way to get the guh out of the 'theID' in the hierarchy.*)
neuper@37906
   283
fun thm2guh (isa, thyID:thyID) (thmID:thmID) =
neuper@37906
   284
    case isa of
neuper@37906
   285
	"Isabelle" => 
neuper@37906
   286
	"thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
neuper@37906
   287
    | "IsacKnowledge" =>
neuper@37906
   288
	"thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
neuper@37906
   289
    | "IsacScripts" =>
neuper@37906
   290
	"thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
neuper@37906
   291
    | str => raise error ("thm2guh called with isa = '"^isa^
neuper@37906
   292
			  "' for thm = "^thmID^"'");
neuper@37906
   293
fun thm2filename (isa_thyID: string * thyID) thmID =
neuper@37906
   294
    (thm2guh isa_thyID thmID) ^ ".xml" : filename;
neuper@37906
   295
neuper@37906
   296
fun rls2guh (isa, thyID:thyID) (rls':rls') =
neuper@37906
   297
    case isa of
neuper@37906
   298
	"Isabelle" => 
neuper@37906
   299
	    "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
neuper@37906
   300
    | "IsacKnowledge" =>
neuper@37906
   301
	    "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
neuper@37906
   302
    | "IsacScripts" =>
neuper@37906
   303
	    "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
neuper@37906
   304
    | str => raise error ("rls2guh called with isa = '"^isa^
neuper@37906
   305
			  "' for rls = '"^rls'^"'");
neuper@37906
   306
	fun rls2filename (isa, thyID) rls' =
neuper@37906
   307
    rls2guh (isa, thyID) rls' ^ ".xml" : filename;
neuper@37906
   308
neuper@37906
   309
fun cal2guh (isa, thyID:thyID) calID =
neuper@37906
   310
    case isa of
neuper@37906
   311
	"Isabelle" => 
neuper@37906
   312
	"thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
neuper@37906
   313
      | "IsacKnowledge" =>
neuper@37906
   314
	"thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
neuper@37906
   315
      | "IsacScripts" =>
neuper@37906
   316
	"thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
neuper@37906
   317
      | str => raise error ("cal2guh called with isa = '"^isa^
neuper@37906
   318
			  "' for cal = '"^calID^"'");
neuper@37906
   319
fun cal2filename (isa, thyID:thyID) calID = 
neuper@37906
   320
    cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;
neuper@37906
   321
neuper@37906
   322
fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') =
neuper@37906
   323
    case isa of
neuper@37906
   324
	"Isabelle" => 
neuper@37906
   325
	"thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
neuper@37906
   326
      | "IsacKnowledge" =>
neuper@37906
   327
	"thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
neuper@37906
   328
      | "IsacScripts" =>
neuper@37906
   329
	"thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
neuper@37906
   330
      | str => raise error ("ord2guh called with isa = '"^isa^
neuper@37906
   331
			  "' for ord = '"^rew_ord'^"'");
neuper@37906
   332
fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =
neuper@37906
   333
    ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;
neuper@37906
   334
neuper@37906
   335
neuper@37906
   336
(**.set up isab_thm_thy in Isac.ML.**)
neuper@37906
   337
neuper@37906
   338
fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm));
neuper@37906
   339
fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm));
neuper@37906
   340
neuper@37906
   341
(*.lookup the missing theorems in some thy (of Isabelle).*)
neuper@37906
   342
fun make_isa missthms thy =
neuper@37906
   343
    map (pair (theory2thyID thy)) 
neuper@37906
   344
	(curry (gen_inter eq_thmI) missthms (thms_of thy))
neuper@37906
   345
	: (thyID * (thmID * Thm.thm)) list;
neuper@37906
   346
neuper@37906
   347
(*.separate handling of sym_thms.*)
neuper@37906
   348
fun make_isab rlsthmsNOTisac isab_thys = 
neuper@37906
   349
    let fun les ((s1,_), (s2,_)) = (s1 : string) < s2
neuper@37906
   350
	val notsym = filter_out (is_sym o #1) rlsthmsNOTisac
neuper@37906
   351
	val notsym_isab = (flat o (map (make_isa notsym))) isab_thys
neuper@37906
   352
			  
neuper@37906
   353
	val sym = filter (is_sym o #1) rlsthmsNOTisac
neuper@37906
   354
		  
neuper@37906
   355
	val symsym = map ((apfst sym_drop) o (apsnd sym_thm)) sym
neuper@37906
   356
	val symsym_isab = (flat o (map (make_isa symsym))) isab_thys
neuper@37906
   357
			  
neuper@37906
   358
	val sym_isab = map (((apsnd o apfst) sym_drop) o 
neuper@37906
   359
			    ((apsnd o apsnd) sym_thm)) symsym_isab
neuper@37906
   360
		       
neuper@37906
   361
	val isab = notsym_isab @ symsym_isab @ sym_isab
neuper@37906
   362
    in ((map rearrange) o (gen_sort les)) isab 
neuper@37906
   363
       : (thmID * (thyID * Thm.thm)) list
neuper@37906
   364
    end;
neuper@37906
   365
neuper@37906
   366
(*.which theory below thy' contains a theorem; this can be in isabelle !
neuper@37906
   367
get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
neuper@37906
   368
(* val (str, (_, thy)) = ("real_diff_minus", ("Root.thy", Root.thy));
neuper@37906
   369
   val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));
neuper@37906
   370
   *)
neuper@37906
   371
fun thy_contains_thm (str:xstring) (_, thy) = 
neuper@37930
   372
    member str (map (strip_thy o fst) (thms_of thy));
neuper@37906
   373
(* val (thy', str) = ("Isac.thy", "real_mult_minus1");
neuper@37906
   374
   val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
neuper@37906
   375
   *)
neuper@37906
   376
fun thy_containing_thm (thy':theory') (str:xstring) =
neuper@37906
   377
    let val thy' = thyID2theory' thy'
neuper@37906
   378
	val str = sym_drop str
neuper@37906
   379
	val startsearch = dropuntil ((curry op= thy') o 
neuper@37906
   380
				     (#1:theory' * theory -> theory')) 
neuper@37906
   381
				    (rev (!theory'))
neuper@37906
   382
    in case find_first (thy_contains_thm str) startsearch of
neuper@37926
   383
	   SOME (thy',_) => ("IsacKnowledge", thy')
neuper@37926
   384
	 | NONE => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of
neuper@37926
   385
		     SOME (thyID,_) => ("Isabelle", thyID)
neuper@37926
   386
		   | NONE => 
neuper@37906
   387
		     raise error ("thy_containing_thm: theorem '"^str^
neuper@37906
   388
				  "' not in !theory' above thy '"^thy'^"'"))
neuper@37906
   389
    end;
neuper@37906
   390
neuper@37906
   391
neuper@37906
   392
(*.which theory below thy' contains a ruleset;
neuper@37906
   393
get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
neuper@37906
   394
(* val (thy', rls') = ("PolyEq.thy", "separate_bdv");
neuper@37906
   395
   *)
neuper@37906
   396
fun thy_containing_rls (thy':theory') (rls':rls') =
neuper@37906
   397
    let val rls' = strip_thy rls'
neuper@37906
   398
	val thy' = thyID2theory' thy'
neuper@37906
   399
	(*take thys between "Isac" and thy' not to search #1#*)
neuper@37906
   400
	val dropthys = takewhile [] (not o (curry op= thy') o 
neuper@37906
   401
				     (#1:theory' * theory -> theory')) 
neuper@37906
   402
				 (rev (!theory'))
neuper@37906
   403
	val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
neuper@37906
   404
			    dropthys
neuper@37906
   405
	(*drop those rulesets which are generated in a theory found in #1#*)
neuper@37906
   406
	val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
neuper@37906
   407
				      ((#1 o #2) : rls' * (theory' * rls) 
neuper@37906
   408
						   -> theory'))
neuper@37906
   409
				     (rev (!ruleset'))
neuper@37906
   410
    in case assoc (startsearch, rls') of
neuper@37926
   411
	   SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
neuper@37906
   412
	 | _ => raise error ("thy_containing_rls : rls '"^rls'^
neuper@37906
   413
			     "' not in !rulset' above thy '"^thy'^"'")
neuper@37906
   414
    end;
neuper@37906
   415
(* val (thy', termop) = (thyID, termop);
neuper@37906
   416
   *)
neuper@37906
   417
fun thy_containing_cal (thy':theory') termop =
neuper@37906
   418
    let val thy' = thyID2theory' thy'
neuper@37906
   419
	val dropthys = takewhile [] (not o (curry op= thy') o 
neuper@37906
   420
				     (#1:theory' * theory -> theory')) 
neuper@37906
   421
				 (rev (!theory'))
neuper@37906
   422
	val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
neuper@37906
   423
			    dropthys
neuper@37906
   424
	val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
neuper@37906
   425
				      (#1 : calc -> string)) (rev (!calclist'))
neuper@37906
   426
    in case assoc (startsearch, strip_thy termop) of
neuper@37926
   427
	   SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
neuper@37906
   428
	 | _ => raise error ("thy_containing_rls : rls '"^termop^
neuper@37906
   429
			     "' not in !calclist' above thy '"^thy'^"'")
neuper@37906
   430
    end;
neuper@37906
   431
	
neuper@37906
   432
(* print_depth 99; map #1 startsearch; print_depth 3;
neuper@37906
   433
   *)
neuper@37906
   434
neuper@37906
   435
(*.packing return-values to matchTheory, contextToThy for xml-generation.*)
neuper@37906
   436
datatype contthy =  (*also an item from KEStore on Browser ......#*)
neuper@37906
   437
	 EContThy   (*not from KEStore ...........................*)
neuper@37906
   438
       | ContThm of (*a theorem in contex =============*)
neuper@37906
   439
	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)
neuper@37906
   440
	  thm     : guh,           (*theorem in the context      .*)
neuper@37906
   441
	  applto  : term,	   (*applied to formula ...      .*)
neuper@37906
   442
	  applat  : term,	   (*...  with lhs inserted      .*)
neuper@37906
   443
	  reword  : rew_ord',      (*order used for rewrite      .*)
neuper@37906
   444
	  asms    : (term          (*asumption instantiated      .*)
neuper@37906
   445
		     * term) list, (*asumption evaluated         .*)
neuper@37906
   446
	  lhs     : term           (*lhs of the theorem ...      #*)
neuper@37906
   447
		    * term,        (*... instantiated            .*)
neuper@37906
   448
	  rhs     : term           (*rhs of the theorem ...      #*)
neuper@37906
   449
		    * term,        (*... instantiated            .*)
neuper@37906
   450
	  result  : term,	   (*resulting from the rewrite  .*)
neuper@37906
   451
	  resasms : term list,     (*... with asms stored        .*)
neuper@37906
   452
	  asmrls  : rls'           (*ruleset for evaluating asms .*)
neuper@37906
   453
		    }						 
neuper@37906
   454
	| ContThmInst of (*a theorem with bdvs in contex ======== *)
neuper@37906
   455
	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)
neuper@37906
   456
	  thm     : guh,           (*theorem in the context      .*)
neuper@37906
   457
	  bdvs    : subst,         (*bound variables to modify....*)
neuper@37906
   458
	  thminst : term,          (*... theorem instantiated    .*)
neuper@37906
   459
	  applto  : term,	   (*applied to formula ...      .*)
neuper@37906
   460
	  applat  : term,	   (*...  with lhs inserted      .*)
neuper@37906
   461
	  reword  : rew_ord',      (*order used for rewrite      .*)
neuper@37906
   462
	  asms    : (term          (*asumption instantiated      .*)
neuper@37906
   463
		     * term) list, (*asumption evaluated         .*)
neuper@37906
   464
	  lhs     : term           (*lhs of the theorem ...      #*)
neuper@37906
   465
		    * term,        (*... instantiated            .*)
neuper@37906
   466
	  rhs     : term           (*rhs of the theorem ...      #*)
neuper@37906
   467
		    * term,        (*... instantiated            .*)
neuper@37906
   468
	  result  : term,	   (*resulting from the rewrite  .*)
neuper@37906
   469
	  resasms : term list,     (*... with asms stored        .*)
neuper@37906
   470
	  asmrls  : rls'           (*ruleset for evaluating asms .*)
neuper@37906
   471
		      }						 
neuper@37906
   472
	| ContRls of (*a rule set in contex ===================== *)
neuper@37906
   473
	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)
neuper@37906
   474
	  rls     : guh,           (*rule set in the context     .*)
neuper@37906
   475
	  applto  : term,	   (*rewrite this formula        .*)
neuper@37906
   476
	  result  : term,	   (*resulting from the rewrite  .*)
neuper@37906
   477
	  asms    : term list      (*... with asms stored        .*)
neuper@37906
   478
		    }						 
neuper@37906
   479
	| ContRlsInst of (*a rule set with bdvs in contex ======= *)
neuper@37906
   480
	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)
neuper@37906
   481
	  rls     : guh,           (*rule set in the context     .*)
neuper@37906
   482
	  bdvs    : subst,         (*for bound variables in thms .*)
neuper@37906
   483
	  applto  : term,	   (*rewrite this formula        .*)
neuper@37906
   484
	  result  : term,	   (*resulting from the rewrite  .*)
neuper@37906
   485
	  asms    : term list      (*... with asms stored        .*)
neuper@37906
   486
		    }
neuper@37906
   487
	| ContNOrew of (*no rewrite for thm or rls ============== *)
neuper@37906
   488
	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)
neuper@37906
   489
	  thm_rls : guh,           (*thm or rls in the context   .*)
neuper@37906
   490
	  applto  : term	   (*rewrite this formula        .*)
neuper@37906
   491
		    }						 
neuper@37906
   492
	| ContNOrewInst of (*no rewrite for some instantiation == *)
neuper@37906
   493
	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)
neuper@37906
   494
	  thm_rls : guh,           (*thm or rls in the context   .*)
neuper@37906
   495
	  bdvs    : subst,         (*for bound variables in thms .*)
neuper@37906
   496
	  thminst : term,          (*... theorem instantiated    .*)
neuper@37906
   497
	  applto  : term	   (*rewrite this formula        .*)
neuper@37906
   498
		    };
neuper@37906
   499
neuper@37906
   500
(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
neuper@37906
   501
   pass other tacs unchanged.*)
neuper@37906
   502
fun get_tac_checked pt ((p,p_) : pos') = get_obj g_tac pt p;
neuper@37906
   503
neuper@37906
   504
(*..*)
neuper@37906
   505
neuper@37906
   506
neuper@37906
   507
neuper@37906
   508
(*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*)
neuper@37906
   509
(* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac';
neuper@37906
   510
   *)
neuper@37906
   511
fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) = 
neuper@37906
   512
    (case applicable_in pos pt tac of
neuper@37906
   513
	Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>
neuper@37906
   514
	let val thy = assoc_thy thy'
neuper@37906
   515
	    val thm = (norm o #prop o rep_thm o (get_thm thy)) thmID
neuper@37906
   516
    (*WN060616 the following must be done on subterm found _IN_ rew_sub
neuper@37906
   517
	val (lhs,rhs) = (dest_equals' o strip_trueprop 
neuper@37906
   518
			 o Logic.strip_imp_concl) thm
neuper@37906
   519
	val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)
neuper@37906
   520
	val thm' = ren_inst (insts, thm, lhs, f)
neuper@37906
   521
	val (lhs',rhs') = (dest_equals' o strip_trueprop 
neuper@37906
   522
			   o Logic.strip_imp_concl) thm'
neuper@37906
   523
	val asms = map strip_trueprop (Logic.strip_imp_prems thm)
neuper@37906
   524
	val asms' = map strip_trueprop (Logic.strip_imp_prems thm')
neuper@37906
   525
     *)
neuper@37906
   526
	in ContThm {thyID   = theory'2thyID thy',
neuper@37906
   527
		    thm     = thm2guh (thy_containing_thm thy' thmID) thmID,
neuper@37906
   528
		    applto  = f,
neuper@37906
   529
		    applat  = e_term,
neuper@37906
   530
		    reword  = ord',
neuper@37906
   531
		    asms    = [](*asms ~~ asms'*),
neuper@37906
   532
		    lhs     = (e_term, e_term)(*(lhs, lhs')*),
neuper@37906
   533
		    rhs     = (e_term, e_term)(*(rhs, rhs')*),
neuper@37906
   534
		    result  = res,
neuper@37906
   535
		    resasms = asm,
neuper@37906
   536
		    asmrls  = id_rls erls}
neuper@37906
   537
	end
neuper@37906
   538
      | Notappl _ =>
neuper@37906
   539
	let val pp = par_pblobj pt p
neuper@37906
   540
	    val thy' = get_obj g_domID pt pp
neuper@37906
   541
	    val f = case p_ of
neuper@37906
   542
			Frm => get_obj g_form pt p
neuper@37906
   543
		      | Res => (fst o (get_obj g_result pt)) p
neuper@37906
   544
	in ContNOrew {thyID   = theory'2thyID thy',
neuper@37906
   545
		    thm_rls = thm2guh (thy_containing_thm thy' thmID) thmID,
neuper@37906
   546
		      applto = f}
neuper@37906
   547
	end)
neuper@37906
   548
    
neuper@37906
   549
(* val ((pt,p), tac as Rewrite_Inst (subs, (thmID,_))) = ((pt,pos), tac);
neuper@37906
   550
   *)
neuper@37906
   551
      | context_thy (pt, pos as (p,p_)) 
neuper@37906
   552
		    (tac as Rewrite_Inst (subs, (thmID,_))) =
neuper@37906
   553
	(case applicable_in pos pt tac of
neuper@37906
   554
(* val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), 
neuper@37906
   555
			    f, (res,asm))) = applicable_in p pt tac;
neuper@37906
   556
   *)
neuper@37906
   557
	     Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), 
neuper@37906
   558
				  f, (res,(*path to subterm,*)asm))) =>
neuper@37906
   559
	     let val thm = (norm o #prop o rep_thm o 
neuper@37906
   560
			    (get_thm (assoc_thy thy'))) thmID
neuper@37906
   561
	    val thminst = inst_bdv subst thm
neuper@37906
   562
    (*WN060616 the following must be done on subterm found _IN_ rew_sub
neuper@37906
   563
	val (lhs,rhs) = (dest_equals' o strip_trueprop 
neuper@37906
   564
			 o Logic.strip_imp_concl) thminst
neuper@37906
   565
	val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)
neuper@37906
   566
	val thm' = ren_inst (insts, thminst, lhs, f)
neuper@37906
   567
	val (lhs',rhs') = (dest_equals' o strip_trueprop 
neuper@37906
   568
			   o Logic.strip_imp_concl) thm'
neuper@37906
   569
	val asms = map strip_trueprop (Logic.strip_imp_prems thminst)
neuper@37906
   570
	val asms' = map strip_trueprop (Logic.strip_imp_prems thm')
neuper@37906
   571
     *)
neuper@37906
   572
	     in ContThmInst {thyID   = theory'2thyID thy',
neuper@37906
   573
		    thm     = thm2guh (thy_containing_thm 
neuper@37906
   574
						    thy' thmID) thmID,
neuper@37906
   575
			     bdvs    = subst,
neuper@37906
   576
			     thminst = thminst,
neuper@37906
   577
			     applto  = f,
neuper@37906
   578
			     applat  = e_term,
neuper@37906
   579
			     reword  = ord',
neuper@37906
   580
			     asms    = [](*asms ~~ asms'*),
neuper@37906
   581
			     lhs     = (e_term, e_term)(*(lhs, lhs')*),
neuper@37906
   582
			     rhs     = (e_term, e_term)(*(rhs, rhs')*),
neuper@37906
   583
			     result  = res,
neuper@37906
   584
			     resasms = asm,
neuper@37906
   585
			     asmrls  = id_rls erls}
neuper@37906
   586
	     end
neuper@37906
   587
      | Notappl _ =>
neuper@37906
   588
	let val pp = par_pblobj pt p
neuper@37906
   589
	    val thy' = get_obj g_domID pt pp
neuper@37906
   590
	    val subst = subs2subst (assoc_thy thy') subs
neuper@37906
   591
	    val thm = (norm o #prop o rep_thm o 
neuper@37906
   592
			    (get_thm (assoc_thy thy'))) thmID
neuper@37906
   593
	    val thminst = inst_bdv subst thm
neuper@37906
   594
	    val f = case p_ of
neuper@37906
   595
			Frm => get_obj g_form pt p
neuper@37906
   596
		      | Res => (fst o (get_obj g_result pt)) p
neuper@37906
   597
	in ContNOrewInst {thyID   = theory'2thyID thy',
neuper@37906
   598
			  thm_rls = thm2guh (thy_containing_thm 
neuper@37906
   599
						 thy' thmID) thmID, 
neuper@37906
   600
			  bdvs    = subst,
neuper@37906
   601
			  thminst = thminst,
neuper@37906
   602
			  applto = f}
neuper@37906
   603
	end)
neuper@37906
   604
  | context_thy (pt,p) (tac as Rewrite_Set rls') =
neuper@37906
   605
    (case applicable_in p pt tac of
neuper@37906
   606
	 Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) =>
neuper@37906
   607
	 ContRls {thyID   = theory'2thyID thy',
neuper@37906
   608
		  rls     = rls2guh (thy_containing_rls thy' rls') rls',
neuper@37906
   609
		  applto  = f,	  
neuper@37906
   610
		  result  = res,	  
neuper@37906
   611
		  asms    = asm})
neuper@37906
   612
  | context_thy (pt,p) (tac as Rewrite_Set_Inst (subs, rls')) = 
neuper@37906
   613
    (case applicable_in p pt tac of
neuper@37906
   614
	 Appl (Rewrite_Set_Inst' (thy', _, subst, rls, f, (res,asm))) =>
neuper@37906
   615
	 ContRlsInst {thyID   = theory'2thyID thy',
neuper@37906
   616
		      rls     = rls2guh (thy_containing_rls thy' rls') rls',
neuper@37906
   617
		      bdvs    = subst,
neuper@37906
   618
		      applto  = f,	  
neuper@37906
   619
		      result  = res,	  
neuper@37906
   620
		      asms    = asm});
neuper@37906
   621
neuper@37906
   622
(*.get all theorems in a rule set (recursivley containing rule sets).*)
neuper@37906
   623
fun thm_of_rule Erule = []
neuper@37906
   624
  | thm_of_rule (thm as Thm _) = [thm]
neuper@37906
   625
  | thm_of_rule (Calc _) = []
neuper@37906
   626
  | thm_of_rule (Cal1 _) = []
neuper@37906
   627
  | thm_of_rule (Rls_ rls) = thms_of_rls rls
neuper@37906
   628
and thms_of_rls Erls = []
neuper@37906
   629
  | thms_of_rls (Rls {rules,...}) = (flat o (map  thm_of_rule)) rules
neuper@37906
   630
  | thms_of_rls (Seq {rules,...}) = (flat o (map  thm_of_rule)) rules
neuper@37906
   631
  | thms_of_rls (Rrls _) = [];
neuper@37906
   632
(* val Hrls {thy_rls = (_, rls),...} =
neuper@37906
   633
       get_the ["IsacKnowledge", "Test", "Rulesets", "expand_binomtest"];
neuper@37906
   634
> thms_of_rls rls;
neuper@37906
   635
   *)
neuper@37906
   636
neuper@37906
   637
(*. check if a rule is contained in a rule-set (recursivley down in Rls_);
neuper@37906
   638
    this rule can even be a rule-set itself.*)
neuper@37906
   639
fun contains_rule r rls = 
neuper@37906
   640
    let fun find (r, Rls_ rls) = finds (get_rules rls)
neuper@37906
   641
	  | find r12 = eq_rule r12
neuper@37906
   642
	and finds [] = false
neuper@37906
   643
	  | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;
neuper@37906
   644
    in 
neuper@37906
   645
    (*writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*)
neuper@37906
   646
    finds (get_rules rls) 
neuper@37906
   647
    end;
neuper@37906
   648
neuper@37906
   649
(*. try if a rewrite-rule is applicable to a given formula; 
neuper@37906
   650
    in case of rule-sets (recursivley) collect all _atomic_ rewrites .*) 
neuper@37906
   651
fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =
neuper@37906
   652
    if contains_bdv thm
neuper@37906
   653
    then case rewrite_inst_ thy ro erls false subst thm f of
neuper@37926
   654
	      SOME (f',_) =>[rule2tac subst thm']
neuper@37926
   655
	    | NONE => []
neuper@37906
   656
    else (case rewrite_ thy ro erls false thm f of
neuper@37926
   657
	SOME (f',_) => [rule2tac [] thm']
neuper@37926
   658
	    | NONE => [])
neuper@37906
   659
  | try_rew thy _ _ _ f (cal as Calc c) = 
neuper@37906
   660
    (case get_calculation_ thy c f of
neuper@37926
   661
	SOME (str, _) => [rule2tac [] cal]
neuper@37926
   662
      | NONE => [])
neuper@37906
   663
  | try_rew thy _ _ _ f (cal as Cal1 c) = 
neuper@37906
   664
    (case get_calculation_ thy c f of
neuper@37926
   665
	SOME (str, _) => [rule2tac [] cal]
neuper@37926
   666
      | NONE => [])
neuper@37906
   667
  | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
neuper@37906
   668
and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) = 
neuper@37906
   669
    distinct (flat (map (try_rew thy ro erls subst f) rules))
neuper@37906
   670
  | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) = 
neuper@37906
   671
    distinct (flat (map (try_rew thy ro erls subst f) rules))
neuper@37906
   672
  | filter_appl_rews thy subst f (Rrls _) = [];
neuper@37906
   673
neuper@37906
   674
(*. decide if a tactic is applicable to a given formula; 
neuper@37906
   675
    in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
neuper@37906
   676
(* val 
neuper@37906
   677
   *)
neuper@37906
   678
fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
neuper@37906
   679
    try_rew thy e_rew_ordX e_rls [] f (Calc (snd(assoc1 (!calclist', scrID))))
neuper@37906
   680
  | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) =
neuper@37906
   681
    try_rew thy (ro, assoc_rew_ord ro) erls [] f 
neuper@37906
   682
	    (Thm (thmID, assoc_thm' thy thm'))
neuper@37906
   683
  | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm' as (thmID, _))) =
neuper@37906
   684
    try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f 
neuper@37906
   685
	    (Thm (thmID, assoc_thm' thy thm'))
neuper@37906
   686
neuper@37906
   687
  | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
neuper@37906
   688
    filter_appl_rews thy [] f (assoc_rls rls')
neuper@37906
   689
  | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
neuper@37906
   690
    filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')
neuper@37906
   691
  | atomic_appl_tacs _ _ _ _ tac = 
neuper@37906
   692
    (writeln ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");
neuper@37906
   693
     []);
neuper@37906
   694
neuper@37906
   695
neuper@37906
   696
neuper@37906
   697
neuper@37906
   698
neuper@37906
   699
(*.not only for thydata, but also for thy's etc.*)
neuper@37906
   700
fun theID2guh (theID:theID) =
neuper@37906
   701
    case length theID of
neuper@37906
   702
	0 => raise error ("theID2guh: called with theID = "^strs2str' theID)
neuper@37906
   703
      | 1 => part2guh theID
neuper@37906
   704
      | 2 => thy2guh theID
neuper@37906
   705
      | 3 => thypart2guh theID
neuper@37906
   706
      | 4 => let val [isa, thyID, typ, elemID] = theID
neuper@37906
   707
	     in case typ of
neuper@37906
   708
		    "Theorems" => thm2guh (isa, thyID) elemID
neuper@37906
   709
		  | "Rulesets" => rls2guh (isa, thyID) elemID
neuper@37906
   710
		  | "Calculations" => cal2guh (isa, thyID) elemID
neuper@37906
   711
		  | "Orders" => ord2guh (isa, thyID) elemID
neuper@37906
   712
		  | "Theorems" => thy2guh [isa, thyID]
neuper@37906
   713
		  | str => raise error ("theID2guh: called with theID = "^
neuper@37906
   714
					strs2str' theID)
neuper@37906
   715
	     end
neuper@37906
   716
      | n => raise error ("theID2guh called with theID = "^strs2str' theID);
neuper@37906
   717
(*.filenames not only for thydata, but also for thy's etc.*)
neuper@37906
   718
fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
neuper@37906
   719
neuper@37906
   720
fun guh2theID (guh:guh) =
neuper@37906
   721
    let val guh' = explode guh
neuper@37906
   722
	val part = implode (take_fromto 1 4 guh')
neuper@37906
   723
	val isa = implode (take_fromto 5 9 guh')
neuper@37930
   724
    in if not (member op = part ["exp_", "thy_", "pbl_", "met_"])
neuper@37906
   725
       then raise error ("guh '"^guh^"' does not begin with \
neuper@37906
   726
				     \exp_ | thy_ | pbl_ | met_")
neuper@37906
   727
       else let val chap = case isa of
neuper@37906
   728
				"isab_" => "Isabelle"
neuper@37906
   729
			      | "scri_" => "IsacScripts"
neuper@37906
   730
			      | "isac_" => "IsacKnowledge"
neuper@37906
   731
			      | _ => 
neuper@37906
   732
				raise error ("guh2theID: '"^guh^
neuper@37906
   733
					     "' does not have isab_ | scri_ | \
neuper@37906
   734
					     \isac_ at position 5..9")
neuper@37906
   735
		val rest = takerest (9, guh') 
neuper@37906
   736
		val thyID = takewhile [] (not o (curry op= "-")) rest
neuper@37906
   737
		val rest' = dropuntil (curry op= "-") rest
neuper@37906
   738
	    in case implode rest' of
neuper@37906
   739
		   "-part" => [chap] : theID
neuper@37906
   740
		 | "" => [chap, implode thyID]
neuper@37906
   741
		 | "-Theorems" => [chap, implode thyID, "Theorems"]
neuper@37906
   742
		 | "-Rulesets" => [chap, implode thyID, "Rulesets"]
neuper@37906
   743
		 | "-Operations" => [chap, implode thyID, "Operations"]
neuper@37906
   744
		 | "-Orders" => [chap, implode thyID, "Orders"]
neuper@37906
   745
		 | _ => 
neuper@37906
   746
		   let val sect = implode (take_fromto 1 5 rest')
neuper@37906
   747
		       val sect' = 
neuper@37906
   748
			   case sect of
neuper@37906
   749
			       "-thm-" => "Theorems"
neuper@37906
   750
			     | "-rls-" => "Rulesets"
neuper@37906
   751
			     | "-cal-" => "Operations"
neuper@37906
   752
			     | "-ord-" => "Orders"
neuper@37906
   753
			     | str => 
neuper@37906
   754
			       raise error ("guh2theID: '"^guh^"' has '"^sect^
neuper@37906
   755
					    "' instead -thm- | -rls- | \
neuper@37906
   756
					    \-cal- | -ord-")
neuper@37906
   757
		   in [chap, implode thyID, sect', implode 
neuper@37906
   758
						       (takerest (5, rest'))]
neuper@37906
   759
		   end
neuper@37906
   760
	    end	
neuper@37906
   761
    end;
neuper@37906
   762
(*> guh2theID "thy_isac_Biegelinie-Theorems";
neuper@37906
   763
val it = ["IsacKnowledge", "Biegelinie", "Theorems"] : theID
neuper@37906
   764
> guh2theID "thy_scri_ListG-thm-zip_Nil";
neuper@37906
   765
val it = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] : theID*)
neuper@37906
   766
neuper@37906
   767
fun guh2filename (guh : guh) = guh ^ ".xml" : filename;
neuper@37906
   768
neuper@37906
   769
neuper@37906
   770
(*..*)
neuper@37906
   771
fun guh2rewtac (guh:guh) ([] : subs) =
neuper@37906
   772
    let val [isa, thy, sect, xstr] = guh2theID guh
neuper@37906
   773
    in case sect of
neuper@37906
   774
	   "Theorems" => Rewrite (xstr, "")
neuper@37906
   775
	 | "Rulesets" => Rewrite_Set xstr
neuper@37906
   776
	 | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'") 
neuper@37906
   777
    end
neuper@37906
   778
  | guh2rewtac (guh:guh) subs =
neuper@37906
   779
    let val [isa, thy, sect, xstr] = guh2theID guh
neuper@37906
   780
    in case sect of
neuper@37906
   781
	   "Theorems" => Rewrite_Inst (subs, (xstr, ""))
neuper@37906
   782
	 | "Rulesets" => Rewrite_Set_Inst (subs,  xstr)
neuper@37906
   783
	 | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'") 
neuper@37906
   784
    end;
neuper@37906
   785
(*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];
neuper@37906
   786
val it = Rewrite ("constant_mult_square", "") : tac
neuper@37906
   787
> guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"];
neuper@37906
   788
val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac
neuper@37906
   789
> guh2rewtac "thy_isac_Test-rls-Test_simplify" [];
neuper@37906
   790
val it = Rewrite_Set "Test_simplify" : tac
neuper@37906
   791
> guh2rewtac "thy_isac_Test-rls-isolate_bdv" ["(bdv, x)"];
neuper@37906
   792
val it = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") : tac*)
neuper@37906
   793
neuper@37906
   794
neuper@37906
   795
(*.the front-end may request a context for any element of the hierarchy.*)
neuper@37906
   796
(* val guh = "thy_isac_Test-rls-Test_simplify";
neuper@37906
   797
   *)
neuper@37906
   798
fun no_thycontext (guh : guh) = (guh2theID guh; false)
neuper@37906
   799
    handle _ => true;
neuper@37906
   800
neuper@37906
   801
(*> has_thycontext  "thy_isac_Test";
neuper@37906
   802
if has_thycontext  "thy_isac_Test" then "OK" else "NOTOK";
neuper@37906
   803
 *)
neuper@37906
   804
neuper@37906
   805
neuper@37906
   806
neuper@37906
   807
(*.get the substitution of bound variables for matchTheory:
neuper@37906
   808
   # lookup the thm|rls' in the script
neuper@37906
   809
   # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
neuper@37906
   810
   # instantiate this subs with the istates env to [(bdv, x),..]
neuper@37906
   811
   # otherwise [].*)
neuper@37906
   812
(*WN060617 hack assuming that all scripts use only one bound variable
neuper@37906
   813
and use 'v_' as the formal argument for this bound variable*)
neuper@37906
   814
(* val (ScrState (env,_,_,_,_,_), _, guh) = (is, "dummy", guh);
neuper@37906
   815
   *)
neuper@37906
   816
fun subs_from (ScrState (env,_,_,_,_,_)) _(*:Script sc*) (guh:guh) =
neuper@37906
   817
    let val theID as [isa, thyID, sect, xstr] = guh2theID guh
neuper@37906
   818
    in case sect of
neuper@37906
   819
	   "Theorems" => 
neuper@37906
   820
	   let val thm = get_thm (assoc_thy (thyID2theory' thyID)) xstr
neuper@37906
   821
	   in if contains_bdv thm
neuper@37906
   822
	      then let val formal_arg = str2term "v_"
neuper@37906
   823
		       val value = subst_atomic env formal_arg
neuper@37906
   824
		   in ["(bdv," ^ term2str value ^ ")"]:subs end
neuper@37906
   825
	      else []
neuper@37906
   826
	   end
neuper@37906
   827
	 | "Rulesets" => 
neuper@37906
   828
	   let val rules = (get_rules o assoc_rls) xstr
neuper@37906
   829
	   in if contain_bdv rules
neuper@37906
   830
	      then let val formal_arg = str2term"v_"
neuper@37906
   831
		       val value = subst_atomic env formal_arg
neuper@37906
   832
		   in ["(bdv,"^term2str value^")"]:subs end
neuper@37906
   833
	      else []
neuper@37906
   834
	   end
neuper@37906
   835
    end;
neuper@37906
   836
neuper@37906
   837
(* use"ME/rewtools.sml";
neuper@37906
   838
   *)
neuper@37906
   839