--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 18 16:47:40 2014 +0200
@@ -231,7 +231,6 @@
ML_file "Tools/BNF/bnf_lfp_compat.ML"
ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
ML_file "Tools/BNF/bnf_lfp_size.ML"
-ML_file "Tools/Function/old_size.ML"
hide_fact (open) id_transfer
--- a/src/HOL/Basic_BNF_Least_Fixpoints.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy Thu Sep 18 16:47:40 2014 +0200
@@ -9,32 +9,6 @@
imports BNF_Least_Fixpoint
begin
-subsection {* Size setup (TODO: Merge with rest of file) *}
-
-lemma size_bool[code]: "size (b\<Colon>bool) = 0"
- by (cases b) auto
-
-lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
- by (induct n) simp_all
-
-declare prod.size[no_atp]
-
-lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
- by (rule ext) (case_tac x, auto)
-
-lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
- by (rule ext) auto
-
-setup {*
-BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
- @{thms size_sum_o_map}
-#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
- @{thms size_prod_o_map}
-*}
-
-
-subsection {* FP sugar setup *}
-
definition xtor :: "'a \<Rightarrow> 'a" where
"xtor x = x"
@@ -55,15 +29,6 @@
lemmas xtor_inject = xtor_rel[of "op ="]
-definition ctor_rec :: "'a \<Rightarrow> 'a" where
- "ctor_rec x = x"
-
-lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
- unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
-
-lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
- unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
-
lemma xtor_rel_induct: "(\<And>x y. vimage2p id_bnf id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR"
unfolding xtor_def vimage2p_def id_bnf_def by default
@@ -76,12 +41,30 @@
lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
unfolding xtor_def id_bnf_def by (rule reflexive)
+definition ctor_rec :: "'a \<Rightarrow> 'a" where
+ "ctor_rec x = x"
+
+lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
+ unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
+
+lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
+ unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
+
+lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
+ unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
+
ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
+thm sum.rec_o_map
+thm sum.size_o_map
+
+thm prod.rec_o_map
+thm prod.size_o_map
+
hide_const (open) xtor ctor_rec
hide_fact (open)
xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
- ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
+ ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
end
--- a/src/HOL/Code_Numeral.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Code_Numeral.thy Thu Sep 18 16:47:40 2014 +0200
@@ -809,22 +809,6 @@
shows P
using assms by transfer blast
-lemma [simp, code]:
- "size_natural = nat_of_natural"
-proof (rule ext)
- fix n
- show "size_natural n = nat_of_natural n"
- by (induct n) simp_all
-qed
-
-lemma [simp, code]:
- "size = nat_of_natural"
-proof (rule ext)
- fix n
- show "size n = nat_of_natural n"
- by (induct n) simp_all
-qed
-
lemma natural_decr [termination_simp]:
"n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
by transfer simp
--- a/src/HOL/Fun_Def.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Fun_Def.thy Thu Sep 18 16:47:40 2014 +0200
@@ -5,7 +5,7 @@
header {* Function Definitions and Termination Proofs *}
theory Fun_Def
-imports Partial_Function SAT
+imports Basic_BNF_Least_Fixpoints Partial_Function SAT
keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl
begin
--- a/src/HOL/Library/Old_Datatype.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Library/Old_Datatype.thy Thu Sep 18 16:47:40 2014 +0200
@@ -10,6 +10,10 @@
keywords "old_datatype" :: thy_decl
begin
+ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
+ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
+
+
subsection {* The datatype universe *}
definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
@@ -523,6 +527,5 @@
ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
-ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
end
--- a/src/HOL/Main.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Main.thy Thu Sep 18 16:47:40 2014 +0200
@@ -2,7 +2,7 @@
theory Main
imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
- Basic_BNF_Least_Fixpoints BNF_Greatest_Fixpoint
+ BNF_Greatest_Fixpoint
begin
text {*
--- a/src/HOL/Nat.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Nat.thy Thu Sep 18 16:47:40 2014 +0200
@@ -1185,7 +1185,7 @@
by (fact Let_def)
-subsubsection {* Monotonicity of Multiplication *}
+subsubsection {* Monotonicity of multiplication *}
lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
by (simp add: mult_right_mono)
@@ -1390,7 +1390,7 @@
qed
-subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
+subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *}
context semiring_1
begin
@@ -1512,7 +1512,7 @@
by (auto simp add: fun_eq_iff)
-subsection {* The Set of Natural Numbers *}
+subsection {* The set of natural numbers *}
context semiring_1
begin
@@ -1567,7 +1567,7 @@
end
-subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
+subsection {* Further arithmetic facts concerning the natural numbers *}
lemma subst_equals:
assumes 1: "t = s" and 2: "u = t"
@@ -1825,6 +1825,7 @@
"i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
by (induct j arbitrary: i) (auto simp: le_Suc_eq)
+
subsection {* The divides relation on @{typ nat} *}
lemma dvd_1_left [iff]: "Suc 0 dvd k"
@@ -1962,7 +1963,7 @@
qed
-subsection {* aliases *}
+subsection {* Aliases *}
lemma nat_mult_1: "(1::nat) * n = n"
by (rule mult_1_left)
@@ -1971,13 +1972,23 @@
by (rule mult_1_right)
-subsection {* size of a datatype value *}
+subsection {* Size of a datatype value *}
class size =
fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
-
-subsection {* code module namespace *}
+instantiation nat :: size
+begin
+
+definition size_nat where
+ [simp, code]: "size (n \<Colon> nat) = n"
+
+instance ..
+
+end
+
+
+subsection {* Code module namespace *}
code_identifier
code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 18 16:47:40 2014 +0200
@@ -15,7 +15,6 @@
open BNF_FP_Rec_Sugar_Util
open BNF_FP_Util
open BNF_FP_Def_Sugar
-open BNF_LFP_Size
fun trivial_absT_info_of fpT =
{absT = fpT,
@@ -38,10 +37,10 @@
dtors = [Const (@{const_name xtor}, fpT --> fpT)],
xtor_co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))],
xtor_co_induct = @{thm xtor_induct},
- dtor_ctors = [@{thm xtor_xtor}],
- ctor_dtors = [@{thm xtor_xtor}],
- ctor_injects = [@{thm xtor_inject}],
- dtor_injects = [@{thm xtor_inject}],
+ dtor_ctors = @{thms xtor_xtor},
+ ctor_dtors = @{thms xtor_xtor},
+ ctor_injects = @{thms xtor_inject},
+ dtor_injects = @{thms xtor_inject},
xtor_map_thms = [xtor_map],
xtor_set_thmss = [xtor_sets],
xtor_rel_thms = [xtor_rel],
@@ -80,10 +79,10 @@
ctr_defs = @{thms Inl_def_alt Inr_def_alt},
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
- co_rec_def = @{thm case_sum_def},
+ co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
maps = @{thms map_sum.simps},
- common_co_inducts = [@{thm sum.induct}],
- co_inducts = [@{thm sum.induct}],
+ common_co_inducts = @{thms sum.induct},
+ co_inducts = @{thms sum.induct},
co_rec_thms = @{thms sum.case},
co_rec_discs = [],
co_rec_selss = [],
@@ -118,22 +117,22 @@
fp_nesting_bnfs = [],
live_nesting_bnfs = [],
ctrXs_Tss = [ctr_Ts],
- ctr_defs = [@{thm Pair_def_alt}],
+ ctr_defs = @{thms Pair_def_alt},
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
- co_rec_def = @{thm case_prod_def},
- maps = [@{thm map_prod_simp}],
- common_co_inducts = [@{thm prod.induct}],
- co_inducts = [@{thm prod.induct}],
- co_rec_thms = [@{thm prod.case}],
+ co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
+ maps = @{thms map_prod_simp},
+ common_co_inducts = @{thms prod.induct},
+ co_inducts = @{thms prod.induct},
+ co_rec_thms = @{thms prod.case},
co_rec_discs = [],
co_rec_selss = [],
- rel_injects = [@{thm rel_prod_apply}],
+ rel_injects = @{thms rel_prod_apply},
rel_distincts = []}
end;
val _ = Theory.setup (map_local_theory (fn lthy =>
- fold (BNF_FP_Def_Sugar.register_fp_sugars (fn s => s <> size_plugin) o single o (fn f => f lthy))
+ fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy))
[fp_sugar_of_sum, fp_sugar_of_prod] lthy));
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 18 16:47:40 2014 +0200
@@ -67,8 +67,7 @@
fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
ctor_rec_o_map =
- unfold_thms_tac ctxt [rec_def] THEN
- HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN'
+ HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' rtac (ctor_rec_o_map RS trans) THEN'
CONVERSION Thm.eta_long_conversion THEN'
asm_simp_tac (ss_only (pre_map_defs @
distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps)
--- a/src/HOL/Tools/Function/old_size.ML Thu Sep 18 16:47:40 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,228 +0,0 @@
-(* Title: HOL/Tools/Function/old_size.ML
- Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
-
-Size functions for old-style datatypes.
-*)
-
-structure Old_Size: sig end =
-struct
-
-fun plus (t1, t2) = Const (@{const_name Groups.plus},
- HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
-
-fun size_of_type f g h (T as Type (s, Ts)) =
- (case f s of
- SOME t => SOME t
- | NONE => (case g s of
- SOME size_name =>
- SOME (list_comb (Const (size_name,
- map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
- map (size_of_type' f g h) Ts))
- | NONE => NONE))
- | size_of_type _ _ h (TFree (s, _)) = h s
-and size_of_type' f g h T = (case size_of_type f g h T of
- NONE => Abs ("x", T, HOLogic.zero)
- | SOME t => t);
-
-fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) =
- is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts
- | is_poly _ _ = true;
-
-fun constrs_of thy name =
- let
- val {descr, index, ...} = Old_Datatype_Data.the_info thy name
- val SOME (_, _, constrs) = AList.lookup op = descr index
- in constrs end;
-
-val app = curry (list_comb o swap);
-
-fun prove_size_thms (info : Old_Datatype_Aux.info) new_type_names thy =
- let
- val {descr, rec_names, rec_rewrites, induct, ...} = info;
- val l = length new_type_names;
- val descr' = List.take (descr, l);
- val tycos = map (#1 o snd) descr';
- in
- if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then
- (* nothing to do -- the "size" function is already defined *)
- thy
- else
- let
- val recTs = Old_Datatype_Aux.get_rec_types descr;
- val (recTs1, recTs2) = chop l recTs;
- val (_, (_, paramdts, _)) :: _ = descr;
- val paramTs = map (Old_Datatype_Aux.typ_of_dtyp descr) paramdts;
- val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
- map (fn T as TFree (s, _) =>
- let
- val name = "f" ^ unprefix "'" s;
- val U = T --> HOLogic.natT
- in
- (((s, Free (name, U)), U), name)
- end) |> split_list |>> split_list;
- val param_size = AList.lookup op = param_size_fs;
-
- val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
- map_filter (Option.map (fst o snd) o BNF_LFP_Size.size_of_global thy) |> flat;
- val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy;
-
- val (((size_names, size_fns), def_names), def_names') =
- recTs1 |> map (fn T as Type (s, _) =>
- let
- val s' = "size_" ^ Long_Name.base_name s;
- val s'' = Sign.full_bname thy s';
- in
- (s'',
- (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
- map snd param_size_fs),
- (s' ^ "_def", s' ^ "_overloaded_def")))
- end) |> split_list ||>> split_list ||>> split_list;
- val overloaded_size_fns = map HOLogic.size_const recTs1;
-
- (* instantiation for primrec combinator *)
- fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
- let
- val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
- val k = length (filter Old_Datatype_Aux.is_rec_type cargs);
- val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
- if Old_Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
- else
- (if b andalso is_poly thy dt' then
- case size_of_type (K NONE) extra_size size_ofp T of
- NONE => us | SOME sz => sz $ Bound j :: us
- else us, i, j + 1))
- (cargs ~~ cargs' ~~ Ts) ([], 0, k);
- val t =
- if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
- then HOLogic.zero
- else foldl1 plus (ts @ [HOLogic.Suc_zero])
- in
- fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
- end;
-
- val fs = maps (fn (_, (name, _, constrs)) =>
- map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
- val fs' = maps (fn (n, (name, _, constrs)) =>
- map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
- val fTs = map fastype_of fs;
-
- val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
- Const (rec_name, fTs @ [T] ---> HOLogic.natT))
- (recTs ~~ rec_names));
-
- fun define_overloaded (def_name, eq) lthy =
- let
- val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
- val (thm, lthy') = lthy
- |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
- |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
- val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
- val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
- in (thm', lthy') end;
-
- val ((size_def_thms, size_def_thms'), thy') =
- thy
- |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s),
- param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
- (size_names ~~ recTs1))
- |> Global_Theory.add_defs false
- (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
- (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
- ||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size])
- ||>> fold_map define_overloaded
- (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
- ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- ||> Local_Theory.exit_global;
-
- val ctxt = Proof_Context.init_global thy';
-
- val simpset1 =
- put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
- size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
- val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
-
- fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) =
- HOLogic.mk_eq (app fs r $ Free p,
- the (size_of_type tab extra_size size_ofp T) $ Free p);
-
- fun prove_unfolded_size_eqs size_ofp fs =
- if null recTs2 then []
- else Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
- (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (replicate l @{term True} @
- map (mk_unfolded_size_eq (AList.lookup op =
- (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
- (xs ~~ recTs2 ~~ rec_combs2))))
- (fn _ => (Old_Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
-
- val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
- val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
-
- (* characteristic equations for size functions *)
- fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
- let
- val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
- val tnames = Name.variant_list f_names (Old_Datatype_Prop.make_tnames Ts);
- val ts = map_filter (fn (sT as (_, T), dt) =>
- Option.map (fn sz => sz $ Free sT)
- (if p dt then size_of_type size_of extra_size size_ofp T
- else NONE)) (tnames ~~ Ts ~~ cargs)
- in
- HOLogic.mk_Trueprop (HOLogic.mk_eq
- (size_const $ list_comb (Const (cname, Ts ---> T),
- map2 (curry Free) tnames Ts),
- if null ts then HOLogic.zero
- else foldl1 plus (ts @ [HOLogic.Suc_zero])))
- end;
-
- val simpset2 =
- put_simpset HOL_basic_ss ctxt
- addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1);
- val simpset3 =
- put_simpset HOL_basic_ss ctxt
- addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2);
-
- fun prove_size_eqs p size_fns size_ofp simpset =
- maps (fn (((_, (_, _, constrs)), size_const), T) =>
- map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
- (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
- size_ofp size_const T constr)
- (fn _ => simp_tac simpset 1))) constrs)
- (descr' ~~ size_fns ~~ recTs1);
-
- val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
- prove_size_eqs Old_Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
-
- val ([(_, size_thms)], thy'') = thy'
- |> Global_Theory.note_thmss ""
- [((Binding.name "size",
- [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
- Thm.declaration_attribute (fn thm =>
- Context.mapping (Code.add_default_eqn thm) I)]),
- [(size_eqns, [])])];
-
- in
- fold2 (fn new_type_name => fn size_name =>
- BNF_LFP_Size.register_size_global new_type_name size_name size_thms [])
- new_type_names size_names thy''
- end
- end;
-
-fun add_size_thms _ (new_type_names as name :: _) thy =
- let
- val info as {descr, ...} = Old_Datatype_Data.the_info thy name;
- val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
- val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
- Old_Datatype_Aux.is_rec_type dt andalso
- not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
- in
- if no_size then thy
- else
- thy
- |> Sign.add_path prefix
- |> prove_size_thms info new_type_names
- |> Sign.restore_naming thy
- end;
-
-val _ = Context.>> (Context.map_theory (Old_Datatype_Data.interpretation add_size_thms));
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Old_Datatype/old_size.ML Thu Sep 18 16:47:40 2014 +0200
@@ -0,0 +1,229 @@
+(* Title: HOL/Tools/Old_Datatype/old_size.ML
+ Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+
+Size functions for old-style datatypes.
+*)
+
+structure Old_Size: sig end =
+struct
+
+fun plus (t1, t2) = Const (@{const_name Groups.plus},
+ HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
+
+fun size_of_type f g h (T as Type (s, Ts)) =
+ (case f s of
+ SOME t => SOME t
+ | NONE => (case g s of
+ SOME size_name =>
+ SOME (list_comb (Const (size_name,
+ map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
+ map (size_of_type' f g h) Ts))
+ | NONE => NONE))
+ | size_of_type _ _ h (TFree (s, _)) = h s
+and size_of_type' f g h T = (case size_of_type f g h T of
+ NONE => Abs ("x", T, HOLogic.zero)
+ | SOME t => t);
+
+fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) =
+ is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts
+ | is_poly _ _ = true;
+
+fun constrs_of thy name =
+ let
+ val {descr, index, ...} = Old_Datatype_Data.the_info thy name
+ val SOME (_, _, constrs) = AList.lookup op = descr index
+ in constrs end;
+
+val app = curry (list_comb o swap);
+
+fun prove_size_thms (info : Old_Datatype_Aux.info) new_type_names thy =
+ let
+ val {descr, rec_names, rec_rewrites, induct, ...} = info;
+ val l = length new_type_names;
+ val descr' = List.take (descr, l);
+ val tycos = map (#1 o snd) descr';
+ in
+ if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then
+ (* nothing to do -- the "size" function is already defined *)
+ thy
+ else
+ let
+ val recTs = Old_Datatype_Aux.get_rec_types descr;
+ val (recTs1, recTs2) = chop l recTs;
+ val (_, (_, paramdts, _)) :: _ = descr;
+ val paramTs = map (Old_Datatype_Aux.typ_of_dtyp descr) paramdts;
+ val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
+ map (fn T as TFree (s, _) =>
+ let
+ val name = "f" ^ unprefix "'" s;
+ val U = T --> HOLogic.natT
+ in
+ (((s, Free (name, U)), U), name)
+ end) |> split_list |>> split_list;
+ val param_size = AList.lookup op = param_size_fs;
+
+ val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
+ map_filter (Option.map (fst o snd) o BNF_LFP_Size.size_of_global thy) |> flat;
+ val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy;
+
+ val (((size_names, size_fns), def_names), def_names') =
+ recTs1 |> map (fn T as Type (s, _) =>
+ let
+ val s' = "size_" ^ Long_Name.base_name s;
+ val s'' = Sign.full_bname thy s';
+ in
+ (s'',
+ (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
+ map snd param_size_fs),
+ (s' ^ "_def", s' ^ "_overloaded_def")))
+ end) |> split_list ||>> split_list ||>> split_list;
+ val overloaded_size_fns = map HOLogic.size_const recTs1;
+
+ (* instantiation for primrec combinator *)
+ fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
+ let
+ val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
+ val k = length (filter Old_Datatype_Aux.is_rec_type cargs);
+ val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
+ if Old_Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
+ else
+ (if b andalso is_poly thy dt' then
+ case size_of_type (K NONE) extra_size size_ofp T of
+ NONE => us | SOME sz => sz $ Bound j :: us
+ else us, i, j + 1))
+ (cargs ~~ cargs' ~~ Ts) ([], 0, k);
+ val t =
+ if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
+ then HOLogic.zero
+ else foldl1 plus (ts @ [HOLogic.Suc_zero])
+ in
+ fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
+ end;
+
+ val fs = maps (fn (_, (name, _, constrs)) =>
+ map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
+ val fs' = maps (fn (n, (name, _, constrs)) =>
+ map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
+ val fTs = map fastype_of fs;
+
+ val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
+ Const (rec_name, fTs @ [T] ---> HOLogic.natT))
+ (recTs ~~ rec_names));
+
+ fun define_overloaded (def_name, eq) lthy =
+ let
+ val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
+ val (thm, lthy') = lthy
+ |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
+ |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
+ val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
+ val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
+ in (thm', lthy') end;
+
+ val ((size_def_thms, size_def_thms'), thy') =
+ thy
+ |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s),
+ param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
+ (size_names ~~ recTs1))
+ |> Global_Theory.add_defs false
+ (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
+ (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
+ ||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size])
+ ||>> fold_map define_overloaded
+ (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
+ ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+ ||> Local_Theory.exit_global;
+
+ val ctxt = Proof_Context.init_global thy';
+
+ val simpset1 =
+ put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
+ size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
+ val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
+
+ fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) =
+ HOLogic.mk_eq (app fs r $ Free p,
+ the (size_of_type tab extra_size size_ofp T) $ Free p);
+
+ fun prove_unfolded_size_eqs size_ofp fs =
+ if null recTs2 then []
+ else Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
+ (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (replicate l @{term True} @
+ map (mk_unfolded_size_eq (AList.lookup op =
+ (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
+ (xs ~~ recTs2 ~~ rec_combs2))))
+ (fn _ => (Old_Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
+
+ val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
+ val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
+
+ (* characteristic equations for size functions *)
+ fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
+ let
+ val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
+ val tnames = Name.variant_list f_names (Old_Datatype_Prop.make_tnames Ts);
+ val ts = map_filter (fn (sT as (_, T), dt) =>
+ Option.map (fn sz => sz $ Free sT)
+ (if p dt then size_of_type size_of extra_size size_ofp T
+ else NONE)) (tnames ~~ Ts ~~ cargs)
+ in
+ HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (size_const $ list_comb (Const (cname, Ts ---> T),
+ map2 (curry Free) tnames Ts),
+ if null ts then HOLogic.zero
+ else foldl1 plus (ts @ [HOLogic.Suc_zero])))
+ end;
+
+ val simpset2 =
+ put_simpset HOL_basic_ss ctxt
+ addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1);
+ val simpset3 =
+ put_simpset HOL_basic_ss ctxt
+ addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2);
+
+ fun prove_size_eqs p size_fns size_ofp simpset =
+ maps (fn (((_, (_, _, constrs)), size_const), T) =>
+ map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
+ (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
+ size_ofp size_const T constr)
+ (fn _ => simp_tac simpset 1))) constrs)
+ (descr' ~~ size_fns ~~ recTs1);
+
+ val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
+ prove_size_eqs Old_Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
+
+ val ([(_, size_thms)], thy'') = thy'
+ |> Global_Theory.note_thmss ""
+ [((Binding.name "size",
+ [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
+ Thm.declaration_attribute (fn thm =>
+ Context.mapping (Code.add_default_eqn thm) I)]),
+ [(size_eqns, [])])];
+
+ in
+ fold2 (fn new_type_name => fn size_name =>
+ BNF_LFP_Size.register_size_global new_type_name size_name size_thms [])
+ new_type_names size_names thy''
+ end
+ end;
+
+fun add_size_thms _ (new_type_names as name :: _) thy =
+ let
+ val info as {descr, ...} = Old_Datatype_Data.the_info thy name;
+ val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
+ val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
+ Old_Datatype_Aux.is_rec_type dt andalso
+ not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
+val _ = tracing ("NAME: " ^ @{make_string} (name, no_size))(*###*)
+ in
+ if no_size then thy
+ else
+ thy
+ |> Sign.add_path prefix
+ |> prove_size_thms info new_type_names
+ |> Sign.restore_naming thy
+ end;
+
+val _ = Theory.setup (Old_Datatype_Data.interpretation add_size_thms);
+
+end;