Renovate StaticFun a bit.
The functor is gone, and instead StaticFun exports two more general operators, one for defining a partial map by a tree, and one for extracting the theorems from an existing partial map definition. The extraction process uses simplification in a more conservative manner than before, and is guaranteed to produce exactly the expected theorems.
This commit is contained in:
Thomas Sewell
parent
0c004d2a93
commit
8e427dcb3b
|
|
@ -102,38 +102,33 @@ fun prove_impl_tac ctxt ss =
|
|||
in simp_tac (put_simpset ss ctxt addsimps unfolds) n
|
||||
end);
|
||||
|
||||
fun convert_impls prefix src_ctxt convs ctxt = let
|
||||
fun convert_impls ctxt = let
|
||||
|
||||
val tree_lemmata = StaticFun.prove_tree_lemmata ctxt
|
||||
(Proof_Context.get_thm ctxt "\<Gamma>_def");
|
||||
val thm = Proof_Context.get_thm ctxt "\<Gamma>_def"
|
||||
|
||||
val ss = simpset_of (put_simpset HOL_ss ctxt addsimps tree_lemmata);
|
||||
val proc_defs = (Term.add_const_names (concl_of thm) [])
|
||||
|> filter (String.isSuffix Hoare.proc_deco)
|
||||
|> map (suffix "_def" #> Proof_Context.get_thm ctxt)
|
||||
|
||||
fun convert_impl (impl, long_name) = let
|
||||
val prop = Thm.prop_of impl;
|
||||
val conv_prop = map_aterms (term_convert prefix convs) prop
|
||||
|> Envir.beta_eta_contract;
|
||||
val name = Long_Name.base_name long_name;
|
||||
in
|
||||
(name, Goal.prove ctxt [] [] conv_prop
|
||||
(fn v => prove_impl_tac (#context v) ss 1))
|
||||
end
|
||||
val tree_lemmata = StaticFun.prove_partial_map_thms thm
|
||||
(ctxt addsimps proc_defs)
|
||||
|
||||
val impls = Termtab.keys convs
|
||||
|> map (dest_Const #> fst #> Long_Name.base_name)
|
||||
|> filter (String.isSuffix "_body")
|
||||
|> map (suffix "_impl" o unsuffix "_body")
|
||||
|> map_filter (try (` (Proof_Context.get_thm src_ctxt)))
|
||||
|> map convert_impl;
|
||||
fun impl_name_from_proc (Const (s, _)) = s
|
||||
|> Long_Name.base_name
|
||||
|> unsuffix Hoare.proc_deco
|
||||
|> suffix HoarePackage.implementationN
|
||||
| impl_name_from_proc t = raise TERM ("impl_name_from_proc", [t])
|
||||
|
||||
in Local_Theory.notes (map (fn (n, t) => ((Binding.name n, []), [([t], [])])) impls)
|
||||
val saves = tree_lemmata |> map (apfst (fst #> impl_name_from_proc))
|
||||
|
||||
in Local_Theory.notes (map (fn (n, t) => ((Binding.name n, []), [([t], [])])) saves)
|
||||
ctxt |> snd end
|
||||
|
||||
fun take_all_actions prefix src_ctxt proc tm csenv
|
||||
styargs loc_name ctxt = let
|
||||
val (convs, ctxt) = convert prefix src_ctxt proc tm (Termtab.empty, ctxt);
|
||||
styargs ctxt = let
|
||||
val (_, ctxt) = convert prefix src_ctxt proc tm (Termtab.empty, ctxt);
|
||||
in ctxt
|
||||
|> convert_impls prefix src_ctxt convs
|
||||
|> convert_impls
|
||||
|> Modifies_Proofs.prove_all_modifies_goals_local csenv (fn _ => true) styargs
|
||||
end
|
||||
|
||||
|
|
@ -346,7 +341,6 @@ SubstituteSpecs.take_all_actions
|
|||
@{term kernel_all_global_addresses.\<Gamma>}
|
||||
(CalculateState.get_csenv @{theory} "c/kernel_all.c_pp" |> the)
|
||||
[@{typ "globals myvars"}, @{typ int}, @{typ strictc_errortype}]
|
||||
"kernel_all_substitute"
|
||||
*}
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -73,6 +73,7 @@ definition
|
|||
where
|
||||
"cchaos upd \<equiv> Spec { (s0,s) . \<exists>v. s = upd v s0 }"
|
||||
|
||||
ML_file "isa_termstypes.ML"
|
||||
ML_file "StrictC.grm.sig"
|
||||
ML_file "StrictC.grm.sml"
|
||||
ML_file "StrictC.lex.sml"
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ sig
|
|||
(typ,'a,'b) Element.ctxt list ->
|
||||
(* globals living in the globals locale *)
|
||||
theory ->
|
||||
(string * (binding * thm list) list * theory)
|
||||
(string * theory)
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -329,10 +329,10 @@ let
|
|||
val thy = Local_Theory.exit_global lthy
|
||||
|
||||
(* set up _impl by defining \<Gamma> *)
|
||||
val (defs, thy) =
|
||||
val thy =
|
||||
if List.exists (isSome o #body) fninfo then let
|
||||
val lthy = Named_Target.init globloc thy
|
||||
fun expfname fni = let
|
||||
fun get_body fni = let
|
||||
val nm = #fname fni
|
||||
in
|
||||
case (#body fni, #mod_annotated_protop fni) of
|
||||
|
|
@ -344,24 +344,14 @@ let
|
|||
SOME (Syntax.check_term lthy (Const(realnm, dummyT)))
|
||||
end
|
||||
end
|
||||
val blist' = map expfname fninfo
|
||||
val bnm = ListPair.zip (blist',nmdefs)
|
||||
val triples =
|
||||
ListPair.zip (bnm,
|
||||
map (suffix HoarePackage.implementationN o #fname)
|
||||
fninfo)
|
||||
val (defs, lthy) =
|
||||
StaticFun.define_tree_and_thms "\<Gamma>" triples lthy
|
||||
val lthy' = Local_Theory.restore lthy
|
||||
val morph = Proof_Context.export_morphism lthy lthy'
|
||||
val defs' = map (fn (n, t) =>
|
||||
(Morphism.binding morph (Binding.name n),
|
||||
map (Morphism.thm morph) t))
|
||||
defs
|
||||
(* name for thm, (proc constant, body constant) *)
|
||||
val (_, lthy) = StaticFun.define_tree_and_thms_with_defs
|
||||
@{binding \<Gamma>} (map (suffix HoarePackage.implementationN o #fname) fninfo)
|
||||
nmdefs (map get_body fninfo) @{term "id :: int => int"} lthy
|
||||
in
|
||||
(defs', Local_Theory.exit_global lthy')
|
||||
Local_Theory.exit_global lthy
|
||||
end
|
||||
else ([], thy)
|
||||
else thy
|
||||
|
||||
val globloc_expr = ([(globloc, (("", false), Expression.Named []))], [])
|
||||
|
||||
|
|
@ -413,7 +403,7 @@ let
|
|||
Expression.add_locale localename_b localename_b globloc_expr [] thy
|
||||
|
||||
in
|
||||
(globloc, defs, Local_Theory.exit_global ctxt)
|
||||
(globloc, Local_Theory.exit_global ctxt)
|
||||
end
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -10,11 +10,7 @@
|
|||
|
||||
theory StaticFun
|
||||
imports
|
||||
"../../lib/StringOrd"
|
||||
"../../lib/WordLib"
|
||||
"~~/src/HOL/Library/Numeral_Type"
|
||||
keywords
|
||||
"test_tree" "test_tree2" :: thy_decl
|
||||
Main
|
||||
begin
|
||||
|
||||
datatype ('a, 'b) Tree = Node 'a 'b "('a, 'b) Tree" "('a, 'b) Tree" | Leaf
|
||||
|
|
@ -27,74 +23,134 @@ where
|
|||
else if fn x < fn y then lookup_tree l fn x
|
||||
else lookup_tree r fn x)"
|
||||
|
||||
definition
|
||||
tree_gives_vals :: "('a, 'b) Tree \<Rightarrow> ('a \<Rightarrow> 'c :: linorder) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'c set \<Rightarrow> bool"
|
||||
definition optional_strict_range :: "('a :: linorder) option \<Rightarrow> 'a option \<Rightarrow> 'a set"
|
||||
where
|
||||
"tree_gives_vals T ord f S \<equiv> \<forall>x. (ord x \<in> S) \<longrightarrow> f x = lookup_tree T ord x"
|
||||
"optional_strict_range x y = {z. (x = None \<or> the x < z) \<and> (y = None \<or> z < the y)}"
|
||||
|
||||
lemma tree_gives_valsI:
|
||||
"\<lbrakk> f \<equiv> lookup_tree T ord \<rbrakk> \<Longrightarrow> tree_gives_vals T ord f UNIV"
|
||||
by (simp add: tree_gives_vals_def)
|
||||
lemma optional_strict_range_split:
|
||||
"z \<in> optional_strict_range x y
|
||||
\<Longrightarrow> optional_strict_range x (Some z) = ({..< z} \<inter> optional_strict_range x y)
|
||||
\<and> optional_strict_range (Some z) y = ({z <..} \<inter> optional_strict_range x y)"
|
||||
by (auto simp add: optional_strict_range_def)
|
||||
|
||||
lemma tree_gives_valsD:
|
||||
assumes "tree_gives_vals (Node y v l r) ord f S"
|
||||
shows "ord y \<in> S \<longrightarrow> f y = Some v"
|
||||
and "tree_gives_vals l ord f (S \<inter> {..<ord y})"
|
||||
and "tree_gives_vals r ord f (S \<inter> {ord y<..})"
|
||||
using assms
|
||||
apply -
|
||||
apply (simp add: tree_gives_vals_def)+
|
||||
lemma optional_strict_rangeI:
|
||||
"z \<in> optional_strict_range None None"
|
||||
"z < y \<Longrightarrow> z \<in> optional_strict_range None (Some y)"
|
||||
"x < z \<Longrightarrow> z \<in> optional_strict_range (Some x) None"
|
||||
"x < z \<Longrightarrow> z < y \<Longrightarrow> z \<in> optional_strict_range (Some x) (Some y)"
|
||||
by (simp_all add: optional_strict_range_def)
|
||||
|
||||
definition
|
||||
tree_eq_fun_in_range :: "('a, 'b) Tree \<Rightarrow> ('a \<Rightarrow> 'c :: linorder) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'c set \<Rightarrow> bool"
|
||||
where
|
||||
"tree_eq_fun_in_range T ord f S \<equiv> \<forall>x. (ord x \<in> S) \<longrightarrow> f x = lookup_tree T ord x"
|
||||
|
||||
lemma tree_eq_fun_in_range_from_def:
|
||||
"\<lbrakk> f \<equiv> lookup_tree T ord \<rbrakk>
|
||||
\<Longrightarrow> tree_eq_fun_in_range T ord f (optional_strict_range None None)"
|
||||
by (simp add: tree_eq_fun_in_range_def)
|
||||
|
||||
lemma tree_eq_fun_in_range_split:
|
||||
"tree_eq_fun_in_range (Node z v l r) ord f (optional_strict_range x y)
|
||||
\<Longrightarrow> ord z \<in> optional_strict_range x y
|
||||
\<Longrightarrow> tree_eq_fun_in_range l ord f (optional_strict_range x (Some (ord z)))
|
||||
\<and> f z = Some v
|
||||
\<and> tree_eq_fun_in_range r ord f (optional_strict_range (Some (ord z)) y)"
|
||||
apply (simp add: tree_eq_fun_in_range_def optional_strict_range_split)
|
||||
apply fastforce
|
||||
done
|
||||
|
||||
lemma tree_gives_vals_setonly_cong:
|
||||
"\<lbrakk> S = S' \<rbrakk> \<Longrightarrow> tree_gives_vals T ord f S = tree_gives_vals T ord f S'"
|
||||
by simp
|
||||
ML {*
|
||||
|
||||
lemma tree_vals_set_Int_simps:
|
||||
"UNIV \<inter> S = S"
|
||||
"({..<(x :: 'a :: linorder)} \<inter> {..<y}) = (if x < y then {..<x} else {..<y})"
|
||||
"({x<..} \<inter> {y<..}) = (if x < y then {y<..} else {x<..})"
|
||||
"({..<x} \<inter> {y<..}) = ({y<..} \<inter> {..<x})"
|
||||
"(({y<..} \<inter> {..<x}) \<inter> {z<..}) = ((if y < z then {z<..} else {y<..}) \<inter> {..<x})"
|
||||
"(({y<..} \<inter> {..<x}) \<inter> {..<z}) = ((if x < z then {..<x} else {..<z}) \<inter> {y<..})"
|
||||
by auto
|
||||
structure StaticFun = struct
|
||||
|
||||
lemmas tree_vals_set_simps =
|
||||
Int_iff greaterThan_iff lessThan_iff simp_thms UNIV_I
|
||||
tree_vals_set_Int_simps if_True if_False
|
||||
(* Actually build the tree -- theta (n lg(n)) *)
|
||||
fun build_tree' _ mk_leaf [] = mk_leaf
|
||||
| build_tree' mk_node mk_leaf xs = let
|
||||
val len = length xs
|
||||
val (ys, zs) = chop (len div 2) xs
|
||||
in case zs of [] => error "build_tree': impossible"
|
||||
| ((a, b) :: zs) => mk_node a b (build_tree' mk_node mk_leaf ys)
|
||||
(build_tree' mk_node mk_leaf zs)
|
||||
end
|
||||
|
||||
lemma int_0_less_1: "0 < (1::int)" by simp
|
||||
fun build_tree ord xs = case xs of [] => error "build_tree : empty"
|
||||
| (idx, v) :: _ => let
|
||||
val idxT = fastype_of idx
|
||||
val vT = fastype_of v
|
||||
val treeT = Type (@{type_name StaticFun.Tree}, [idxT, vT])
|
||||
val mk_leaf = Const (@{const_name StaticFun.Leaf}, treeT)
|
||||
val node = Const (@{const_name StaticFun.Node},
|
||||
idxT --> vT --> treeT --> treeT --> treeT)
|
||||
fun mk_node a b l r = node $ a $ b $ l $ r
|
||||
val lookup = Const (@{const_name StaticFun.lookup_tree},
|
||||
treeT --> fastype_of ord --> idxT
|
||||
--> Type (@{type_name option}, [vT]))
|
||||
in
|
||||
lookup $ (build_tree' mk_node mk_leaf xs) $ ord
|
||||
end
|
||||
|
||||
lemmas int_simpset = arith_simps rel_simps id_apply arith_special int_0_less_1
|
||||
fun define_partial_map_tree name mappings ord ctxt = let
|
||||
val tree = build_tree ord mappings
|
||||
in Local_Theory.define
|
||||
((name, NoSyn), ((Thm.def_binding name, []), tree)) ctxt
|
||||
|> apfst (apsnd snd)
|
||||
end
|
||||
|
||||
ML_file "isa_termstypes.ML"
|
||||
ML_file "static-fun.ML"
|
||||
fun prove_partial_map_thms thm ctxt = let
|
||||
val init = thm RS @{thm tree_eq_fun_in_range_from_def}
|
||||
fun rec_tree thm = case concl_of thm of
|
||||
@{term Trueprop} $ (Const (@{const_name tree_eq_fun_in_range}, _)
|
||||
$ (Const (@{const_name Node}, _) $ z $ v $ _ $ _) $ _ $ _ $ _) => let
|
||||
val t' = thm RS @{thm tree_eq_fun_in_range_split}
|
||||
val solve_simp_tac = SUBGOAL (fn (t, i) =>
|
||||
(simp_tac ctxt THEN_ALL_NEW SUBGOAL (fn (t', _) =>
|
||||
raise TERM ("prove_partial_map_thms: unsolved", [t, t']))) i)
|
||||
val r = t' |> (resolve_tac @{thms optional_strict_rangeI}
|
||||
THEN_ALL_NEW solve_simp_tac) 1 |> Seq.hd
|
||||
val l = r RS @{thm conjunct1}
|
||||
val kr = r RS @{thm conjunct2}
|
||||
val k = kr RS @{thm conjunct1}
|
||||
val r = kr RS @{thm conjunct2}
|
||||
in rec_tree l @ [((z, v), k)] @ rec_tree r end
|
||||
| _ => []
|
||||
in rec_tree init end
|
||||
|
||||
(*
|
||||
test_tree "gamma" 100
|
||||
locale foo =
|
||||
fixes x :: int
|
||||
;
|
||||
context foo
|
||||
begin
|
||||
;
|
||||
test_tree "gamma" 100
|
||||
fun define_tree_and_save_thms name names mappings ord exsimps ctxt = let
|
||||
val ((tree, def_thm), ctxt) = define_partial_map_tree name mappings ord ctxt
|
||||
val thms = prove_partial_map_thms def_thm (ctxt addsimps exsimps)
|
||||
val (idents, thms) = map_split I thms
|
||||
val _ = map (fn ((x, y), (x', y')) => (x aconv x' andalso y aconv y')
|
||||
orelse raise TERM ("define_tree_and_thms: different", [x, y, x', y']))
|
||||
(mappings ~~ idents)
|
||||
val (_, ctxt) = Local_Theory.notes
|
||||
(map (fn (s, t) => ((Binding.name s, []), [([t], [])]))
|
||||
(names ~~ thms)) ctxt
|
||||
in (tree, ctxt) end
|
||||
|
||||
Timing:
|
||||
|
||||
test_tree "gamma" 10000
|
||||
|
||||
int/\<longrightarrow>/700 = 32.582
|
||||
nat/\<longrightarrow>/700 = 49.643
|
||||
int/700 = 33. \<dots>
|
||||
int/simps/700 = 6.123
|
||||
int/simps/5000 = 65.184 secs
|
||||
int/simps/10000 = 154.166
|
||||
int/allsimps/700 = 3.00
|
||||
int/allsimps/5000 = 26.00 (TS: simps ran in 50sec on mine)
|
||||
string/allsimps/700 = 5.76
|
||||
string/allsimps/5000 = 47.53
|
||||
*)
|
||||
fun define_tree_and_thms_with_defs name names key_defs opt_values ord ctxt = let
|
||||
val data = names ~~ (key_defs ~~ opt_values)
|
||||
|> map_filter (fn (_, (_, NONE)) => NONE | (nm, (thm, SOME v))
|
||||
=> SOME (nm, (fst (Logic.dest_equals (concl_of thm)), v)))
|
||||
val (names, mappings) = map_split I data
|
||||
in define_tree_and_save_thms name names mappings ord key_defs ctxt end
|
||||
|
||||
end
|
||||
|
||||
*}
|
||||
|
||||
(* testing
|
||||
|
||||
local_setup {* StaticFun.define_tree_and_save_thms @{binding tree}
|
||||
["one", "two", "three"]
|
||||
[(@{term "Suc 0"}, @{term "Suc 0"}),
|
||||
(@{term "2 :: nat"}, @{term "15 :: nat"}),
|
||||
(@{term "3 :: nat"}, @{term "1 :: nat"})]
|
||||
@{term "id :: nat \<Rightarrow> nat"}
|
||||
#> snd
|
||||
*}
|
||||
print_theorems
|
||||
|
||||
*)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -65,9 +65,11 @@ fun define_naming_scheme [] _ = I
|
|||
fun name_term fni = SOME (HOLogic.mk_string (#fname fni))
|
||||
fun name_name fni = #fname fni ^ "_name"
|
||||
|
||||
in StaticFun.define_tree_and_thms NameGeneration.naming_scheme_name
|
||||
((map name_term fninfo ~~ nmdefs) ~~ map name_name fninfo)
|
||||
#> snd end
|
||||
in StaticFun.define_tree_and_thms_with_defs
|
||||
(Binding.name NameGeneration.naming_scheme_name)
|
||||
(map name_name fninfo) nmdefs
|
||||
(map name_term fninfo) @{term "id :: int => int"}
|
||||
#> snd end
|
||||
|
||||
fun define_function_names fninfo thy = let
|
||||
open Feedback
|
||||
|
|
@ -324,7 +326,7 @@ in
|
|||
fninfo
|
||||
rcdinfo
|
||||
ms
|
||||
val (globloc, _ (* binding list *), thy) =
|
||||
val (globloc, thy) =
|
||||
HPInter.make_function_definitions localename
|
||||
cse
|
||||
styargs
|
||||
|
|
|
|||
Loading…
Reference in New Issue