--- 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
*)
--- 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 \<le> - k" by simp
--- 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
*)
--- 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)
--- 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\<Inter> _<_./ _)" 10)
syntax (xsymbols)
- "@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
- "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
- "@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
- "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
+ "@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10)
+ "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10)
+ "@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10)
+ "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(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 \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
+ "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
+ "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
+ "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
+syntax (xsymbols)
+ "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
+ "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
+ "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
+ "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+syntax (HTML output)
+ "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
+ "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
+ "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
+ "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+syntax (latex_prod output)
+ "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
+ "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
+ "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
+ "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
+
+translations
+ "\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}"
+ "\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}"
+ "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
+ "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
+
end
--- a/src/HOL/Tools/refute.ML Wed Feb 18 09:07:36 2009 -0800
+++ b/src/HOL/Tools/refute.ML Wed Feb 18 09:08:04 2009 -0800
@@ -2662,6 +2662,34 @@
(* theory -> 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 #>
--- 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.
*)
--- 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;
--- 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;