Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Root.thy
changeset 60297 73e7175a7d3f
parent 60296 81b6519da42b
child 60309 70a1d102660d
equal deleted inserted replaced
60296:81b6519da42b 60297:73e7175a7d3f 
   160  ]);
 
   160  ]);
 
   161 
   161 
   162 (*-------------------------rulse-------------------------*)
 
   162 (*-------------------------rulse-------------------------*)
 
   163 val Root_crls = 
   163 val Root_crls = 
   164       Rule_Set.append_rules "Root_crls" Atools_erls 
   164       Rule_Set.append_rules "Root_crls" Atools_erls 
   165        [Rule.Thm  ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
 
   165        [\<^rule_thm>\<open>real_unari_minus\<close>,
 
   166         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
 
   166         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
 
   167         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
 
   167         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
 
   168         \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
 
   168         \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
 
   169         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   169         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   170         \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
 
   170         \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
 
   172         \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_") 
   172         \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_") 
   173         ];
 
   173         ];
 
   174 
   174 
   175 val Root_erls = 
   175 val Root_erls = 
   176       Rule_Set.append_rules "Root_erls" Atools_erls 
   176       Rule_Set.append_rules "Root_erls" Atools_erls 
   177        [Rule.Thm  ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
 
   177        [\<^rule_thm>\<open>real_unari_minus\<close>,
 
   178         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
 
   178         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
 
   179         \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
 
   179         \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
 
   180         \<^rule_eval>\<open>Transcendental.powr\<close> (**)(eval_binop "#power_"),
 
   180         \<^rule_eval>\<open>Transcendental.powr\<close> (**)(eval_binop "#power_"),
 
   181         \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"), 
   181         \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"), 
   182         \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),
 
   182         \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),
 
   190 val make_rooteq = prep_rls'(
 
   190 val make_rooteq = prep_rls'(
 
   191   Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list, 
   191   Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list, 
   192       rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
 
   192       rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
 
   193       erls = Atools_erls, srls = Rule_Set.Empty,
 
   193       erls = Atools_erls, srls = Rule_Set.Empty,
 
   194       calc = [], errpatts = [],
 
   194       calc = [], errpatts = [],
 
   195       rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),			
   195       rules = [\<^rule_thm>\<open>real_diff_minus\<close>,			
   196 	       (*"a - b = a + (-1) * b"*)
 
   196 	       (*"a - b = a + (-1) * b"*)
 
   197 
   197 
   198 	       Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),	
   198 	       \<^rule_thm>\<open>distrib_right\<close>,	
   199 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
 
   199 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
 
   200 	       Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),	
   200 	       \<^rule_thm>\<open>distrib_left\<close>,	
   201 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
 
   201 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
 
   202 	       Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),	
   202 	       \<^rule_thm>\<open>left_diff_distrib\<close>,	
   203 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
 
   203 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
 
   204 	       Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),	
   204 	       \<^rule_thm>\<open>right_diff_distrib\<close>,	
   205 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
 
   205 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
 
   206 
   206 
   207 	       Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),                         
   207 	       \<^rule_thm>\<open>mult_1_left\<close>,                         
   208 	       (*"1 * z = z"*)
 
   208 	       (*"1 * z = z"*)
 
   209 	       Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),                         
   209 	       \<^rule_thm>\<open>mult_zero_left\<close>,                         
   210 	       (*"0 * z = 0"*)
 
   210 	       (*"0 * z = 0"*)
 
   211 	       Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),		
   211 	       \<^rule_thm>\<open>add_0_left\<close>,		
   212 	       (*"0 + z = z"*)
 
   212 	       (*"0 + z = z"*)
 
   213  
   213  
   214 	       Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
 
   214 	       \<^rule_thm>\<open>mult.commute\<close>,
 
   215 		(*AC-rewriting*)
 
   215 		(*AC-rewriting*)
 
   216 	       Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
 
   216 	       \<^rule_thm>\<open>real_mult_left_commute\<close>,
 
   217          	(**)
 
   217          	(**)
 
   218 	       Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
 
   218 	       \<^rule_thm>\<open>mult.assoc\<close>,
 
   219 	        (**)
 
   219 	        (**)
 
   220 	       Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
 
   220 	       \<^rule_thm>\<open>add.commute\<close>,
 
   221 		(**)
 
   221 		(**)
 
   222 	       Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
 
   222 	       \<^rule_thm>\<open>add.left_commute\<close>,
 
   223 	        (**)
 
   223 	        (**)
 
   224 	       Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
 
   224 	       \<^rule_thm>\<open>add.assoc\<close>,
 
   225 	        (**)
 
   225 	        (**)
 
   226 
   226 
   227 	       \<^rule_thm_sym>\<open>realpow_twoI\<close>,
 
   227 	       \<^rule_thm_sym>\<open>realpow_twoI\<close>,
 
   228 	       (*"r1 * r1 = r1  \<up>  2"*)
 
   228 	       (*"r1 * r1 = r1  \<up>  2"*)
 
   229 	       Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),			
   229 	       \<^rule_thm>\<open>realpow_plus_1\<close>,			
   230 	       (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)
 
   230 	       (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)
 
   231 	       \<^rule_thm_sym>\<open>real_mult_2\<close>,
 
   231 	       \<^rule_thm_sym>\<open>real_mult_2\<close>,
 
   232 	       (*"z1 + z1 = 2 * z1"*)
 
   232 	       (*"z1 + z1 = 2 * z1"*)
 
   233 	       Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),		
   233 	       \<^rule_thm>\<open>real_mult_2_assoc\<close>,		
   234 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
 
   234 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
 
   235 
   235 
   236 	       Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}), 
   236 	       \<^rule_thm>\<open>real_num_collect\<close>, 
   237 	       (*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)
 
   237 	       (*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)
 
   238 	       Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),	
   238 	       \<^rule_thm>\<open>real_num_collect_assoc\<close>,	
   239 	       (*"[| l is_const; m is_const |] ==>  
   239 	       (*"[| l is_const; m is_const |] ==>  
   240                                    l * n + (m * n + k) =  (l + m) * n + k"*)
 
   240                                    l * n + (m * n + k) =  (l + m) * n + k"*)
 
   241 	       Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),		
   241 	       \<^rule_thm>\<open>real_one_collect\<close>,		
   242 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
 
   242 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
 
   243 	       Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}), 
   243 	       \<^rule_thm>\<open>real_one_collect_assoc\<close>, 
   244 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
   244 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
   245 
   245 
   246 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   246 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   247 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
 
   247 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
 
   248 	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
 
   248 	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
 
   258 val expand_rootbinoms = prep_rls'(
 
   258 val expand_rootbinoms = prep_rls'(
 
   259   Rule_Def.Repeat{id = "expand_rootbinoms", preconds = [], 
   259   Rule_Def.Repeat{id = "expand_rootbinoms", preconds = [], 
   260       rew_ord = ("termlessI",termlessI),
 
   260       rew_ord = ("termlessI",termlessI),
 
   261       erls = Atools_erls, srls = Rule_Set.Empty,
 
   261       erls = Atools_erls, srls = Rule_Set.Empty,
 
   262       calc = [], errpatts = [],
 
   262       calc = [], errpatts = [],
 
   263       rules = [Rule.Thm ("real_plus_binom_pow2"  ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),     
   263       rules = [\<^rule_thm>\<open>real_plus_binom_pow2\<close>,     
   264 	       (*"(a + b)  \<up>  2 = a  \<up>  2 + 2 * a * b + b  \<up>  2"*)
 
   264 	       (*"(a + b)  \<up>  2 = a  \<up>  2 + 2 * a * b + b  \<up>  2"*)
 
   265 	       Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),    
   265 	       \<^rule_thm>\<open>real_plus_binom_times\<close>,    
   266 	       (*"(a + b)*(a + b) = ...*)
 
   266 	       (*"(a + b)*(a + b) = ...*)
 
   267 	       Rule.Thm ("real_minus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),    
   267 	       \<^rule_thm>\<open>real_minus_binom_pow2\<close>,    
   268 		(*"(a - b)  \<up>  2 = a  \<up>  2 - 2 * a * b + b  \<up>  2"*)
 
   268 		(*"(a - b)  \<up>  2 = a  \<up>  2 - 2 * a * b + b  \<up>  2"*)
 
   269 	       Rule.Thm ("real_minus_binom_times",ThmC.numerals_to_Free @{thm real_minus_binom_times}),   
   269 	       \<^rule_thm>\<open>real_minus_binom_times\<close>,   
   270 	       (*"(a - b)*(a - b) = ...*)
 
   270 	       (*"(a - b)*(a - b) = ...*)
 
   271 	       Rule.Thm ("real_plus_minus_binom1",ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),   
   271 	       \<^rule_thm>\<open>real_plus_minus_binom1\<close>,   
   272 		(*"(a + b) * (a - b) = a  \<up>  2 - b  \<up>  2"*)
 
   272 		(*"(a + b) * (a - b) = a  \<up>  2 - b  \<up>  2"*)
 
   273 	       Rule.Thm ("real_plus_minus_binom2",ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),   
   273 	       \<^rule_thm>\<open>real_plus_minus_binom2\<close>,   
   274 		(*"(a - b) * (a + b) = a  \<up>  2 - b  \<up>  2"*)
 
   274 		(*"(a - b) * (a + b) = a  \<up>  2 - b  \<up>  2"*)
 
   275 	       (*RL 020915*)
 
   275 	       (*RL 020915*)
 
   276 	       Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}), 
   276 	       \<^rule_thm>\<open>real_pp_binom_times\<close>, 
   277 		(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
 
   277 		(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
 
   278                Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}), 
   278                \<^rule_thm>\<open>real_pm_binom_times\<close>, 
   279 		(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
 
   279 		(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
 
   280                Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}), 
   280                \<^rule_thm>\<open>real_mp_binom_times\<close>, 
   281 		(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
 
   281 		(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
 
   282                Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}), 
   282                \<^rule_thm>\<open>real_mm_binom_times\<close>, 
   283 		(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
 
   283 		(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
 
   284 	       Rule.Thm ("realpow_mul",ThmC.numerals_to_Free @{thm realpow_mul}),                 
   284 	       \<^rule_thm>\<open>realpow_mul\<close>,                 
   285 		(*(a*b) \<up> n = a \<up> n * b \<up> n*)
 
   285 		(*(a*b) \<up> n = a \<up> n * b \<up> n*)
 
   286 
   286 
   287 	       Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),         (*"1 * z = z"*)
 
   287 	       \<^rule_thm>\<open>mult_1_left\<close>,         (*"1 * z = z"*)
 
   288 	       Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),         (*"0 * z = 0"*)
 
   288 	       \<^rule_thm>\<open>mult_zero_left\<close>,         (*"0 * z = 0"*)
 
   289 	       Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}), 
   289 	       \<^rule_thm>\<open>add_0_left\<close>, 
   290                  (*"0 + z = z"*)
 
   290                  (*"0 + z = z"*)
 
   291 
   291 
   292 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   292 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   293 	       \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 
   293 	       \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 
   294 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
 
   294 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
 
   296 	       \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
 
   296 	       \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
 
   297 	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
 
   297 	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
 
   298 
   298 
   299 	       \<^rule_thm_sym>\<open>realpow_twoI\<close>,
 
   299 	       \<^rule_thm_sym>\<open>realpow_twoI\<close>,
 
   300 	       (*"r1 * r1 = r1  \<up>  2"*)
 
   300 	       (*"r1 * r1 = r1  \<up>  2"*)
 
   301 	       Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),			
   301 	       \<^rule_thm>\<open>realpow_plus_1\<close>,			
   302 	       (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)
 
   302 	       (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)
 
   303 	       Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),		
   303 	       \<^rule_thm>\<open>real_mult_2_assoc\<close>,		
   304 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
 
   304 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
 
   305 
   305 
   306 	       Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}), 
   306 	       \<^rule_thm>\<open>real_num_collect\<close>, 
   307 	       (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
 
   307 	       (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
 
   308 	       Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),	
   308 	       \<^rule_thm>\<open>real_num_collect_assoc\<close>,	
   309 	       (*"[| l is_const; m is_const |] ==>
 
   309 	       (*"[| l is_const; m is_const |] ==>
 
   310                   l * n + (m * n + k) =  (l + m) * n + k"*)
 
   310                   l * n + (m * n + k) =  (l + m) * n + k"*)
 
   311 	       Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),		
   311 	       \<^rule_thm>\<open>real_one_collect\<close>,		
   312 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
 
   312 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
 
   313 	       Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}), 
   313 	       \<^rule_thm>\<open>real_one_collect_assoc\<close>, 
   314 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
   314 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
   315 
   315 
   316 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   316 	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
   317 	       \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 
   317 	       \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 
   318 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
 
   318 	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
wneuper/isa