wneuper/isa: src/Tools/isac/ProgLang/Tools.thy@77138c64f4f6

     1 (* auxiliary functions used in scripts

     2    author: Walther Neuper 000301

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

     5    (c) copyright due to lincense terms.

     6 *)

     8 theory Tools imports ListC begin

    10 (*belongs to theory ListC*)

    11 ML {*

    12 val first_isac_thy = @{theory ListC}

    13 *}

    15 (*for Descript.thy*)

    17   (***********************************************************************)

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

    19   (***********************************************************************)

    20 typedecl nam     (* named variables                                             *)

    21 typedecl  una     (* unnamed variables                                           *)

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

    23 typedecl  str     (* structured variables                                        *)

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

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

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

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

    28 typedecl  cpy     (* UNUSED: copy-named variables

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

    30   (***********************************************************************)

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

    32   (***********************************************************************)

    34 consts

    36   UniversalList   :: "bool list"

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

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

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

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

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

    44 (*

    45 constdefs

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

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

    49 *)

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

    52 (* auxiliary functions for scripts  WN.9.00*)

    53 (*11.02: for equation solving only*)

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

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

    57 (*+ for Or_to_List +*)

    58 fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)

    59   | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)

    60   | or2list (t as Const ("HOL.eq",_) $ _ $ _) =

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

    62   | or2list ors =

    63     (tracing"### or2list _ | _";

    64     let fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =

    65 	    case o2 of

    66 		Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2

    67 	      | _ => ls @ [o1, o2]

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

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

    70 	);

    71 (*>val t = @{term True};

    72 > val t' = or2list t;

    73 > term2str t';

    74 "Atools.UniversalList"

    75 > val t = @{term False};

    76 > val t' = or2list t;

    77 > term2str t';

    78 "[]"

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

    80 > val t' = or2list t;

    81 > term2str t';

    82 "[x = 3]"

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

    84 > val t' = or2list t;

    85 > term2str t';

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

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

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

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

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

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

    95     if matches thy tst pat

    96     then

    97       let

    98         val prop = Trueprop $ (mk_equality (t, @{term True}))

    99 	    in SOME (term_to_string''' thy prop, prop) end

   100     else

   101       let

   102         val prop = Trueprop $ (mk_equality (t, @{term False}))

   103 	    in SOME (term_to_string''' thy prop, prop) end

   104   | eval_matches _ _ _ _ = NONE;

   105 (*

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

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

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

   109 val it =

   110   SOME

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

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

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

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

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

   117 val it =

   118   SOME

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

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

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

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

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

   125 val it =

   126   SOME

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

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

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

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

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

   133 val it =

   134   SOME

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

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

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

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

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

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

   141 SOME

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

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

   144   : (string * term) option

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

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

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

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

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

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

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

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

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

   156 *)

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

   159 fun matchsub thy t pat =

   160   let

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

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

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

   164 	      | matchs (Bound _) = false

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

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

   167 	      | matchs (t as f1 $ f2) =

   168 	          if matches thy t pat then true

   169 	            else if matchs f1 then true else matchs f2

   170   in matchs t end;

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

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

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

   175     if matchsub thy tst pat

   176     then

   177       let val prop = Trueprop $ (mk_equality (t, @{term True}))

   178       in SOME (term_to_string''' thy prop, prop) end

   179     else

   180       let val prop = Trueprop $ (mk_equality (t, @{term False}))

   181       in SOME (term_to_string''' thy prop, prop) end

   182   | eval_matchsub _ _ _ _ = NONE;

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

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

   186 fun eval_var (thmid:string) "Tools.Vars" (t as (Const(op0,t0) $ arg)) thy =

   187     let

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

   189       val thmId = thmid ^ term_to_string''' thy arg;

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

   191   | eval_var _ _ _ _ = NONE;

   193 fun lhs (Const ("HOL.eq",_) $ l $ _) = l

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

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

   196 fun eval_lhs _ "Tools.lhs"

   197 	     (t as (Const ("Tools.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =

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

   199 	  Trueprop $ (mk_equality (t, l)))

   200   | eval_lhs _ _ _ _ = NONE;

   201 (*

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

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

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

   205 > term2str t';

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

   207 *)

   209 fun rhs (Const ("HOL.eq",_) $ _ $ r) = r

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

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

   212 fun eval_rhs _ "Tools.rhs"

   213 	     (t as (Const ("Tools.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =

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

   215 	  Trueprop $ (mk_equality (t, r)))

   216   | eval_rhs _ _ _ _ = NONE;

   219 (*for evaluating scripts*)

   221 val list_rls = append_rls "list_rls" list_rls

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

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

   224   [("list_rls",list_rls)

   225    ]);

   226 calclist':= overwritel (!calclist',

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

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

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

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

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

   232     ]);

   234 *}

   235 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 22 Jul 2013 13:52:18 +0200
changeset 52070	77138c64f4f6
parent 48761	4162c4f6f897
child 52125	6f1d3415dc68
permissions	-rw-r--r--