1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Mar 25 11:01:02 2020 +0100
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Mar 26 16:17:21 2020 +0100
1.3 @@ -85,6 +85,11 @@
1.4
1.5 val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string
1.6 (*\\------------------------- from Atools.thy------------------------------------------------//*)
1.7 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.8 + (*NONE*)
1.9 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.10 + (*NONE*)
1.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.12 end
1.13
1.14 (**)
1.15 @@ -126,8 +131,7 @@
1.16
1.17 (*. evaluate the predicate matches (match on whole term only) .*)
1.18 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
1.19 -fun eval_matches (_:string) "Prog_Expr.matches"
1.20 - (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =
1.21 +fun eval_matches (_:string) "Prog_Expr.matches" (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =
1.22 if TermC.matches thy tst pat
1.23 then
1.24 let
1.25 @@ -207,7 +211,7 @@
1.26
1.27 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
1.28 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
1.29 - (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =
1.30 + (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =
1.31 if matchsub thy tst pat
1.32 then
1.33 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
1.34 @@ -229,8 +233,7 @@
1.35 fun lhs (Const ("HOL.eq",_) $ l $ _) = l
1.36 | lhs t = error("lhs called with (" ^ Rule.term2str t ^ ")");
1.37 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
1.38 -fun eval_lhs _ "Prog_Expr.lhs"
1.39 - (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
1.40 +fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
1.41 SOME ((Rule.term2str t) ^ " = " ^ (Rule.term2str l),
1.42 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
1.43 | eval_lhs _ _ _ _ = NONE;
1.44 @@ -245,8 +248,7 @@
1.45 fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
1.46 | rhs t = error("rhs called with (" ^ Rule.term2str t ^ ")");
1.47 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
1.48 -fun eval_rhs _ "Prog_Expr.rhs"
1.49 - (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
1.50 +fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
1.51 SOME (Rule.term2str t ^ " = " ^ Rule.term2str r,
1.52 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
1.53 | eval_rhs _ _ _ _ = NONE;
1.54 @@ -256,8 +258,7 @@
1.55 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
1.56
1.57 (*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
1.58 -fun eval_occurs_in _ "Prog_Expr.occurs'_in"
1.59 - (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
1.60 +fun eval_occurs_in _ "Prog_Expr.occurs'_in" (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
1.61 ((*tracing("#>@ eval_occurs_in: v= "^(Rule.term2str v));
1.62 tracing("#>@ eval_occurs_in: t= "^(Rule.term2str t));*)
1.63 if occurs_in v t
1.64 @@ -275,8 +276,7 @@
1.65 (*("some_occur_in", ("Prog_Expr.some'_occur'_in",
1.66 eval_some_occur_in "#eval_some_occur_in_"))*)
1.67 fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"
1.68 - (p as (Const ("Prog_Expr.some'_occur'_in",_)
1.69 - $ vs $ t)) _ =
1.70 + (p as (Const ("Prog_Expr.some'_occur'_in",_) $ vs $ t)) _ =
1.71 if some_occur_in (TermC.isalist2list vs) t
1.72 then SOME ((Rule.term2str p) ^ " = True",
1.73 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.74 @@ -412,47 +412,26 @@
1.75 val it = "(0 =!= 0) = True" : string
1.76 *)
1.77
1.78 -(*.evaluate identity of terms, which stay ready for evaluation in turn;
1.79 - thus returns False only for atoms.*)
1.80 +
1.81 +(* evaluate identity of terms, which stay ready for further evaluation;
1.82 + thus returns False only for atoms *)
1.83 (*("equal" ,("HOL.eq", Prog_Expr.eval_equal "#equal_")):calc*)
1.84 fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
1.85 if t1 = t2
1.86 - then SOME (TermC.mk_thmid thmid
1.87 - ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
1.88 - ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
1.89 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.90 - else (case (TermC.is_atom t1, TermC.is_atom t2) of
1.91 - (true, true) =>
1.92 - SOME (TermC.mk_thmid thmid
1.93 - ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
1.94 - ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
1.95 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.96 - | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
1.97 - | eval_equal _ _ _ _ = NONE; (* error-exit *)
1.98 -(*
1.99 -val t = str2term "x ~= 0";
1.100 -val NONE = eval_equal "equal_" "b" t thy;
1.101 -
1.102 -
1.103 -> val t = str2term "(x + 1) = (x + 1)";
1.104 -> val SOME (str, t') = eval_equal "equal_" "b" t thy;
1.105 -> Rule.term2str t';
1.106 -val str = "equal_(x + 1)_(x + 1)" : string
1.107 -val it = "(x + 1 = x + 1) = True" : string
1.108 -> val t = str2term "x = 0";
1.109 -> val NONE = eval_equal "equal_" "b" t thy;
1.110 -
1.111 -> val t = str2term "1 = 0";
1.112 -> val SOME (str, t') = eval_equal "equal_" "b" t thy;
1.113 -> Rule.term2str t';
1.114 -val str = "equal_(1)_(0)" : string
1.115 -val it = "(1 = 0) = False" : string
1.116 -> val t = str2term "0 = 0";
1.117 -> val SOME (str, t') = eval_equal "equal_" "b" t thy;
1.118 -> Rule.term2str t';
1.119 -val str = "equal_(0)_(0)" : string
1.120 -val it = "(0 = 0) = True" : string
1.121 -*)
1.122 + then
1.123 + SOME (TermC.mk_thmid thmid
1.124 + ("(" ^ Rule.term_to_string''' thy t1 ^ ")") ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
1.125 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.126 + else
1.127 + (case (TermC.is_atom t1, TermC.is_atom t2) of
1.128 + (true, true) =>
1.129 + if TermC.variable_constant_pair (t1, t2)
1.130 + then NONE
1.131 + else SOME (TermC.mk_thmid thmid
1.132 + ("(" ^ Rule.term_to_string''' thy t1 ^ ")") ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
1.133 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.134 + | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
1.135 + | eval_equal _ _ _ _ = NONE; (* error-exit *)
1.136
1.137 (*. evaluate HOL.divide .*)
1.138 (*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)