(* auxiliary functions used in scripts

   author: Walther Neuper 000301

   WN0509 shift into Atools ?!? (because used also in where of models !)

   (c) copyright due to lincense terms.

remove_thy"Tools";

use_thy"Scripts/Tools";

*)

theory Tools

imports ListG

begin

(*belongs to theory ListG*)

ML {*

val first_isac_thy = @{theory ListG}

*}

(*for Descript.thy*)

  (***********************************************************************)

  (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*)

  (***********************************************************************)

typedecl nam     (* named variables                                             *)

typedecl  una     (* unnamed variables                                           *)

typedecl  unl     (* unnamed variables of type list, elementwise input prohibited*)

typedecl  str     (* structured variables                                        *)

typedecl  toreal  (* var with undef real value: forces typing                    *)

typedecl  toreall (* var with undef real list value: forces typing               *)

typedecl  tobooll (* var with undef bool list value: forces typing               *)

typedecl  unknow  (* input without dsc in fmz=[]                                 *)

typedecl  cpy     (* UNUSED: copy-named variables

             identified by .._0, .._i .._' in pbt                        *)

  (***********************************************************************)

  (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*)

  (***********************************************************************)

consts

  UniversalList   :: "bool list"

  lhs             :: "bool => real"           (*of an equality*)

  rhs             :: "bool => real"           (*of an equality*)

  Vars            :: "'a => real list"        (*get the variables of a term *)

  matches         :: "['a, 'a] => bool"

  matchsub        :: "['a, 'a] => bool"

constdefs

  Testvar   :: "[real, 'a] => bool"  (*is a variable in a term: unused 6.5.03*)

 "Testvar v t == v mem (Vars t)"     (*by rewriting only,no Calcunused 6.5.03*)

ML {* (*the former Tools.ML*)

(* auxiliary functions for scripts  WN.9.00*)

(*11.02: for equation solving only*)

val UniversalList = (term_of o the o (parse @{theory})) "UniversalList";

val EmptyList = (term_of o the o (parse @{theory}))  "[]::bool list";     

(*+ for Or_to_List +*)

fun or2list (Const ("True",_)) = (writeln"### or2list True";UniversalList)

  | or2list (Const ("False",_)) = (writeln"### or2list False";EmptyList)

  | or2list (t as Const ("op =",_) $ _ $ _) = 

    (writeln"### or2list _ = _";list2isalist bool [t])

  | or2list ors =

    (writeln"### or2list _ | _";

    let fun get ls (Const ("op |",_) $ o1 $ o2) =

	    case o2 of

		Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2

	      | _ => ls @ [o1, o2] 

    in (((list2isalist bool) o (get [])) ors)

       handle _ => raise error ("or2list: no ORs= "^(term2str ors)) end

	);

(*>val t = HOLogic.true_const;

> val t' = or2list t;

> term2str t';

"Atools.UniversalList"

> val t = HOLogic.false_const;

> val t' = or2list t;

> term2str t';

"[]"

> val t=(term_of o the o (parse thy)) "x=3";

> val t' = or2list t;

> term2str t';

"[x = 3]"

> val t=(term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";

> val t' = or2list t;

> term2str t';

"[x = #3, x = #-3, x = #0]" : string *)

(** evaluation on the meta-level **)

(*. evaluate the predicate matches (match on whole term only) .*)

(*("matches",("Tools.matches",eval_matches "#matches_")):calc*)

fun eval_matches (thmid:string) "Tools.matches"

		 (t as Const ("Tools.matches",_) $ pat $ tst) thy = 

    if matches thy tst pat

    then let val prop = Trueprop $ (mk_equality (t, true_as_term))

	 in SOME (Syntax.string_of_term @{context} prop, prop) end

    else let val prop = Trueprop $ (mk_equality (t, false_as_term))

	 in SOME (Syntax.string_of_term @{context} prop, prop) end

  | eval_matches _ _ _ _ = NONE; 

(*

> val t  = (term_of o the o (parse thy)) 

	      "matches (?x = 0) (1 * x ^^^ 2 = 0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (term_of o the o (parse thy)) 

	      "matches (?a = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (term_of o the o (parse thy)) 

	      "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (term_of o the o (parse thy)) 

	      "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option                  

----- before ?patterns ---:

> val t  = (term_of o the o (parse thy)) 

	      "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME

    ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",

     Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

  : (string * term) option 

> val t = (term_of o the o (parse thy)) 

	      "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",

     Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

> val t = (term_of o the o (parse thy)) 

               "matches (a = b) (x + #1 + #-1 * #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))

*)

(*.does a pattern match some subterm ?.*)

fun matchsub thy t pat =  

    let fun matchs (t as Const _) = matches thy t pat

	  | matchs (t as Free _) = matches thy t pat

	  | matchs (t as Var _) = matches thy t pat

	  | matchs (Bound _) = false

	  | matchs (t as Abs (_, _, body)) = 

	    if matches thy t pat then true else matches thy body pat

	  | matchs (t as f1 $ f2) =

	     if matches thy t pat then true 

	     else if matchs f1 then true else matchs f2

    in matchs t end;

(*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*)

fun eval_matchsub (thmid:string) "Tools.matchsub"

		 (t as Const ("Tools.matchsub",_) $ pat $ tst) thy = 

    if matchsub thy tst pat

    then let val prop = Trueprop $ (mk_equality (t, true_as_term))

	 in SOME (Syntax.string_of_term @{context} prop, prop) end

    else let val prop = Trueprop $ (mk_equality (t, false_as_term))

	 in SOME (Syntax.string_of_term @{context} prop, prop) end

  | eval_matchsub _ _ _ _ = NONE; 

(*get the variables in an isabelle-term*)

(*("Vars"    ,("Tools.Vars"    ,eval_var "#Vars_")):calc*)

fun eval_var (thmid:string) "Tools.Vars"

  (t as (Const(op0,t0) $ arg)) thy = 

  let 

    val t' = ((list2isalist HOLogic.realT) o vars) t;

    val thmId = thmid^(Syntax.string_of_term @{context} arg);

  in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end

  | eval_var _ _ _ _ = NONE;

fun lhs (Const ("op =",_) $ l $ _) = l

  | lhs t = error("lhs called with (" ^ term2str t ^ ")");

(*("lhs"    ,("Tools.lhs"    ,eval_lhs "")):calc*)

fun eval_lhs _ "Tools.lhs"

	     (t as (Const ("Tools.lhs",_) $ (Const ("op =",_) $ l $ _))) _ = 

    SOME ((term2str t) ^ " = " ^ (term2str l),

	  Trueprop $ (mk_equality (t, l)))

  | eval_lhs _ _ _ _ = NONE;

(*

> val t = (term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";

> val SOME (id,t') = eval_lhs 0 0 t 0;

val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string

> term2str t';

val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string

*)

fun rhs (Const ("op =",_) $ _ $ r) = r

  | rhs t = error("rhs called with (" ^ term2str t ^ ")");

(*("rhs"    ,("Tools.rhs"    ,eval_rhs "")):calc*)

fun eval_rhs _ "Tools.rhs"

	     (t as (Const ("Tools.rhs",_) $ (Const ("op =",_) $ _ $ r))) _ = 

    SOME ((term2str t) ^ " = " ^ (term2str r),

	  Trueprop $ (mk_equality (t, r)))

  | eval_rhs _ _ _ _ = NONE;

(*for evaluating scripts*) 

val list_rls = append_rls "list_rls" list_rls

			  [Calc ("Tools.rhs",eval_rhs "")];

ruleset' := overwritelthy @{theory} (!ruleset',

  [("list_rls",list_rls)

   ]);

calclist':= overwritel (!calclist', 

   [("matches",("Tools.matches",eval_matches "#matches_")),

    ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")),

    ("Vars"    ,("Tools.Vars"    ,eval_var "#Vars_")),

    ("lhs"    ,("Tools.lhs"    ,eval_lhs "")),

    ("rhs"    ,("Tools.rhs"    ,eval_rhs ""))

    ]);

*}

end