# HG changeset patch # User huffman # Date 1234976884 28800 # Node ID 3241eb2737b985b0ab381dd0abd6a7254c314be9 # Parent 28c5322f0df33a336fbfb8b07392eb3506961fa2# Parent f14ce13c73c18aa64c8fffc04674952cee408365 merged diff -r 28c5322f0df3 -r 3241eb2737b9 src/HOL/Finite_Set.thy diff -r 28c5322f0df3 -r 3241eb2737b9 src/HOL/Induct/Common_Patterns.thy --- a/src/HOL/Induct/Common_Patterns.thy Wed Feb 18 09:07:36 2009 -0800 +++ b/src/HOL/Induct/Common_Patterns.thy Wed Feb 18 09:08:04 2009 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Induct/Common_Patterns.thy - ID: $Id$ Author: Makarius *) diff -r 28c5322f0df3 -r 3241eb2737b9 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Feb 18 09:07:36 2009 -0800 +++ b/src/HOL/Int.thy Wed Feb 18 09:08:04 2009 -0800 @@ -1627,7 +1627,7 @@ context ring_1 begin -lemma of_int_of_nat: +lemma of_int_of_nat [nitpick_const_simp]: "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" proof (cases "k < 0") case True then have "0 \ - k" by simp diff -r 28c5322f0df3 -r 3241eb2737b9 src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Wed Feb 18 09:07:36 2009 -0800 +++ b/src/HOL/Library/Enum.thy Wed Feb 18 09:08:04 2009 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Library/Enum.thy - ID: $Id$ Author: Florian Haftmann, TU Muenchen *) diff -r 28c5322f0df3 -r 3241eb2737b9 src/HOL/NatBin.thy --- a/src/HOL/NatBin.thy Wed Feb 18 09:07:36 2009 -0800 +++ b/src/HOL/NatBin.thy Wed Feb 18 09:08:04 2009 -0800 @@ -362,9 +362,14 @@ unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp) lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})" -apply (induct "n") -apply (auto simp add: power_Suc power_add) -done +proof (induct n) + case 0 show ?case by simp +next + case (Suc n) then show ?case by (simp add: power_Suc power_add) +qed + +lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})" + by (simp add: power_Suc) lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2" by (subst mult_commute) (simp add: power_mult) diff -r 28c5322f0df3 -r 3241eb2737b9 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Wed Feb 18 09:07:36 2009 -0800 +++ b/src/HOL/SetInterval.thy Wed Feb 18 09:08:04 2009 -0800 @@ -66,10 +66,10 @@ "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) syntax (xsymbols) - "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10) - "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10) - "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10) - "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10) + "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) + "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) + "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) + "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) translations "UN i<=n. A" == "UN i:{..n}. A" @@ -946,4 +946,37 @@ show ?case by simp qed +subsection {* Products indexed over intervals *} + +syntax + "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) + "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) + "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10) + "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10) +syntax (xsymbols) + "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) + "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) + "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) + "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) +syntax (HTML output) + "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) + "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) + "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) + "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) +syntax (latex_prod output) + "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" + ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) + "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" + ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) + "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" + ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10) + "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" + ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10) + +translations + "\x=a..b. t" == "CONST setprod (%x. t) {a..b}" + "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}" + "\ii. t) {.. model -> arguments -> Term.term -> (interpretation * model * arguments) option *) + fun set_interpreter thy model args t = + let + val (typs, terms) = model + in + case AList.lookup (op =) terms t of + SOME intr => + (* return an existing interpretation *) + SOME (intr, model, args) + | NONE => + (case t of + (* 'Collect' == identity *) + Const (@{const_name Collect}, _) $ t1 => + SOME (interpret thy model args t1) + | Const (@{const_name Collect}, _) => + SOME (interpret thy model args (eta_expand t 1)) + (* 'op :' == application *) + | Const (@{const_name "op :"}, _) $ t1 $ t2 => + SOME (interpret thy model args (t2 $ t1)) + | Const (@{const_name "op :"}, _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const (@{const_name "op :"}, _) => + SOME (interpret thy model args (eta_expand t 2)) + | _ => NONE) + end; + + (* theory -> model -> arguments -> Term.term -> + (interpretation * model * arguments) option *) + (* only an optimization: 'card' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) @@ -3271,6 +3299,7 @@ add_interpreter "stlc" stlc_interpreter #> add_interpreter "Pure" Pure_interpreter #> add_interpreter "HOLogic" HOLogic_interpreter #> + add_interpreter "set" set_interpreter #> add_interpreter "IDT" IDT_interpreter #> add_interpreter "IDT_constructor" IDT_constructor_interpreter #> add_interpreter "IDT_recursion" IDT_recursion_interpreter #> diff -r 28c5322f0df3 -r 3241eb2737b9 src/Tools/code/code_funcgr.ML --- a/src/Tools/code/code_funcgr.ML Wed Feb 18 09:07:36 2009 -0800 +++ b/src/Tools/code/code_funcgr.ML Wed Feb 18 09:08:04 2009 -0800 @@ -1,8 +1,7 @@ (* Title: Tools/code/code_funcgr.ML - ID: $Id$ Author: Florian Haftmann, TU Muenchen -Retrieving, normalizing and structuring defining equations in graph +Retrieving, normalizing and structuring code equations in graph with explicit dependencies. *) diff -r 28c5322f0df3 -r 3241eb2737b9 src/Tools/code/code_funcgr_new.ML --- a/src/Tools/code/code_funcgr_new.ML Wed Feb 18 09:07:36 2009 -0800 +++ b/src/Tools/code/code_funcgr_new.ML Wed Feb 18 09:08:04 2009 -0800 @@ -1,9 +1,8 @@ (* Title: Tools/code/code_funcgr.ML - ID: $Id$ Author: Florian Haftmann, TU Muenchen -Retrieving, well-sorting and structuring defining equations in graph -with explicit dependencies. +Retrieving, well-sorting and structuring code equations in graph +with explicit dependencies -- the waisenhaus algorithm. *) signature CODE_FUNCGR = @@ -28,12 +27,8 @@ type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T; -fun eqns funcgr = - these o Option.map snd o try (Graph.get_node funcgr); - -fun typ funcgr = - fst o Graph.get_node funcgr; - +fun eqns funcgr = these o Option.map snd o try (Graph.get_node funcgr); +fun typ funcgr = fst o Graph.get_node funcgr; fun all funcgr = Graph.keys funcgr; fun pretty thy funcgr = @@ -48,23 +43,22 @@ |> Pretty.chunks; -(** generic combinators **) - -fun fold_consts f thms = - thms - |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of) - |> (fold o fold_aterms) (fn Const c => f c | _ => I); - -fun consts_of (const, []) = [] - | consts_of (const, thms as _ :: _) = - let - fun the_const (c, _) = if c = const then I else insert (op =) c - in fold_consts the_const (map fst thms) [] end; - - (** graph algorithm **) -(* some nonsense -- FIXME *) +(* generic *) + +fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); + +fun complete_proper_sort thy = + Sign.complete_sort thy #> filter (can (AxClass.get_info thy)); + +fun inst_params thy tyco class = + map (fn (c, _) => AxClass.param_of_inst thy (c, tyco)) + ((#params o AxClass.get_info thy) class); + +fun consts_of thy eqns = [] |> (fold o fold o fold_aterms) + (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) + (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); fun lhs_rhss_of thy c = let @@ -73,33 +67,9 @@ |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var); val (lhs, _) = case eqns of [] => Code.default_typscheme thy c | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm; - val rhss = fold_consts (fn (c, ty) => - insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty))) (map fst eqns) []; + val rhss = consts_of thy eqns; in (lhs, rhss) end; -fun inst_params thy tyco class = - map (fn (c, _) => AxClass.param_of_inst thy (c, tyco)) - ((#params o AxClass.get_info thy) class); - -fun complete_proper_sort thy sort = - Sign.complete_sort thy sort |> filter (can (AxClass.get_info thy)); - -fun minimal_proper_sort thy sort = - complete_proper_sort thy sort |> Sign.minimize_sort thy; - -fun dicts_of thy algebra (T, sort) = - let - fun class_relation (x, _) _ = x; - fun type_constructor tyco xs class = - inst_params thy tyco class @ (maps o maps) fst xs; - fun type_variable (TFree (_, sort)) = map (pair []) sort; - in - flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra - { class_relation = class_relation, type_constructor = type_constructor, - type_variable = type_variable } (T, minimal_proper_sort thy sort) - handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) - end; - (* data structures *) @@ -179,6 +149,7 @@ val classess = map (complete_proper_sort thy) (Sign.arity_sorts thy tyco [class]); val inst_params = inst_params thy tyco class; + (*FIXME also consider existing things here*) in vardeps |> fold (fn superclass => assert thy (Inst (superclass, tyco))) superclasses @@ -199,6 +170,7 @@ let val _ = tracing "add_const"; val (lhs, rhss) = lhs_rhss_of thy c; + (*FIXME build lhs_rhss_of such that it points to existing graph if possible*) fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys) | styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs); val rhss' = (map o apsnd o map) styp_of rhss; @@ -220,33 +192,62 @@ (* applying instantiations *) +fun dicts_of thy (proj_sort, algebra) (T, sort) = + let + fun class_relation (x, _) _ = x; + fun type_constructor tyco xs class = + inst_params thy tyco class @ (maps o maps) fst xs; + fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort); + in + flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra + { class_relation = class_relation, type_constructor = type_constructor, + type_variable = type_variable } (T, proj_sort sort) + handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) + end; + +fun instances_of (*FIXME move to sorts.ML*) algebra = + let + val { classes, arities } = Sorts.rep_algebra algebra; + val sort_classes = fn cs => filter (member (op = o apsnd fst) cs) + (flat (rev (Graph.strong_conn classes))); + in + Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs)) + arities [] + end; + fun algebra_of thy vardeps = let val pp = Syntax.pp_global thy; val thy_algebra = Sign.classes_of thy; val is_proper = can (AxClass.get_info thy); - val arities = Vargraph.fold (fn ((Fun _, _), _) => I + val classrels = Sorts.classrels_of thy_algebra + |> filter (is_proper o fst) + |> (map o apsnd) (filter is_proper); + val instances = instances_of thy_algebra + |> filter (is_proper o snd); + fun add_class (class, superclasses) algebra = + Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra; + val arity_constraints = Vargraph.fold (fn ((Fun _, _), _) => I | ((Inst (class, tyco), k), ((_, classes), _)) => AList.map_default (op =) ((tyco, class), replicate (Sign.arity_number thy tyco) []) (nth_map k (K classes))) vardeps []; - val classrels = Sorts.classrels_of thy_algebra - |> filter (is_proper o fst) - |> (map o apsnd) (filter is_proper); - fun add_arity (tyco, class) = case AList.lookup (op =) arities (tyco, class) - of SOME sorts => Sorts.add_arities pp (tyco, [(class, sorts)]) - | NONE => if Sign.arity_number thy tyco = 0 - then (tracing (tyco ^ "::" ^ class); Sorts.add_arities pp (tyco, [(class, [])])) - else I; - val instances = Sorts.instances_of thy_algebra - |> filter (is_proper o snd) + fun add_arity (tyco, class) algebra = + case AList.lookup (op =) arity_constraints (tyco, class) + of SOME sorts => (tracing (Pretty.output (Syntax.pretty_arity (ProofContext.init thy) + (tyco, sorts, [class]))); + Sorts.add_arities pp + (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra) + | NONE => if Sign.arity_number thy tyco = 0 + then Sorts.add_arities pp (tyco, [(class, [])]) algebra + else algebra; in Sorts.empty_algebra - |> fold (Sorts.add_class pp) classrels + |> fold add_class classrels |> fold add_arity instances end; -fun add_eqs thy algebra vardeps c gr = +fun add_eqs thy (proj_sort, algebra) vardeps c gr = let val eqns = Code.these_eqns thy c |> burrow_fst (Code_Unit.norm_args thy) @@ -260,28 +261,27 @@ val tyscm = case eqns' of [] => Code.default_typscheme thy c | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm; val _ = tracing ("tyscm " ^ makestring (map snd (fst tyscm))); - val rhss = fold_consts (fn (c, ty) => - insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty))) (map fst eqns') []; + val rhss = consts_of thy eqns'; in gr |> Graph.new_node (c, (tyscm, eqns')) - |> fold (fn (c', Ts) => ensure_eqs_dep thy algebra vardeps c c' + |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' #-> (fn (vs, _) => - fold2 (ensure_match thy algebra vardeps c) Ts (map snd vs))) rhss + fold2 (ensure_match thy (proj_sort, algebra) vardeps c) Ts (map snd vs))) rhss |> pair tyscm end -and ensure_match thy algebra vardeps c T sort gr = +and ensure_match thy (proj_sort, algebra) vardeps c T sort gr = gr - |> fold (fn c' => ensure_eqs_dep thy algebra vardeps c c' #> snd) - (dicts_of thy algebra (T, sort)) -and ensure_eqs_dep thy algebra vardeps c c' gr = + |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' #> snd) + (dicts_of thy (proj_sort, algebra) (T, proj_sort sort)) +and ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' gr = gr - |> ensure_eqs thy algebra vardeps c' + |> ensure_eqs thy (proj_sort, algebra) vardeps c' ||> Graph.add_edge (c, c') -and ensure_eqs thy algebra vardeps c gr = +and ensure_eqs thy (proj_sort, algebra) vardeps c gr = case try (Graph.get_node gr) c of SOME (tyscm, _) => (tyscm, gr) - | NONE => add_eqs thy algebra vardeps c gr; + | NONE => add_eqs thy (proj_sort, algebra) vardeps c gr; fun extend_graph thy cs gr = let @@ -291,13 +291,10 @@ val _ = tracing "obtaining algebra"; val algebra = algebra_of thy vardeps; val _ = tracing "obtaining equations"; - val (_, gr) = fold_map (ensure_eqs thy algebra vardeps) cs gr; + val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra; + val (_, gr') = fold_map (ensure_eqs thy (proj_sort, algebra) vardeps) cs gr; val _ = tracing "sort projection"; - val minimal_proper_sort = fn sort => sort - |> Sorts.complete_sort (Sign.classes_of thy) - |> filter (can (AxClass.get_info thy)) - |> Sorts.minimize_sort algebra; - in ((minimal_proper_sort, algebra), gr) end; + in ((proj_sort, algebra), gr') end; (** retrieval interfaces **) @@ -320,7 +317,7 @@ insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' []; val typ_matches = maps (fn (tys, c) => tys ~~ map snd (fst (fst (Graph.get_node funcgr' c)))) const_matches; - val dicts = maps (dicts_of thy (snd algebra')) typ_matches; + val dicts = maps (dicts_of thy algebra') typ_matches; val (algebra'', funcgr'') = extend_graph thy dicts funcgr'; in (evaluator_lift (evaluator_funcgr algebra'') thm funcgr'', funcgr'') end; diff -r 28c5322f0df3 -r 3241eb2737b9 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Wed Feb 18 09:07:36 2009 -0800 +++ b/src/Tools/code/code_thingol.ML Wed Feb 18 09:08:04 2009 -0800 @@ -109,7 +109,7 @@ let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; -(** language core - types, patterns, expressions **) +(** language core - types, terms **) type vname = string; @@ -131,31 +131,6 @@ | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; (*see also signature*) -(* - variable naming conventions - - bare names: - variable names v - class names class - type constructor names tyco - datatype names dtco - const names (general) c (const) - constructor names co - class parameter names classparam - arbitrary name s - - v, c, co, classparam also annotated with types etc. - - constructs: - sort sort - type parameters vs - type ty - type schemes tysm - term t - (term as pattern) p - instance (class, tyco) inst - *) - val op `$$ = Library.foldl (op `$); val op `|--> = Library.foldr (op `|->); @@ -543,16 +518,8 @@ Global ((class, tyco), yss) | class_relation (Local (classrels, v), subclass) superclass = Local ((subclass, superclass) :: classrels, v); - fun norm_typargs ys = - let - val raw_sort = map snd ys; - val sort = Sorts.minimize_sort algebra raw_sort; - in - map_filter (fn (y, class) => - if member (op =) sort class then SOME y else NONE) ys - end; fun type_constructor tyco yss class = - Global ((class, tyco), map norm_typargs yss); + Global ((class, tyco), (map o map) fst yss); fun type_variable (TFree (v, sort)) = let val sort' = proj_sort sort;