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/Poly.thy
changeset 59489 cfcbcac0bae8
parent 59473 28b67cae58c3
child 59504 546bd1b027cc
equal deleted inserted replaced
59488:10a9e97e77c3 59489:cfcbcac0bae8 
   916 
   916 
   917 (* probably perfectly replaced by auto-generated version *)
 
   917 (* probably perfectly replaced by auto-generated version *)
 
   918 val scr_make_polynomial = 
   918 val scr_make_polynomial = 
   919 "Script Expand_binoms t_t =                                  " ^
 
   919 "Script Expand_binoms t_t =                                  " ^
 
   920 "(Repeat                                                    " ^
 
   920 "(Repeat                                                    " ^
 
   921 "((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^ 
   921 "((Try (Repeat (Rewrite ''real_diff_minus''         False))) @@ " ^ 
   922 
   922 
   923 " (Try (Repeat (Rewrite distrib_right   False))) @@ " ^	 
   923 " (Try (Repeat (Rewrite ''distrib_right''   False))) @@ " ^	 
   924 " (Try (Repeat (Rewrite distrib_left  False))) @@ " ^	
   924 " (Try (Repeat (Rewrite ''distrib_left''  False))) @@ " ^	
   925 " (Try (Repeat (Rewrite left_diff_distrib  False))) @@ " ^	
   925 " (Try (Repeat (Rewrite ''left_diff_distrib''  False))) @@ " ^	
   926 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^	
   926 " (Try (Repeat (Rewrite ''right_diff_distrib'' False))) @@ " ^	
   927 
   927 
   928 " (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^		   
   928 " (Try (Repeat (Rewrite ''mult_1_left''             False))) @@ " ^		   
   929 " (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^		   
   929 " (Try (Repeat (Rewrite ''mult_zero_left''             False))) @@ " ^		   
   930 " (Try (Repeat (Rewrite add_0_left      False))) @@ " ^	 
   930 " (Try (Repeat (Rewrite ''add_0_left''      False))) @@ " ^	 
   931 
   931 
   932 " (Try (Repeat (Rewrite mult_commute       False))) @@ " ^		
   932 " (Try (Repeat (Rewrite ''mult_commute''       False))) @@ " ^		
   933 " (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ " ^	
   933 " (Try (Repeat (Rewrite ''real_mult_left_commute''  False))) @@ " ^	
   934 " (Try (Repeat (Rewrite mult_assoc         False))) @@ " ^		
   934 " (Try (Repeat (Rewrite ''mult_assoc''        False))) @@ " ^		
   935 " (Try (Repeat (Rewrite add_commute        False))) @@ " ^		
   935 " (Try (Repeat (Rewrite ''add_commute''        False))) @@ " ^		
   936 " (Try (Repeat (Rewrite add_left_commute   False))) @@ " ^	 
   936 " (Try (Repeat (Rewrite ''add_left_commute''   False))) @@ " ^	 
   937 " (Try (Repeat (Rewrite add_assoc          False))) @@ " ^	 
   937 " (Try (Repeat (Rewrite ''add_assoc''          False))) @@ " ^	 
   938 
   938 
   939 " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^	 
   939 " (Try (Repeat (Rewrite ''sym_realpow_twoI''        False))) @@ " ^	 
   940 " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^	 
   940 " (Try (Repeat (Rewrite ''realpow_plus_1''          False))) @@ " ^	 
   941 " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^		
   941 " (Try (Repeat (Rewrite ''sym_real_mult_2''         False))) @@ " ^		
   942 " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^		
   942 " (Try (Repeat (Rewrite ''real_mult_2_assoc''       False))) @@ " ^		
   943 
   943 
   944 " (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^		
   944 " (Try (Repeat (Rewrite ''real_num_collect''        False))) @@ " ^		
   945 " (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^	
   945 " (Try (Repeat (Rewrite ''real_num_collect_assoc''  False))) @@ " ^	
   946 
   946 
   947 " (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^		
   947 " (Try (Repeat (Rewrite ''real_one_collect''        False))) @@ " ^		
   948 " (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^   
   948 " (Try (Repeat (Rewrite ''real_one_collect_assoc''  False))) @@ " ^   
   949 
   949 
   950 " (Try (Repeat (Calculate PLUS  ))) @@                      " ^
 
   950 " (Try (Repeat (Calculate ''PLUS''  ))) @@                      " ^
 
   951 " (Try (Repeat (Calculate TIMES ))) @@                      " ^
 
   951 " (Try (Repeat (Calculate ''TIMES'' ))) @@                      " ^
 
   952 " (Try (Repeat (Calculate POWER))))                        " ^  
   952 " (Try (Repeat (Calculate ''POWER''))))                        " ^  
   953 " t_t)";
 
   953 " t_t)";
 
   954 
   954 
   955 (*version used by MG.02/03, overwritten by version AG in 04 below
 
   955 (*version used by MG.02/03, overwritten by version AG in 04 below
 
   956 val make_polynomial = prep_rls'(
 
   956 val make_polynomial = prep_rls'(
 
   957   Rule.Seq{id = "make_polynomial", preconds = []:term list, 
   957   Rule.Seq{id = "make_polynomial", preconds = []:term list, 
   971 
   971 
   972 (* replacement by auto-generated version seemed to cause ERROR in algein.sml *)
 
   972 (* replacement by auto-generated version seemed to cause ERROR in algein.sml *)
 
   973 val scr_expand_binoms =
 
   973 val scr_expand_binoms =
 
   974 "Script Expand_binoms t_t =" ^
 
   974 "Script Expand_binoms t_t =" ^
 
   975 "(Repeat                       " ^
 
   975 "(Repeat                       " ^
 
   976 "((Try (Repeat (Rewrite real_plus_binom_pow2    False))) @@ " ^
 
   976 "((Try (Repeat (Rewrite ''real_plus_binom_pow2''    False))) @@ " ^
 
   977 " (Try (Repeat (Rewrite real_plus_binom_times   False))) @@ " ^
 
   977 " (Try (Repeat (Rewrite ''real_plus_binom_times''   False))) @@ " ^
 
   978 " (Try (Repeat (Rewrite real_minus_binom_pow2   False))) @@ " ^
 
   978 " (Try (Repeat (Rewrite ''real_minus_binom_pow2''   False))) @@ " ^
 
   979 " (Try (Repeat (Rewrite real_minus_binom_times  False))) @@ " ^
 
   979 " (Try (Repeat (Rewrite ''real_minus_binom_times''  False))) @@ " ^
 
   980 " (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ " ^
 
   980 " (Try (Repeat (Rewrite ''real_plus_minus_binom1''  False))) @@ " ^
 
   981 " (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ " ^
 
   981 " (Try (Repeat (Rewrite ''real_plus_minus_binom2''  False))) @@ " ^
 
   982 
   982 
   983 " (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^
 
   983 " (Try (Repeat (Rewrite ''mult_1_left''             False))) @@ " ^
 
   984 " (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^
 
   984 " (Try (Repeat (Rewrite ''mult_zero_left''             False))) @@ " ^
 
   985 " (Try (Repeat (Rewrite add_0_left      False))) @@ " ^
 
   985 " (Try (Repeat (Rewrite ''add_0_left''      False))) @@ " ^
 
   986 
   986 
   987 " (Try (Repeat (Calculate PLUS  ))) @@ " ^
 
   987 " (Try (Repeat (Calculate ''PLUS''  ))) @@ " ^
 
   988 " (Try (Repeat (Calculate TIMES ))) @@ " ^
 
   988 " (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
 
   989 " (Try (Repeat (Calculate POWER))) @@ " ^
 
   989 " (Try (Repeat (Calculate ''POWER''))) @@ " ^
 
   990 
   990 
   991 " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^
 
   991 " (Try (Repeat (Rewrite ''sym_realpow_twoI''        False))) @@ " ^
 
   992 " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^
 
   992 " (Try (Repeat (Rewrite ''realpow_plus_1''          False))) @@ " ^
 
   993 " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^
 
   993 " (Try (Repeat (Rewrite ''sym_real_mult_2''         False))) @@ " ^
 
   994 " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^
 
   994 " (Try (Repeat (Rewrite ''real_mult_2_assoc''       False))) @@ " ^
 
   995 
   995 
   996 " (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^
 
   996 " (Try (Repeat (Rewrite ''real_num_collect''        False))) @@ " ^
 
   997 " (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^
 
   997 " (Try (Repeat (Rewrite ''real_num_collect_assoc''  False))) @@ " ^
 
   998 
   998 
   999 " (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^
 
   999 " (Try (Repeat (Rewrite ''real_one_collect''        False))) @@ " ^
 
  1000 " (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^ 
  1000 " (Try (Repeat (Rewrite ''real_one_collect_assoc''  False))) @@ " ^ 
  1001 
  1001 
  1002 " (Try (Repeat (Calculate PLUS  ))) @@ " ^
 
  1002 " (Try (Repeat (Calculate ''PLUS''  ))) @@ " ^
 
  1003 " (Try (Repeat (Calculate TIMES ))) @@ " ^
 
  1003 " (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
 
  1004 " (Try (Repeat (Calculate POWER)))) " ^  
  1004 " (Try (Repeat (Calculate ''POWER'')))) " ^  
  1005 " t_t)";
 
  1005 " t_t)";
 
  1006 
  1006 
  1007 val expand_binoms = 
  1007 val expand_binoms = 
  1008   Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
 
  1008   Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
 
  1009       erls = Atools_erls, srls = Rule.Erls,
 
  1009       erls = Atools_erls, srls = Rule.Erls,
 
  1612 (*-----
 
  1612 (*-----
 
  1613 consts
 
  1613 consts
 
  1614   norm_Poly :: ID
 
  1614   norm_Poly :: ID
 
  1615 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
 
  1615 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
 
  1616   where
 
  1616   where
 
  1617     "simplify term = ((Rewrite_Set norm_Poly False) term)"
 
  1617     "simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
 
  1618 
  1618 
  1619 -----*)
 
  1619 -----*)
 
  1620 setup \<open>KEStore_Elems.add_mets
 
  1620 setup \<open>KEStore_Elems.add_mets
 
  1621     [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
 
  1621     [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
 
  1622 	    (["simplification","for_polynomials"],
 
  1622 	    (["simplification","for_polynomials"],
 
  1627 	        prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls 
  1627 	        prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls 
  1628 				    [(*for preds in where_*)
 
  1628 				    [(*for preds in where_*)
 
  1629 				      Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
 
  1629 				      Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
 
  1630 				  crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
 
  1630 				  crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
 
  1631 	      "Script SimplifyScript (t_t::real) =                " ^
 
  1631 	      "Script SimplifyScript (t_t::real) =                " ^
 
  1632 	        "  ((Rewrite_Set norm_Poly False) t_t)")]
 
  1632 	        "  ((Rewrite_Set ''norm_Poly'' False) t_t)")]
 
  1633 \<close>
 
  1633 \<close>
 
  1634 
  1634 
  1635 ML \<open>
 
  1635 ML \<open>
 
  1636 \<close> ML \<open>
 
  1636 \<close> ML \<open>
 
  1637 \<close> 
  1637 \<close>
wneuper/isa