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 abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)

    19 where "x \<up> a \<equiv> x powr a"

    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" ("filter'_sameFunId _ _" 10)

    46   boollist2sum     :: "bool list => real"

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

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

    50 ML \<open>

    51 signature PROG_EXPR =

    52   sig

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

    54     val lhs: term -> term

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

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

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

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

    59     val rhs: term -> term

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

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

    63     val or2list: term -> term

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

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

    66     val occurs_in: term -> term -> bool

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

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

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

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

    71     val even: int -> bool

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

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

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

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

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

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

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

    79     val same_funid: term -> term -> bool

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

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

    82     val list2sum: term list -> term

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

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

    86   end

    88 (**)

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

    90 struct

    91 (**)

    93 (*+ for Or_to_List +*)

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

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

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

    97   | or2list ors =

    98     let

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

   100 	        (case o2 of

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

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

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

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

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

   106 > val t' = or2list t;

   107 > term2str t';

   108 "ListC.UniversalList"

   109 > val t = @{term False};

   110 > val t' = or2list t;

   111 > term2str t';

   112 "[]"

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

   114 > val t' = or2list t;

   115 > term2str t';

   116 "[x = 3]"

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

   118 > val t' = or2list t;

   119 > term2str t';

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

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

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

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

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

   128     if TermC.matches thy tst pat

   129     then

   130       let

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

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

   133     else

   134       let

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

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

   137   | eval_matches _ _ _ _ = NONE;

   138 (*

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

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

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

   142 val it =

   143   SOME

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

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

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

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

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

   150 val it =

   151   SOME

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

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

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

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

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

   158 val it =

   159   SOME

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

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

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

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

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

   166 val it =

   167   SOME

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

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

   170 ----- before ?patterns ---:

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

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

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

   174 SOME

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

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

   177   : (string * term) option

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

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

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

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

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

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

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

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

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

   189 *)

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

   192 fun matchsub thy t pat =

   193   let

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

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

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

   197 	      | matchs (Bound _) = false

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

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

   200 	      | matchs (t as f1 $ f2) =

   201 	          if TermC.matches thy t pat then true

   202 	            else if matchs f1 then true else matchs f2

   203   in matchs t end;

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

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

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

   208     if matchsub thy tst pat

   209     then

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

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

   212     else

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

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

   215   | eval_matchsub _ _ _ _ = NONE;

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

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

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

   220     let

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

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

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

   224   | eval_var _ _ _ _ = NONE;

   226 (* refer to Thm.lhs_of *)

   227 fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l

   228   | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");

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

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

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

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

   233   | eval_lhs _ _ _ _ = NONE;

   234 (*

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

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

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

   238 > term2str t';

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

   240 *)

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

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

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

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

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

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

   248   | eval_rhs _ _ _ _ = NONE;

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

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

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

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

   255 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const ("Prog_Expr.occurs_in",_) $ v $ t)) _ =

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

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

   258      if occurs_in v t

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

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

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

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

   263   | eval_occurs_in _ _ _ _ = NONE;

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

   266 fun some_occur_in vs t =

   267     let fun occurs_in' a b = occurs_in b a

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

   270 (*("some_occur_in", ("Prog_Expr.some_occur_in",

   271 			eval_some_occur_in "#eval_some_occur_in_"))*)

   272 fun eval_some_occur_in _ "Prog_Expr.some_occur_in"

   273 			  (p as (Const ("Prog_Expr.some_occur_in",_) $ vs $ t)) _ =

   274     if some_occur_in (TermC.isalist2list vs) t

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

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

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

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

   279   | eval_some_occur_in _ _ _ _ = NONE;

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

   282 fun eval_is_atom (thmid:string) "Prog_Expr.is_atom"

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

   284     (case arg of

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

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

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

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

   289   | eval_is_atom _ _ _ _ = NONE;

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

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

   293 fun eval_is_even (thmid:string) "Prog_Expr.is_even"

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

   295     (case arg of

   296 	Free (n,_) =>

   297 	 (case ThmC_Def.int_opt_of_string n of

   298 	      SOME i =>

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

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

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

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

   303 	    | _ => NONE)

   304        | _ => NONE)

   305   | eval_is_even _ _ _ _ = NONE;

   307 (*evaluate 'is_const'*)

   308 (*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)

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

   310     (case arg of

   311        Const (n1, _) =>

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

   313      | Free (n1, _) =>

   314 	     if TermC.is_num' n1

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

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

   317      | _ => (*NONE*)

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

   319   | eval_const _ _ _ _ = NONE;

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

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

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

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

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

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

   328    *)

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

   330   thmid ^ "Float ((" ^

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

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

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

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

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

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

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

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

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

   341     (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of

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

   343   if Eval.calc_equ (strip_thy op0) (n1', n2')

   344     then SOME (TermC.mk_thmid thmid n1 n2,

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

   346   else SOME (TermC.mk_thmid thmid n1 n2,

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

   348        | _ => NONE)

   350   | eval_equ _ _ _ _ = NONE;

   353 (*evaluate identity

   354 > reflI;

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

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

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

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

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

   361 ----------- thus needs Rule.Eval !

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

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

   364 > UnparseC.term t';

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

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

   368 atomt t; UnparseC.term t;

   369 *** -------------

   370 *** Const ( Not)

   371 *** . Const ( op =)

   372 *** . . Free ( x, )

   373 *** . . Free ( 0, )

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

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

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

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

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

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

   381   if t1 = t2

   382   then SOME (TermC.mk_thmid thmid

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

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

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

   386   else SOME (TermC.mk_thmid thmid

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

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

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

   390   | eval_ident _ _ _ _ = NONE;

   391 (* TODO

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

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

   394 > UnparseC.term t';

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

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

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

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

   399 > UnparseC.term t';

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

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

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

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

   404 > UnparseC.term t';

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

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

   407 *)

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

   411   thus returns False only for atoms *)

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

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

   414   if t1 = t2

   415   then

   416     SOME (TermC.mk_thmid thmid

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

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

   419   else

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

   421       (true, true) =>

   422         if TermC.variable_constant_pair (t1, t2)

   423         then NONE

   424         else SOME (TermC.mk_thmid thmid

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

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

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

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

   430 (*. evaluate HOL.divide .*)

   431 (*("DIVIDE" ,(\<^const_name>\<open>divide\<close>  , eval_cancel "#divide_e"))*)

   432 fun eval_cancel (thmid: string) \<^const_name>\<open>divide\<close> (t as

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

   434     (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of

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

   436         let

   437           val sg = Eval.sign_mult n1' n2';

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

   439           val gcd' = Eval.gcd (abs n1') (abs n2');

   440         in if gcd' = abs n2'

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

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

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

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

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

   446     	  			   ((abs n2') div gcd')

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

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

   449         end

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

   451   | eval_cancel _ _ _ _ = NONE;

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

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

   455 fun eval_argument_in _ "Prog_Expr.argument_in"

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

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

   458     then

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

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

   461     else NONE

   462   | eval_argument_in _ _ _ _ = NONE;

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

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

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

   467 fun eval_sameFunId _ "Prog_Expr.sameFunId"

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

   469     if f1 = f2

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

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

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

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

   474 | eval_sameFunId _ _ _ _ = NONE;

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

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

   479    as the fst argument;

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

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

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

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

   484 (*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",

   485 		   eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*)

   486 fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId"

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

   488 			(fid $ _) $ fs) _ =

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

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

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

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

   493 | eval_filter_sameFunId _ _ _ _ = NONE;

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

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

   497   | list2sum [s] = s

   498   | list2sum (s::ss) =

   499     let

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

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

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

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

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

   505     in sum s ss end;

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

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

   509 fun eval_boollist2sum _ "Prog_Expr.boollist2sum"

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

   511     let

   512       val isal = TermC.isalist2list l

   513 	    val lhss = map lhs isal

   514 	    val sum = list2sum lhss

   515     in

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

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

   518     end

   519   | eval_boollist2sum _ _ _ _ = NONE;

   521 (**) end (*struct*)

   522 \<close> text \<open>

   523 open Prog_Expr

   524 \<close> ML \<open>

   525 \<close> ML \<open>

   526 \<close>

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

   529 ML \<open>

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

   531 \<close> ML \<open>

   532 \<close> ML \<open>

   533 \<close>

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

   537 rule_set_knowledge prog_expr = prog_expr

   538 setup \<open>KEStore_Elems.add_calcs

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

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

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

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

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

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

   545 ML \<open>

   546 \<close> ML \<open>

   547 \<close> ML \<open>

   548 \<close>

   550 end

author	wenzelm
	Mon, 21 Jun 2021 15:36:09 +0200
changeset 60309	70a1d102660d
parent 60294	6623f5cdcb19
child 60312	35f7b2f61797
permissions	-rw-r--r--