1.1 --- a/src/Tools/isac/Scripts/Tools.thy Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,230 +0,0 @@
1.4 -(* auxiliary functions used in scripts
1.5 - author: Walther Neuper 000301
1.6 - WN0509 shift into Atools ?!? (because used also in where of models !)
1.7 -
1.8 - (c) copyright due to lincense terms.
1.9 -
1.10 -remove_thy"Tools";
1.11 -use_thy"Scripts/Tools";
1.12 -*)
1.13 -
1.14 -theory Tools imports ListG begin
1.15 -
1.16 -(*belongs to theory ListG*)
1.17 -ML {*
1.18 -val first_isac_thy = @{theory ListG}
1.19 -*}
1.20 -
1.21 -(*for Descript.thy*)
1.22 -
1.23 - (***********************************************************************)
1.24 - (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*)
1.25 - (***********************************************************************)
1.26 -typedecl nam (* named variables *)
1.27 -typedecl una (* unnamed variables *)
1.28 -typedecl unl (* unnamed variables of type list, elementwise input prohibited*)
1.29 -typedecl str (* structured variables *)
1.30 -typedecl toreal (* var with undef real value: forces typing *)
1.31 -typedecl toreall (* var with undef real list value: forces typing *)
1.32 -typedecl tobooll (* var with undef bool list value: forces typing *)
1.33 -typedecl unknow (* input without dsc in fmz=[] *)
1.34 -typedecl cpy (* UNUSED: copy-named variables
1.35 - identified by .._0, .._i .._' in pbt *)
1.36 - (***********************************************************************)
1.37 - (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*)
1.38 - (***********************************************************************)
1.39 -
1.40 -consts
1.41 -
1.42 - UniversalList :: "bool list"
1.43 -
1.44 - lhs :: "bool => real" (*of an equality*)
1.45 - rhs :: "bool => real" (*of an equality*)
1.46 - Vars :: "'a => real list" (*get the variables of a term *)
1.47 - matches :: "['a, 'a] => bool"
1.48 - matchsub :: "['a, 'a] => bool"
1.49 -
1.50 -constdefs
1.51 -
1.52 - Testvar :: "[real, 'a] => bool" (*is a variable in a term: unused 6.5.03*)
1.53 - "Testvar v t == v mem (Vars t)" (*by rewriting only,no Calcunused 6.5.03*)
1.54 -
1.55 -ML {* (*the former Tools.ML*)
1.56 -(* auxiliary functions for scripts WN.9.00*)
1.57 -(*11.02: for equation solving only*)
1.58 -val UniversalList = (term_of o the o (parse @{theory})) "UniversalList";
1.59 -val EmptyList = (term_of o the o (parse @{theory})) "[]::bool list";
1.60 -
1.61 -(*+ for Or_to_List +*)
1.62 -fun or2list (Const ("True",_)) = (writeln"### or2list True";UniversalList)
1.63 - | or2list (Const ("False",_)) = (writeln"### or2list False";EmptyList)
1.64 - | or2list (t as Const ("op =",_) $ _ $ _) =
1.65 - (writeln"### or2list _ = _";list2isalist bool [t])
1.66 - | or2list ors =
1.67 - (writeln"### or2list _ | _";
1.68 - let fun get ls (Const ("op |",_) $ o1 $ o2) =
1.69 - case o2 of
1.70 - Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2
1.71 - | _ => ls @ [o1, o2]
1.72 - in (((list2isalist bool) o (get [])) ors)
1.73 - handle _ => raise error ("or2list: no ORs= "^(term2str ors)) end
1.74 - );
1.75 -(*>val t = HOLogic.true_const;
1.76 -> val t' = or2list t;
1.77 -> term2str t';
1.78 -"Atools.UniversalList"
1.79 -> val t = HOLogic.false_const;
1.80 -> val t' = or2list t;
1.81 -> term2str t';
1.82 -"[]"
1.83 -> val t=(term_of o the o (parse thy)) "x=3";
1.84 -> val t' = or2list t;
1.85 -> term2str t';
1.86 -"[x = 3]"
1.87 -> val t=(term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
1.88 -> val t' = or2list t;
1.89 -> term2str t';
1.90 -"[x = #3, x = #-3, x = #0]" : string *)
1.91 -
1.92 -
1.93 -(** evaluation on the meta-level **)
1.94 -
1.95 -(*. evaluate the predicate matches (match on whole term only) .*)
1.96 -(*("matches",("Tools.matches",eval_matches "#matches_")):calc*)
1.97 -fun eval_matches (thmid:string) "Tools.matches"
1.98 - (t as Const ("Tools.matches",_) $ pat $ tst) thy =
1.99 - if matches thy tst pat
1.100 - then let val prop = Trueprop $ (mk_equality (t, true_as_term))
1.101 - in SOME (Syntax.string_of_term @{context} prop, prop) end
1.102 - else let val prop = Trueprop $ (mk_equality (t, false_as_term))
1.103 - in SOME (Syntax.string_of_term @{context} prop, prop) end
1.104 - | eval_matches _ _ _ _ = NONE;
1.105 -(*
1.106 -> val t = (term_of o the o (parse thy))
1.107 - "matches (?x = 0) (1 * x ^^^ 2 = 0)";
1.108 -> eval_matches "/thmid/" "/op_/" t thy;
1.109 -val it =
1.110 - SOME
1.111 - ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
1.112 - Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.113 -
1.114 -> val t = (term_of o the o (parse thy))
1.115 - "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
1.116 -> eval_matches "/thmid/" "/op_/" t thy;
1.117 -val it =
1.118 - SOME
1.119 - ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
1.120 - Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.121 -
1.122 -> val t = (term_of o the o (parse thy))
1.123 - "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
1.124 -> eval_matches "/thmid/" "/op_/" t thy;
1.125 -val it =
1.126 - SOME
1.127 - ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
1.128 - Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.129 -
1.130 -> val t = (term_of o the o (parse thy))
1.131 - "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
1.132 -> eval_matches "/thmid/" "/op_/" t thy;
1.133 -val it =
1.134 - SOME
1.135 - ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
1.136 - Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.137 ------ before ?patterns ---:
1.138 -> val t = (term_of o the o (parse thy))
1.139 - "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
1.140 -> eval_matches "/thmid/" "/op_/" t thy;
1.141 -SOME
1.142 - ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
1.143 - Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
1.144 - : (string * term) option
1.145 -
1.146 -> val t = (term_of o the o (parse thy))
1.147 - "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
1.148 -> eval_matches "/thmid/" "/op_/" t thy;
1.149 -SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
1.150 - Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
1.151 -
1.152 -> val t = (term_of o the o (parse thy))
1.153 - "matches (a = b) (x + #1 + #-1 * #2 = #0)";
1.154 -> eval_matches "/thmid/" "/op_/" t thy;
1.155 -SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
1.156 -*)
1.157 -
1.158 -(*.does a pattern match some subterm ?.*)
1.159 -fun matchsub thy t pat =
1.160 - let fun matchs (t as Const _) = matches thy t pat
1.161 - | matchs (t as Free _) = matches thy t pat
1.162 - | matchs (t as Var _) = matches thy t pat
1.163 - | matchs (Bound _) = false
1.164 - | matchs (t as Abs (_, _, body)) =
1.165 - if matches thy t pat then true else matches thy body pat
1.166 - | matchs (t as f1 $ f2) =
1.167 - if matches thy t pat then true
1.168 - else if matchs f1 then true else matchs f2
1.169 - in matchs t end;
1.170 -
1.171 -(*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*)
1.172 -fun eval_matchsub (thmid:string) "Tools.matchsub"
1.173 - (t as Const ("Tools.matchsub",_) $ pat $ tst) thy =
1.174 - if matchsub thy tst pat
1.175 - then let val prop = Trueprop $ (mk_equality (t, true_as_term))
1.176 - in SOME (Syntax.string_of_term @{context} prop, prop) end
1.177 - else let val prop = Trueprop $ (mk_equality (t, false_as_term))
1.178 - in SOME (Syntax.string_of_term @{context} prop, prop) end
1.179 - | eval_matchsub _ _ _ _ = NONE;
1.180 -
1.181 -(*get the variables in an isabelle-term*)
1.182 -(*("Vars" ,("Tools.Vars" ,eval_var "#Vars_")):calc*)
1.183 -fun eval_var (thmid:string) "Tools.Vars"
1.184 - (t as (Const(op0,t0) $ arg)) thy =
1.185 - let
1.186 - val t' = ((list2isalist HOLogic.realT) o vars) t;
1.187 - val thmId = thmid^(Syntax.string_of_term @{context} arg);
1.188 - in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
1.189 - | eval_var _ _ _ _ = NONE;
1.190 -
1.191 -fun lhs (Const ("op =",_) $ l $ _) = l
1.192 - | lhs t = error("lhs called with (" ^ term2str t ^ ")");
1.193 -(*("lhs" ,("Tools.lhs" ,eval_lhs "")):calc*)
1.194 -fun eval_lhs _ "Tools.lhs"
1.195 - (t as (Const ("Tools.lhs",_) $ (Const ("op =",_) $ l $ _))) _ =
1.196 - SOME ((term2str t) ^ " = " ^ (term2str l),
1.197 - Trueprop $ (mk_equality (t, l)))
1.198 - | eval_lhs _ _ _ _ = NONE;
1.199 -(*
1.200 -> val t = (term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
1.201 -> val SOME (id,t') = eval_lhs 0 0 t 0;
1.202 -val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
1.203 -> term2str t';
1.204 -val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
1.205 -*)
1.206 -
1.207 -fun rhs (Const ("op =",_) $ _ $ r) = r
1.208 - | rhs t = error("rhs called with (" ^ term2str t ^ ")");
1.209 -(*("rhs" ,("Tools.rhs" ,eval_rhs "")):calc*)
1.210 -fun eval_rhs _ "Tools.rhs"
1.211 - (t as (Const ("Tools.rhs",_) $ (Const ("op =",_) $ _ $ r))) _ =
1.212 - SOME ((term2str t) ^ " = " ^ (term2str r),
1.213 - Trueprop $ (mk_equality (t, r)))
1.214 - | eval_rhs _ _ _ _ = NONE;
1.215 -
1.216 -
1.217 -(*for evaluating scripts*)
1.218 -
1.219 -val list_rls = append_rls "list_rls" list_rls
1.220 - [Calc ("Tools.rhs",eval_rhs "")];
1.221 -ruleset' := overwritelthy @{theory} (!ruleset',
1.222 - [("list_rls",list_rls)
1.223 - ]);
1.224 -calclist':= overwritel (!calclist',
1.225 - [("matches",("Tools.matches",eval_matches "#matches_")),
1.226 - ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")),
1.227 - ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
1.228 - ("lhs" ,("Tools.lhs" ,eval_lhs "")),
1.229 - ("rhs" ,("Tools.rhs" ,eval_rhs ""))
1.230 - ]);
1.231 -
1.232 -*}
1.233 -end