jan@42443: 
wneuper@59592: theory example_2 imports Isac.Isac_Knowledge
jan@42443: begin
jan@42443: 
wneuper@59472: section\<open>Symbol Representation\<close>
jan@42444: 
wneuper@59472: ML \<open>
jan@42444:   (* 
jan@42444:    * alpha -->  "</alpha>" 
jan@42444:    *)
jan@42443:   @{term "\<alpha> "};
jan@42443:   @{term "\<delta> "};
jan@42443:   @{term "\<phi> "};
jan@42443:   @{term "\<rho> "};
walther@59868:   UnparseC.term @{term "\<rho> "};
wneuper@59472: \<close>
jan@42443: 
wneuper@59472: section\<open>Working with Rulesets\<close>
jan@42444: 
jan@42443: axiomatization where 
jan@42443:   rule1: "1 = \<delta>[n]" and
jan@42443:   rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
jan@42443:   rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and 
walther@60242:   rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>\<up>n * u [n]"
jan@42443: 
wneuper@59472: ML \<open>
jan@42443:   @{thm rule1};
jan@42443:   @{thm rule2};
jan@42443:   @{thm rule3};
jan@42443:   @{thm rule4};
wneuper@59472: \<close>
jan@42443: 
wneuper@59472: text\<open>Create Ruleset and insert rules\<close>
jan@42444: 
wneuper@59472: ML \<open>
walther@59852:   val transform = Rule_Set.append_rules "transform" Rule_Set.empty
walther@59871:     [ Thm  ("rule3",ThmC.numerals_to_Free @{thm rule3}),
walther@59871:       Thm  ("rule4",ThmC.numerals_to_Free @{thm rule4}),
walther@59871:       Thm  ("rule1",ThmC.numerals_to_Free @{thm rule1})   
jan@42443:     ];
wneuper@59472: \<close>
jan@42443: 
wneuper@59472: text\<open>Apply the Ruleset to a term\<close>
jan@42444: 
wneuper@59472: ML \<open>
Walther@60565:   val t = parse_test @{context} "z / (z - 1) + z / (z - \<alpha>) + 1::real";
jan@42444:   val SOME (t', asm) = rewrite_set_ thy true transform t;
wneuper@59472: \<close>
jan@42443: 
wneuper@59472: ML\<open>
walther@59868:  UnparseC.term t';
walther@59868:  UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
walther@60242:  UnparseC.term t' = "?u [?n] + \<alpha>\<up>?n u[n] + ?\<delta> [?n]";
wneuper@59472: \<close>
jan@42443: 
wneuper@59472: text\<open>Problems: Rule~1 is applied before the expression is checked for Rule~4
jan@42444:       which would be the correct one. Rule~1 only matches a part of the 
wneuper@59472:       expression.\<close>
jan@42443: 
jan@42443: end