# HG changeset patch # User haftmann # Date 1270997496 -7200 # Node ID 853c777f29074c62ca7a7a5d4def25e6c48fff0b # Parent 03aa51cf85a2e659b29459baff231e324f3f45d0# Parent 7fa17a225852db0672ddf20474dc12bc38588fae merged diff -r 03aa51cf85a2 -r 853c777f2907 src/HOL/Library/AssocList.thy --- a/src/HOL/Library/AssocList.thy Sun Apr 11 15:42:05 2010 +0200 +++ b/src/HOL/Library/AssocList.thy Sun Apr 11 16:51:36 2010 +0200 @@ -659,49 +659,49 @@ subsection {* Implementation of mappings *} -definition AList :: "('a \ 'b) list \ ('a, 'b) mapping" where - "AList xs = Mapping (map_of xs)" +definition Mapping :: "('a \ 'b) list \ ('a, 'b) mapping" where + "Mapping xs = Mapping.Mapping (map_of xs)" -code_datatype AList +code_datatype Mapping -lemma lookup_AList [simp, code]: - "Mapping.lookup (AList xs) = map_of xs" - by (simp add: AList_def) +lemma lookup_Mapping [simp, code]: + "Mapping.lookup (Mapping xs) = map_of xs" + by (simp add: Mapping_def) -lemma empty_AList [code]: - "Mapping.empty = AList []" +lemma empty_Mapping [code]: + "Mapping.empty = Mapping []" by (rule mapping_eqI) simp -lemma is_empty_AList [code]: - "Mapping.is_empty (AList xs) \ null xs" +lemma is_empty_Mapping [code]: + "Mapping.is_empty (Mapping xs) \ null xs" by (cases xs) (simp_all add: is_empty_def) -lemma update_AList [code]: - "Mapping.update k v (AList xs) = AList (update k v xs)" +lemma update_Mapping [code]: + "Mapping.update k v (Mapping xs) = Mapping (update k v xs)" by (rule mapping_eqI) (simp add: update_conv') -lemma delete_AList [code]: - "Mapping.delete k (AList xs) = AList (delete k xs)" +lemma delete_Mapping [code]: + "Mapping.delete k (Mapping xs) = Mapping (delete k xs)" by (rule mapping_eqI) (simp add: delete_conv') -lemma keys_AList [code]: - "Mapping.keys (AList xs) = set (map fst xs)" +lemma keys_Mapping [code]: + "Mapping.keys (Mapping xs) = set (map fst xs)" by (simp add: keys_def dom_map_of_conv_image_fst) -lemma ordered_keys_AList [code]: - "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))" - by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups) +lemma ordered_keys_Mapping [code]: + "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))" + by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) -lemma size_AList [code]: - "Mapping.size (AList xs) = length (remdups (map fst xs))" +lemma size_Mapping [code]: + "Mapping.size (Mapping xs) = length (remdups (map fst xs))" by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst) -lemma tabulate_AList [code]: - "Mapping.tabulate ks f = AList (map (\k. (k, f k)) ks)" +lemma tabulate_Mapping [code]: + "Mapping.tabulate ks f = Mapping (map (\k. (k, f k)) ks)" by (rule mapping_eqI) (simp add: map_of_map_restrict) -lemma bulkload_AList [code]: - "Mapping.bulkload vs = AList (map (\n. (n, vs ! n)) [0..n. (n, vs ! n)) [0.. ?dlist" by simp qed + text {* Formal, totalized constructor for @{typ "'a dlist"}: *} definition Dlist :: "'a list \ 'a dlist" where @@ -60,7 +61,7 @@ "list_of_dlist (Dlist xs) = remdups xs" by (simp add: Dlist_def Abs_dlist_inverse) -lemma Dlist_list_of_dlist [simp]: +lemma Dlist_list_of_dlist [simp, code abstype]: "Dlist (list_of_dlist dxs) = dxs" by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id) @@ -100,9 +101,6 @@ section {* Executable version obeying invariant *} -code_abstype Dlist list_of_dlist - by simp - lemma list_of_dlist_empty [simp, code abstract]: "list_of_dlist empty = []" by (simp add: empty_def) diff -r 03aa51cf85a2 -r 853c777f2907 src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Sun Apr 11 15:42:05 2010 +0200 +++ b/src/HOL/Library/Mapping.thy Sun Apr 11 16:51:36 2010 +0200 @@ -122,6 +122,10 @@ "bulkload xs = tabulate [0.. m = Mapping Map.empty" + by (cases m) (simp add: is_empty_def) + subsection {* Some technical code lemmas *} diff -r 03aa51cf85a2 -r 853c777f2907 src/HOL/Library/Table.thy --- a/src/HOL/Library/Table.thy Sun Apr 11 15:42:05 2010 +0200 +++ b/src/HOL/Library/Table.thy Sun Apr 11 16:51:36 2010 +0200 @@ -3,7 +3,7 @@ header {* Tables: finite mappings implemented by red-black trees *} theory Table -imports Main RBT +imports Main RBT Mapping begin subsection {* Type definition *} @@ -23,7 +23,8 @@ "t1 = t2 \ tree_of t1 = tree_of t2" by (simp add: tree_of_inject) -code_abstype Table tree_of +lemma [code abstype]: + "Table (tree_of t) = t" by (simp add: tree_of_inverse) @@ -56,6 +57,9 @@ definition entries :: "('a\linorder, 'b) table \ ('a \ 'b) list" where [code]: "entries t = RBT.entries (tree_of t)" +definition keys :: "('a\linorder, 'b) table \ 'a list" where + [code]: "keys t = RBT.keys (tree_of t)" + definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) table" where "bulkload xs = Table (RBT.bulkload xs)" @@ -101,6 +105,10 @@ "RBT.entries (tree_of t) = entries t" by (simp add: entries_def) +lemma keys_tree_of: + "RBT.keys (tree_of t) = keys t" + by (simp add: keys_def) + lemma lookup_empty [simp]: "lookup empty = Map.empty" by (simp add: empty_def lookup_Table expand_fun_eq) @@ -111,15 +119,19 @@ lemma lookup_delete [simp]: "lookup (delete k t) = (lookup t)(k := None)" - by (simp add: delete_def lookup_Table lookup_delete lookup_tree_of restrict_complement_singleton_eq) + by (simp add: delete_def lookup_Table RBT.lookup_delete lookup_tree_of restrict_complement_singleton_eq) lemma map_of_entries [simp]: "map_of (entries t) = lookup t" by (simp add: entries_def map_of_entries lookup_tree_of) +lemma entries_lookup: + "entries t1 = entries t2 \ lookup t1 = lookup t2" + by (simp add: entries_def lookup_def entries_lookup) + lemma lookup_bulkload [simp]: "lookup (bulkload xs) = map_of xs" - by (simp add: bulkload_def lookup_Table lookup_bulkload) + by (simp add: bulkload_def lookup_Table RBT.lookup_bulkload) lemma lookup_map_entry [simp]: "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))" @@ -133,7 +145,85 @@ "fold f t = (\s. foldl (\s (k, v). f k v s) s (entries t))" by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of) +lemma is_empty_empty [simp]: + "is_empty t \ t = empty" + by (simp add: table_eq is_empty_def tree_of_empty split: rbt.split) + +lemma RBT_lookup_empty [simp]: (*FIXME*) + "RBT.lookup t = Map.empty \ t = RBT.Empty" + by (cases t) (auto simp add: expand_fun_eq) + +lemma lookup_empty_empty [simp]: + "lookup t = Map.empty \ t = empty" + by (cases t) (simp add: empty_def lookup_def Table_inject Table_inverse) + +lemma sorted_keys [iff]: + "sorted (keys t)" + by (simp add: keys_def RBT.keys_def sorted_entries) + +lemma distinct_keys [iff]: + "distinct (keys t)" + by (simp add: keys_def RBT.keys_def distinct_entries) + + +subsection {* Implementation of mappings *} + +definition Mapping :: "('a\linorder, 'b) table \ ('a, 'b) mapping" where + "Mapping t = Mapping.Mapping (lookup t)" + +code_datatype Mapping + +lemma lookup_Mapping [simp, code]: + "Mapping.lookup (Mapping t) = lookup t" + by (simp add: Mapping_def) + +lemma empty_Mapping [code]: + "Mapping.empty = Mapping empty" + by (rule mapping_eqI) simp + +lemma is_empty_Mapping [code]: + "Mapping.is_empty (Mapping t) \ is_empty t" + by (simp add: table_eq Mapping.is_empty_empty Mapping_def) + +lemma update_Mapping [code]: + "Mapping.update k v (Mapping t) = Mapping (update k v t)" + by (rule mapping_eqI) simp + +lemma delete_Mapping [code]: + "Mapping.delete k (Mapping xs) = Mapping (delete k xs)" + by (rule mapping_eqI) simp + +lemma keys_Mapping [code]: + "Mapping.keys (Mapping t) = set (keys t)" + by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys) + +lemma ordered_keys_Mapping [code]: + "Mapping.ordered_keys (Mapping t) = keys t" + by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping) + +lemma Mapping_size_card_keys: (*FIXME*) + "Mapping.size m = card (Mapping.keys m)" + by (simp add: Mapping.size_def Mapping.keys_def) + +lemma size_Mapping [code]: + "Mapping.size (Mapping t) = length (keys t)" + by (simp add: Mapping_size_card_keys keys_Mapping distinct_card) + +lemma tabulate_Mapping [code]: + "Mapping.tabulate ks f = Mapping (bulkload (List.map (\k. (k, f k)) ks))" + by (rule mapping_eqI) (simp add: map_of_map_restrict) + +lemma bulkload_Mapping [code]: + "Mapping.bulkload vs = Mapping (bulkload (List.map (\n. (n, vs ! n)) [0.. x = y" by (fact eq_equals) (*FIXME*) + +lemma eq_Mapping [code]: + "HOL.eq (Mapping t1) (Mapping t2) \ entries t1 = entries t2" + by (simp add: eq Mapping_def entries_lookup) + hide (open) const tree_of lookup empty update delete - entries bulkload map_entry map fold + entries keys bulkload map_entry map fold end diff -r 03aa51cf85a2 -r 853c777f2907 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Sun Apr 11 15:42:05 2010 +0200 +++ b/src/HOL/Rat.thy Sun Apr 11 16:51:36 2010 +0200 @@ -1019,11 +1019,9 @@ definition Frct :: "int \ int \ rat" where [simp]: "Frct p = Fract (fst p) (snd p)" -code_abstype Frct quotient_of -proof (rule eq_reflection) - fix r :: rat - show "Frct (quotient_of r) = r" by (cases r) (auto intro: quotient_of_eq) -qed +lemma [code abstype]: + "Frct (quotient_of q) = q" + by (cases q) (auto intro: quotient_of_eq) lemma Frct_code_post [code_post]: "Frct (0, k) = 0" diff -r 03aa51cf85a2 -r 853c777f2907 src/HOL/ex/Execute_Choice.thy --- a/src/HOL/ex/Execute_Choice.thy Sun Apr 11 15:42:05 2010 +0200 +++ b/src/HOL/ex/Execute_Choice.thy Sun Apr 11 16:51:36 2010 +0200 @@ -58,15 +58,15 @@ text {* Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable; - first, we formally insert the constructor @{term AList} and split the one equation into two, + first, we formally insert the constructor @{term Mapping} and split the one equation into two, where the second one provides the necessary context: *} -lemma valuesum_rec_AList: - shows [code]: "valuesum (AList []) = 0" - and "valuesum (AList (x # xs)) = (let l = (SOME l. l \ Mapping.keys (AList (x # xs))) in - the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))" - by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList) +lemma valuesum_rec_Mapping: + shows [code]: "valuesum (Mapping []) = 0" + and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \ Mapping.keys (Mapping (x # xs))) in + the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))" + by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping) text {* As a side effect the precondition disappears (but note this has nothing to do with choice!). @@ -76,27 +76,27 @@ *} lemma valuesum_rec_exec [code]: - "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in - the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))" + "valuesum (Mapping (x # xs)) = (let l = fst (hd (x # xs)) in + the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))" proof - - let ?M = "AList (x # xs)" + let ?M = "Mapping (x # xs)" let ?l1 = "(SOME l. l \ Mapping.keys ?M)" let ?l2 = "fst (hd (x # xs))" - have "finite (Mapping.keys ?M)" by (simp add: keys_AList) + have "finite (Mapping.keys ?M)" by (simp add: keys_Mapping) moreover have "?l1 \ Mapping.keys ?M" - by (rule someI) (auto simp add: keys_AList) + by (rule someI) (auto simp add: keys_Mapping) moreover have "?l2 \ Mapping.keys ?M" - by (simp add: keys_AList) + by (simp add: keys_Mapping) ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) = the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)" by (rule valuesum_choice) - then show ?thesis by (simp add: valuesum_rec_AList) + then show ?thesis by (simp add: valuesum_rec_Mapping) qed text {* See how it works: *} -value "valuesum (AList [(''abc'', (42::int)), (''def'', 1705)])" +value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])" end diff -r 03aa51cf85a2 -r 853c777f2907 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sun Apr 11 15:42:05 2010 +0200 +++ b/src/Pure/Isar/code.ML Sun Apr 11 16:51:36 2010 +0200 @@ -22,8 +22,6 @@ (*constructor sets*) val constrset_of_consts: theory -> (string * typ) list -> string * ((string * sort) list * (string * typ list) list) - val abstype_cert: theory -> string * typ -> string - -> string * ((string * sort) list * ((string * typ) * (string * term))) (*code equations and certificates*) val mk_eqn: theory -> thm * bool -> thm * bool @@ -52,8 +50,7 @@ val datatype_interpretation: (string * ((string * sort) list * (string * typ list) list) -> theory -> theory) -> theory -> theory - val add_abstype: string * typ -> string * typ -> theory -> Proof.state - val add_abstype_cmd: string -> string -> theory -> Proof.state + val add_abstype: thm -> theory -> theory val abstype_interpretation: (string * ((string * sort) list * ((string * typ) * (string * thm))) -> theory -> theory) -> theory -> theory @@ -380,6 +377,7 @@ val tfrees = Term.add_tfreesT ty []; val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty handle TYPE _ => no_constr thy "bad type" c_ty + val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else (); val _ = if has_duplicates (eq_fst (op =)) vs then no_constr thy "duplicate type variables in datatype" c_ty else (); val _ = if length tfrees <> length vs @@ -411,22 +409,6 @@ val cs''' = map (inst vs) cs''; in (tyco, (vs, rev cs''')) end; -fun abstype_cert thy abs_ty rep = - let - val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c - then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (fst abs_ty, rep); - val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy abs_ty; - val (ty, ty_abs) = case ty' - of Type ("fun", [ty, ty_abs]) => (ty, ty_abs) - | _ => error ("Not a datatype abstractor:\n" ^ string_of_const thy abs - ^ " :: " ^ string_of_typ thy ty'); - val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle TYPE _ => - error ("Not a projection:\n" ^ string_of_const thy rep); - val param = Free ("x", ty_abs); - val cert = Logic.all param (Logic.mk_equals - (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty) $ param), param)); - in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end; - fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco) of (_, entry) :: _ => SOME entry | _ => NONE; @@ -657,6 +639,29 @@ fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); +(* abstype certificates *) + +fun check_abstype_cert thy proto_thm = + let + val thm = meta_rewrite thy proto_thm; + fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm); + val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm) + handle TERM _ => bad "Not an equation" + | THM _ => bad "Not a proper equation"; + val ((abs, raw_ty), ((rep, _), param)) = (apsnd (apfst dest_Const o dest_comb) + o apfst dest_Const o dest_comb) lhs + handle TERM _ => bad "Not an abstype certificate"; + val var = (fst o dest_Var) param + handle TERM _ => bad "Not an abstype certificate"; + val _ = if param = rhs then () else bad "Not an abstype certificate"; + val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c + then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); + val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty); + val ty = domain_type ty'; + val ty_abs = range_type ty'; + in (tyco, (vs ~~ sorts, ((abs, ty), (rep, thm)))) end; + + (* code equation certificates *) fun build_head thy (c, ty) = @@ -1152,25 +1157,19 @@ fun abstype_interpretation f = Abstype_Interpretation.interpretation (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy); -fun add_abstype proto_abs proto_rep thy = +fun add_abstype proto_thm thy = let - val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep); - val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep); - fun after_qed [[cert]] = ProofContext.theory - (del_eqns abs - #> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert)))) - #> change_fun_spec false rep ((K o Proj) - (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco)) - #> Abstype_Interpretation.data (tyco, serial ())); + val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) = + check_abstype_cert thy proto_thm; in thy - |> ProofContext.init - |> Proof.theorem_i NONE after_qed [[(cert_prop, [])]] + |> del_eqns abs + |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert)))) + |> change_fun_spec false rep ((K o Proj) + (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco)) + |> Abstype_Interpretation.data (tyco, serial ()) end; -fun add_abstype_cmd raw_abs raw_rep thy = - add_abstype (read_bare_const thy raw_abs) (read_bare_const thy raw_rep) thy; - (** infrastructure **) @@ -1200,6 +1199,7 @@ val code_attribute_parser = Args.del |-- Scan.succeed (mk_attribute del_eqn) || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn) + || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype) || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn) || (Args.$$$ "target" |-- Args.colon |-- Args.name >> (mk_attribute o code_target_attr)) diff -r 03aa51cf85a2 -r 853c777f2907 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sun Apr 11 15:42:05 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sun Apr 11 16:51:36 2010 +0200 @@ -480,11 +480,6 @@ OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); -val _ = - OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal - (P.term -- P.term >> (fn (abs, rep) => Toplevel.print - o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep))); - (** proof commands **)