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 imports Calculate

     8 begin

    10 subsection \<open>General constants\<close>

    11 consts

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

    13   EmptyList :: "bool list"

    14   UniversalList :: "bool list"

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

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

    17   Arbfix :: "real"

    18   Undef :: "real"  (* WN190823 probably an outdated design for DiffApp *)

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

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

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

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

    25 consts

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

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

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

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

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

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

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

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

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

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

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

    38   (*is numeral constant ?*)

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

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

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

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

    44   (* identity on term level*)

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

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

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

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

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

    51 					        ("filter'_sameFunId _ _" 10)

    52   boollist2sum     :: "bool list => real"

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

    55 subsection \<open>Theorems for rule-sets TODO: find a better location in code\<close>

    56 axiomatization where

    57   rle_refl:           "(n::real) <= n" and

    58   not_true:           "(~ True) = False" and

    59   not_false:          "(~ False) = True" and

    60   and_true:           "(a & True) = a" and

    61   and_false:          "(a & False) = False" and

    62   or_true:            "(a | True) = True" and

    63   or_false:           "(a | False) = a" and

    64   and_commute:        "(a & b) = (b & a)" and

    65   or_commute:         "(a | b) = (b | a)"

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

    68 ML \<open>

    69 signature PROG_EXPR =

    70   sig

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

    72     val EmptyList: term

    73     val UniversalList: term

    75     val lhs: term -> term

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

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

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

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

    80     val rhs: term -> term

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

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

    84     val or2list: term -> term

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

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

    87     val occurs_in: term -> term -> bool

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

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

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

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

    92     val even: int -> bool

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

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

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

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

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

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

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

   100     val same_funid: term -> term -> bool

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

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

   103     val list2sum: term list -> term

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

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

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

   108   end

   110 (**)

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

   112 struct

   113 (**)

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

   115 (* auxiliary functions for scripts  WN.9.00*)

   116 (*11.02: for equation solving only*)

   117 val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";

   118 val EmptyList = (Thm.term_of o the o (TermC.parse @{theory}))  "[]::bool list";

   120 (*+ for Or_to_List +*)

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

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

   123   | or2list (t as Const ("HOL.eq",_) $ _ $ _) =

   124     (tracing"### or2list _ = _"; TermC.list2isalist HOLogic.boolT [t])

   125   | or2list ors =

   126     (tracing"### or2list _ | _";

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

   128 	    case o2 of

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

   130 	      | _ => ls @ [o1, o2]

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

   132        handle _ => error ("or2list: no ORs= "^(Rule.term2str ors)) end

   133 	);

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

   135 > val t' = or2list t;

   136 > term2str t';

   137 "Prog_Expr.UniversalList"

   138 > val t = @{term False};

   139 > val t' = or2list t;

   140 > term2str t';

   141 "[]"

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

   143 > val t' = or2list t;

   144 > term2str t';

   145 "[x = 3]"

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

   147 > val t' = or2list t;

   148 > term2str t';

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

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

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

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

   156 fun eval_matches (thmid:string) "Prog_Expr.matches"

   157 		  (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =

   158     if TermC.matches thy tst pat

   159     then

   160       let

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

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

   163     else

   164       let

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

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

   167   | eval_matches _ _ _ _ = NONE;

   168 (*

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

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

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

   172 val it =

   173   SOME

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

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

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

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

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

   180 val it =

   181   SOME

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

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

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

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

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

   188 val it =

   189   SOME

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

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

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

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

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

   196 val it =

   197   SOME

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

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

   200 ----- before ?patterns ---:

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

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

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

   204 SOME

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

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

   207   : (string * term) option

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

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

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

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

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

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

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

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

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

   219 *)

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

   222 fun matchsub thy t pat =

   223   let

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

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

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

   227 	      | matchs (Bound _) = false

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

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

   230 	      | matchs (t as f1 $ f2) =

   231 	          if TermC.matches thy t pat then true

   232 	            else if matchs f1 then true else matchs f2

   233   in matchs t end;

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

   236 fun eval_matchsub (thmid:string) "Prog_Expr.matchsub"

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

   238     if matchsub thy tst pat

   239     then

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

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

   242     else

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

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

   245   | eval_matchsub _ _ _ _ = NONE;

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

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

   249 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const(op0,t0) $ arg)) thy =

   250     let

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

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

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

   254   | eval_var _ _ _ _ = NONE;

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

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

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

   259 fun eval_lhs _ "Prog_Expr.lhs"

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

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

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

   263   | eval_lhs _ _ _ _ = NONE;

   264 (*

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

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

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

   268 > term2str t';

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

   270 *)

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

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

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

   275 fun eval_rhs _ "Prog_Expr.rhs"

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

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

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

   279   | eval_rhs _ _ _ _ = NONE;

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

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

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

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

   286 fun eval_occurs_in _ "Prog_Expr.occurs'_in"

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

   288     ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));

   289      tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)

   290      if occurs_in v t

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

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

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

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

   295   | eval_occurs_in _ _ _ _ = NONE;

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

   298 fun some_occur_in vs t =

   299     let fun occurs_in' a b = occurs_in b a

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

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

   303 			eval_some_occur_in "#eval_some_occur_in_"))*)

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

   305 			  (p as (Const ("Prog_Expr.some'_occur'_in",_)

   306 				       $ vs $ t)) _ =

   307     if some_occur_in (TermC.isalist2list vs) t

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

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

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

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

   312   | eval_some_occur_in _ _ _ _ = NONE;

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

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

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

   317     (case arg of

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

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

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

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

   322   | eval_is_atom _ _ _ _ = NONE;

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

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

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

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

   328     (case arg of

   329 	Free (n,_) =>

   330 	 (case TermC.int_of_str_opt n of

   331 	      SOME i =>

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

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

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

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

   336 	    | _ => NONE)

   337        | _ => NONE)

   338   | eval_is_even _ _ _ _ = NONE;

   340 (*evaluate 'is_const'*)

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

   342 fun eval_const (thmid:string) _(*"Prog_Expr.is'_const" WN050820 diff.beh. rooteq*)

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

   344     (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)

   345     (case arg of

   346        Const (n1,_) =>

   347 	 SOME (TermC.mk_thmid thmid n1 "",

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

   349      | Free (n1,_) =>

   350 	 if TermC.is_num' n1

   351 	   then SOME (TermC.mk_thmid thmid n1 "",

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

   353 	 else SOME (TermC.mk_thmid thmid n1 "",

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

   355      | Const ("Float.Float",_) =>

   356        SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",

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

   358      | _ => (*NONE*)

   359        SOME (TermC.mk_thmid thmid (Rule.term2str arg) "",

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

   361   | eval_const _ _ _ _ = NONE;

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

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

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

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

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

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

   370    *)

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

   372   thmid ^ "Float ((" ^

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

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

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

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

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

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

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

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

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

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

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

   385   if Calc.calc_equ (strip_thy op0) (n1', n2')

   386     then SOME (TermC.mk_thmid thmid n1 n2,

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

   388   else SOME (TermC.mk_thmid thmid n1 n2,

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

   390        | _ => NONE)

   392   | eval_equ _ _ _ _ = NONE;

   395 (*evaluate identity

   396 > reflI;

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

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

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

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

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

   403 ----------- thus needs Rule.Calc !

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

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

   406 > Rule.term2str t';

   407 val it = "HOL.True"

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

   410 atomt t; Rule.term2str t;

   411 *** -------------

   412 *** Const ( Not)

   413 *** . Const ( op =)

   414 *** . . Free ( x, )

   415 *** . . Free ( 0, )

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

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

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

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

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

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

   423   if t1 = t2

   424   then SOME (TermC.mk_thmid thmid

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

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

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

   428   else SOME (TermC.mk_thmid thmid

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

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

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

   432   | eval_ident _ _ _ _ = NONE;

   433 (* TODO

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

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

   436 > Rule.term2str t';

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

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

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

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

   441 > Rule.term2str t';

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

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

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

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

   446 > Rule.term2str t';

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

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

   449 *)

   451 (*.evaluate identity of terms, which stay ready for evaluation in turn;

   452   thus returns False only for atoms.*)

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

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

   455   if t1 = t2

   456   then SOME (TermC.mk_thmid thmid

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

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

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

   460   else (case (TermC.is_atom t1, TermC.is_atom t2) of

   461       (true, true) =>

   462       SOME (TermC.mk_thmid thmid

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

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

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

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

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

   468 (*

   469 val t = str2term "x ~= 0";

   470 val NONE = eval_equal "equal_" "b" t thy;

   473 > val t = str2term "(x + 1) = (x + 1)";

   474 > val SOME (str, t') = eval_equal "equal_" "b" t thy;

   475 > Rule.term2str t';

   476 val str = "equal_(x + 1)_(x + 1)" : string

   477 val it = "(x + 1 = x + 1) = True" : string

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

   479 > val NONE = eval_equal "equal_" "b" t thy;

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

   482 > val SOME (str, t') = eval_equal "equal_" "b" t thy;

   483 > Rule.term2str t';

   484 val str = "equal_(1)_(0)" : string

   485 val it = "(1 = 0) = False" : string

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

   487 > val SOME (str, t') = eval_equal "equal_" "b" t thy;

   488 > Rule.term2str t';

   489 val str = "equal_(0)_(0)" : string

   490 val it = "(0 = 0) = True" : string

   491 *)

   493 (*. evaluate HOL.divide .*)

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

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

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

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

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

   499         let

   500           val sg = Calc.sign_mult n1' n2';

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

   502           val gcd' = Calc.gcd (abs n1') (abs n2');

   503         in if gcd' = abs n2'

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

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

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

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

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

   509     	  			   ((abs n2') div gcd')

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

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

   512         end

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

   514   | eval_cancel _ _ _ _ = NONE;

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

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

   518 fun eval_argument_in _ "Prog_Expr.argument'_in"

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

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

   521     then

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

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

   524     else NONE

   525   | eval_argument_in _ _ _ _ = NONE;

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

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

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

   530 fun eval_sameFunId _ "Prog_Expr.sameFunId"

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

   532     if f1 = f2

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

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

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

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

   537 | eval_sameFunId _ _ _ _ = NONE;

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

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

   542    as the fst argument;

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

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

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

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

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

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

   549 fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId"

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

   551 			(fid $ _) $ fs) _ =

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

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

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

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

   556 | eval_filter_sameFunId _ _ _ _ = NONE;

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

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

   560   | list2sum [s] = s

   561   | list2sum (s::ss) =

   562     let

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

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

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

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

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

   568     in sum s ss end;

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

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

   572 fun eval_boollist2sum _ "Prog_Expr.boollist2sum"

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

   574     let

   575       val isal = TermC.isalist2list l

   576 	    val lhss = map lhs isal

   577 	    val sum = list2sum lhss

   578     in

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

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

   581     end

   582   | eval_boollist2sum _ _ _ _ = NONE;

   584 (**) end (*struct*)

   585 \<close> text \<open>

   586 open Prog_Expr

   587 \<close> ML \<open>

   589 \<close> ML \<open>

   590 \<close> ML \<open>

   591 \<close> ML \<open>

   592 \<close>

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

   595 ML \<open>

   596 val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];

   597 \<close> ML \<open>

   598 \<close> ML \<open>

   599 \<close>

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

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

   603 setup \<open>KEStore_Elems.add_calcs

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

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

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

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

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

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

   610 ML \<open>

   611 \<close> ML \<open>

   612 \<close> ML \<open>

   613 \<close>

   615 end

author	Walther Neuper <walther.neuper@jku.at>
	Tue, 03 Sep 2019 12:40:27 +0200
changeset 59603	30cd47104ad7
child 59618	80efccb7e5c1
permissions	-rw-r--r--