(* Title:  "BaseDefinitions/rewrite-order.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";

"-------- check simple terms -------------------------------------------------------------------";

"-------- check all 'not >' in trace of Test_simplify on: x + 1 + - 1 * 2 = 0 ------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";

"-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";

"-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";

val form = TermC.parse_test @{context} "x + -2 ::real"

val Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify;

val ctxt = Proof_Context.init_global @{theory Test};

(*Rewrite.trace_on := false; (*true false*)*)

(** )val NONE =                                         ( *isa*)

(**)val SOME (form', _) =                             (*isa2*)

      rewrite_ ctxt rew_ord_ erls true @{thm radd_commute} form;

(*

-------------------- code in rew_sub -------------------------------------------------------

(

@{print}{a = "@@@rew_sub.ord.rew: ", perm = TermC.perm lhs rhs, tless = not (tless bdv (t', t))};

    if TermC.perm lhs rhs andalso not (tless bdv (t', t))                     (*ordered rewriting*)

    then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)

    else (t'', p'', [], true)

)

-------------------- output with Rewrite.trace_on := true; ---------------------------------

##  eval asms: "x + -2 = -2 + x" 

{a = "@@@rew_sub.ord.rew: ", b = true, c = false}

*)

"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =

  (@{theory Test}, rew_ord_, erls, true, @{thm radd_commute}, form);

"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =

  (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);

    val (t', asms, _(*lrd*), rew) =

           rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)

		         (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;

"~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =

(thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),

		         (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);

    val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r

    val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)

      handle Pattern.MATCH => raise NO_REWRITE

    val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))

    val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'

    val _ = trace_in2 ctxt i "eval asms" r';

    val (t'', p'') =                                                      (*conditional rewriting*)

      let val (simpl_p', nofalse) = Rewrite.eval__true ctxt (i + 1) p' bdv rls 	     

	    in

	      if nofalse

        then (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)

        else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE)   (* don't go into subtm.of cond*)

	    end;

    (*if*) TermC.perm lhs rhs andalso not (tless bdv (t', t));                     (*ordered rewriting*)

                                      not (tless bdv (t', t)); (*isa = true , isa2 = false*)

                                          (tless bdv (t', t)); (*isa = false, isa2 = true*)

(*WHAT IS ..:

tless <-- Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify; ..in Test_Some.thy

rew_ord_ <-- sqrt_right false @{theory "Pure"}                                    ..in Test.thy

sqrt_right                                                                        ..in Root.thy

CHECK THIS ...(same error as with ^^^^^^^^^tless

CHECK THIS ...(same error as with code copied into Test_Some.thy

*)

if        (sqrt_right false @{theory "Pure"} bdv (t', t)) (*isa = false, isa2 = true*)

(** )then error "sqrt_right: special case NOT ok" else ();     ( *isa*)

(**)then () else error "sqrt_right: special case OK";                      (*isa2*)

"~~~~~ fun sqrt_right , args:"; val ((pr:bool), thy, (_: subst), tu) =

  (false, @{theory "Pure"}, bdv, (t', t));

"~~~~~ fun term_ord' , args:"; val (pr, _(*thy*), (t, u)) = (pr, thy(***), tu);

(*//----------------------------- open local ------------------------------------------------\\* )

val EQUAL =

    (*case*) int_ord (size_of_term' t, size_of_term' u) (*of*);

      val (f, ts) = strip_comb t and (g, us) = strip_comb u

val EQUAL =

        (*case*) hd_ord (f, g) (*of*);

(**)val GREATER =                                             (*isa*)

(** )val LESS =                                               ( *isa2*)

           terms_ord str pr (ts, us)

"~~~~~ and terms_ord , args:"; val (_(*str*), pr, (ts, us)) = (str, pr, (ts, us));

           list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge")) (ts, us);

(*+*)list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order;

(*+*)term_ord' pr (ThyC.get_theory "Isac_Knowledge"): term * term -> order;

"~~~~~ fun list_ord , args:"; val (elem_ord, (xs, ys)) =

  ((term_ord' pr (ThyC.get_theory "Isac_Knowledge")), (ts, us));

(*+*)UnparseC.terms xs = "[\"- 2\", \"x\"]";                  (*isa == ?*)

(*+*)UnparseC.terms ys = "[\"x\", \"- 2\"]";                  (*isa == ?*)

val EQUAL =

      (*case*) int_ord (length xs, length ys) (*of*);

val GREATER =

           dict_ord elem_ord (xs, ys);

"~~~~~ fun dict_ord , args:"; val ( elem_ord, (x :: xs, y :: ys)) = (elem_ord, (xs, ys))

val GREATER =

    (*case*) elem_ord (x, y) (*of*);

val return = GREATER;

( *\\----------------------------- open local ------------------------------------------------//*)

"-------- check simple terms -------------------------------------------------------------------";

"-------- check simple terms -------------------------------------------------------------------";

"-------- check simple terms -------------------------------------------------------------------";

val rew_ord_ = sqrt_right false @{theory "Pure"};

if rew_ord_ [] (@{term "1::real"}, @{term "2::real"}) =    true then () else error "";

if rew_ord_ [] (@{term "3::real"}, @{term "2::real"}) =   false then () else error "";

if rew_ord_ [] (@{term "-1::real"}, @{term "-2::real"}) =  true then () else error "";

if rew_ord_ [] (@{term "-3::real"}, @{term "-2::real"}) = false then () else error "";

if rew_ord_ [] (@{term "1::real"}, @{term "-1::real"}) =  false then () else error "";

if rew_ord_ [] (@{term "-1::real"}, @{term "1::real"}) =   true then () else error "";

if rew_ord_ [] (@{term "x::real"}, @{term "2::real"}) =   false then () else error "";

if rew_ord_ [] (@{term "3::real"}, @{term "x::real"}) =    true then () else error "";

"-------- check all 'not >' in trace of Test_simplify on: x + 1 + - 1 * 2 = 0 ------------------";

"-------- check all 'not >' in trace of Test_simplify on: x + 1 + - 1 * 2 = 0 ------------------";

"-------- check all 'not >' in trace of Test_simplify on: x + 1 + - 1 * 2 = 0 ------------------";

(* the rewrite-order for rewriting single theorems in a Rule_Set is taken from 

*)

val Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify;

(*#  rls: Test_simplify on: x + 1 + - 1 * 2 = 0   ..selected "not >:" from trace:*)

(*##  not >:           "x + 1 + - 1 * 2" >              "x + 1 + - 1 * 2" *)

if rew_ord_ [] (@{term "x + 1 + - 1 * 2::real"}, @{term "x + 1 + - 1 * 2::real"}) = false

then () else error "term_ord' 1";

(*##  not >:           "1 + x + - 1 * 2" >              "- 1 * 2 + (1 + x)" *)

if rew_ord_ [] (@{term "1 + x + - 1 * 2::real"}, @{term "- 1 * 2 + (1 + x)::real"}) = true

then () else error "term_ord' 2";

(*##  not >:           "1 + x" >              "x + 1" *)

if rew_ord_ [] (@{term "1 + x::real"}, @{term "x + 1::real"}) = true

then () else error "term_ord' 3";

(*##  not >:           "- 1 * 2" >              "2 * - 1" *)

if rew_ord_ [] (@{term "- 1 * 2::real"}, @{term "2 * - 1::real"}) = true

then () else error "term_ord' 4";

(*##  not >:           "1 + (x + - 2)" >              "x + - 2 + 1" *)

if rew_ord_ [] (@{term "1 + (x + - 2)::real"}, @{term "x + - 2 + 1::real"}) = true

then () else error "term_ord' 5";

(*##  not >:           "x + - 2" >              "- 2 + x"*)

if rew_ord_ [] (@{term "x + - 2::real"}, @{term "- 2 + x  ::real"}) = false

then () else error "term_ord' 5a";  (*<<<<<<<<<<<<<<----------------- false in trace isa2*)

(*--------------------------------- ordered rew. (NOT) inhibited*)

(*##  not >:           "1 + (-2 + x)" >              "-2 + x + 1" *)

if rew_ord_ [] (@{term "1 + (-2 + x)::real"}, @{term "-2 + x + 1::real"}) = true

then () else error "term_ord' 6";

(*##  not >:           "- 2 + x" >              "x + - 2" *)

if rew_ord_ [] (@{term "- 2 + x::real"}, @{term "x + - 2::real"}) = true

then () else error "term_ord' 7";

(*##  not >:           "- 2 + (1 + x)" >              "1 + (- 2 + x)" *)

if rew_ord_ [] (@{term "- 2 + (1 + x)::real"}, @{term "1 + (- 2 + x)::real"}) = true

then () else error "term_ord' 8";

(*##  not >            "- 1 + x" >              "x + - 1" *)

if rew_ord_ [] (@{term "- 1 + x::real"}, @{term "x + - 1::real"}) = true

then () else error "term_ord' 9";