wneuper/isa: src/Tools/isac/ProgLang/Prog

     1 (* title:  ProgLang/Prog_Expr.thy

     2            functions for expressions (which do NOT contain Prog_Tac and Tactical, by definition))

     3    author: Walther Neuper, Aug.2019

     4    (c) copyright due to lincense terms.

     5 *)

     7 theory Prog_Expr

     8   imports Calculate ListC Program

     9 begin

    11 text \<open>Abstract:

    12   Specific constants are defined for pre-conditions of programs and for program-expressions.

    13   The constants are connected with ML functions for evaluation of respective expressions

    14   (all named eval_*), such that Isac's rewrite engine can handle it.

    15 \<close>

    17 subsection \<open>Power re-defined for a specific type\<close>

    18 consts

    19   pow              :: "[real, real] => real"    (infixr "^^^" 80)

    21 subsection \<open>consts of functions in pre-conditions and program-expressions\<close>

    22 consts

    23   lhs             :: "bool => real"           (*of an equality*)

    24   rhs             :: "bool => real"           (*of an equality*)

    25   Vars            :: "'a => real list"        (*get the variables of a term *)

    26   matches         :: "['a, 'a] => bool"

    27   matchsub        :: "['a, 'a] => bool"

    28   some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")

    29   occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")

    31   abs              :: "real => real"            ("(|| _ ||)")

    32   (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)

    33   absset           :: "real set => real"        ("(||| _ |||)")

    34   (*is numeral constant ?*)

    35   is'_const        :: "real => bool"            ("_ is'_const" 10)

    36   (*is_const rename to is_num FIXXXME.WN.16.5.03 *)

    37   is'_atom         :: "real => bool"            ("_ is'_atom" 10)

    38   is'_even         :: "real => bool"            ("_ is'_even" 10)

    40   (* identity on term level*)

    41   ident            :: "['a, 'a] => bool"        ("(_ =!=/ _)" [51, 51] 50)

    42   argument'_in     :: "real => real"            ("argument'_in _" 10)

    43   sameFunId        :: "[real, bool] => bool"    (* "same'_funid _ _" 10

    44 	                    WN0609 changed the id, because ".. _ _" inhibits currying *)

    45   filter'_sameFunId:: "[real, bool list] => bool list"

    46 					        ("filter'_sameFunId _ _" 10)

    47   boollist2sum     :: "bool list => real"

    48   lastI            :: "'a list \<Rightarrow> 'a"

    50 subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>

    51 ML \<open>

    52 signature PROG_EXPR =

    53   sig

    54 (*//------------------------- from Tools .thy-------------------------------------------------\\*)

    55     val lhs: term -> term

    56     val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option

    57     val eval_matches: string -> string -> term -> theory -> (string * term) option

    58     val matchsub: theory -> term -> term -> bool

    59     val eval_matchsub: string -> string -> term -> theory -> (string * term) option

    60     val rhs: term -> term

    61     val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option

    62     val eval_var: string -> string -> term -> theory -> (string * term) option

    64     val or2list: term -> term

    65 (*\\------------------------- from Tools .thy-------------------------------------------------//*)

    66 (*//------------------------- from Atools .thy------------------------------------------------\\*)

    67     val occurs_in: term -> term -> bool

    68     val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option

    69     val some_occur_in: term list -> term -> bool

    70     val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option

    71     val eval_is_atom: string -> string -> term -> 'a -> (string * term) option

    72     val even: int -> bool

    73     val eval_is_even: string -> string -> term -> 'a -> (string * term) option

    74     val eval_const: string -> string -> term -> 'a -> (string * term) option

    75     val eval_equ: string -> string -> term -> 'a -> (string * term) option

    76     val eval_ident: string -> string -> term -> theory -> (string * term) option

    77     val eval_equal: string -> string -> term -> theory -> (string * term) option

    78     val eval_cancel: string -> string -> term -> 'a -> (string * term) option

    79     val eval_argument_in: string -> string -> term -> 'a -> (string * term) option

    80     val same_funid: term -> term -> bool

    81     val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option

    82     val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option

    83     val list2sum: term list -> term

    84     val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option

    86     val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string

    87 (*\\------------------------- from Atools.thy------------------------------------------------//*)

    88 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

    89   (*NONE*)

    90 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    91   (*NONE*)

    92 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

    93   end

    95 (**)

    96 structure Prog_Expr(**): PROG_EXPR =(**)

    97 struct

    98 (**)

   100 (*+ for Or_to_List +*)

   101 fun or2list (Const ("HOL.True",_)) = ((*tracing"### or2list True";*) UniversalList)

   102   | or2list (Const ("HOL.False",_)) = ((*tracing"### or2list False";*) EmptyList)

   103   | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]

   104   | or2list ors =

   105     let

   106       fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =

   107 	        (case o2 of

   108 	         	Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2

   109 	        | _ => ls @ [o1, o2])

   110         | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])

   111     in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end

   112 (*>val t = @{term True};

   113 > val t' = or2list t;

   114 > term2str t';

   115 "ListC.UniversalList"

   116 > val t = @{term False};

   117 > val t' = or2list t;

   118 > term2str t';

   119 "[]"

   120 > val t=(Thm.term_of o the o (parse thy)) "x=3";

   121 > val t' = or2list t;

   122 > term2str t';

   123 "[x = 3]"

   124 > val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";

   125 > val t' = or2list t;

   126 > term2str t';

   127 "[x = #3, x = #-3, x = #0]" : string *)

   130 (** evaluation on the meta-level **)

   132 (*. evaluate the predicate matches (match on whole term only) .*)

   133 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)

   134 fun eval_matches (_:string) "Prog_Expr.matches" (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =

   135     if TermC.matches thy tst pat

   136     then

   137       let

   138         val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))

   139 	    in SOME (Rule.term_to_string''' thy prop, prop) end

   140     else

   141       let

   142         val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))

   143 	    in SOME (Rule.term_to_string''' thy prop, prop) end

   144   | eval_matches _ _ _ _ = NONE;

   145 (*

   146 > val t  = (Thm.term_of o the o (parse thy))

   147 	      "matches (?x = 0) (1 * x ^^^ 2 = 0)";

   148 > eval_matches "/thmid/" "/op_/" t thy;

   149 val it =

   150   SOME

   151     ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",

   152      Const (#,#) $ (# $ # $ Const #)) : (string * term) option

   154 > val t  = (Thm.term_of o the o (parse thy))

   155 	      "matches (?a = #0) (#1 * x ^^^ #2 = #0)";

   156 > eval_matches "/thmid/" "/op_/" t thy;

   157 val it =

   158   SOME

   159     ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",

   160      Const (#,#) $ (# $ # $ Const #)) : (string * term) option

   162 > val t  = (Thm.term_of o the o (parse thy))

   163 	      "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";

   164 > eval_matches "/thmid/" "/op_/" t thy;

   165 val it =

   166   SOME

   167     ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",

   168      Const (#,#) $ (# $ # $ Const #)) : (string * term) option

   170 > val t  = (Thm.term_of o the o (parse thy))

   171 	      "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";

   172 > eval_matches "/thmid/" "/op_/" t thy;

   173 val it =

   174   SOME

   175     ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",

   176      Const (#,#) $ (# $ # $ Const #)) : (string * term) option

   177 ----- before ?patterns ---:

   178 > val t  = (Thm.term_of o the o (parse thy))

   179 	      "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";

   180 > eval_matches "/thmid/" "/op_/" t thy;

   181 SOME

   182     ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",

   183      Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

   184   : (string * term) option

   186 > val t = (Thm.term_of o the o (parse thy))

   187 	      "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";

   188 > eval_matches "/thmid/" "/op_/" t thy;

   189 SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",

   190      Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

   192 > val t = (Thm.term_of o the o (parse thy))

   193                "matches (a = b) (x + #1 + #-1 * #2 = #0)";

   194 > eval_matches "/thmid/" "/op_/" t thy;

   195 SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))

   196 *)

   198 (*.does a pattern match some subterm ?.*)

   199 fun matchsub thy t pat =

   200   let

   201     fun matchs (t as Const _) = TermC.matches thy t pat

   202 	      | matchs (t as Free _) = TermC.matches thy t pat

   203 	      | matchs (t as Var _) = TermC.matches thy t pat

   204 	      | matchs (Bound _) = false

   205 	      | matchs (t as Abs (_, _, body)) =

   206 	          if TermC.matches thy t pat then true else TermC.matches thy body pat

   207 	      | matchs (t as f1 $ f2) =

   208 	          if TermC.matches thy t pat then true

   209 	            else if matchs f1 then true else matchs f2

   210   in matchs t end;

   212 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)

   213 fun eval_matchsub (_:string) "Prog_Expr.matchsub"

   214       (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =

   215     if matchsub thy tst pat

   216     then

   217       let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))

   218       in SOME (Rule.term_to_string''' thy prop, prop) end

   219     else

   220       let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))

   221       in SOME (Rule.term_to_string''' thy prop, prop) end

   222   | eval_matchsub _ _ _ _ = NONE;

   224 (*get the variables in an isabelle-term*)

   225 (*("Vars"    ,("Prog_Expr.Vars"    , eval_var "#Vars_")):calc*)

   226 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy =

   227     let

   228       val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;

   229       val thmId = thmid ^ Rule.term_to_string''' thy arg;

   230     in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end

   231   | eval_var _ _ _ _ = NONE;

   233 fun lhs (Const ("HOL.eq",_) $ l $ _) = l

   234   | lhs t = error("lhs called with (" ^ Rule.term2str t ^ ")");

   235 (*("lhs"    ,("Prog_Expr.lhs"    , eval_lhs "")):calc*)

   236 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =

   237     SOME ((Rule.term2str t) ^ " = " ^ (Rule.term2str l),

   238 	  HOLogic.Trueprop $ (TermC.mk_equality (t, l)))

   239   | eval_lhs _ _ _ _ = NONE;

   240 (*

   241 > val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";

   242 > val SOME (id,t') = eval_lhs 0 0 t 0;

   243 val id = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string

   244 > term2str t';

   245 val it = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string

   246 *)

   248 fun rhs (Const ("HOL.eq",_) $ _ $ r) = r

   249   | rhs t = error("rhs called with (" ^ Rule.term2str t ^ ")");

   250 (*("rhs"    ,("Prog_Expr.rhs"    , eval_rhs "")):calc*)

   251 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =

   252     SOME (Rule.term2str t ^ " = " ^ Rule.term2str r,

   253 	  HOLogic.Trueprop $ (TermC.mk_equality (t, r)))

   254   | eval_rhs _ _ _ _ = NONE;

   255 (*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)

   257 (*//------------------------- from Atools.thy------------------------------------------------\\*)

   258 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);

   260 (*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)

   261 fun eval_occurs_in _ "Prog_Expr.occurs'_in" (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =

   262     ((*tracing("#>@ eval_occurs_in: v= "^(Rule.term2str v));

   263      tracing("#>@ eval_occurs_in: t= "^(Rule.term2str t));*)

   264      if occurs_in v t

   265     then SOME ((Rule.term2str p) ^ " = True",

   266 	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

   267     else SOME ((Rule.term2str p) ^ " = False",

   268 	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))

   269   | eval_occurs_in _ _ _ _ = NONE;

   271 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)

   272 fun some_occur_in vs t =

   273     let fun occurs_in' a b = occurs_in b a

   274     in foldl or_ (false, map (occurs_in' t) vs) end;

   276 (*("some_occur_in", ("Prog_Expr.some'_occur'_in",

   277 			eval_some_occur_in "#eval_some_occur_in_"))*)

   278 fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"

   279 			  (p as (Const ("Prog_Expr.some'_occur'_in",_) $ vs $ t)) _ =

   280     if some_occur_in (TermC.isalist2list vs) t

   281     then SOME ((Rule.term2str p) ^ " = True",

   282 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

   283     else SOME ((Rule.term2str p) ^ " = False",

   284 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

   285   | eval_some_occur_in _ _ _ _ = NONE;

   287 (*("is_atom",("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)

   288 fun eval_is_atom (thmid:string) "Prog_Expr.is'_atom"

   289 		 (t as (Const _ $ arg)) _ =

   290     (case arg of

   291 	 Free (n,_) => SOME (TermC.mk_thmid thmid n "",

   292 			      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   293        | _ => SOME (TermC.mk_thmid thmid "" "",

   294 		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))

   295   | eval_is_atom _ _ _ _ = NONE;

   297 fun even i = (i div 2) * 2 = i;

   298 (*("is_even",("Prog_Expr.is'_even", eval_is_even "#is_even_"))*)

   299 fun eval_is_even (thmid:string) "Prog_Expr.is'_even"

   300 		 (t as (Const _ $ arg)) _ =

   301     (case arg of

   302 	Free (n,_) =>

   303 	 (case TermC.int_of_str_opt n of

   304 	      SOME i =>

   305 	      if even i then SOME (TermC.mk_thmid thmid n "",

   306 				   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   307 	      else SOME (TermC.mk_thmid thmid "" "",

   308 			 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   309 	    | _ => NONE)

   310        | _ => NONE)

   311   | eval_is_even _ _ _ _ = NONE;

   313 (*evaluate 'is_const'*)

   314 (*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)

   315 fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ =

   316     (case arg of

   317        Const (n1, _) =>

   318 	     SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   319      | Free (n1, _) =>

   320 	     if TermC.is_num' n1

   321 	     then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   322 	     else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   323      | _ => (*NONE*)

   324        SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))

   325   | eval_const _ _ _ _ = NONE;

   327 (*. evaluate binary, associative, commutative operators: *,+,^ .*)

   328 (*("PLUS"    ,("Groups.plus_class.plus"        , (**)eval_binop "#add_")),

   329   ("TIMES"   ,("Groups.times_class.times"        , (**)eval_binop "#mult_")),

   330   ("POWER"  ,("Prog_Expr.pow"  , (**)eval_binop "#power_"))*)

   332 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =

   333        ("xxxxxx",op_,t,thy);

   334    *)

   335 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)

   336   thmid ^ "Float ((" ^

   337   (string_of_int v11)^","^(string_of_int v12)^"), ("^

   338   (string_of_int p11)^","^(string_of_int p12)^")) __ (("^

   339   (string_of_int v21)^","^(string_of_int v22)^"), ("^

   340   (string_of_int p21)^","^(string_of_int p22)^"))";

   342 (*.evaluate < and <= for numerals.*)

   343 (*("le"      ,("Orderings.ord_class.less"        , Prog_Expr.eval_equ "#less_")),

   344   ("leq"     ,("Orderings.ord_class.less_eq"       , Prog_Expr.eval_equ "#less_equal_"))*)

   345 fun eval_equ (thmid:string) (_(*op_*)) (t as

   346 	       (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =

   347     (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of

   348 	 (SOME n1', SOME n2') =>

   349   if Num_Calc.calc_equ (strip_thy op0) (n1', n2')

   350     then SOME (TermC.mk_thmid thmid n1 n2,

   351 	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   352   else SOME (TermC.mk_thmid thmid n1 n2,

   353 	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   354        | _ => NONE)

   356   | eval_equ _ _ _ _ = NONE;

   359 (*evaluate identity

   360 > reflI;

   361 val it = "(?t = ?t) = True"

   362 > val t = str2term "x = 0";

   363 > val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls false reflI t;

   365 > val t = str2term "1 = 0";

   366 > val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls false reflI t;

   367 ----------- thus needs Rule.Num_Calc !

   368 > val t = str2term "0 = 0";

   369 > val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls false reflI t;

   370 > Rule.term2str t';

   371 val it = "HOL.True"

   373 val t = str2term "Not (x = 0)";

   374 atomt t; Rule.term2str t;

   375 *** -------------

   376 *** Const ( Not)

   377 *** . Const ( op =)

   378 *** . . Free ( x, )

   379 *** . . Free ( 0, )

   380 val it = "x ~= 0" : string*)

   382 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of

   383   the arguments: thus special handling by 'fun eval_binop'*)

   384 (*("ident"   ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)

   385 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as

   386 	       (Const _(*op0, t0*) $ t1 $ t2 )) thy =

   387   if t1 = t2

   388   then SOME (TermC.mk_thmid thmid

   389 	              ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")

   390 	              ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),

   391 	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   392   else SOME (TermC.mk_thmid thmid

   393 	              ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")

   394 	              ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),

   395 	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   396   | eval_ident _ _ _ _ = NONE;

   397 (* TODO

   398 > val t = str2term "x =!= 0";

   399 > val SOME (str, t') = eval_ident "ident_" "b" t thy;

   400 > Rule.term2str t';

   401 val str = "ident_(x)_(0)" : string

   402 val it = "(x =!= 0) = False" : string

   403 > val t = str2term "1 =!= 0";

   404 > val SOME (str, t') = eval_ident "ident_" "b" t thy;

   405 > Rule.term2str t';

   406 val str = "ident_(1)_(0)" : string

   407 val it = "(1 =!= 0) = False" : string

   408 > val t = str2term "0 =!= 0";

   409 > val SOME (str, t') = eval_ident "ident_" "b" t thy;

   410 > Rule.term2str t';

   411 val str = "ident_(0)_(0)" : string

   412 val it = "(0 =!= 0) = True" : string

   413 *)

   416 (* evaluate identity of terms, which stay ready for further evaluation;

   417   thus returns False only for atoms *)

   418 (*("equal"   ,("HOL.eq", Prog_Expr.eval_equal "#equal_")):calc*)

   419 fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =

   420   if t1 = t2

   421   then

   422     SOME (TermC.mk_thmid thmid

   423       ("(" ^ Rule.term_to_string''' thy t1 ^ ")") ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),

   424       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   425   else

   426     (case (TermC.is_atom t1, TermC.is_atom t2) of

   427       (true, true) =>

   428         if TermC.variable_constant_pair (t1, t2)

   429         then NONE

   430         else SOME (TermC.mk_thmid thmid

   431           ("(" ^ Rule.term_to_string''' thy t1 ^ ")") ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),

   432           HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   433     | _ => NONE)                                              (* NOT is_atom t1,t2 --> rew_sub *)

   434   | eval_equal _ _ _ _ = NONE;                                                   (* error-exit *)

   436 (*. evaluate HOL.divide .*)

   437 (*("DIVIDE" ,("Rings.divide_class.divide"  , eval_cancel "#divide_e"))*)

   438 fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as

   439 	       (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =

   440     (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of

   441     	(SOME n1', SOME n2') =>

   442         let

   443           val sg = Num_Calc.sign_mult n1' n2';

   444           val (T1,T2,Trange) = TermC.dest_binop_typ t0;

   445           val gcd' = Num_Calc.gcd (abs n1') (abs n2');

   446         in if gcd' = abs n2'

   447            then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')

   448     	        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))

   449     	    in SOME (TermC.mk_thmid thmid n1 n2, prop) end

   450            else if 0 < n2' andalso gcd' = 1 then NONE

   451            else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')

   452     	  			   ((abs n2') div gcd')

   453     	        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))

   454     	    in SOME (TermC.mk_thmid thmid n1 n2, prop) end

   455         end

   456       | _ => ((*tracing"#>@ eval_cancel NONE";*)NONE))

   457   | eval_cancel _ _ _ _ = NONE;

   459 (* get the argument from a function-definition *)

   460 (*("argument_in" ,("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"))*)

   461 fun eval_argument_in _ "Prog_Expr.argument'_in"

   462 		 (t as (Const ("Prog_Expr.argument'_in", _) $ (_(*f*) $ arg))) _ =

   463     if is_Free arg (*could be something to be simplified before*)

   464     then

   465       SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,

   466 	      HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))

   467     else NONE

   468   | eval_argument_in _ _ _ _ = NONE;

   470 (* check if the function-identifier of the first argument matches

   471    the function-identifier of the lhs of the second argument *)

   472 (*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)

   473 fun eval_sameFunId _ "Prog_Expr.sameFunId"

   474 		     (p as Const ("Prog_Expr.sameFunId",_) $  (f1 $ _) $ (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =

   475     if f1 = f2

   476     then SOME ((Rule.term2str p) ^ " = True",

   477 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

   478     else SOME ((Rule.term2str p) ^ " = False",

   479 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

   480 | eval_sameFunId _ _ _ _ = NONE;

   483 (*.from a list of fun-definitions "f x = ..." as 2nd argument

   484    filter the elements with the same fun-identfier in "f y"

   485    as the fst argument;

   486    this is, because Isabelles filter takes more than 1 sec.*)

   487 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2

   488   | same_funid f1 t = error ("same_funid called with t = ("

   489 				   ^Rule.term2str f1^") ("^Rule.term2str t^")");

   490 (*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",

   491 		   eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)

   492 fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId"

   493 		     (p as Const ("Prog_Expr.filter'_sameFunId",_) $

   494 			(fid $ _) $ fs) _ =

   495     let val fs' = ((TermC.list2isalist HOLogic.boolT) o

   496 		   (filter (same_funid fid))) (TermC.isalist2list fs)

   497     in SOME (Rule.term2str (TermC.mk_equality (p, fs')),

   498 	       HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end

   499 | eval_filter_sameFunId _ _ _ _ = NONE;

   501 (* make a list of terms to a sum *)

   502 fun list2sum [] = error ("list2sum called with []")

   503   | list2sum [s] = s

   504   | list2sum (s::ss) =

   505     let

   506       fun sum su [s'] = Const ("Groups.plus_class.plus",

   507            [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'

   508     	  | sum su (s'::ss') = sum (Const ("Groups.plus_class.plus",

   509            [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'

   510     	  | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing"

   511     in sum s ss end;

   513 (* make a list of equalities to the sum of the lhs *)

   514 (*("boollist2sum"    ,("Prog_Expr.boollist2sum"    , eval_boollist2sum "")):calc*)

   515 fun eval_boollist2sum _ "Prog_Expr.boollist2sum"

   516 		  (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const ("List.list.Cons", _) $ _ $ _)) _ =

   517     let

   518       val isal = TermC.isalist2list l

   519 	    val lhss = map lhs isal

   520 	    val sum = list2sum lhss

   521     in

   522       SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),

   523 	      HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))

   524     end

   525   | eval_boollist2sum _ _ _ _ = NONE;

   527 (**) end (*struct*)

   528 \<close> text \<open>

   529 open Prog_Expr

   530 \<close> ML \<open>

   531 \<close> ML \<open>

   532 \<close>

   534 subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>

   535 ML \<open>

   536 val prog_expr = Rule_Set.append_rls "prog_expr" prog_expr [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];

   537 \<close> ML \<open>

   538 \<close> ML \<open>

   539 \<close>

   541 subsection \<open>setup for rule-sets and ML-functions\<close>

   542 setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>

   543 setup \<open>KEStore_Elems.add_calcs

   544   [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),

   545     ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),

   546     ("Vars", ("Prog_Expr.Vars", Prog_Expr.eval_var "#Vars_")),

   547     ("lhs", ("Prog_Expr.lhs", Prog_Expr.eval_lhs "")),

   548     ("rhs", ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""))]\<close>

   549 (*\\------------------------- from Tools .thy-------------------------------------------------//*)

   550 ML \<open>

   551 \<close> ML \<open>

   552 \<close> ML \<open>

   553 \<close>

   555 end

author	Walther Neuper <walther.neuper@jku.at>
	Sat, 04 Apr 2020 12:11:32 +0200
changeset 59850	f3cac3053e7b
parent 59841	aeeec4898fd1
child 59852	ea7e6679080e
permissions	-rw-r--r--