--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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)
--- 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