1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Sep 03 12:40:27 2019 +0200
1.3 @@ -0,0 +1,615 @@
1.4 +(* title: ProgLang/Prog_Expr.thy
1.5 + functions for expressions (which do NOT contain Prog_Tac and Tactical, by definition))
1.6 + author: Walther Neuper, Aug.2019
1.7 + (c) copyright due to lincense terms.
1.8 +*)
1.9 +
1.10 +theory Prog_Expr imports Calculate
1.11 +begin
1.12 +
1.13 +subsection \<open>General constants\<close>
1.14 +consts
1.15 +(*//------------------------- from Tools .thy-------------------------------------------------\\*)
1.16 + EmptyList :: "bool list"
1.17 + UniversalList :: "bool list"
1.18 +(*\\------------------------- from Tools .thy ------------------------------------------------//*)
1.19 +(*\\------------------------- from Atools .thy -----------------------------------------------//*)
1.20 + Arbfix :: "real"
1.21 + Undef :: "real" (* WN190823 probably an outdated design for DiffApp *)
1.22 +
1.23 + pow :: "[real, real] => real" (infixr "^^^" 80)
1.24 +(*\\------------------------- from Atools.thy -----------------------------------------------//*)
1.25 +
1.26 +subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
1.27 +(*//------------------------- from Tools .thy-------------------------------------------------\\*)
1.28 +consts
1.29 + lhs :: "bool => real" (*of an equality*)
1.30 + rhs :: "bool => real" (*of an equality*)
1.31 + Vars :: "'a => real list" (*get the variables of a term *)
1.32 + matches :: "['a, 'a] => bool"
1.33 + matchsub :: "['a, 'a] => bool"
1.34 +(*\\------------------------- from Tools .thy-------------------------------------------------//*)
1.35 + some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
1.36 + occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
1.37 +
1.38 + abs :: "real => real" ("(|| _ ||)")
1.39 +(* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
1.40 + absset :: "real set => real" ("(||| _ |||)")
1.41 + (*is numeral constant ?*)
1.42 + is'_const :: "real => bool" ("_ is'_const" 10)
1.43 + (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
1.44 + is'_atom :: "real => bool" ("_ is'_atom" 10)
1.45 + is'_even :: "real => bool" ("_ is'_even" 10)
1.46 +
1.47 + (* identity on term level*)
1.48 + ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
1.49 +
1.50 + argument'_in :: "real => real" ("argument'_in _" 10)
1.51 + sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
1.52 + WN0609 changed the id, because ".. _ _" inhibits currying**)
1.53 + filter'_sameFunId:: "[real, bool list] => bool list"
1.54 + ("filter'_sameFunId _ _" 10)
1.55 + boollist2sum :: "bool list => real"
1.56 + lastI :: "'a list \<Rightarrow> 'a"
1.57 +
1.58 +subsection \<open>Theorems for rule-sets TODO: find a better location in code\<close>
1.59 +axiomatization where
1.60 + rle_refl: "(n::real) <= n" and
1.61 + not_true: "(~ True) = False" and
1.62 + not_false: "(~ False) = True" and
1.63 + and_true: "(a & True) = a" and
1.64 + and_false: "(a & False) = False" and
1.65 + or_true: "(a | True) = True" and
1.66 + or_false: "(a | False) = a" and
1.67 + and_commute: "(a & b) = (b & a)" and
1.68 + or_commute: "(a | b) = (b | a)"
1.69 +
1.70 +subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>
1.71 +ML \<open>
1.72 +signature PROG_EXPR =
1.73 + sig
1.74 +(*//------------------------- from Tools .thy-------------------------------------------------\\*)
1.75 + val EmptyList: term
1.76 + val UniversalList: term
1.77 +
1.78 + val lhs: term -> term
1.79 + val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
1.80 + val eval_matches: string -> string -> term -> theory -> (string * term) option
1.81 + val matchsub: theory -> term -> term -> bool
1.82 + val eval_matchsub: string -> string -> term -> theory -> (string * term) option
1.83 + val rhs: term -> term
1.84 + val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
1.85 + val eval_var: string -> string -> term -> theory -> (string * term) option
1.86 +
1.87 + val or2list: term -> term
1.88 +(*\\------------------------- from Tools .thy-------------------------------------------------//*)
1.89 +(*//------------------------- from Atools .thy------------------------------------------------\\*)
1.90 + val occurs_in: term -> term -> bool
1.91 + val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option
1.92 + val some_occur_in: term list -> term -> bool
1.93 + val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option
1.94 + val eval_is_atom: string -> string -> term -> 'a -> (string * term) option
1.95 + val even: int -> bool
1.96 + val eval_is_even: string -> string -> term -> 'a -> (string * term) option
1.97 + val eval_const: string -> string -> term -> 'a -> (string * term) option
1.98 + val eval_equ: string -> string -> term -> 'a -> (string * term) option
1.99 + val eval_ident: string -> string -> term -> theory -> (string * term) option
1.100 + val eval_equal: string -> string -> term -> theory -> (string * term) option
1.101 + val eval_cancel: string -> string -> term -> 'a -> (string * term) option
1.102 + val eval_argument_in: string -> string -> term -> 'a -> (string * term) option
1.103 + val same_funid: term -> term -> bool
1.104 + val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option
1.105 + val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option
1.106 + val list2sum: term list -> term
1.107 + val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option
1.108 +
1.109 + val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string
1.110 +(*\\------------------------- from Atools.thy------------------------------------------------//*)
1.111 + end
1.112 +
1.113 +(**)
1.114 +structure Prog_Expr(**): PROG_EXPR =(**)
1.115 +struct
1.116 +(**)
1.117 +(*//------------------------- from Tools .thy-------------------------------------------------\\*)
1.118 +(* auxiliary functions for scripts WN.9.00*)
1.119 +(*11.02: for equation solving only*)
1.120 +val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
1.121 +val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
1.122 +
1.123 +(*+ for Or_to_List +*)
1.124 +fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
1.125 + | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)
1.126 + | or2list (t as Const ("HOL.eq",_) $ _ $ _) =
1.127 + (tracing"### or2list _ = _"; TermC.list2isalist HOLogic.boolT [t])
1.128 + | or2list ors =
1.129 + (tracing"### or2list _ | _";
1.130 + let fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
1.131 + case o2 of
1.132 + Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
1.133 + | _ => ls @ [o1, o2]
1.134 + in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors)
1.135 + handle _ => error ("or2list: no ORs= "^(Rule.term2str ors)) end
1.136 + );
1.137 +(*>val t = @{term True};
1.138 +> val t' = or2list t;
1.139 +> term2str t';
1.140 +"Prog_Expr.UniversalList"
1.141 +> val t = @{term False};
1.142 +> val t' = or2list t;
1.143 +> term2str t';
1.144 +"[]"
1.145 +> val t=(Thm.term_of o the o (parse thy)) "x=3";
1.146 +> val t' = or2list t;
1.147 +> term2str t';
1.148 +"[x = 3]"
1.149 +> val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
1.150 +> val t' = or2list t;
1.151 +> term2str t';
1.152 +"[x = #3, x = #-3, x = #0]" : string *)
1.153 +
1.154 +
1.155 +(** evaluation on the meta-level **)
1.156 +
1.157 +(*. evaluate the predicate matches (match on whole term only) .*)
1.158 +(*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
1.159 +fun eval_matches (thmid:string) "Prog_Expr.matches"
1.160 + (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =
1.161 + if TermC.matches thy tst pat
1.162 + then
1.163 + let
1.164 + val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
1.165 + in SOME (Rule.term_to_string''' thy prop, prop) end
1.166 + else
1.167 + let
1.168 + val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
1.169 + in SOME (Rule.term_to_string''' thy prop, prop) end
1.170 + | eval_matches _ _ _ _ = NONE;
1.171 +(*
1.172 +> val t = (Thm.term_of o the o (parse thy))
1.173 + "matches (?x = 0) (1 * x ^^^ 2 = 0)";
1.174 +> eval_matches "/thmid/" "/op_/" t thy;
1.175 +val it =
1.176 + SOME
1.177 + ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
1.178 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.179 +
1.180 +> val t = (Thm.term_of o the o (parse thy))
1.181 + "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
1.182 +> eval_matches "/thmid/" "/op_/" t thy;
1.183 +val it =
1.184 + SOME
1.185 + ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
1.186 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.187 +
1.188 +> val t = (Thm.term_of o the o (parse thy))
1.189 + "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
1.190 +> eval_matches "/thmid/" "/op_/" t thy;
1.191 +val it =
1.192 + SOME
1.193 + ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
1.194 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.195 +
1.196 +> val t = (Thm.term_of o the o (parse thy))
1.197 + "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
1.198 +> eval_matches "/thmid/" "/op_/" t thy;
1.199 +val it =
1.200 + SOME
1.201 + ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
1.202 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.203 +----- before ?patterns ---:
1.204 +> val t = (Thm.term_of o the o (parse thy))
1.205 + "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
1.206 +> eval_matches "/thmid/" "/op_/" t thy;
1.207 +SOME
1.208 + ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
1.209 + Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
1.210 + : (string * term) option
1.211 +
1.212 +> val t = (Thm.term_of o the o (parse thy))
1.213 + "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
1.214 +> eval_matches "/thmid/" "/op_/" t thy;
1.215 +SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
1.216 + Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
1.217 +
1.218 +> val t = (Thm.term_of o the o (parse thy))
1.219 + "matches (a = b) (x + #1 + #-1 * #2 = #0)";
1.220 +> eval_matches "/thmid/" "/op_/" t thy;
1.221 +SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
1.222 +*)
1.223 +
1.224 +(*.does a pattern match some subterm ?.*)
1.225 +fun matchsub thy t pat =
1.226 + let
1.227 + fun matchs (t as Const _) = TermC.matches thy t pat
1.228 + | matchs (t as Free _) = TermC.matches thy t pat
1.229 + | matchs (t as Var _) = TermC.matches thy t pat
1.230 + | matchs (Bound _) = false
1.231 + | matchs (t as Abs (_, _, body)) =
1.232 + if TermC.matches thy t pat then true else TermC.matches thy body pat
1.233 + | matchs (t as f1 $ f2) =
1.234 + if TermC.matches thy t pat then true
1.235 + else if matchs f1 then true else matchs f2
1.236 + in matchs t end;
1.237 +
1.238 +(*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
1.239 +fun eval_matchsub (thmid:string) "Prog_Expr.matchsub"
1.240 + (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =
1.241 + if matchsub thy tst pat
1.242 + then
1.243 + let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
1.244 + in SOME (Rule.term_to_string''' thy prop, prop) end
1.245 + else
1.246 + let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
1.247 + in SOME (Rule.term_to_string''' thy prop, prop) end
1.248 + | eval_matchsub _ _ _ _ = NONE;
1.249 +
1.250 +(*get the variables in an isabelle-term*)
1.251 +(*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*)
1.252 +fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const(op0,t0) $ arg)) thy =
1.253 + let
1.254 + val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
1.255 + val thmId = thmid ^ Rule.term_to_string''' thy arg;
1.256 + in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
1.257 + | eval_var _ _ _ _ = NONE;
1.258 +
1.259 +fun lhs (Const ("HOL.eq",_) $ l $ _) = l
1.260 + | lhs t = error("lhs called with (" ^ Rule.term2str t ^ ")");
1.261 +(*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
1.262 +fun eval_lhs _ "Prog_Expr.lhs"
1.263 + (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
1.264 + SOME ((Rule.term2str t) ^ " = " ^ (Rule.term2str l),
1.265 + HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
1.266 + | eval_lhs _ _ _ _ = NONE;
1.267 +(*
1.268 +> val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
1.269 +> val SOME (id,t') = eval_lhs 0 0 t 0;
1.270 +val id = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
1.271 +> term2str t';
1.272 +val it = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
1.273 +*)
1.274 +
1.275 +fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
1.276 + | rhs t = error("rhs called with (" ^ Rule.term2str t ^ ")");
1.277 +(*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
1.278 +fun eval_rhs _ "Prog_Expr.rhs"
1.279 + (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
1.280 + SOME (Rule.term2str t ^ " = " ^ Rule.term2str r,
1.281 + HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
1.282 + | eval_rhs _ _ _ _ = NONE;
1.283 +(*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)
1.284 +
1.285 +(*//------------------------- from Atools.thy------------------------------------------------\\*)
1.286 +fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
1.287 +
1.288 +(*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
1.289 +fun eval_occurs_in _ "Prog_Expr.occurs'_in"
1.290 + (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
1.291 + ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));
1.292 + tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)
1.293 + if occurs_in v t
1.294 + then SOME ((Rule.term2str p) ^ " = True",
1.295 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.296 + else SOME ((Rule.term2str p) ^ " = False",
1.297 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
1.298 + | eval_occurs_in _ _ _ _ = NONE;
1.299 +
1.300 +(*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
1.301 +fun some_occur_in vs t =
1.302 + let fun occurs_in' a b = occurs_in b a
1.303 + in foldl or_ (false, map (occurs_in' t) vs) end;
1.304 +
1.305 +(*("some_occur_in", ("Prog_Expr.some'_occur'_in",
1.306 + eval_some_occur_in "#eval_some_occur_in_"))*)
1.307 +fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"
1.308 + (p as (Const ("Prog_Expr.some'_occur'_in",_)
1.309 + $ vs $ t)) _ =
1.310 + if some_occur_in (TermC.isalist2list vs) t
1.311 + then SOME ((Rule.term2str p) ^ " = True",
1.312 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.313 + else SOME ((Rule.term2str p) ^ " = False",
1.314 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.315 + | eval_some_occur_in _ _ _ _ = NONE;
1.316 +
1.317 +(*("is_atom",("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
1.318 +fun eval_is_atom (thmid:string) "Prog_Expr.is'_atom"
1.319 + (t as (Const _ $ arg)) _ =
1.320 + (case arg of
1.321 + Free (n,_) => SOME (TermC.mk_thmid thmid n "",
1.322 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.323 + | _ => SOME (TermC.mk_thmid thmid "" "",
1.324 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
1.325 + | eval_is_atom _ _ _ _ = NONE;
1.326 +
1.327 +fun even i = (i div 2) * 2 = i;
1.328 +(*("is_even",("Prog_Expr.is'_even", eval_is_even "#is_even_"))*)
1.329 +fun eval_is_even (thmid:string) "Prog_Expr.is'_even"
1.330 + (t as (Const _ $ arg)) _ =
1.331 + (case arg of
1.332 + Free (n,_) =>
1.333 + (case TermC.int_of_str_opt n of
1.334 + SOME i =>
1.335 + if even i then SOME (TermC.mk_thmid thmid n "",
1.336 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.337 + else SOME (TermC.mk_thmid thmid "" "",
1.338 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.339 + | _ => NONE)
1.340 + | _ => NONE)
1.341 + | eval_is_even _ _ _ _ = NONE;
1.342 +
1.343 +(*evaluate 'is_const'*)
1.344 +(*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)
1.345 +fun eval_const (thmid:string) _(*"Prog_Expr.is'_const" WN050820 diff.beh. rooteq*)
1.346 + (t as (Const _ $ arg)) _ =
1.347 + (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
1.348 + (case arg of
1.349 + Const (n1,_) =>
1.350 + SOME (TermC.mk_thmid thmid n1 "",
1.351 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.352 + | Free (n1,_) =>
1.353 + if TermC.is_num' n1
1.354 + then SOME (TermC.mk_thmid thmid n1 "",
1.355 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.356 + else SOME (TermC.mk_thmid thmid n1 "",
1.357 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.358 + | Const ("Float.Float",_) =>
1.359 + SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",
1.360 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.361 + | _ => (*NONE*)
1.362 + SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",
1.363 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
1.364 + | eval_const _ _ _ _ = NONE;
1.365 +
1.366 +(*. evaluate binary, associative, commutative operators: *,+,^ .*)
1.367 +(*("PLUS" ,("Groups.plus_class.plus" , (**)eval_binop "#add_")),
1.368 + ("TIMES" ,("Groups.times_class.times" , (**)eval_binop "#mult_")),
1.369 + ("POWER" ,("Prog_Expr.pow" , (**)eval_binop "#power_"))*)
1.370 +
1.371 +(* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
1.372 + ("xxxxxx",op_,t,thy);
1.373 + *)
1.374 +fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
1.375 + thmid ^ "Float ((" ^
1.376 + (string_of_int v11)^","^(string_of_int v12)^"), ("^
1.377 + (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
1.378 + (string_of_int v21)^","^(string_of_int v22)^"), ("^
1.379 + (string_of_int p21)^","^(string_of_int p22)^"))";
1.380 +
1.381 +(*.evaluate < and <= for numerals.*)
1.382 +(*("le" ,("Orderings.ord_class.less" , Prog_Expr.eval_equ "#less_")),
1.383 + ("leq" ,("Orderings.ord_class.less_eq" , Prog_Expr.eval_equ "#less_equal_"))*)
1.384 +fun eval_equ (thmid:string) (_(*op_*)) (t as
1.385 + (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =
1.386 + (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
1.387 + (SOME n1', SOME n2') =>
1.388 + if Calc.calc_equ (strip_thy op0) (n1', n2')
1.389 + then SOME (TermC.mk_thmid thmid n1 n2,
1.390 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.391 + else SOME (TermC.mk_thmid thmid n1 n2,
1.392 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.393 + | _ => NONE)
1.394 +
1.395 + | eval_equ _ _ _ _ = NONE;
1.396 +
1.397 +
1.398 +(*evaluate identity
1.399 +> reflI;
1.400 +val it = "(?t = ?t) = True"
1.401 +> val t = str2term "x = 0";
1.402 +> val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
1.403 +
1.404 +> val t = str2term "1 = 0";
1.405 +> val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
1.406 +----------- thus needs Rule.Calc !
1.407 +> val t = str2term "0 = 0";
1.408 +> val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
1.409 +> Rule.term2str t';
1.410 +val it = "HOL.True"
1.411 +
1.412 +val t = str2term "Not (x = 0)";
1.413 +atomt t; Rule.term2str t;
1.414 +*** -------------
1.415 +*** Const ( Not)
1.416 +*** . Const ( op =)
1.417 +*** . . Free ( x, )
1.418 +*** . . Free ( 0, )
1.419 +val it = "x ~= 0" : string*)
1.420 +
1.421 +(*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
1.422 + the arguments: thus special handling by 'fun eval_binop'*)
1.423 +(*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)
1.424 +fun eval_ident (thmid:string) "Prog_Expr.ident" (t as
1.425 + (Const _(*op0, t0*) $ t1 $ t2 )) thy =
1.426 + if t1 = t2
1.427 + then SOME (TermC.mk_thmid thmid
1.428 + ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
1.429 + ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
1.430 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.431 + else SOME (TermC.mk_thmid thmid
1.432 + ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
1.433 + ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
1.434 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.435 + | eval_ident _ _ _ _ = NONE;
1.436 +(* TODO
1.437 +> val t = str2term "x =!= 0";
1.438 +> val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.439 +> Rule.term2str t';
1.440 +val str = "ident_(x)_(0)" : string
1.441 +val it = "(x =!= 0) = False" : string
1.442 +> val t = str2term "1 =!= 0";
1.443 +> val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.444 +> Rule.term2str t';
1.445 +val str = "ident_(1)_(0)" : string
1.446 +val it = "(1 =!= 0) = False" : string
1.447 +> val t = str2term "0 =!= 0";
1.448 +> val SOME (str, t') = eval_ident "ident_" "b" t thy;
1.449 +> Rule.term2str t';
1.450 +val str = "ident_(0)_(0)" : string
1.451 +val it = "(0 =!= 0) = True" : string
1.452 +*)
1.453 +
1.454 +(*.evaluate identity of terms, which stay ready for evaluation in turn;
1.455 + thus returns False only for atoms.*)
1.456 +(*("equal" ,("HOL.eq", Prog_Expr.eval_equal "#equal_")):calc*)
1.457 +fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
1.458 + if t1 = t2
1.459 + then SOME (TermC.mk_thmid thmid
1.460 + ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
1.461 + ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
1.462 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.463 + else (case (TermC.is_atom t1, TermC.is_atom t2) of
1.464 + (true, true) =>
1.465 + SOME (TermC.mk_thmid thmid
1.466 + ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
1.467 + ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
1.468 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.469 + | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
1.470 + | eval_equal _ _ _ _ = NONE; (* error-exit *)
1.471 +(*
1.472 +val t = str2term "x ~= 0";
1.473 +val NONE = eval_equal "equal_" "b" t thy;
1.474 +
1.475 +
1.476 +> val t = str2term "(x + 1) = (x + 1)";
1.477 +> val SOME (str, t') = eval_equal "equal_" "b" t thy;
1.478 +> Rule.term2str t';
1.479 +val str = "equal_(x + 1)_(x + 1)" : string
1.480 +val it = "(x + 1 = x + 1) = True" : string
1.481 +> val t = str2term "x = 0";
1.482 +> val NONE = eval_equal "equal_" "b" t thy;
1.483 +
1.484 +> val t = str2term "1 = 0";
1.485 +> val SOME (str, t') = eval_equal "equal_" "b" t thy;
1.486 +> Rule.term2str t';
1.487 +val str = "equal_(1)_(0)" : string
1.488 +val it = "(1 = 0) = False" : string
1.489 +> val t = str2term "0 = 0";
1.490 +> val SOME (str, t') = eval_equal "equal_" "b" t thy;
1.491 +> Rule.term2str t';
1.492 +val str = "equal_(0)_(0)" : string
1.493 +val it = "(0 = 0) = True" : string
1.494 +*)
1.495 +
1.496 +(*. evaluate HOL.divide .*)
1.497 +(*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
1.498 +fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as
1.499 + (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =
1.500 + (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
1.501 + (SOME n1', SOME n2') =>
1.502 + let
1.503 + val sg = Calc.sign_mult n1' n2';
1.504 + val (T1,T2,Trange) = TermC.dest_binop_typ t0;
1.505 + val gcd' = Calc.gcd (abs n1') (abs n2');
1.506 + in if gcd' = abs n2'
1.507 + then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
1.508 + val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
1.509 + in SOME (TermC.mk_thmid thmid n1 n2, prop) end
1.510 + else if 0 < n2' andalso gcd' = 1 then NONE
1.511 + else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
1.512 + ((abs n2') div gcd')
1.513 + val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
1.514 + in SOME (TermC.mk_thmid thmid n1 n2, prop) end
1.515 + end
1.516 + | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
1.517 + | eval_cancel _ _ _ _ = NONE;
1.518 +
1.519 +(* get the argument from a function-definition *)
1.520 +(*("argument_in" ,("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"))*)
1.521 +fun eval_argument_in _ "Prog_Expr.argument'_in"
1.522 + (t as (Const ("Prog_Expr.argument'_in", _) $ (_(*f*) $ arg))) _ =
1.523 + if is_Free arg (*could be something to be simplified before*)
1.524 + then
1.525 + SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,
1.526 + HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
1.527 + else NONE
1.528 + | eval_argument_in _ _ _ _ = NONE;
1.529 +
1.530 +(* check if the function-identifier of the first argument matches
1.531 + the function-identifier of the lhs of the second argument *)
1.532 +(*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)
1.533 +fun eval_sameFunId _ "Prog_Expr.sameFunId"
1.534 + (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
1.535 + if f1 = f2
1.536 + then SOME ((Rule.term2str p) ^ " = True",
1.537 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.538 + else SOME ((Rule.term2str p) ^ " = False",
1.539 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.540 +| eval_sameFunId _ _ _ _ = NONE;
1.541 +
1.542 +
1.543 +(*.from a list of fun-definitions "f x = ..." as 2nd argument
1.544 + filter the elements with the same fun-identfier in "f y"
1.545 + as the fst argument;
1.546 + this is, because Isabelles filter takes more than 1 sec.*)
1.547 +fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
1.548 + | same_funid f1 t = error ("same_funid called with t = ("
1.549 + ^Rule.term2str f1^") ("^Rule.term2str t^")");
1.550 +(*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",
1.551 + eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)
1.552 +fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId"
1.553 + (p as Const ("Prog_Expr.filter'_sameFunId",_) $
1.554 + (fid $ _) $ fs) _ =
1.555 + let val fs' = ((TermC.list2isalist HOLogic.boolT) o
1.556 + (filter (same_funid fid))) (TermC.isalist2list fs)
1.557 + in SOME (Rule.term2str (TermC.mk_equality (p, fs')),
1.558 + HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
1.559 +| eval_filter_sameFunId _ _ _ _ = NONE;
1.560 +
1.561 +(* make a list of terms to a sum *)
1.562 +fun list2sum [] = error ("list2sum called with []")
1.563 + | list2sum [s] = s
1.564 + | list2sum (s::ss) =
1.565 + let
1.566 + fun sum su [s'] = Const ("Groups.plus_class.plus",
1.567 + [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
1.568 + | sum su (s'::ss') = sum (Const ("Groups.plus_class.plus",
1.569 + [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'
1.570 + | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing"
1.571 + in sum s ss end;
1.572 +
1.573 +(* make a list of equalities to the sum of the lhs *)
1.574 +(*("boollist2sum" ,("Prog_Expr.boollist2sum" , eval_boollist2sum "")):calc*)
1.575 +fun eval_boollist2sum _ "Prog_Expr.boollist2sum"
1.576 + (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
1.577 + let
1.578 + val isal = TermC.isalist2list l
1.579 + val lhss = map lhs isal
1.580 + val sum = list2sum lhss
1.581 + in
1.582 + SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
1.583 + HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
1.584 + end
1.585 + | eval_boollist2sum _ _ _ _ = NONE;
1.586 +
1.587 +(**) end (*struct*)
1.588 +\<close> text \<open>
1.589 +open Prog_Expr
1.590 +\<close> ML \<open>
1.591 +
1.592 +\<close> ML \<open>
1.593 +\<close> ML \<open>
1.594 +\<close> ML \<open>
1.595 +\<close>
1.596 +
1.597 +subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
1.598 +ML \<open>
1.599 +val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
1.600 +\<close> ML \<open>
1.601 +\<close> ML \<open>
1.602 +\<close>
1.603 +
1.604 +subsection \<open>setup for rule-sets and ML-functions\<close>
1.605 +setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
1.606 +setup \<open>KEStore_Elems.add_calcs
1.607 + [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),
1.608 + ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),
1.609 + ("Vars", ("Prog_Expr.Vars", Prog_Expr.eval_var "#Vars_")),
1.610 + ("lhs", ("Prog_Expr.lhs", Prog_Expr.eval_lhs "")),
1.611 + ("rhs", ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""))]\<close>
1.612 +(*\\------------------------- from Tools .thy-------------------------------------------------//*)
1.613 +ML \<open>
1.614 +\<close> ML \<open>
1.615 +\<close> ML \<open>
1.616 +\<close>
1.617 +
1.618 +end
1.619 \ No newline at end of file