(*. reverse rewriting

    WN.12.8.02

    use"Isa02/reverse-rew.sml";

.*)

fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str r)^", ("^

			    (term2str t')^", "^(terms2str a)^"))";

fun trtas2str trtas = (strs2str o (map trta2str)) trtas;

fun rta2str (r,(t,a)) = "\n("^(rule2str r)^", ("^

			    (term2str t)^", "^(terms2str a)^"))";

fun rtas2str rtas = (strs2str o (map rta2str)) rtas;

(*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*)

fun sym_thm thm =

  let 

    val {sign_ref = sign_ref, der = der, maxidx = maxidx,

	    shyps = shyps, hyps = hyps, prop = prop} = rep_thm_G thm;

    val (lhs,rhs) = (dest_equals' o strip_trueprop 

		     o Logic.strip_imp_concl) prop;

    val prop' = case strip_imp_prems' prop of

		   None => Trueprop $ (mk_equality (rhs, lhs))

		 | Some cs => 

		   ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));

  in assbl_thm sign_ref der maxidx shyps hyps prop' end;

(*

  (sym RS real_mult_div_cancel1) handle e => print_exn e;

Exception THM 1 raised:

RSN: no unifiers

"?s = ?t ==> ?t = ?s"

"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"

  val thm = real_mult_div_cancel1;

  val prop = (#prop o rep_thm) thm;

  atomt prop;

  val ppp = Logic.strip_imp_concl prop;

  atomt ppp;

  ((#prop o rep_thm o sym_thm o sym_thm) thm) = (#prop o rep_thm) thm;

val it = true : bool

  ((sym_thm o sym_thm) thm) = thm;

val it = true : bool

  val thm = real_le_anti_sym;

  ((sym_thm o sym_thm) thm) = thm;

val it = true : bool                                                           

  val thm = real_minus_zero;

  ((sym_thm o sym_thm) thm) = thm;

val it = true : bool                                                           

*)

(*.derive normalform of a rls, or derive until Some goal,

   and record rules applied and rewrites.

val it = fn

  : theory

    -> rls

    -> rule list

    -> rew_ord       : the order of this rls, which 1 theorem of is used 

                       for rewriting 1 single step (?14.4.03)

    -> term option 

    -> term 

    -> (term *       : to this term ...

        rule * 	     : ... this rule is applied yielding ...

        (term *      : ... this term ...

         term list)) : ... under these assumptions.

       list          :

*)

fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt = 

    let

	datatype switch = Appl | Noap;

	fun rew_once rts t Noap [] = 

	    (case goal of 

		 None => rts

	       | Some g => 

		 raise error ("make_deriv: no derivation for "^(term2str t)))

	  | rew_once rts t Appl [] = 

	    (*(case rs of Rls _ =>*) rew_once rts t Noap rs

	  (*| Seq _ => rts) FIXXXXXME 14.3.03*)

	  | rew_once rts t apno rs' =

	    (case goal of 

		 None => rew_or_calc rts t apno rs'

	       | Some g => 

		 if g = t then rts

		 else rew_or_calc rts t apno rs')

	and rew_or_calc rts t apno (rrs' as (r::rs')) =

	    case r of

		Thm (thmid, tm) =>

		(if not (!trace_rewrite) then () else

		 writeln ("### trying thm '" ^ thmid ^ "'");

		 case rewrite_ thy ro erls true tm t of

		     None => rew_once rts t apno rs'

		   | Some (t',a') =>

		     (if ! trace_rewrite 

		      then writeln ("### rewrites to: "^(term2str t')) else ();

		      rew_once (rts@[(t,r,(t',a'))]) t' Appl rrs'))

	      | Calc (c as (op_,_)) => 

		let val _ = if not (!trace_rewrite) then () else

			    writeln ("### trying calc. '" ^ op_ ^ "'")

		    val t = app_num_tr'2 t

		in case get_calculation_ thy c t of

		       None => rew_once rts t apno rs'

		     | Some (thmid, tm) => 

		       (let val Some (t',a') = rewrite_ thy ro erls true tm t

			    val _ = if not (!trace_rewrite) then () else

				    writeln("### calc. to: " ^ (term2str t'))

			    val r' = Thm (thmid, tm)

			in rew_once (rts@[(t,r',(t',a'))]) t' Appl rrs'  end) 

		       handle _ => raise error "derive_norm, Calc: no rewrite"

		end

	      (*| Rls_ <> rule list !!! FIXXXXXME 14.3.03*) 

    in rew_once [] tt Noap rs end;

(*

  val t9 = (term_of o the o (parse thy)) "(8*(-1 + x))/(9*(-1 + x))";

  val rst = make_deriv thy eval_rls make_polynomial None t9;

  writeln(trtas2str rst);

*)

fun sym_thmID thmID =

    case explode thmID of

	"s"::"y"::"m"::"_"::id => implode id

      | id => "sym_"^thmID;

(* 

  val thmID = "sym_real_mult_2";

  sym_thmID thmID;

val it = "real_mult_2" : string

  val thmID = "real_num_collect";

  sym_thmID thmID;

val it = "sym_real_num_collect" : string*)

fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)

  | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));

(*

  val th =  Thm ("real_one_collect",num_str real_one_collect);

  sym_Thm th;

val th =

  Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")

  : rule

ML> val it =

  Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)

fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));

fun reverse_deriv trta = (rev o (map rev_deriv)) trta;

fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =

    (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);

(*

  val rev_rew = reverse_deriv thy e_rls ; 

  writeln(rtas2str rev_rew);

*)

fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2

  | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^

				(rule2str r1)^"' '"^(rule2str r2)^"'");

fun distinct_Thm r = gen_distinct eq_Thm r;

fun eq_Thms thmIDs thm = (id_of_thm thm) mem thmIDs

  | eq_Thms _ thm = raise error ("eq_Thms: called with '"^(rule2str thm)^"'");

(* use"Isa02/reverse-rew.sml";

   *)