
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 \<open>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: \<close>
walther@59619: 
walther@59619: subsection \<open>Power re-defined for a specific type\<close>
walther@60275: abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
walther@60275: where "x \<up> a \<equiv> x powr a"
walther@59603: 
walther@59603: subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
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 \<Rightarrow> 'a"
walther@59603: 
walther@59603: subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>
walther@59603: ML \<open>
walther@59603: signature PROG_EXPR =
walther@59603:   sig
walther@59603: (*//------------------------- from Tools .thy-------------------------------------------------\\*)
walther@59603:     val lhs: term -> term
walther@59603:     val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
walther@59603:     val eval_matches: string -> string -> term -> theory -> (string * term) option
walther@59603:     val matchsub: theory -> term -> term -> bool
walther@59603:     val eval_matchsub: string -> string -> term -> theory -> (string * term) option
walther@59603:     val rhs: term -> term
walther@59603:     val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
walther@59603:     val eval_var: string -> string -> term -> theory -> (string * term) option
walther@59603: 
walther@59603:     val or2list: term -> term
walther@59603: (*\\------------------------- from Tools .thy-------------------------------------------------//*)
walther@59603: (*//------------------------- from Atools .thy------------------------------------------------\\*)
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_const: string -> string -> term -> 'a -> (string * term) option
walther@59603:     val eval_equ: string -> string -> term -> 'a -> (string * term) option
walther@59603:     val eval_ident: string -> string -> term -> theory -> (string * term) option
walther@59603:     val eval_equal: string -> string -> term -> theory -> (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@59603: 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>\<open>True\<close>,_)) = ((*tracing"### or2list True";*) UniversalList)
wenzelm@60309:   | or2list (Const (\<^const_name>\<open>False\<close>,_)) = ((*tracing"### or2list False";*) EmptyList)
wenzelm@60309:   | or2list (t as Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
walther@59603:   | or2list ors =
walther@59618:     let
wenzelm@60309:       fun get ls (Const (\<^const_name>\<open>disj\<close>,_) $ o1 $ o2) =
walther@59618: 	        (case o2 of
wenzelm@60309: 	         	Const (\<^const_name>\<open>disj\<close>,_) $ _ $ _ => 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: (*>val t = @{term True};
walther@59603: > val t' = or2list t;
walther@59603: > term2str t';
walther@59620: "ListC.UniversalList"
walther@59603: > val t = @{term False};
walther@59603: > val t' = or2list t;
walther@59603: > term2str t';
walther@59603: "[]"
walther@59603: > val t=(Thm.term_of o the o (parse thy)) "x=3";
walther@59603: > val t' = or2list t;
walther@59603: > term2str t';
walther@59603: "[x = 3]"
walther@59603: > val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
walther@59603: > val t' = or2list t;
walther@59603: > term2str t';
walther@59603: "[x = #3, x = #-3, x = #0]" : string *)
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@60335: fun eval_matches (_:string) "Prog_Expr.matches" (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) thy = 
walther@59603:     if TermC.matches thy tst pat
walther@59603:     then 
walther@59603:       let
walther@59603:         val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
walther@59870: 	    in SOME (UnparseC.term_in_thy thy prop, prop) end
walther@59603:     else 
walther@59603:       let 
walther@59603:         val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
walther@59870: 	    in SOME (UnparseC.term_in_thy thy prop, prop) end
walther@59603:   | eval_matches _ _ _ _ = NONE; 
walther@59603: (*
walther@59603: > val t  = (Thm.term_of o the o (parse thy)) 
walther@60242: 	      "matches (?x = 0) (1 * x \<up> 2 = 0)";
walther@59603: > eval_matches "/thmid/" "/op_/" t thy;
walther@59603: val it =
walther@59603:   SOME
walther@60242:     ("matches (x = 0) (1 * x \<up> 2 = 0) = False",
walther@59603:      Const (#,#) $ (# $ # $ Const #)) : (string * term) option
walther@59603: 
walther@59603: > val t  = (Thm.term_of o the o (parse thy)) 
walther@60242: 	      "matches (?a = #0) (#1 * x \<up> #2 = #0)";
walther@59603: > eval_matches "/thmid/" "/op_/" t thy;
walther@59603: val it =
walther@59603:   SOME
walther@60242:     ("matches (?a = #0) (#1 * x \<up> #2 = #0) = True",
walther@59603:      Const (#,#) $ (# $ # $ Const #)) : (string * term) option
walther@59603: 
walther@59603: > val t  = (Thm.term_of o the o (parse thy)) 
walther@60242: 	      "matches (?a * x = #0) (#1 * x \<up> #2 = #0)";
walther@59603: > eval_matches "/thmid/" "/op_/" t thy;
walther@59603: val it =
walther@59603:   SOME
walther@60242:     ("matches (?a * x = #0) (#1 * x \<up> #2 = #0) = False",
walther@59603:      Const (#,#) $ (# $ # $ Const #)) : (string * term) option
walther@59603: 
walther@59603: > val t  = (Thm.term_of o the o (parse thy)) 
walther@60242: 	      "matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0)";
walther@59603: > eval_matches "/thmid/" "/op_/" t thy;
walther@59603: val it =
walther@59603:   SOME
walther@60242:     ("matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0) = True",
walther@59603:      Const (#,#) $ (# $ # $ Const #)) : (string * term) option                  
walther@59603: ----- before ?patterns ---:
walther@59603: > val t  = (Thm.term_of o the o (parse thy)) 
walther@60260: 	      "matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1)";
walther@59603: > eval_matches "/thmid/" "/op_/" t thy;
walther@59603: SOME
walther@60242:     ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1) = True",
walther@59997:      Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
walther@59603:   : (string * term) option 
walther@59603: 
walther@59603: > val t = (Thm.term_of o the o (parse thy)) 
walther@60260: 	      "matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1)";
walther@59603: > eval_matches "/thmid/" "/op_/" t thy;
walther@60242: SOME ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1) = False",
walther@59997:      Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
walther@59603: 
walther@59603: > val t = (Thm.term_of o the o (parse thy)) 
walther@59603:                "matches (a = b) (x + #1 + #-1 * #2 = #0)";
walther@59603: > eval_matches "/thmid/" "/op_/" t thy;
walther@59603: SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
walther@59603: *)
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@60335:       (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) thy = 
walther@59603:     if matchsub thy tst pat
walther@59603:     then 
walther@59603:       let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
walther@59870:       in SOME (UnparseC.term_in_thy thy prop, prop) end
walther@59603:     else 
walther@59603:       let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
walther@59870:       in SOME (UnparseC.term_in_thy thy 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@59618: fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy = 
walther@59603:     let 
walther@59603:       val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
walther@59870:       val thmId = thmid ^ UnparseC.term_in_thy thy arg;
walther@59603:     in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
walther@59603:   | eval_var _ _ _ _ = NONE;
walther@59603: 
walther@60089: (* refer to Thm.lhs_of *)
wenzelm@60309: fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
walther@59962:   | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
walther@59603: (*("lhs"    ,("Prog_Expr.lhs"    , eval_lhs "")):calc*)
walther@60335: fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ 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: (*
walther@60242: > val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x \<up> 2 = 0)";
walther@59603: > val SOME (id,t') = eval_lhs 0 0 t 0;
walther@60242: val id = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
walther@59603: > term2str t';
walther@60242: val it = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
walther@59603: *)
walther@59603: 
wenzelm@60309: fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ 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>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ 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: (*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)
walther@59603: 
walther@59603: (*//------------------------- from Atools.thy------------------------------------------------\\*)
walther@59603: fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
walther@59603: 
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>\<open>occurs_in\<close>, _) $ 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>\<open>some_occur_in\<close>,_) $ 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@60385: (*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
walther@60385: fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
walther@60318:     (*TODO get rid of this special case*)
walther@60318:     SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
walther@60318:       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
walther@60385:   | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const _)) _ =
walther@60318:     SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
walther@60318:       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
walther@60385:   | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ n)) _ =
walther@60318: 	   if TermC.is_num n
walther@60318: 	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
walther@60318:        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
walther@60318: 	   else SOME (TermC.mk_thmid thmid (UnparseC.term n) "",
walther@60318:        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
walther@59603:   | eval_const _ _ _ _ = NONE; 
walther@59603: 
walther@59603: (*. evaluate binary, associative, commutative operators: *,+,^ .*)
wenzelm@60309: (*("PLUS"    ,(\<^const_name>\<open>plus\<close>        , (**)eval_binop "#add_")),
wenzelm@60309:   ("TIMES"   ,(\<^const_name>\<open>times\<close>        , (**)eval_binop "#mult_")),
wenzelm@60309:   ("POWER"  ,(\<^const_name>\<open>powr\<close>  , (**)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>\<open>less\<close>        , Prog_Expr.eval_equ "#less_")),
wenzelm@60309:   ("leq"     ,(\<^const_name>\<open>less_eq\<close>       , 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@59857: > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
walther@59603: 
walther@59603: > val t = str2term "1 = 0";
walther@59857: > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
walther@59878: ----------- thus needs Rule.Eval !
walther@59603: > val t = str2term "0 = 0";
walther@59857: > val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
walther@59868: > UnparseC.term t';
wenzelm@60309: val it = \<^const_name>\<open>True\<close>
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@59603: 	       (Const _(*op0, t0*) $ t1 $ t2 )) thy = 
walther@59603:   if t1 = t2
walther@59603:   then SOME (TermC.mk_thmid thmid 
walther@59870: 	              ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
walther@59870: 	              ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"), 
walther@59603: 	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
walther@59603:   else SOME (TermC.mk_thmid thmid  
walther@59870: 	              ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
walther@59870: 	              ("(" ^ (UnparseC.term_in_thy thy 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>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*)
wenzelm@60309: fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy = 
walther@59603:   if t1 = t2
walther@59841:   then
walther@59841:     SOME (TermC.mk_thmid thmid
walther@59870:       ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy 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@59870:           ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy 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@60317:         val res_int as (_, (i1', i2')) = Eval.cancel_int (i1, i2);
walther@60317:       in
walther@60317:         if (i1', i2') = (i1, 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@59603:     if is_Free 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>\<open>HOL.eq\<close>, _) $ (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>\<open>HOL.eq\<close>, _) $ (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>\<open>plus\<close>,
walther@59603:            [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
wenzelm@60309:     	  | sum su (s'::ss') = sum (Const (\<^const_name>\<open>plus\<close>,
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>\<open>Cons\<close>, _) $ _ $ _)) _ =
walther@59603:     let
walther@59603:       val isal = TermC.isalist2list l
walther@59603: 	    val lhss = map 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: \<close> text \<open>
walther@59603: open Prog_Expr
walther@59603: \<close> ML \<open>
walther@59603: \<close> ML \<open>
walther@59603: \<close>
walther@59603: 
walther@59603: subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
walther@59603: ML \<open>
wenzelm@60294: val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "")];
walther@59603: \<close> ML \<open>
walther@59603: \<close> ML \<open>
walther@59603: \<close>
walther@59603: 
walther@59603: subsection \<open>setup for rule-sets and ML-functions\<close>
wenzelm@60286: 
wenzelm@60289: rule_set_knowledge prog_expr = prog_expr
wenzelm@60313: 
wenzelm@60313: calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>
wenzelm@60313: calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>
wenzelm@60313: calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
wenzelm@60313: calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
wenzelm@60313: calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
walther@59603: (*\\------------------------- from Tools .thy-------------------------------------------------//*)
walther@59603: ML \<open>
walther@59603: \<close> ML \<open>
walther@59603: \<close> ML \<open>
walther@59603: \<close>
walther@59603: 
walther@60275: end




