1 (* Title: ProgLang/program.sml
2 Author: Walther Neuper 190922
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "table of contents -----------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "-----------------------------------------------------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
16 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
17 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
18 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
21 val t = str2term "x = 0";
22 val NONE(*= indetermined*) = eval_equal "equal_" "HOL.eq" t thy;
24 val t = str2term "(x + 1) = (x + 1)";
25 val (Const _(*op0,t0*) $ t1 $ t2 ) = t
26 val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" "HOL.eq" t thy;
27 if term2str t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
29 val t as Const _ $ v $ c = str2term "1 = 0";
30 val false = variable_constant_pair (v, c);
31 val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;
32 if term2str t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
34 val t = str2term "0 = 0";
35 val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;
36 if term2str t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";