1.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed Jul 27 16:56:45 2011 +0200
1.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Thu Jul 28 10:58:17 2011 +0200
1.3 @@ -16,7 +16,7 @@
1.4 "----------- calculate from script ----------------------";
1.5 "----------- calculate check test-root-equ --------------";
1.6 "----------- check calculate bottom up ------------------";
1.7 -" ================= calculate.sml:10.8.02 2002:///->/ ===";
1.8 +"----------- Atools.pow Power.power_class.power ---------";
1.9 " ================= calculate.sml: calculate_ 2002 ======";
1.10 "----------- get_pair with 3 args -----------------------";
1.11 "----------- calculate (2 * x is_const) -----------------";
1.12 @@ -73,7 +73,6 @@
1.13 "----------- calculate from script ----------------------";
1.14 "----------- calculate from script ----------------------";
1.15 "----------- calculate from script ----------------------";
1.16 -
1.17 store_pbt
1.18 (prep_pbt (@{theory "Test"}) "pbl_ttest" [] e_pblID
1.19 (["test"],
1.20 @@ -315,116 +314,23 @@
1.21 *)
1.22 trace_rewrite:=false;
1.23
1.24 -" ================= calculate.sml:10.8.02 2002:///->/ ======== ";
1.25 -" ================= calculate.sml:10.8.02 2002:///->/ ======== ";
1.26 -" ================= calculate.sml:10.8.02 2002:///->/ ======== ";
1.27 -" ----------------- rewriting works ? -----------------------";
1.28 - val thy = (@{theory "Isac"});
1.29 -
1.30 - val prop = (#prop o rep_thm) @{thm divide_1};
1.31 -(* AK110727 changed real_divide_1 to @{thm divide_1} *)
1.32 - atomty prop;
1.33 -
1.34 -(*** -------------
1.35 -*** Const ( Trueprop, bool => prop)
1.36 -*** . Const ( op =, [real, real] => bool)
1.37 -*** . . Const ( HOL.divide, [real, real] => real)
1.38 -*** . . . Var ((x, 0), real)
1.39 -*** . . . Const ( 1, real)
1.40 -*** . . Var ((x, 0), real) *)
1.41 - val prop' = (#prop o rep_thm o num_str) @{thm divide_1};
1.42 -(* AK110727 changed real_divide_1 to @{thm divide_1} *)
1.43 - atomty prop';
1.44 -
1.45 -(*** -------------
1.46 -*** Const ( Trueprop, bool => prop)
1.47 -*** . Const ( op =, [real, real] => bool)
1.48 -*** . . Const ( HOL.divide, [real, real] => real)
1.49 -*** . . . Var ((x, 0), real)
1.50 -*** . . . Free ( 1, real) (*app_num_tr'*)
1.51 -*** . . Var ((x, 0), real)*)
1.52 - val t = (term_of o the o (parseold thy)) "aaa/1";
1.53 - atomty t;
1.54 -(*** -------------
1.55 -*** Csnst ( HOL.divide, ['a, 'a] => 'a)
1.56 -*** . Free ( aaa, 'a)
1.57 -*** . Free ( 1, 'a) *)
1.58 - val t = (term_of o the o (parse thy)) "aaa/1";
1.59 - atomty t;
1.60 -(*** -------------
1.61 -*** Const ( HOL.divide, [real, real] => real)
1.62 -*** . Free ( aaa, real)
1.63 -*** . Free ( 1, real) *)
1.64 -
1.65 - val thm = num_str @{thm divide_1};
1.66 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.67 -(*val t = Free ("aaa","RealDef.real") : term*)
1.68 -
1.69 - val prop = (#prop o rep_thm) @{thm realpow_eq_oneI};
1.70 -(* AK110727 replaced realpow_eq_one with @{thm realpow_eq_oneI} *)
1.71 - atomty prop;
1.72 -
1.73 -(*** -------------
1.74 -*** Const ( Trueprop, bool => prop)
1.75 -*** . Const ( op =, [real, real] => bool)
1.76 -*** . . Const ( Nat.power, [real, nat] => real)
1.77 -*** . . . Const ( 1, real)
1.78 -*** . . . Var ((n, 0), nat)
1.79 -*** . . Const ( 1, real) *)
1.80 - val prop' = (#prop o rep_thm o num_str) @{thm realpow_eq_oneI};
1.81 -(* AK110727 replaced realpow_eq_one with @{thm realpow_eq_oneI} *)
1.82 - atomty prop';
1.83 -
1.84 -(*** -------------
1.85 -*** Const ( Trueprop, bool => prop)
1.86 -*** . Const ( op =, [real, real] => bool)
1.87 -*** . . Const ( Nat.power, [real, nat] => real)
1.88 -*** . . . Free ( 1, real)
1.89 -*** . . . Var ((n, 0), nat)
1.90 -*** . . Free ( 1, real)*)
1.91 - val t = (term_of o the o (parseold thy)) "1 ^ aaa";
1.92 - atomty t;
1.93 +"----------- Atools.pow Power.power_class.power ---------";
1.94 +"----------- Atools.pow Power.power_class.power ---------";
1.95 +"----------- Atools.pow Power.power_class.power ---------";
1.96 +val t = (term_of o the o (parseold thy)) "1 ^ aaa";
1.97 +atomty t;
1.98 (*** -------------
1.99 *** Const ( Nat.power, ['a, nat] => 'a)
1.100 *** . Free ( 1, 'a)
1.101 *** . Free ( aaa, nat) *)
1.102 - val t = (term_of o the o (parse thy)) "1 ^ aaa";
1.103 - atomty t;
1.104 -(*** -------------
1.105 -*** Const ( Nat.power, [real, nat] => real)
1.106 -*** . Free ( 1, real)
1.107 -*** . Free ( aaa, nat) .......................... nat !!! *)
1.108
1.109 - val thm = num_str @{thm realpow_eq_oneI};
1.110 -(* AK110727 replaced realpow_eq_one with @{thm realpow_eq_oneI} *)
1.111 -
1.112 -(*===== inhibit exn AK110725 ===========================================================
1.113 -(* ERROR: Exception Bind raised *)
1.114 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.115 -===== inhibit exn AK110725 ===========================================================*)
1.116 -(* (*AK110727 Debugging (not finished)*)
1.117 - rewrite_ thy tless_true tval_rls true thm t; (* returns NONE *)
1.118 -"~~~~~ fun rewrite_, args:"; val (thy, rew_ord, erls, bool, thm, term)
1.119 - = (thy, tless_true, tval_rls, true, thm, t);
1.120 - rewrite__ thy 1 [] rew_ord erls bool thm term; (* returns NONE *)
1.121 -
1.122 -"~~~~~ fun rewrite__, args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
1.123 - = (thy, 1, [], rew_ord, erls, bool, thm, term);
1.124 -
1.125 - rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
1.126 - (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct; (* rew is FALSE -> returns SOME *)
1.127 - rew_sub;
1.128 -
1.129 - print_depth 999;
1.130 - val (t',asms,lrd,rew) =
1.131 - rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
1.132 - (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct; (* rew is FALSE -> returns SOME *)
1.133 -
1.134 -"~~~~~ and rew_sub, args:";
1.135 - (* rew_sub returns (t1 $ t2,[], lrd, false) - see last line of function rew_sub *)
1.136 -*)
1.137 -
1.138 -(*val t = Free ("1","RealDef.real") : term*)
1.139 +val t = str2term "1 ^^^ aaa";
1.140 +atomty t;
1.141 +(****
1.142 +*** Const (Atools.pow, real => real => real)
1.143 +*** . Free (1, real)
1.144 +*** . Free (aaa, real)
1.145 +*** *);
1.146
1.147 " ================= calculate.sml: calculate_ 2002 =================== ";
1.148 " ================= calculate.sml: calculate_ 2002 =================== ";
2.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Wed Jul 27 16:56:45 2011 +0200
2.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Thu Jul 28 10:58:17 2011 +0200
2.3 @@ -19,6 +19,7 @@
2.4 "----------- check diff 2002--2009-3 --------------------";
2.5 "----------- compare all prepat's existing 2010 ---------";
2.6 "----------- fun app_rev, Rrls, -------------------------";
2.7 +"----------- 2011 thms with axclasses -------------------";
2.8 "--------------------------------------------------------";
2.9 "--------------------------------------------------------";
2.10 "--------------------------------------------------------";
2.11 @@ -491,3 +492,16 @@
2.12 case eval__true thy i asms bdv rls of
2.13 ([], true) => ()
2.14 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
2.15 +
2.16 +"----------- 2011 thms with axclasses -------------------";
2.17 +"----------- 2011 thms with axclasses -------------------";
2.18 +"----------- 2011 thms with axclasses -------------------";
2.19 +val thm = num_str @{thm divide_1};
2.20 +val prop = prop_of thm;
2.21 +atomty prop; (*Type 'a*)
2.22 +val t = str2term "(2*x)/1"; (*Type real*)
2.23 +
2.24 +val (thy, ro, er, inst) =
2.25 + (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
2.26 +val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
2.27 +
3.1 --- a/test/Tools/isac/Test_Isac.thy Wed Jul 27 16:56:45 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jul 28 10:58:17 2011 +0200
3.3 @@ -100,7 +100,7 @@
3.4 use "library.sml"
3.5 use "calcelems.sml"
3.6 use "ProgLang/termC.sml"
3.7 - use "ProgLang/calculate.sml" (*part.*)
3.8 + use "ProgLang/calculate.sml"
3.9 use "ProgLang/rewrite.sml" (*?complete?*)
3.10 (*use "ProgLang/listC.sml" 2002*)
3.11 use "ProgLang/scrtools.sml" (*complete*)
4.1 --- a/test/Tools/isac/Test_Some.thy Wed Jul 27 16:56:45 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jul 28 10:58:17 2011 +0200
4.3 @@ -5,18 +5,20 @@
4.4
4.5 theory Test_Some imports Isac begin
4.6
4.7 -ML{* writeln "**** run the test ***************************************" *}
4.8 -
4.9 -use"../../../test/Tools/isac/Frontend/interface.sml"
4.10 +use"../../../test/Tools/isac/ProgLang/rewrite.sml"
4.11
4.12 ML {*
4.13
4.14 -
4.15 -
4.16 -
4.17 -
4.18 -
4.19 -
4.20 +*}
4.21 +ML{*
4.22 +*}
4.23 +ML{*
4.24 +*}
4.25 +ML{*
4.26 +*}
4.27 +ML{*
4.28 +*}
4.29 +ML{*
4.30
4.31
4.32 *}