1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Fri Sep 13 18:35:51 2019 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sat Sep 14 16:15:05 2019 +0200
     1.3 @@ -4,36 +4,32 @@
     1.4     (c) copyright due to lincense terms.
     1.5  *)
     1.6  
     1.7 -theory Prog_Expr imports Calculate
     1.8 +theory Prog_Expr
     1.9 +  imports Calculate
    1.10  begin
    1.11  
    1.12 -subsection \<open>General constants\<close>
    1.13 +text \<open>Abstract:
    1.14 +  Specific constants are defined for pre-conditions of programs and for program-expressions.
    1.15 +  The constants are connected with ML functions for evaluation of respective expressions
    1.16 +  (all named eval_*), such that Isac's rewrite engine can handle it.
    1.17 +\<close>
    1.18 +
    1.19 +subsection \<open>Power re-defined for a specific type\<close>
    1.20  consts
    1.21 -(*//------------------------- from Tools .thy-------------------------------------------------\\*)
    1.22 -  EmptyList :: "bool list" 
    1.23 -  UniversalList :: "bool list" 
    1.24 -(*\\------------------------- from Tools .thy ------------------------------------------------//*)
    1.25 -(*\\------------------------- from Atools .thy -----------------------------------------------//*)
    1.26 -  Arbfix :: "real"
    1.27 -  Undef :: "real"  (* WN190823 probably an outdated design for DiffApp *)
    1.28 -
    1.29    pow              :: "[real, real] => real"    (infixr "^^^" 80)
    1.30 -(*\\------------------------- from Atools.thy -----------------------------------------------//*)
    1.31  
    1.32  subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
    1.33 -(*//------------------------- from Tools .thy-------------------------------------------------\\*)
    1.34  consts
    1.35    lhs             :: "bool => real"           (*of an equality*)
    1.36    rhs             :: "bool => real"           (*of an equality*)
    1.37    Vars            :: "'a => real list"        (*get the variables of a term *)
    1.38    matches         :: "['a, 'a] => bool"
    1.39    matchsub        :: "['a, 'a] => bool"
    1.40 -(*\\------------------------- from Tools .thy-------------------------------------------------//*)
    1.41    some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
    1.42    occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")
    1.43  
    1.44    abs              :: "real => real"            ("(|| _ ||)")
    1.45 -(* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
    1.46 +  (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
    1.47    absset           :: "real set => real"        ("(||| _ |||)")
    1.48    (*is numeral constant ?*)
    1.49    is'_const        :: "real => bool"            ("_ is'_const" 10)
    1.50 @@ -43,27 +39,14 @@
    1.51  		
    1.52    (* identity on term level*)
    1.53    ident            :: "['a, 'a] => bool"        ("(_ =!=/ _)" [51, 51] 50)
    1.54 -
    1.55    argument'_in     :: "real => real"            ("argument'_in _" 10)
    1.56 -  sameFunId        :: "[real, bool] => bool"    (**"same'_funid _ _" 10
    1.57 -	WN0609 changed the id, because ".. _ _" inhibits currying**)
    1.58 +  sameFunId        :: "[real, bool] => bool"    (* "same'_funid _ _" 10
    1.59 +	                    WN0609 changed the id, because ".. _ _" inhibits currying *)
    1.60    filter'_sameFunId:: "[real, bool list] => bool list" 
    1.61  					        ("filter'_sameFunId _ _" 10)
    1.62    boollist2sum     :: "bool list => real"
    1.63    lastI            :: "'a list \<Rightarrow> 'a"
    1.64  
    1.65 -subsection \<open>Theorems for rule-sets TODO: find a better location in code\<close>
    1.66 -axiomatization where
    1.67 -  rle_refl:           "(n::real) <= n" and
    1.68 -  not_true:           "(~ True) = False" and
    1.69 -  not_false:          "(~ False) = True" and
    1.70 -  and_true:           "(a & True) = a" and
    1.71 -  and_false:          "(a & False) = False" and
    1.72 -  or_true:            "(a | True) = True" and
    1.73 -  or_false:           "(a | False) = a" and
    1.74 -  and_commute:        "(a & b) = (b & a)" and
    1.75 -  or_commute:         "(a | b) = (b | a)" 
    1.76 -
    1.77  subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>
    1.78  ML \<open>
    1.79  signature PROG_EXPR =
    1.80 @@ -574,9 +557,6 @@
    1.81  \<close> text \<open>
    1.82  open Prog_Expr
    1.83  \<close> ML \<open>
    1.84 -
    1.85 -\<close> ML \<open>
    1.86 -\<close> ML \<open>
    1.87  \<close> ML \<open>
    1.88  \<close>
    1.89