walther@59603: (* title: ProgLang/Prog_Expr.thy walther@59603: functions for expressions (which do NOT contain Prog_Tac and Tactical, by definition)) walther@59603: author: Walther Neuper, Aug.2019 walther@59603: (c) copyright due to lincense terms. walther@59603: *) walther@59603: walther@59619: theory Prog_Expr walther@59717: imports Calculate ListC Program walther@59603: begin walther@59603: walther@59619: text \Abstract: walther@59619: Specific constants are defined for pre-conditions of programs and for program-expressions. walther@59619: The constants are connected with ML functions for evaluation of respective expressions walther@59619: (all named eval_*), such that Isac's rewrite engine can handle it. walther@59619: \ walther@59619: walther@59603: subsection \consts of functions in pre-conditions and program-expressions\ walther@59603: consts walther@59603: lhs :: "bool => real" (*of an equality*) walther@59603: rhs :: "bool => real" (*of an equality*) walther@59603: Vars :: "'a => real list" (*get the variables of a term *) walther@59603: matches :: "['a, 'a] => bool" walther@59603: matchsub :: "['a, 'a] => bool" walther@60278: some_occur_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _") walther@60278: occurs_in :: "[real , 'a] => bool" ("_ occurs'_in _") walther@59603: walther@59603: abs :: "real => real" ("(|| _ ||)") walther@59619: (* ~~~ FIXXXME Isabelle2002 has abs already !!!*) walther@59603: absset :: "real set => real" ("(||| _ |||)") walther@60278: is_atom :: "real => bool" ("_ is'_atom" 10) walther@60343: is_num :: "real => bool" ("_ is'_num" 10) walther@60278: is_even :: "real => bool" ("_ is'_even" 10) walther@59603: walther@59603: (* identity on term level*) walther@59603: ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50) walther@60278: argument_in :: "real => real" ("argument'_in _" 10) walther@60278: sameFunId :: "[real, bool] => bool" (* "same_funid _ _" 10 walther@59619: WN0609 changed the id, because ".. _ _" inhibits currying *) walther@60278: filter_sameFunId:: "[real, bool list] => bool list" ("filter'_sameFunId _ _" 10) walther@59603: boollist2sum :: "bool list => real" walther@59603: lastI :: "'a list \ 'a" walther@59603: walther@59603: subsection \ML code for functions in pre-conditions and program-expressions\ walther@59603: ML \ walther@59603: signature PROG_EXPR = walther@59603: sig walther@59603: val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option Walther@60504: val eval_matches: string -> string -> term -> Proof.context -> (string * term) option walther@59603: val matchsub: theory -> term -> term -> bool Walther@60504: val eval_matchsub: string -> string -> term -> Proof.context -> (string * term) option walther@59603: val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option Walther@60504: val eval_var: string -> string -> term -> Proof.context -> (string * term) option walther@59603: walther@59603: val or2list: term -> term walther@60391: walther@59603: val occurs_in: term -> term -> bool walther@59603: val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option walther@59603: val some_occur_in: term list -> term -> bool walther@59603: val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option walther@59603: val eval_is_atom: string -> string -> term -> 'a -> (string * term) option walther@60343: val eval_is_num: string -> string -> term -> 'a -> (string * term) option walther@59603: val even: int -> bool walther@59603: val eval_is_even: string -> string -> term -> 'a -> (string * term) option walther@59603: val eval_equ: string -> string -> term -> 'a -> (string * term) option Walther@60504: val eval_ident: string -> string -> term -> Proof.context -> (string * term) option Walther@60504: val eval_equal: string -> string -> term -> Proof.context -> (string * term) option walther@59603: val eval_cancel: string -> string -> term -> 'a -> (string * term) option walther@59603: val eval_argument_in: string -> string -> term -> 'a -> (string * term) option walther@59603: val same_funid: term -> term -> bool walther@59603: val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option walther@59603: val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option walther@59603: val list2sum: term list -> term walther@59603: val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option walther@59603: walther@59603: val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string walther@59603: end walther@59603: walther@59603: (**) Walther@60504: structure Prog_Expr(**): PROG_EXPR(**) = walther@59603: struct walther@59603: (**) walther@59603: walther@59603: (*+ for Or_to_List +*) wenzelm@60309: fun or2list (Const (\<^const_name>\True\,_)) = ((*tracing"### or2list True";*) UniversalList) wenzelm@60309: | or2list (Const (\<^const_name>\False\,_)) = ((*tracing"### or2list False";*) EmptyList) wenzelm@60309: | or2list (t as Const (\<^const_name>\HOL.eq\,_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t] walther@59603: | or2list ors = walther@59618: let wenzelm@60309: fun get ls (Const (\<^const_name>\disj\,_) $ o1 $ o2) = walther@59618: (case o2 of wenzelm@60309: Const (\<^const_name>\disj\,_) $ _ $ _ => get (ls @ [o1]) o2 walther@59618: | _ => ls @ [o1, o2]) walther@59618: | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t]) walther@59618: in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end walther@59603: walther@59603: walther@59603: (** evaluation on the meta-level **) walther@59603: walther@59603: (*. evaluate the predicate matches (match on whole term only) .*) walther@59603: (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*) Walther@60504: fun eval_matches (_:string) "Prog_Expr.matches" Walther@60504: (t as Const (\<^const_name>\Prog_Expr.matches\, _) $ pat $ tst) ctxt = Walther@60504: if TermC.matches (Proof_Context.theory_of ctxt) tst pat walther@59603: then walther@59603: let walther@59603: val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})) Walther@60504: in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end walther@59603: else walther@59603: let walther@59603: val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})) Walther@60504: in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end walther@59603: | eval_matches _ _ _ _ = NONE; walther@59603: walther@59603: (*.does a pattern match some subterm ?.*) walther@59603: fun matchsub thy t pat = walther@59603: let walther@59603: fun matchs (t as Const _) = TermC.matches thy t pat walther@59603: | matchs (t as Free _) = TermC.matches thy t pat walther@59603: | matchs (t as Var _) = TermC.matches thy t pat walther@59603: | matchs (Bound _) = false walther@59603: | matchs (t as Abs (_, _, body)) = walther@59603: if TermC.matches thy t pat then true else TermC.matches thy body pat walther@59603: | matchs (t as f1 $ f2) = walther@59603: if TermC.matches thy t pat then true walther@59603: else if matchs f1 then true else matchs f2 walther@59603: in matchs t end; walther@59603: walther@59603: (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*) walther@59618: fun eval_matchsub (_:string) "Prog_Expr.matchsub" Walther@60504: (t as Const (\<^const_name>\Prog_Expr.matchsub\, _) $ pat $ tst) ctxt = Walther@60504: if matchsub (Proof_Context.theory_of ctxt) tst pat walther@59603: then walther@59603: let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})) Walther@60504: in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end walther@59603: else walther@59603: let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})) Walther@60504: in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end walther@59603: | eval_matchsub _ _ _ _ = NONE; walther@59603: walther@59603: (*get the variables in an isabelle-term*) walther@59603: (*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*) Walther@60504: fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) ctxt = walther@59603: let walther@59603: val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t; Walther@60504: val thmId = thmid ^ UnparseC.term_in_ctxt ctxt arg; walther@59603: in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end walther@59603: | eval_var _ _ _ _ = NONE; walther@59603: walther@59603: (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*) walther@60335: fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\lhs\,_) $ (Const (\<^const_name>\HOL.eq\,_) $ l $ _))) _ = walther@59868: SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l), walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (t, l))) walther@59603: | eval_lhs _ _ _ _ = NONE; walther@59603: wenzelm@60309: fun rhs (Const (\<^const_name>\HOL.eq\,_) $ _ $ r) = r walther@59962: | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")"); walther@59603: (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*) walther@60335: fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\rhs\,_) $ (Const (\<^const_name>\HOL.eq\,_) $ _ $ r))) _ = walther@59868: SOME (UnparseC.term t ^ " = " ^ UnparseC.term r, walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (t, r))) walther@59603: | eval_rhs _ _ _ _ = NONE; walther@59603: Walther@60504: walther@59603: fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v); walther@60278: (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*) walther@60335: fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\occurs_in\, _) $ v $ t)) _ = walther@59868: ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v)); walther@59868: tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*) walther@59603: if occurs_in v t walther@59868: then SOME ((UnparseC.term p) ^ " = True", walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) walther@59868: else SOME ((UnparseC.term p) ^ " = False", walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))) walther@59603: | eval_occurs_in _ _ _ _ = NONE; walther@59603: walther@59603: (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*) walther@59603: fun some_occur_in vs t = walther@59603: let fun occurs_in' a b = occurs_in b a walther@59603: in foldl or_ (false, map (occurs_in' t) vs) end; walther@59603: walther@60278: (*("some_occur_in", ("Prog_Expr.some_occur_in", walther@59603: eval_some_occur_in "#eval_some_occur_in_"))*) walther@60278: fun eval_some_occur_in _ "Prog_Expr.some_occur_in" walther@60335: (p as (Const (\<^const_name>\some_occur_in\,_) $ vs $ t)) _ = walther@59603: if some_occur_in (TermC.isalist2list vs) t walther@59868: then SOME ((UnparseC.term p) ^ " = True", walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) walther@59868: else SOME ((UnparseC.term p) ^ " = False", walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) walther@59603: | eval_some_occur_in _ _ _ _ = NONE; walther@59603: walther@60278: (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*) walther@60320: fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ = walther@60320: if TermC.is_atom arg walther@60322: then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", walther@60320: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) walther@60322: else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", walther@60320: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) walther@59603: | eval_is_atom _ _ _ _ = NONE; walther@59603: walther@60343: (*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*) walther@60343: fun eval_is_num (thmid:string) "Prog_Expr.is_num" (t as (Const _ $ arg)) _ = walther@60343: if TermC.is_num arg walther@60343: then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", walther@60343: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) walther@60343: else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", walther@60343: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) walther@60343: | eval_is_num _ _ _ _ = NONE; walther@60343: walther@59603: fun even i = (i div 2) * 2 = i; walther@60278: (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*) walther@60318: fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ = walther@60318: if TermC.is_num arg walther@60318: then walther@60318: let walther@60318: val i = arg |> HOLogic.dest_number |> snd walther@60318: in walther@60318: if even i walther@60318: then SOME (TermC.mk_thmid thmid (string_of_int i) "", walther@60318: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) walther@59603: else SOME (TermC.mk_thmid thmid "" "", walther@60318: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) walther@60318: end walther@60318: else NONE walther@59603: | eval_is_even _ _ _ _ = NONE; walther@59603: walther@59603: (*. evaluate binary, associative, commutative operators: *,+,^ .*) wenzelm@60309: (*("PLUS" ,(\<^const_name>\plus\ , (**)eval_binop "#add_")), wenzelm@60309: ("TIMES" ,(\<^const_name>\times\ , (**)eval_binop "#mult_")), wenzelm@60405: ("POWER" ,(\<^const_name>\realpow\ , (**)eval_binop "#power_"))*) walther@59603: walther@59603: (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) = walther@59603: ("xxxxxx",op_,t,thy); walther@59603: *) walther@59603: fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *) walther@59603: thmid ^ "Float ((" ^ walther@59997: (string_of_int v11)^", "^(string_of_int v12)^"), ("^ walther@59997: (string_of_int p11)^", "^(string_of_int p12)^")) __ (("^ walther@59997: (string_of_int v21)^", "^(string_of_int v22)^"), ("^ walther@59997: (string_of_int p21)^", "^(string_of_int p22)^"))"; walther@59603: walther@59603: (*.evaluate < and <= for numerals.*) wenzelm@60309: (*("le" ,(\<^const_name>\less\ , Prog_Expr.eval_equ "#less_")), wenzelm@60309: ("leq" ,(\<^const_name>\less_eq\ , Prog_Expr.eval_equ "#less_equal_"))*) walther@60331: walther@60317: fun eval_equ (thmid:string) (_(*op_*)) (t as (Const (op0, _)) $ t1 $ t2) _ = walther@60317: if TermC.is_num t1 andalso TermC.is_num t2 then walther@60317: let walther@60317: val n1 = t1 |> HOLogic.dest_number |> snd walther@60317: val n2 = t2 |> HOLogic.dest_number |> snd walther@60317: in walther@60317: if Eval.calc_equ (strip_thy op0) (n1, n2) walther@60317: then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2), walther@60317: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) walther@60317: else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2), walther@60317: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) walther@60317: end walther@60317: else NONE walther@59603: | eval_equ _ _ _ _ = NONE; walther@59603: walther@59603: walther@59603: (*evaluate identity walther@59603: > reflI; walther@59603: val it = "(?t = ?t) = True" walther@59603: > val t = str2term "x = 0"; Walther@60509: > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; walther@59603: walther@59603: > val t = str2term "1 = 0"; Walther@60509: > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; walther@59878: ----------- thus needs Rule.Eval ! walther@59603: > val t = str2term "0 = 0"; Walther@60509: > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; walther@59868: > UnparseC.term t'; wenzelm@60309: val it = \<^const_name>\True\ walther@59603: walther@59603: val t = str2term "Not (x = 0)"; walther@59868: atomt t; UnparseC.term t; walther@59603: *** ------------- walther@59603: *** Const ( Not) walther@59603: *** . Const ( op =) walther@59603: *** . . Free ( x, ) walther@59603: *** . . Free ( 0, ) walther@59603: val it = "x ~= 0" : string*) walther@59603: walther@59603: (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of walther@59603: the arguments: thus special handling by 'fun eval_binop'*) walther@59603: (*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*) walther@59603: fun eval_ident (thmid:string) "Prog_Expr.ident" (t as Walther@60504: (Const _(*op0, t0*) $ t1 $ t2 )) ctxt = walther@59603: if t1 = t2 walther@59603: then SOME (TermC.mk_thmid thmid Walther@60504: ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")") Walther@60504: ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"), walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) walther@59603: else SOME (TermC.mk_thmid thmid Walther@60504: ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")") Walther@60504: ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"), walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) walther@59603: | eval_ident _ _ _ _ = NONE; walther@59603: (* TODO walther@59603: > val t = str2term "x =!= 0"; walther@59603: > val SOME (str, t') = eval_ident "ident_" "b" t thy; walther@59868: > UnparseC.term t'; walther@59603: val str = "ident_(x)_(0)" : string walther@59603: val it = "(x =!= 0) = False" : string walther@59603: > val t = str2term "1 =!= 0"; walther@59603: > val SOME (str, t') = eval_ident "ident_" "b" t thy; walther@59868: > UnparseC.term t'; walther@59603: val str = "ident_(1)_(0)" : string walther@59603: val it = "(1 =!= 0) = False" : string walther@59603: > val t = str2term "0 =!= 0"; walther@59603: > val SOME (str, t') = eval_ident "ident_" "b" t thy; walther@59868: > UnparseC.term t'; walther@59603: val str = "ident_(0)_(0)" : string walther@59603: val it = "(0 =!= 0) = True" : string walther@59603: *) walther@59603: walther@59841: walther@59841: (* evaluate identity of terms, which stay ready for further evaluation; walther@59841: thus returns False only for atoms *) wenzelm@60309: (*("equal" ,(\<^const_name>\HOL.eq\, Prog_Expr.eval_equal "#equal_")):calc*) Walther@60504: fun eval_equal (thmid : string) \<^const_name>\HOL.eq\ (t as (Const _(*op0,t0*) $ t1 $ t2 )) ctxt = walther@59603: if t1 = t2 walther@59841: then walther@59841: SOME (TermC.mk_thmid thmid Walther@60504: ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"), walther@59841: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) walther@59841: else walther@59841: (case (TermC.is_atom t1, TermC.is_atom t2) of walther@59841: (true, true) => walther@59841: if TermC.variable_constant_pair (t1, t2) walther@59841: then NONE walther@59841: else SOME (TermC.mk_thmid thmid Walther@60504: ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"), walther@59841: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) walther@59841: | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *) walther@59841: | eval_equal _ _ _ _ = NONE; (* error-exit *) walther@59603: walther@59603: (*. evaluate HOL.divide .*) walther@59603: (*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*) walther@60317: fun eval_cancel thmid "Rings.divide_class.divide" (t as (Const _ $ t1 $ t2)) _ = walther@60317: if TermC.is_num t1 andalso TermC.is_num t2 then walther@60317: let walther@60317: val (T, _) = HOLogic.dest_number t1; walther@60317: val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2); walther@60392: val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2); walther@60317: in walther@60392: if abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') then NONE walther@60317: else walther@60317: let walther@60317: val res = TermC.mk_frac T res_int; walther@60317: val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); walther@60317: in SOME (TermC.mk_thmid thmid (string_of_int i1) (string_of_int i2), prop) end walther@60317: end walther@60317: else NONE walther@59603: | eval_cancel _ _ _ _ = NONE; walther@59603: walther@59603: (* get the argument from a function-definition *) walther@60278: (*("argument_in" ,("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"))*) walther@60278: fun eval_argument_in _ "Prog_Expr.argument_in" walther@60278: (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ = walther@60396: if TermC.is_atom arg (*could be something to be simplified before*) walther@59603: then walther@59868: SOME (UnparseC.term t ^ " = " ^ UnparseC.term arg, walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (t, arg))) walther@59603: else NONE walther@59603: | eval_argument_in _ _ _ _ = NONE; walther@59603: walther@59603: (* check if the function-identifier of the first argument matches walther@59603: the function-identifier of the lhs of the second argument *) walther@59603: (*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*) walther@59603: fun eval_sameFunId _ "Prog_Expr.sameFunId" wenzelm@60309: (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const (\<^const_name>\HOL.eq\, _) $ (f2 $ _) $ _)) _ = walther@59603: if f1 = f2 walther@59868: then SOME ((UnparseC.term p) ^ " = True", walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) walther@59868: else SOME ((UnparseC.term p) ^ " = False", walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) walther@59603: | eval_sameFunId _ _ _ _ = NONE; walther@59603: walther@59603: walther@59603: (*.from a list of fun-definitions "f x = ..." as 2nd argument walther@59603: filter the elements with the same fun-identfier in "f y" walther@59603: as the fst argument; walther@59603: this is, because Isabelles filter takes more than 1 sec.*) wenzelm@60309: fun same_funid f1 (Const (\<^const_name>\HOL.eq\, _) $ (f2 $ _) $ _) = f1 = f2 walther@59962: | same_funid f1 t = raise ERROR ("same_funid called with t = (" walther@59868: ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")"); walther@60278: (*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId", walther@60278: eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*) walther@60278: fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId" walther@60278: (p as Const ("Prog_Expr.filter_sameFunId",_) $ walther@59603: (fid $ _) $ fs) _ = walther@59603: let val fs' = ((TermC.list2isalist HOLogic.boolT) o walther@59603: (filter (same_funid fid))) (TermC.isalist2list fs) walther@59868: in SOME (UnparseC.term (TermC.mk_equality (p, fs')), walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end walther@59603: | eval_filter_sameFunId _ _ _ _ = NONE; walther@59603: walther@59603: (* make a list of terms to a sum *) walther@59962: fun list2sum [] = raise ERROR ("list2sum called with []") walther@59603: | list2sum [s] = s walther@59603: | list2sum (s::ss) = walther@59603: let wenzelm@60309: fun sum su [s'] = Const (\<^const_name>\plus\, walther@59603: [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s' wenzelm@60309: | sum su (s'::ss') = sum (Const (\<^const_name>\plus\, walther@59603: [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss' walther@59603: | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing" walther@59603: in sum s ss end; walther@59603: walther@59603: (* make a list of equalities to the sum of the lhs *) walther@59603: (*("boollist2sum" ,("Prog_Expr.boollist2sum" , eval_boollist2sum "")):calc*) walther@59603: fun eval_boollist2sum _ "Prog_Expr.boollist2sum" wenzelm@60309: (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const (\<^const_name>\Cons\, _) $ _ $ _)) _ = walther@59603: let walther@59603: val isal = TermC.isalist2list l walther@60391: val lhss = map TermC.lhs isal walther@59603: val sum = list2sum lhss walther@59603: in walther@59868: SOME ((UnparseC.term p) ^ " = " ^ (UnparseC.term sum), walther@59603: HOLogic.Trueprop $ (TermC.mk_equality (p, sum))) walther@59603: end walther@59603: | eval_boollist2sum _ _ _ _ = NONE; walther@59603: walther@59603: (**) end (*struct*) walther@59603: \ text \ walther@59603: open Prog_Expr walther@59603: \ ML \ walther@59603: \ ML \ walther@59603: \ walther@59603: walther@59603: subsection \extend rule-set for evaluating pre-conditions and program-expressions\ walther@59603: ML \ wenzelm@60294: val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [\<^rule_eval>\Prog_Expr.rhs\ (Prog_Expr.eval_rhs "")]; walther@59603: \ ML \ walther@59603: \ ML \ walther@59603: \ walther@59603: walther@59603: subsection \setup for rule-sets and ML-functions\ wenzelm@60286: wenzelm@60289: rule_set_knowledge prog_expr = prog_expr wenzelm@60313: walther@60387: calculation lhs = \Prog_Expr.eval_lhs ""\ walther@60387: calculation rhs = \Prog_Expr.eval_rhs ""\ walther@60387: calculation Vars = \Prog_Expr.eval_var "#Vars_"\ wenzelm@60313: calculation matches = \Prog_Expr.eval_matches "#matches_"\ wenzelm@60313: calculation matchsub = \Prog_Expr.eval_matchsub "#matchsub_"\ walther@60387: walther@60387: calculation some_occur_in = \Prog_Expr.eval_some_occur_in "#some_occur_in_"\ walther@60387: calculation occurs_in = \Prog_Expr.eval_occurs_in "#occurs_in_"\ walther@60387: calculation is_atom = \Prog_Expr.eval_is_atom "#is_atom_"\ walther@60387: calculation is_num = \Prog_Expr.eval_is_num "#is_num_"\ walther@60387: calculation is_even = \Prog_Expr.eval_is_even "#is_even_"\ walther@59603: ML \ walther@59603: \ ML \ walther@59603: \ ML \ walther@59603: \ walther@59603: walther@60275: end