Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Rational.thy
changeset 60405 d4ebe139100d
parent 60400 2d97d160a183
child 60449 2406d378cede 
     1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Thu Sep 16 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Sep 16 17:23:54 2021 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ Free _) = true
     1.5    | is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ Free _ $ Free _) = true
     1.6    | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ Free _ $ Free _) = true
     1.7 -  | is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ Free _ $ Free _) = true
     1.8 +  | is_ratpolyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ Free _ $ Free _) = true
     1.9    | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ Free _ $ Free _) = true
    1.10    | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) = 
    1.11                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.12 @@ -33,7 +33,7 @@
    1.13                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.14    | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) = 
    1.15                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.16 -  | is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ t1 $ t2) = 
    1.17 +  | is_ratpolyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ t1 $ t2) = 
    1.18                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.19    | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) = 
    1.20                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.21 @@ -131,10 +131,10 @@
    1.22      (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
    1.23    | monom_of_term  vs (c, es) (t as Free _) =
    1.24      (c, list_update es (find_index (curry op = t) vs) 1)
    1.25 -  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
    1.26 +  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>realpow\<close>, _) $ (b as Free _) $
    1.27        (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
    1.28      (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
    1.29 -  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
    1.30 +  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>realpow\<close>, _) $ (b as Free _) $
    1.31        (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
    1.32      (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
    1.33  
    1.34 @@ -154,7 +154,7 @@
    1.35      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.36    | monoms_of_term vs (t as Free _) =
    1.37      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.38 -  | monoms_of_term vs (t as Const (\<^const_name>\<open>powr\<close>, _) $ _ $  _) =
    1.39 +  | monoms_of_term vs (t as Const (\<^const_name>\<open>realpow\<close>, _) $ _ $  _) =
    1.40      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.41    | monoms_of_term vs (t as Const (\<^const_name>\<open>times\<close>, _) $ _ $  _) =
    1.42      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.43 @@ -195,7 +195,7 @@
    1.44    | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
    1.45    | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
    1.46    | term_of_es baseT expT (v :: vs) (e :: es) =
    1.47 -    Const (\<^const_name>\<open>Transcendental.powr\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
    1.48 +    Const (\<^const_name>\<open>realpow\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
    1.49      :: term_of_es baseT expT vs es
    1.50    | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
    1.51  
    1.52 @@ -519,7 +519,7 @@
    1.53  	  [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    1.54  	  ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    1.55  	  ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    1.56 -	  ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
    1.57 +	  ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
    1.58      errpatts = [],
    1.59  	scr =
    1.60  	  Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
    1.61 @@ -586,7 +586,7 @@
    1.62      calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    1.63        ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    1.64        ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    1.65 -      ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
    1.66 +      ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
    1.67      errpatts = [],
    1.68      scr = Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
    1.69        normal_form = add_fraction_p_ \<^theory>,
wneuper/isa