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>consts of functions in pre-conditions and program-expressions\<close>

    18 consts

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

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

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

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

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

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

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

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

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

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

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

    31   is_num         :: "real => bool"             ("_ is'_num" 10)

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

    34   (* identity on term level*)

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

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

    37   sameFunId        :: "[real, bool] => bool"    (* "same_funid _ _" 10

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

    39   filter_sameFunId:: "[real, bool list] => bool list" ("filter'_sameFunId _ _" 10)

    40   boollist2sum     :: "bool list => real"

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

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

    44 ML \<open>

    45 signature PROG_EXPR =

    46   sig

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

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

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

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

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

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

    54     val or2list: term -> term

    56     val occurs_in: term -> term -> bool

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

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

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

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

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

    62     val even: int -> bool

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

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

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

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

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

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

    69     val same_funid: term -> term -> bool

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

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

    72     val list2sum: term list -> term

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

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

    76   end

    78 (**)

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

    80 struct

    81 (**)

    83 (*+ for Or_to_List +*)

    84 fun or2list (Const (\<^const_name>\<open>True\<close>,_)) = ((*tracing"### or2list True";*) UniversalList)

    85   | or2list (Const (\<^const_name>\<open>False\<close>,_)) = ((*tracing"### or2list False";*) EmptyList)

    86   | or2list (t as Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]

    87   | or2list ors =

    88     let

    89       fun get ls (Const (\<^const_name>\<open>disj\<close>,_) $ o1 $ o2) =

    90 	        (case o2 of

    91 	         	Const (\<^const_name>\<open>disj\<close>,_) $ _ $ _ => get (ls @ [o1]) o2

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

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

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

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

    96 > val t' = or2list t;

    97 > term2str t';

    98 "ListC.UniversalList"

    99 > val t = @{term False};

   100 > val t' = or2list t;

   101 > term2str t';

   102 "[]"

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

   104 > val t' = or2list t;

   105 > term2str t';

   106 "[x = 3]"

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

   108 > val t' = or2list t;

   109 > term2str t';

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

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

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

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

   117 fun eval_matches (_:string) "Prog_Expr.matches" (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) thy =

   118     if TermC.matches thy tst pat

   119     then

   120       let

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

   122 	    in SOME (UnparseC.term_in_thy thy prop, prop) end

   123     else

   124       let

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

   126 	    in SOME (UnparseC.term_in_thy thy prop, prop) end

   127   | eval_matches _ _ _ _ = NONE;

   128 (*

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

   130 	      "matches (?x = 0) (1 * x \<up> 2 = 0)";

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

   132 val it =

   133   SOME

   134     ("matches (x = 0) (1 * x \<up> 2 = 0) = False",

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

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

   138 	      "matches (?a = #0) (#1 * x \<up> #2 = #0)";

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

   140 val it =

   141   SOME

   142     ("matches (?a = #0) (#1 * x \<up> #2 = #0) = True",

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

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

   146 	      "matches (?a * x = #0) (#1 * x \<up> #2 = #0)";

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

   148 val it =

   149   SOME

   150     ("matches (?a * x = #0) (#1 * x \<up> #2 = #0) = False",

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

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

   154 	      "matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0)";

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

   156 val it =

   157   SOME

   158     ("matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0) = True",

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

   160 ----- before ?patterns ---:

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

   162 	      "matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1)";

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

   164 SOME

   165     ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1) = True",

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

   167   : (string * term) option

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

   170 	      "matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1)";

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

   172 SOME ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1) = False",

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

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

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

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

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

   179 *)

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

   182 fun matchsub thy t pat =

   183   let

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

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

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

   187 	      | matchs (Bound _) = false

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

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

   190 	      | matchs (t as f1 $ f2) =

   191 	          if TermC.matches thy t pat then true

   192 	            else if matchs f1 then true else matchs f2

   193   in matchs t end;

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

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

   197       (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) thy =

   198     if matchsub thy tst pat

   199     then

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

   201       in SOME (UnparseC.term_in_thy thy prop, prop) end

   202     else

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

   204       in SOME (UnparseC.term_in_thy thy prop, prop) end

   205   | eval_matchsub _ _ _ _ = NONE;

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

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

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

   210     let

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

   212       val thmId = thmid ^ UnparseC.term_in_thy thy arg;

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

   214   | eval_var _ _ _ _ = NONE;

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

   217 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ =

   218     SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),

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

   220   | eval_lhs _ _ _ _ = NONE;

   221 (*

   222 > val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x \<up> 2 = 0)";

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

   224 val id = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string

   225 > term2str t';

   226 val it = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string

   227 *)

   229 fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r

   230   | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");

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

   232 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ =

   233     SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,

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

   235   | eval_rhs _ _ _ _ = NONE;

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

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

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

   241 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)

   242 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =

   243     ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));

   244      tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*)

   245      if occurs_in v t

   246     then SOME ((UnparseC.term p) ^ " = True",

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

   248     else SOME ((UnparseC.term p) ^ " = False",

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

   250   | eval_occurs_in _ _ _ _ = NONE;

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

   253 fun some_occur_in vs t =

   254     let fun occurs_in' a b = occurs_in b a

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

   257 (*("some_occur_in", ("Prog_Expr.some_occur_in",

   258 			eval_some_occur_in "#eval_some_occur_in_"))*)

   259 fun eval_some_occur_in _ "Prog_Expr.some_occur_in"

   260 			  (p as (Const (\<^const_name>\<open>some_occur_in\<close>,_) $ vs $ t)) _ =

   261     if some_occur_in (TermC.isalist2list vs) t

   262     then SOME ((UnparseC.term p) ^ " = True",

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

   264     else SOME ((UnparseC.term p) ^ " = False",

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

   266   | eval_some_occur_in _ _ _ _ = NONE;

   268 (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)

   269 fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ =

   270     if TermC.is_atom arg

   271     then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",

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

   273     else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",

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

   275   | eval_is_atom _ _ _ _ = NONE;

   277 (*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)

   278 fun eval_is_num (thmid:string) "Prog_Expr.is_num" (t as (Const _ $ arg)) _ =

   279     if TermC.is_num arg

   280     then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",

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

   282     else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",

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

   284   | eval_is_num _ _ _ _ = NONE;

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

   287 (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)

   288 fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ =

   289     if TermC.is_num arg

   290     then

   291       let

   292         val i = arg |> HOLogic.dest_number |> snd

   293       in

   294 	      if even i

   295         then SOME (TermC.mk_thmid thmid (string_of_int i) "",

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

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

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

   299       end

   300     else NONE

   301   | eval_is_even _ _ _ _ = NONE;

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

   304 (*("PLUS"    ,(\<^const_name>\<open>plus\<close>        , (**)eval_binop "#add_")),

   305   ("TIMES"   ,(\<^const_name>\<open>times\<close>        , (**)eval_binop "#mult_")),

   306   ("POWER"  ,(\<^const_name>\<open>realpow\<close>  , (**)eval_binop "#power_"))*)

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

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

   310    *)

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

   312   thmid ^ "Float ((" ^

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

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

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

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

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

   319 (*("le"      ,(\<^const_name>\<open>less\<close>        , Prog_Expr.eval_equ "#less_")),

   320   ("leq"     ,(\<^const_name>\<open>less_eq\<close>       , Prog_Expr.eval_equ "#less_equal_"))*)

   322 fun eval_equ (thmid:string) (_(*op_*)) (t as (Const (op0, _)) $ t1 $ t2) _ =

   323     if TermC.is_num t1 andalso TermC.is_num t2 then

   324       let

   325         val n1 = t1 |> HOLogic.dest_number |> snd

   326         val n2 = t2 |> HOLogic.dest_number |> snd

   327       in

   328         if Eval.calc_equ (strip_thy op0) (n1, n2)

   329         then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),

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

   331         else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),

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

   333       end

   334     else NONE

   335   | eval_equ _ _ _ _ = NONE;

   338 (*evaluate identity

   339 > reflI;

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

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

   342 > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;

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

   345 > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;

   346 ----------- thus needs Rule.Eval !

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

   348 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;

   349 > UnparseC.term t';

   350 val it = \<^const_name>\<open>True\<close>

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

   353 atomt t; UnparseC.term t;

   354 *** -------------

   355 *** Const ( Not)

   356 *** . Const ( op =)

   357 *** . . Free ( x, )

   358 *** . . Free ( 0, )

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

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

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

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

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

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

   366   if t1 = t2

   367   then SOME (TermC.mk_thmid thmid

   368 	              ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")

   369 	              ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),

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

   371   else SOME (TermC.mk_thmid thmid

   372 	              ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")

   373 	              ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),

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

   375   | eval_ident _ _ _ _ = NONE;

   376 (* TODO

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

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

   379 > UnparseC.term t';

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

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

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

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

   384 > UnparseC.term t';

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

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

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

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

   389 > UnparseC.term t';

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

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

   392 *)

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

   396   thus returns False only for atoms *)

   397 (*("equal"   ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*)

   398 fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =

   399   if t1 = t2

   400   then

   401     SOME (TermC.mk_thmid thmid

   402       ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),

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

   404   else

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

   406       (true, true) =>

   407         if TermC.variable_constant_pair (t1, t2)

   408         then NONE

   409         else SOME (TermC.mk_thmid thmid

   410           ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),

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

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

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

   415 (*. evaluate HOL.divide .*)

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

   417 fun eval_cancel thmid "Rings.divide_class.divide" (t as (Const _ $ t1 $ t2)) _ =

   418     if TermC.is_num t1 andalso TermC.is_num t2 then

   419       let

   420         val (T, _) = HOLogic.dest_number t1;

   421         val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);

   422         val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2);

   423       in

   424         if abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') then NONE

   425         else

   426           let

   427             val res = TermC.mk_frac T res_int;

   428             val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));

   429           in SOME (TermC.mk_thmid thmid (string_of_int i1) (string_of_int i2), prop) end

   430       end

   431     else NONE

   432   | eval_cancel _ _ _ _ = NONE;

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

   435 (*("argument_in" ,("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"))*)

   436 fun eval_argument_in _ "Prog_Expr.argument_in"

   437 		 (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ =

   438     if TermC.is_atom arg (*could be something to be simplified before*)

   439     then

   440       SOME (UnparseC.term t ^ " = " ^ UnparseC.term arg,

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

   442     else NONE

   443   | eval_argument_in _ _ _ _ = NONE;

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

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

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

   448 fun eval_sameFunId _ "Prog_Expr.sameFunId"

   449 		     (p as Const ("Prog_Expr.sameFunId",_) $  (f1 $ _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) _ =

   450     if f1 = f2

   451     then SOME ((UnparseC.term p) ^ " = True",

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

   453     else SOME ((UnparseC.term p) ^ " = False",

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

   455 | eval_sameFunId _ _ _ _ = NONE;

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

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

   460    as the fst argument;

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

   462 fun same_funid f1 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _) = f1 = f2

   463   | same_funid f1 t = raise ERROR ("same_funid called with t = ("

   464 		  ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")");

   465 (*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",

   466 		   eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*)

   467 fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId"

   468 		     (p as Const ("Prog_Expr.filter_sameFunId",_) $

   469 			(fid $ _) $ fs) _ =

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

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

   472     in SOME (UnparseC.term (TermC.mk_equality (p, fs')),

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

   474 | eval_filter_sameFunId _ _ _ _ = NONE;

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

   477 fun list2sum [] = raise ERROR ("list2sum called with []")

   478   | list2sum [s] = s

   479   | list2sum (s::ss) =

   480     let

   481       fun sum su [s'] = Const (\<^const_name>\<open>plus\<close>,

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

   483     	  | sum su (s'::ss') = sum (Const (\<^const_name>\<open>plus\<close>,

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

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

   486     in sum s ss end;

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

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

   490 fun eval_boollist2sum _ "Prog_Expr.boollist2sum"

   491 		  (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const (\<^const_name>\<open>Cons\<close>, _) $ _ $ _)) _ =

   492     let

   493       val isal = TermC.isalist2list l

   494 	    val lhss = map TermC.lhs isal

   495 	    val sum = list2sum lhss

   496     in

   497       SOME ((UnparseC.term p) ^ " = " ^ (UnparseC.term sum),

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

   499     end

   500   | eval_boollist2sum _ _ _ _ = NONE;

   502 (**) end (*struct*)

   503 \<close> text \<open>

   504 open Prog_Expr

   505 \<close> ML \<open>

   506 \<close> ML \<open>

   507 \<close>

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

   510 ML \<open>

   511 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "")];

   512 \<close> ML \<open>

   513 \<close> ML \<open>

   514 \<close>

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

   518 rule_set_knowledge prog_expr = prog_expr

   520 calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>

   521 calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>

   522 calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>

   523 calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>

   524 calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>

   526 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>

   527 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>

   528 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>

   529 calculation is_num = \<open>Prog_Expr.eval_is_num "#is_num_"\<close>

   530 calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>

   531 ML \<open>

   532 \<close> ML \<open>

   533 \<close> ML \<open>

   534 \<close>

   536 end

author	wenzelm
	Thu, 16 Sep 2021 17:23:54 +0200
changeset 60405	d4ebe139100d
parent 60396	c36af6b22ad4
child 60417	00ba9518dc35
permissions	-rw-r--r--