theory example_2 imports Isac.Isac_Knowledge

 begin

 section\<open>Symbol Representation\<close>

 ML \<open>

   (* 

    * alpha -->  "</alpha>" 

    *)

   @{term "\<alpha> "};

   @{term "\<delta> "};

   @{term "\<phi> "};

   @{term "\<rho> "};

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

 \<close>

 section\<open>Working with Rulesets\<close>

 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 \<open>

   @{thm rule1};

   @{thm rule2};

   @{thm rule3};

   @{thm rule4};

 \<close>

 text\<open>Create Ruleset and insert rules\<close>

 ML \<open>

   val transform = Rule_Set.append_rules "transform" Rule_Set.empty

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

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

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

     ];

 \<close>

 text\<open>Apply the Ruleset to a term\<close>

 ML \<open>

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

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

 \<close>

 ML\<open>

  term2str t';

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

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

 \<close>

 text\<open>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.\<close>

 end