theory example_2 imports Isac.Isac

begin

section{*Symbol Representation*}

ML {*

  (* 

   * alpha -->  "</alpha>" 

   *)

  @{term "\<alpha> "};

  @{term "\<delta> "};

  @{term "\<phi> "};

  @{term "\<rho> "};

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

*}

section{*Working with Rulesets*}

axiomatization where 

  rule1: "1 = \<delta>[n]" and

  rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and

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

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

ML {*

  @{thm rule1};

  @{thm rule2};

  @{thm rule3};

  @{thm rule4};

*}

text{*Create Ruleset and insert rules*}

ML {*

  val transform = append_rls "transform" e_rls

    [ Thm  ("rule3",num_str @{thm rule3}),

      Thm  ("rule4",num_str @{thm rule4}),

      Thm  ("rule1",num_str @{thm rule1})   

    ];

*}

text{*Apply the Ruleset to a term*}

ML {*

  val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real";

  val SOME (t', asm) = rewrite_set_ thy true transform t;

*}

ML{*

 term2str t';

 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";

 term2str t' = "?u [?n] + \<alpha>^^^?n u[n] + ?\<delta> [?n]";

*}

text{*Problems: Rule~1 is applied before the expression is checked for Rule~4

      which would be the correct one. Rule~1 only matches a part of the 

      expression.*}

end