# HG changeset patch
# User nipkow
# Date 1711288247 -3600
# Node ID 4aeb25ba90f3871ce70f5b823ca30f89a619999a
# Parent  f1c29e366c096275dab20a0d133ba0736c3d63a4
more uniform command names

diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -472,19 +472,19 @@
 
 subsubsection \<open>Timing Functions\<close>
 
-define_time_fun link
+time_fun link
 
 lemma T_link[simp]: "T_link t\<^sub>1 t\<^sub>2 = 0"
 by(cases t\<^sub>1; cases t\<^sub>2, auto)
 
-define_time_fun rank
+time_fun rank
 
 lemma T_rank[simp]: "T_rank t = 0"
 by(cases t, auto)
 
-define_time_fun ins_tree
+time_fun ins_tree
 
-define_time_fun insert
+time_fun insert
 
 lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
 by (induction t ts rule: T_ins_tree.induct) auto
@@ -504,7 +504,7 @@
 
 subsubsection \<open>\<open>T_merge\<close>\<close>
 
-define_time_fun merge
+time_fun merge
 
 (* Warning: \<open>T_merge.induct\<close> is less convenient than the equivalent \<open>merge.induct\<close>,
 apparently because of the \<open>let\<close> clauses introduced by pattern_aliases; should be investigated.
@@ -547,14 +547,14 @@
 
 subsubsection \<open>\<open>T_get_min\<close>\<close>
 
-define_time_fun root
+time_fun root
 
 lemma T_root[simp]: "T_root t = 0"
 by(cases t)(simp_all)
 
-define_time_fun min
+time_fun min
 
-define_time_fun get_min
+time_fun get_min
 
 lemma T_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts"
 by (induction ts rule: T_get_min.induct) auto
@@ -571,7 +571,7 @@
 
 subsubsection \<open>\<open>T_del_min\<close>\<close>
 
-define_time_fun get_min_rest
+time_fun get_min_rest
 (*fun T_get_min_rest :: "'a::linorder trees \<Rightarrow> nat" where
   "T_get_min_rest [t] = 1"
 | "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"*)
@@ -595,7 +595,7 @@
 
 definition "T_rev xs = length xs + 1"
 
-define_time_fun del_min
+time_fun del_min
 
 lemma T_del_min_bound:
   fixes ts
diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Define_Time_0.ML
--- a/src/HOL/Data_Structures/Define_Time_0.ML	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_0.ML	Sun Mar 24 14:50:47 2024 +0100
@@ -37,7 +37,7 @@
 end
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>define_time_0\<close> "ML setup for global theory"
+  Outer_Syntax.command \<^command_keyword>\<open>time_fun_0\<close> "ML setup for global theory"
     (Parse.prop >> (Toplevel.theory o save));
 
 end
\ No newline at end of file
diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Define_Time_Function.ML
--- a/src/HOL/Data_Structures/Define_Time_Function.ML	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML	Sun Mar 24 14:50:47 2024 +0100
@@ -16,11 +16,10 @@
 val print_timing':  Proof.context -> pfunc -> pfunc -> unit
 val print_timing:  Proof.context -> Function.info -> Function.info -> unit
 
-val reg_and_proove_time_func: theory -> term list -> term list -> term option converter
-      -> (bool -> local_theory -> term list -> term option -> term)
+val reg_and_proove_time_func: theory -> term list -> term list
       -> bool -> Function.info * theory
-val reg_time_func: theory -> term list -> term list -> term option converter
-      -> (bool -> local_theory -> term list -> term option -> term) -> bool -> theory
+val reg_time_func: theory -> term list -> term list
+      -> bool -> theory
 
 val time_dom_tac: Proof.context -> thm -> thm list -> int -> tactic
 
@@ -316,10 +315,10 @@
   if not (casecIsCase T) then error "Internal error: invalid case type" else
     let val (nconst, args') = casecArgs f args in
       plus
+        (f (List.last args))
         (if nconst then
           SOME (build_func (Const (t,casecTyp T), args'))
          else NONE)
-        (f (List.last args))
     end
   | casec _ _ _ _ _ = error "Internal error: invalid case term"
 
@@ -332,8 +331,8 @@
     val tt = f tt
     val ft = f ft
   in
-    plus (case (tt,ft) of (NONE, NONE) => NONE | _ =>
-       (SOME ((Const (If_name, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft)))) (f cond)
+    plus (f cond) (case (tt,ft) of (NONE, NONE) => NONE | _ =>
+       (SOME ((Const (If_name, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft))))
   end
 
 fun letc_change_typ (Type ("fun", [T1, Type ("fun", [T2, _])])) = (Type ("fun", [T1, Type ("fun", [change_typ T2, HOLogic.natT])]))
@@ -363,16 +362,16 @@
 fun top_converter is_rec _ _ = opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE))
 
 (* Use converter to convert right side of a term *)
-fun to_time ctxt origin converter top_converter term =
-  top_converter ctxt origin (walk ctxt origin converter term)
+fun to_time ctxt origin is_rec term =
+  top_converter is_rec ctxt origin (walk ctxt origin converter term)
 
 (* Converts a term to its running time version *)
-fun convert_term ctxt (origin: term list) conv topConv (pT $ (Const (eqN, _) $ l $ r)) =
+fun convert_term ctxt (origin: term list) is_rec (pT $ (Const (eqN, _) $ l $ r)) =
       pT
       $ (Const (eqN, @{typ "nat \<Rightarrow> nat \<Rightarrow> bool"})
         $ (build_func ((walk_func l []) |>> (fun_to_time ctxt origin) |>> Option.valOf ||> conv_args ctxt origin))
-        $ (to_time ctxt origin conv topConv r))
-  | convert_term _ _ _ _ _ = error "Internal error: invalid term to convert"
+        $ (to_time ctxt origin is_rec r))
+  | convert_term _ _ _ _ = error "Internal error: invalid term to convert"
 
 (* 4. Tactic to prove "f_dom n" *)
 fun time_dom_tac ctxt induct_rule domintros =
@@ -389,10 +388,10 @@
    handle Empty => error "Function or terms of function not found"
 
 (* Register timing function of a given function *)
-fun reg_and_proove_time_func (theory: theory) (term: term list) (terms: term list) conv topConv print =
-  reg_time_func theory term terms conv topConv false
+fun reg_and_proove_time_func (theory: theory) (term: term list) (terms: term list) print =
+  reg_time_func theory term terms false
   |> proove_termination term terms print
-and reg_time_func (theory: theory) (term: term list) (terms: term list) conv topConv print =
+and reg_time_func (theory: theory) (term: term list) (terms: term list) print =
   let
     val lthy = Named_Target.theory_init theory
     val _ =
@@ -403,7 +402,7 @@
 
     (* 1. Fix all terms *)
     (* Exchange Var in types and terms to Free and check constraints *)
-    val terms = map 
+    val terms = map
       (map_aterms fixTerms
         #> map_types (map_atyps fixTypes)
         #> fixPartTerms lthy term)
@@ -417,7 +416,7 @@
       - On left side change name of function to timing function
       - Convert right side of equation with conversion schema
     *)
-    val timing_terms = map (convert_term lthy term conv (topConv is_rec)) terms
+    val timing_terms = map (convert_term lthy term is_rec) terms
 
     (* 4. Register function and prove termination *)
     val names = map Term.term_name term
@@ -522,38 +521,60 @@
     (time_info, Local_Theory.exit_global lthy')
   end
 
+fun fix_definition (Const ("Pure.eq", _) $ l $ r) = Const ("HOL.Trueprop", @{typ "bool \<Rightarrow> prop"})
+      $ (Const ("HOL.eq", @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}) $ l $ r)
+  | fix_definition t = t
+fun check_definition [t] = [t]
+  | check_definition _ = error "Only a single defnition is allowed"
+
 (* Convert function into its timing function (called by command) *)
-fun reg_time_fun_cmd (funcs, thms) conv topConv (theory: theory) =
+fun reg_time_fun_cmd (funcs, thms) (theory: theory) =
 let
   val ctxt = Proof_Context.init_global theory
   val fterms = map (Syntax.read_term ctxt) funcs
   val (_, lthy') = reg_and_proove_time_func theory fterms
     (case thms of NONE => get_terms theory (hd fterms)
                 | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
-    conv topConv true
+    true
 in lthy'
 end
 
 (* Convert function into its timing function (called by command) with termination proof provided by user*)
-fun reg_time_function_cmd (funcs, thms) conv topConv (theory: theory) =
+fun reg_time_function_cmd (funcs, thms) (theory: theory) =
 let
   val ctxt = Proof_Context.init_global theory
   val fterms = map (Syntax.read_term ctxt) funcs
   val theory = reg_time_func theory fterms
     (case thms of NONE => get_terms theory (hd fterms)
                 | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
-    conv topConv true
+    true
 in theory
 end
 
+(* Convert function into its timing function (called by command) *)
+fun reg_time_definition_cmd (funcs, thms) (theory: theory) =
+let
+  val ctxt = Proof_Context.init_global theory
+  val fterms = map (Syntax.read_term ctxt) funcs
+  val (_, lthy') = reg_and_proove_time_func theory fterms
+    (case thms of NONE => get_terms theory (hd fterms) |> check_definition |> map fix_definition
+                | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
+    true
+in lthy'
+end
+
 val parser = (Scan.repeat1 Parse.prop) -- (Scan.option (Parse.keyword_improper "equations" -- Parse.thms1 >> snd))
 
-val _ = Outer_Syntax.command @{command_keyword "define_time_fun"}
+val _ = Outer_Syntax.command @{command_keyword "time_fun"}
   "Defines runtime function of a function"
-  (parser >> (fn p => Toplevel.theory (reg_time_fun_cmd p converter top_converter)))
+  (parser >> (fn p => Toplevel.theory (reg_time_fun_cmd p)))
 
-val _ = Outer_Syntax.command @{command_keyword "define_time_function"}
+val _ = Outer_Syntax.command @{command_keyword "time_function"}
   "Defines runtime function of a function"
-  (parser >> (fn p => Toplevel.theory (reg_time_function_cmd p converter top_converter)))
+  (parser >> (fn p => Toplevel.theory (reg_time_function_cmd p)))
+
+val _ = Outer_Syntax.command @{command_keyword "time_definition"}
+  "Defines runtime function of a definition"
+  (parser >> (fn p => Toplevel.theory (reg_time_definition_cmd p)))
 
 end
diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Define_Time_Function.thy
--- a/src/HOL/Data_Structures/Define_Time_Function.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -8,10 +8,11 @@
 
 theory Define_Time_Function
   imports Main
-  keywords "define_time_fun" :: thy_decl
-    and    "define_time_function" :: thy_goal
+  keywords "time_fun" :: thy_decl
+    and    "time_function" :: thy_goal
+    and    "time_definition" :: thy_goal
     and    "equations"
-    and    "define_time_0" :: thy_decl
+    and    "time_fun_0" :: thy_decl
 begin
 
 ML_file Define_Time_0.ML
@@ -31,17 +32,17 @@
 The constant-time assumption for \<open>(=)\<close> is justified for recursive data types such as lists and trees
 as long as the comparison is of the form \<open>t = c\<close> where \<open>c\<close> is a constant term, for example \<open>xs = []\<close>.\<close>
 
-define_time_0 "(+)"
-define_time_0 "(-)"
-define_time_0 "(*)"
-define_time_0 "(/)"
-define_time_0 "(div)"
-define_time_0 "(<)"
-define_time_0 "(\<le>)"
-define_time_0 "Not"
-define_time_0 "(\<and>)"
-define_time_0 "(\<or>)"
-define_time_0 "Num.numeral_class.numeral"
-define_time_0 "(=)"
+time_fun_0 "(+)"
+time_fun_0 "(-)"
+time_fun_0 "(*)"
+time_fun_0 "(/)"
+time_fun_0 "(div)"
+time_fun_0 "(<)"
+time_fun_0 "(\<le>)"
+time_fun_0 "Not"
+time_fun_0 "(\<and>)"
+time_fun_0 "(\<or>)"
+time_fun_0 "Num.numeral_class.numeral"
+time_fun_0 "(=)"
 
 end
\ No newline at end of file
diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -160,16 +160,16 @@
 subsection "Complexity"
 
 text \<open>Auxiliary time functions (which are both 0):\<close>
-define_time_fun mht
-define_time_fun node
+time_fun mht
+time_fun node
 
 lemma T_mht_0[simp]: "T_mht t = 0"
 by(cases t)auto
 
 text \<open>Define timing function\<close>
-define_time_fun merge
-define_time_fun insert
-define_time_fun del_min
+time_fun merge
+time_fun insert
+time_fun del_min
 
 lemma T_merge_min_height: "ltree l \<Longrightarrow> ltree r \<Longrightarrow> T_merge l r \<le> min_height l + min_height r + 1"
 proof(induction l r rule: merge.induct)
diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Queue_2Lists.thy
--- a/src/HOL/Data_Structures/Queue_2Lists.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -59,10 +59,10 @@
 
 text \<open>Running times:\<close>
 
-define_time_fun norm
-define_time_fun enq
-define_time_fun tl
-define_time_fun deq
+time_fun norm
+time_fun enq
+time_fun tl
+time_fun deq
 
 lemma T_tl_0: "T_tl xs = 0"
 by(cases xs)auto
diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Reverse.thy
--- a/src/HOL/Data_Structures/Reverse.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Reverse.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -2,8 +2,8 @@
 imports Define_Time_Function
 begin
 
-define_time_fun append
-define_time_fun rev
+time_fun append
+time_fun rev
 
 lemma T_append: "T_append xs ys = length xs + 1"
 by(induction xs) auto
@@ -21,7 +21,7 @@
 lemma itrev_Nil: "itrev xs [] = rev xs"
 by(simp add: itrev)
 
-define_time_fun itrev
+time_fun itrev
 
 lemma T_itrev: "T_itrev xs ys = length xs + 1"
 by(induction xs arbitrary: ys) auto
diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Time_Funs.thy
--- a/src/HOL/Data_Structures/Time_Funs.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -48,8 +48,8 @@
 
 lemmas [simp del] = T_nth.simps
 
-define_time_fun take
-define_time_fun drop
+time_fun take
+time_fun drop
 
 lemma T_take_eq: "T_take n xs = min n (length xs) + 1"
   by (induction xs arbitrary: n) (auto split: nat.splits)
diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Tree23_of_List.thy
--- a/src/HOL/Data_Structures/Tree23_of_List.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -118,10 +118,10 @@
 
 subsection "Linear running time"
 
-define_time_fun join_adj
-define_time_fun join_all
-define_time_fun leaves
-define_time_fun tree23_of_list
+time_fun join_adj
+time_fun join_all
+time_fun leaves
+time_fun tree23_of_list
 
 lemma T_join_adj: "not_T ts \<Longrightarrow> T_join_adj ts \<le> len ts div 2"
 by(induction ts rule: T_join_adj.induct) auto