theory Test_Z_Transform imports Isac begin

 text {*examples copied from NEWS, HOL, Nat*}

 axiomatization

     eq  (infix "===" 50) where

     eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"

 axiomatization

   Zero_Rep :: ind and

   Suc_Rep :: "ind => ind"

 where

   -- {* the axiom of infinity in 2 parts *}

   Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and

   Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"

 definition "f x y = x + y + 1"

 definition g where "g x = f x x"

 ML {* 

 term2str @{term "f 2 3"}

 *}

 section {*trials towards Z transform *}

 subsection {*terms*}

 ML {*

 @{term "1 < || z ||"};

 @{term "z / (z - 1)"};

 @{term "-u -n - 1"};

 @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)

 @{term "z /(z - 1) = -u [-n - 1]"};

 @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};

 term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};

 *}

 ML {*

 @{term "\<alpha> "};

 @{term "\<delta> "};

 @{term "\<phi> "};

 @{term "\<rho> "};

 term2str @{term "\<rho> "};

 *}

 subsection {*rules*}

 (*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)

 (*definition     "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)

 axioms 

   rule1: "\<forall>x. \<delta>[n] = 1"

   rule3: "1 < || z || ==> z / (z - 1) = -u [-n - 1]"

 (*rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha>^n * [n]" 

                             Type unification failed: Clash of types "_ list" and "real"*)

   rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha> * u [n]"

 ML {*

 @{thm rule1};

 @{thm rule3};

 @{thm rule4};

 *}

 subsection {*apply rules*}

 ML {*

 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);

 *}

 ML {*

 val t = @{term "z / (z - 1) = -u [-n - 1]"};

 *}

 ML {*

 print_depth 999; Pattern.match thy;  print_depth 999

 *}

 ML {*

 *}

 ML {*

 rewrite_ thy ro er true @{thm rule3} t

 *}

 ML {*

 *}

 ML {*

 *}

 ML {*

 *}

 ML {*

 @{term "1"};

 *}

 end