1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isac/jrocnik/Test_Complex.thy Fri Jul 22 10:21:49 2011 +0200
1.3 @@ -0,0 +1,34 @@
1.4 +(* theory Test_Complex imports Isac begin
1.5 +ERROR TODO ^^^^:
1.6 +ML {*
1.7 +@{term "Complex 1 2 ^ Complex 3 4"};
1.8 +*}
1.9 +Type unification failed: Clash of types "complex" and "nat"
1.10 +Operator: op ^ (Complex 1 2) :: nat \<Rightarrow> complex
1.11 +Operand: Complex 3 4 :: complex
1.12 +*)
1.13 +
1.14 +theory Test_Complex imports Main begin
1.15 +
1.16 +ML {*
1.17 +@{term "Complex 1 2"};
1.18 +@{term "Complex 1 2 + Complex 3 4"};
1.19 +@{term "Complex 1 2 * Complex 3 4"};
1.20 +@{term "Complex 1 2 - Complex 3 4"};
1.21 +@{term "Complex 1 2 / Complex 3 4"};
1.22 +@{term "Complex 1 2 ^ Complex 3 4"};
1.23 +*}
1.24 +ML {*
1.25 +val a = @{term "Complex 1 2"};
1.26 +val b = @{term "Complex 3 4"};
1.27 +(*a + (b::complex); ERROR: term + term*)
1.28 +*}
1.29 +ML {*
1.30 +@{term "let a = Complex 1 2; b = Complex 3 4 in a + b"};
1.31 +*}
1.32 +ML {*
1.33 +(*TODO rules for simplification*)
1.34 +*}
1.35 +
1.36 +end
1.37 +
2.1 --- a/doc-src/isac/jrocnik/Test_SUM.thy Thu Jul 21 17:04:04 2011 +0200
2.2 +++ b/doc-src/isac/jrocnik/Test_SUM.thy Fri Jul 22 10:21:49 2011 +0200
2.3 @@ -1,22 +1,45 @@
2.4
2.5 theory Test_SUM imports Isac begin
2.6
2.7 +ML{* writeln "**** run the test ***************************************" *}
2.8 +
2.9 +use"../../../test/Tools/isac/Interpret/script.sml"
2.10 +
2.11 ML {*
2.12 -@{term "(SUM i = 0..< k. f i)"};
2.13 -@{term "(SUM iii = 0..< k. aaa * iii)"}
2.14 +@{term "(SUM i = 0..< k. f i)"}
2.15 +*}
2.16 +ML {*
2.17 +@{term "(%n :: nat. n) 2"};
2.18 +@{term "(%n. n) 2"};
2.19 +@{term "2"};
2.20 +*}
2.21 +ML {*
2.22 +@{term "(%n. n+n)"};
2.23 +@{term "(%n. n+n) a"};
2.24 +@{term "a+a"};
2.25 +*}
2.26 +ML {*
2.27 +@{term "Integral s f k"}
2.28 *}
2.29 ML {*
2.30 *}
2.31 ML {*
2.32 *}
2.33 -ML {*
2.34 -@{term "(%n :: nat. n) 2"};
2.35 -@{term "(%n. n) 2"};
2.36 -@{term "2"};
2.37 -@{term "(%n. n+n)"};
2.38 -@{term "(%n. n+n) a"};
2.39 -@{term "a+a"};
2.40 -*}
2.41
2.42 end
2.43
2.44 +
2.45 +(*=== inhibit exn ?=============================================================
2.46 +===== inhibit exn ?===========================================================*)
2.47 +
2.48 +
2.49 +(*========== inhibit exn 110415 ================================================
2.50 +
2.51 +"########### testcode inserted vvv ###########################################";
2.52 +"########### testcode inserted ^^^ ###########################################";
2.53 +
2.54 +============ inhibit exn 110415 ==============================================*)
2.55 +
2.56 +
2.57 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2.58 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/isac/jrocnik/Test_Z_Transform.thy Fri Jul 22 10:21:49 2011 +0200
3.3 @@ -0,0 +1,83 @@
3.4 +theory Test_Z_Transform imports Isac begin
3.5 +
3.6 +text {*examples copied from NEWS, HOL, Nat*}
3.7 +axiomatization
3.8 + eq (infix "===" 50) where
3.9 + eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
3.10 +
3.11 +axiomatization
3.12 + Zero_Rep :: ind and
3.13 + Suc_Rep :: "ind => ind"
3.14 +where
3.15 + -- {* the axiom of infinity in 2 parts *}
3.16 + Suc_Rep_inject: "Suc_Rep x = Suc_Rep y ==> x = y" and
3.17 + Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
3.18 +
3.19 +definition "f x y = x + y + 1"
3.20 +definition g where "g x = f x x"
3.21 +ML {*
3.22 +term2str @{term "f 2 3"}
3.23 +*}
3.24 +
3.25 +section {*trials towards Z transform *}
3.26 +subsection {*terms*}
3.27 +ML {*
3.28 +@{term "1 < || z ||"};
3.29 +@{term "z / (z - 1)"};
3.30 +@{term "-u -n - 1"};
3.31 +@{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
3.32 +@{term "z /(z - 1) = -u [-n - 1]"};
3.33 +@{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
3.34 +term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
3.35 +*}
3.36 +ML {*
3.37 +@{term "\<alpha> "};
3.38 +@{term "\<delta> "};
3.39 +@{term "\<phi> "};
3.40 +@{term "\<rho> "};
3.41 +term2str @{term "\<rho> "};
3.42 +*}
3.43 +
3.44 +subsection {*rules*}
3.45 +(*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
3.46 +(*definition "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)
3.47 +axioms
3.48 + rule1: "\<forall>x. \<delta>[n] = 1"
3.49 + rule3: "1 < || z || ==> z / (z - 1) = -u [-n - 1]"
3.50 +(*rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha>^n * [n]"
3.51 + Type unification failed: Clash of types "_ list" and "real"*)
3.52 + rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha> * u [n]"
3.53 +ML {*
3.54 +@{thm rule1};
3.55 +@{thm rule3};
3.56 +@{thm rule4};
3.57 +*}
3.58 +
3.59 +subsection {*apply rules*}
3.60 +ML {*
3.61 +val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
3.62 +*}
3.63 +ML {*
3.64 +val t = @{term "z / (z - 1) = -u [-n - 1]"};
3.65 +*}
3.66 +ML {*
3.67 +print_depth 999; Pattern.match thy; print_depth 999
3.68 +*}
3.69 +ML {*
3.70 +*}
3.71 +ML {*
3.72 +rewrite_ thy ro er true @{thm rule3} t
3.73 +*}
3.74 +ML {*
3.75 +
3.76 +*}
3.77 +ML {*
3.78 +*}
3.79 +ML {*
3.80 +*}
3.81 +ML {*
3.82 +@{term "1"};
3.83 +*}
3.84 +
3.85 +end
3.86 +