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