1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,230 @@
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"ProgLang/Tools";
1.12 +*)
1.13 +
1.14 +theory Tools imports ListC begin
1.15 +
1.16 +(*belongs to theory ListC*)
1.17 +ML {*
1.18 +val first_isac_thy = @{theory ListC}
1.19 +*}
1.20 +
1.21 +(*for Descript.thy*)
1.22 +
1.23 + (***********************************************************************)
1.24 + (* 'fun is_dsc' in ProgLang/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 ProgLang/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