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