--- a/src/CCL/Term.thy Wed Aug 17 18:51:27 2011 +0200
+++ b/src/CCL/Term.thy Wed Aug 17 18:52:21 2011 +0200
@@ -58,18 +58,18 @@
(* FIXME does not handle "_idtdummy" *)
(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
-fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
+fun let_tr [Free x, a, b] = Const(@{const_syntax let},dummyT) $ a $ absfree x b;
fun let_tr' [a,Abs(id,T,b)] =
let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
-fun letrec_tr [Free(f,S),Free(x,T),a,b] =
- Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
-fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
- Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
-fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
- Const(@{const_syntax letrec3},dummyT) $
- absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
+fun letrec_tr [Free f, Free x, a, b] =
+ Const(@{const_syntax letrec}, dummyT) $ absfree x (absfree f a) $ absfree f b;
+fun letrec2_tr [Free f, Free x, Free y, a, b] =
+ Const(@{const_syntax letrec2}, dummyT) $ absfree x (absfree y (absfree f a)) $ absfree f b;
+fun letrec3_tr [Free f, Free x, Free y, Free z, a, b] =
+ Const(@{const_syntax letrec3}, dummyT) $
+ absfree x (absfree y (absfree z (absfree f a))) $ absfree f b;
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
--- a/src/FOL/fologic.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/FOL/fologic.ML Wed Aug 17 18:52:21 2011 +0200
@@ -76,10 +76,10 @@
| dest_eq t = raise TERM ("dest_eq", [t])
fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
-fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
+fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
-fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
+fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
(* binary oprations and relations *)
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Wed Aug 17 18:52:21 2011 +0200
@@ -393,7 +393,7 @@
quant "forall" HOLogic.all_const ||
quant "exists" HOLogic.exists_const ||
scan_fail "illegal quantifier kind"
- fun mk_quant q (n, T) t = q T $ Term.absfree (n, T, t)
+ fun mk_quant q (x, T) t = q T $ absfree (x, T) t
val patternT = @{typ "SMT.pattern"}
fun mk_pattern _ [] = raise TERM ("mk_pattern", [])
--- a/src/HOL/HOLCF/Tools/cpodef.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Wed Aug 17 18:52:21 2011 +0200
@@ -54,7 +54,7 @@
(* building terms *)
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT)
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P)
+fun mk_adm (x, T, P) = adm_const T $ absfree (x, T) P
fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT)
--- a/src/HOL/Hoare/Separation.thy Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Hoare/Separation.thy Wed Aug 17 18:52:21 2011 +0200
@@ -68,11 +68,11 @@
fun singl_tr [p, q] = Syntax.const @{const_syntax singl} $ Syntax.free "H" $ p $ q
| singl_tr ts = raise TERM ("singl_tr", ts);
fun star_tr [P,Q] = Syntax.const @{const_syntax star} $
- absfree ("H", dummyT, free_tr P) $ absfree ("H", dummyT, free_tr Q) $
+ absfree ("H", dummyT) (free_tr P) $ absfree ("H", dummyT) (free_tr Q) $
Syntax.free "H"
| star_tr ts = raise TERM ("star_tr", ts);
fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} $
- absfree ("H", dummyT, P) $ absfree ("H", dummyT, Q) $ Syntax.free "H"
+ absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H"
| wand_tr ts = raise TERM ("wand_tr", ts);
*}
--- a/src/HOL/Hoare/hoare_tac.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Wed Aug 17 18:52:21 2011 +0200
@@ -28,17 +28,21 @@
(** abstraction of body over a tuple formed from a list of free variables.
Types are also built **)
-fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT, body)
- | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
- in if w=[] then absfree (n, T, body)
- else let val z = mk_abstupleC w body;
- val T2 = case z of Abs(_,T,_) => T
- | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
- in
+fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT) body
+ | mk_abstupleC [v] body = absfree (dest_Free v) body
+ | mk_abstupleC (v :: w) body =
+ let
+ val (x, T) = dest_Free v;
+ val z = mk_abstupleC w body;
+ val T2 =
+ (case z of
+ Abs (_, T, _) => T
+ | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
+ in
Const (@{const_name prod_case},
- (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T,T2) --> HOLogic.boolT)
- $ absfree (n, T, z)
- end end;
+ (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
+ absfree (x, T) z
+ end;
(** maps [x1,...,xn] to (x1,...,xn) and types**)
fun mk_bodyC [] = HOLogic.unit
--- a/src/HOL/IsaMakefile Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 17 18:52:21 2011 +0200
@@ -437,39 +437,35 @@
Library/Code_Char_ord.thy Library/Code_Integer.thy \
Library/Code_Natural.thy Library/Code_Prolog.thy \
Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \
- Library/Cset.thy Library/Cset_Monad.thy \
- Library/Continuity.thy Library/Convex.thy Library/Countable.thy \
- Library/Diagonalize.thy Library/Dlist.thy Library/Dlist_Cset.thy \
- Library/Efficient_Nat.thy Library/Eval_Witness.thy \
- Library/Executable_Set.thy Library/Extended_Real.thy \
- Library/Extended_Nat.thy Library/Float.thy \
+ Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \
+ Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy \
+ Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy \
+ Library/Eval_Witness.thy Library/Executable_Set.thy \
+ Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \
- Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy \
- Library/Glbs.thy Library/Indicator_Function.thy \
- Library/Infinite_Set.thy Library/Inner_Product.thy \
- Library/Kleene_Algebra.thy Library/LaTeXsugar.thy \
- Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
- Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy \
- Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \
- Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \
- Library/Nat_Bijection.thy Library/Nested_Environment.thy \
- Library/Numeral_Type.thy Library/Old_Recdef.thy \
- Library/OptionalSugar.thy \
- Library/Order_Relation.thy Library/Permutation.thy \
- Library/Permutations.thy Library/Poly_Deriv.thy \
- Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \
- Library/Preorder.thy Library/Product_Vector.thy \
- Library/Product_ord.thy Library/Product_plus.thy \
- Library/Product_Lattice.thy \
- Library/Quickcheck_Types.thy \
- Library/Quotient_List.thy Library/Quotient_Option.thy \
- Library/Quotient_Product.thy Library/Quotient_Sum.thy \
- Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
- Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy \
- Library/README.html \
- Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
- Library/Reflection.thy \
+ Library/Function_Algebras.thy \
+ Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \
+ Library/Indicator_Function.thy Library/Infinite_Set.thy \
+ Library/Inner_Product.thy Library/Kleene_Algebra.thy \
+ Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
+ Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy \
+ Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
+ Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
+ Library/Multiset.thy Library/Nat_Bijection.thy \
+ Library/Numeral_Type.thy Library/Old_Recdef.thy \
+ Library/OptionalSugar.thy Library/Order_Relation.thy \
+ Library/Permutation.thy Library/Permutations.thy \
+ Library/Poly_Deriv.thy Library/Polynomial.thy \
+ Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy \
+ Library/Product_Vector.thy Library/Product_ord.thy \
+ Library/Product_plus.thy Library/Product_Lattice.thy \
+ Library/Quickcheck_Types.thy Library/Quotient_List.thy \
+ Library/Quotient_Option.thy Library/Quotient_Product.thy \
+ Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \
+ Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy \
+ Library/RBT_Mapping.thy Library/README.html Library/Set_Algebras.thy \
+ Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy \
Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
Library/Sum_of_Squares/sos_wrapper.ML \
Library/Sum_of_Squares/sum_of_squares.ML \
@@ -830,9 +826,9 @@
HOL-Unix: HOL $(LOG)/HOL-Unix.gz
-$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
- Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
- Unix/document/root.bib Unix/document/root.tex
+$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML \
+ Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib \
+ Unix/document/root.tex
@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
--- a/src/HOL/Library/Library.thy Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Library/Library.thy Wed Aug 17 18:52:21 2011 +0200
@@ -37,7 +37,6 @@
Monad_Syntax
More_List
Multiset
- Nested_Environment
Numeral_Type
Old_Recdef
OptionalSugar
--- a/src/HOL/Library/Nested_Environment.thy Wed Aug 17 18:51:27 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,571 +0,0 @@
-(* Title: HOL/Library/Nested_Environment.thy
- Author: Markus Wenzel, TU Muenchen
-*)
-
-header {* Nested environments *}
-
-theory Nested_Environment
-imports Main
-begin
-
-text {*
- Consider a partial function @{term [source] "e :: 'a => 'b option"};
- this may be understood as an \emph{environment} mapping indexes
- @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
- @{text Map} of Isabelle/HOL). This basic idea is easily generalized
- to that of a \emph{nested environment}, where entries may be either
- basic values or again proper environments. Then each entry is
- accessed by a \emph{path}, i.e.\ a list of indexes leading to its
- position within the structure.
-*}
-
-datatype ('a, 'b, 'c) env =
- Val 'a
- | Env 'b "'c => ('a, 'b, 'c) env option"
-
-text {*
- \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
- 'a} refers to basic values (occurring in terminal positions), type
- @{typ 'b} to values associated with proper (inner) environments, and
- type @{typ 'c} with the index type for branching. Note that there
- is no restriction on any of these types. In particular, arbitrary
- branching may yield rather large (transfinite) tree structures.
-*}
-
-
-subsection {* The lookup operation *}
-
-text {*
- Lookup in nested environments works by following a given path of
- index elements, leading to an optional result (a terminal value or
- nested environment). A \emph{defined position} within a nested
- environment is one where @{term lookup} at its path does not yield
- @{term None}.
-*}
-
-primrec
- lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
- and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
- "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
- | "lookup (Env b es) xs =
- (case xs of
- [] => Some (Env b es)
- | y # ys => lookup_option (es y) ys)"
- | "lookup_option None xs = None"
- | "lookup_option (Some e) xs = lookup e xs"
-
-hide_const lookup_option
-
-text {*
- \medskip The characteristic cases of @{term lookup} are expressed by
- the following equalities.
-*}
-
-theorem lookup_nil: "lookup e [] = Some e"
- by (cases e) simp_all
-
-theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"
- by simp
-
-theorem lookup_env_cons:
- "lookup (Env b es) (x # xs) =
- (case es x of
- None => None
- | Some e => lookup e xs)"
- by (cases "es x") simp_all
-
-lemmas lookup_lookup_option.simps [simp del]
- and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
-
-theorem lookup_eq:
- "lookup env xs =
- (case xs of
- [] => Some env
- | x # xs =>
- (case env of
- Val a => None
- | Env b es =>
- (case es x of
- None => None
- | Some e => lookup e xs)))"
- by (simp split: list.split env.split)
-
-text {*
- \medskip Displaced @{term lookup} operations, relative to a certain
- base path prefix, may be reduced as follows. There are two cases,
- depending whether the environment actually extends far enough to
- follow the base path.
-*}
-
-theorem lookup_append_none:
- assumes "lookup env xs = None"
- shows "lookup env (xs @ ys) = None"
- using assms
-proof (induct xs arbitrary: env)
- case Nil
- then have False by simp
- then show ?case ..
-next
- case (Cons x xs)
- show ?case
- proof (cases env)
- case Val
- then show ?thesis by simp
- next
- case (Env b es)
- show ?thesis
- proof (cases "es x")
- case None
- with Env show ?thesis by simp
- next
- case (Some e)
- note es = `es x = Some e`
- show ?thesis
- proof (cases "lookup e xs")
- case None
- then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)
- with Env Some show ?thesis by simp
- next
- case Some
- with Env es have False using Cons.prems by simp
- then show ?thesis ..
- qed
- qed
- qed
-qed
-
-theorem lookup_append_some:
- assumes "lookup env xs = Some e"
- shows "lookup env (xs @ ys) = lookup e ys"
- using assms
-proof (induct xs arbitrary: env e)
- case Nil
- then have "env = e" by simp
- then show "lookup env ([] @ ys) = lookup e ys" by simp
-next
- case (Cons x xs)
- note asm = `lookup env (x # xs) = Some e`
- show "lookup env ((x # xs) @ ys) = lookup e ys"
- proof (cases env)
- case (Val a)
- with asm have False by simp
- then show ?thesis ..
- next
- case (Env b es)
- show ?thesis
- proof (cases "es x")
- case None
- with asm Env have False by simp
- then show ?thesis ..
- next
- case (Some e')
- note es = `es x = Some e'`
- show ?thesis
- proof (cases "lookup e' xs")
- case None
- with asm Env es have False by simp
- then show ?thesis ..
- next
- case Some
- with asm Env es have "lookup e' xs = Some e"
- by simp
- then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)
- with Env es show ?thesis by simp
- qed
- qed
- qed
-qed
-
-text {*
- \medskip Successful @{term lookup} deeper down an environment
- structure means we are able to peek further up as well. Note that
- this is basically just the contrapositive statement of @{thm
- [source] lookup_append_none} above.
-*}
-
-theorem lookup_some_append:
- assumes "lookup env (xs @ ys) = Some e"
- shows "\<exists>e. lookup env xs = Some e"
-proof -
- from assms have "lookup env (xs @ ys) \<noteq> None" by simp
- then have "lookup env xs \<noteq> None"
- by (rule contrapos_nn) (simp only: lookup_append_none)
- then show ?thesis by (simp)
-qed
-
-text {*
- The subsequent statement describes in more detail how a successful
- @{term lookup} with a non-empty path results in a certain situation
- at any upper position.
-*}
-
-theorem lookup_some_upper:
- assumes "lookup env (xs @ y # ys) = Some e"
- shows "\<exists>b' es' env'.
- lookup env xs = Some (Env b' es') \<and>
- es' y = Some env' \<and>
- lookup env' ys = Some e"
- using assms
-proof (induct xs arbitrary: env e)
- case Nil
- from Nil.prems have "lookup env (y # ys) = Some e"
- by simp
- then obtain b' es' env' where
- env: "env = Env b' es'" and
- es': "es' y = Some env'" and
- look': "lookup env' ys = Some e"
- by (auto simp add: lookup_eq split: option.splits env.splits)
- from env have "lookup env [] = Some (Env b' es')" by simp
- with es' look' show ?case by blast
-next
- case (Cons x xs)
- from Cons.prems
- obtain b' es' env' where
- env: "env = Env b' es'" and
- es': "es' x = Some env'" and
- look': "lookup env' (xs @ y # ys) = Some e"
- by (auto simp add: lookup_eq split: option.splits env.splits)
- from Cons.hyps [OF look'] obtain b'' es'' env'' where
- upper': "lookup env' xs = Some (Env b'' es'')" and
- es'': "es'' y = Some env''" and
- look'': "lookup env'' ys = Some e"
- by blast
- from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
- by simp
- with es'' look'' show ?case by blast
-qed
-
-
-subsection {* The update operation *}
-
-text {*
- Update at a certain position in a nested environment may either
- delete an existing entry, or overwrite an existing one. Note that
- update at undefined positions is simple absorbed, i.e.\ the
- environment is left unchanged.
-*}
-
-primrec
- update :: "'c list => ('a, 'b, 'c) env option
- => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
- and update_option :: "'c list => ('a, 'b, 'c) env option
- => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
- "update xs opt (Val a) =
- (if xs = [] then (case opt of None => Val a | Some e => e)
- else Val a)"
- | "update xs opt (Env b es) =
- (case xs of
- [] => (case opt of None => Env b es | Some e => e)
- | y # ys => Env b (es (y := update_option ys opt (es y))))"
- | "update_option xs opt None =
- (if xs = [] then opt else None)"
- | "update_option xs opt (Some e) =
- (if xs = [] then opt else Some (update xs opt e))"
-
-hide_const update_option
-
-text {*
- \medskip The characteristic cases of @{term update} are expressed by
- the following equalities.
-*}
-
-theorem update_nil_none: "update [] None env = env"
- by (cases env) simp_all
-
-theorem update_nil_some: "update [] (Some e) env = e"
- by (cases env) simp_all
-
-theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"
- by simp
-
-theorem update_cons_nil_env:
- "update [x] opt (Env b es) = Env b (es (x := opt))"
- by (cases "es x") simp_all
-
-theorem update_cons_cons_env:
- "update (x # y # ys) opt (Env b es) =
- Env b (es (x :=
- (case es x of
- None => None
- | Some e => Some (update (y # ys) opt e))))"
- by (cases "es x") simp_all
-
-lemmas update_update_option.simps [simp del]
- and update_simps [simp] = update_nil_none update_nil_some
- update_cons_val update_cons_nil_env update_cons_cons_env
-
-lemma update_eq:
- "update xs opt env =
- (case xs of
- [] =>
- (case opt of
- None => env
- | Some e => e)
- | x # xs =>
- (case env of
- Val a => Val a
- | Env b es =>
- (case xs of
- [] => Env b (es (x := opt))
- | y # ys =>
- Env b (es (x :=
- (case es x of
- None => None
- | Some e => Some (update (y # ys) opt e)))))))"
- by (simp split: list.split env.split option.split)
-
-text {*
- \medskip The most basic correspondence of @{term lookup} and @{term
- update} states that after @{term update} at a defined position,
- subsequent @{term lookup} operations would yield the new value.
-*}
-
-theorem lookup_update_some:
- assumes "lookup env xs = Some e"
- shows "lookup (update xs (Some env') env) xs = Some env'"
- using assms
-proof (induct xs arbitrary: env e)
- case Nil
- then have "env = e" by simp
- then show ?case by simp
-next
- case (Cons x xs)
- note hyp = Cons.hyps
- and asm = `lookup env (x # xs) = Some e`
- show ?case
- proof (cases env)
- case (Val a)
- with asm have False by simp
- then show ?thesis ..
- next
- case (Env b es)
- show ?thesis
- proof (cases "es x")
- case None
- with asm Env have False by simp
- then show ?thesis ..
- next
- case (Some e')
- note es = `es x = Some e'`
- show ?thesis
- proof (cases xs)
- case Nil
- with Env show ?thesis by simp
- next
- case (Cons x' xs')
- from asm Env es have "lookup e' xs = Some e" by simp
- then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
- with Env es Cons show ?thesis by simp
- qed
- qed
- qed
-qed
-
-text {*
- \medskip The properties of displaced @{term update} operations are
- analogous to those of @{term lookup} above. There are two cases:
- below an undefined position @{term update} is absorbed altogether,
- and below a defined positions @{term update} affects subsequent
- @{term lookup} operations in the obvious way.
-*}
-
-theorem update_append_none:
- assumes "lookup env xs = None"
- shows "update (xs @ y # ys) opt env = env"
- using assms
-proof (induct xs arbitrary: env)
- case Nil
- then have False by simp
- then show ?case ..
-next
- case (Cons x xs)
- note hyp = Cons.hyps
- and asm = `lookup env (x # xs) = None`
- show "update ((x # xs) @ y # ys) opt env = env"
- proof (cases env)
- case (Val a)
- then show ?thesis by simp
- next
- case (Env b es)
- show ?thesis
- proof (cases "es x")
- case None
- note es = `es x = None`
- show ?thesis
- by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
- next
- case (Some e)
- note es = `es x = Some e`
- show ?thesis
- proof (cases xs)
- case Nil
- with asm Env Some have False by simp
- then show ?thesis ..
- next
- case (Cons x' xs')
- from asm Env es have "lookup e xs = None" by simp
- then have "update (xs @ y # ys) opt e = e" by (rule hyp)
- with Env es Cons show "update ((x # xs) @ y # ys) opt env = env"
- by (simp add: fun_upd_idem_iff)
- qed
- qed
- qed
-qed
-
-theorem update_append_some:
- assumes "lookup env xs = Some e"
- shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
- using assms
-proof (induct xs arbitrary: env e)
- case Nil
- then have "env = e" by simp
- then show ?case by simp
-next
- case (Cons x xs)
- note hyp = Cons.hyps
- and asm = `lookup env (x # xs) = Some e`
- show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
- Some (update (y # ys) opt e)"
- proof (cases env)
- case (Val a)
- with asm have False by simp
- then show ?thesis ..
- next
- case (Env b es)
- show ?thesis
- proof (cases "es x")
- case None
- with asm Env have False by simp
- then show ?thesis ..
- next
- case (Some e')
- note es = `es x = Some e'`
- show ?thesis
- proof (cases xs)
- case Nil
- with asm Env es have "e = e'" by simp
- with Env es Nil show ?thesis by simp
- next
- case (Cons x' xs')
- from asm Env es have "lookup e' xs = Some e" by simp
- then have "lookup (update (xs @ y # ys) opt e') xs =
- Some (update (y # ys) opt e)" by (rule hyp)
- with Env es Cons show ?thesis by simp
- qed
- qed
- qed
-qed
-
-text {*
- \medskip Apparently, @{term update} does not affect the result of
- subsequent @{term lookup} operations at independent positions, i.e.\
- in case that the paths for @{term update} and @{term lookup} fork at
- a certain point.
-*}
-
-theorem lookup_update_other:
- assumes neq: "y \<noteq> (z::'c)"
- shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
- lookup env (xs @ y # ys)"
-proof (induct xs arbitrary: env)
- case Nil
- show ?case
- proof (cases env)
- case Val
- then show ?thesis by simp
- next
- case Env
- show ?thesis
- proof (cases zs)
- case Nil
- with neq Env show ?thesis by simp
- next
- case Cons
- with neq Env show ?thesis by simp
- qed
- qed
-next
- case (Cons x xs)
- note hyp = Cons.hyps
- show ?case
- proof (cases env)
- case Val
- then show ?thesis by simp
- next
- case (Env y es)
- show ?thesis
- proof (cases xs)
- case Nil
- show ?thesis
- proof (cases "es x")
- case None
- with Env Nil show ?thesis by simp
- next
- case Some
- with neq hyp and Env Nil show ?thesis by simp
- qed
- next
- case (Cons x' xs')
- show ?thesis
- proof (cases "es x")
- case None
- with Env Cons show ?thesis by simp
- next
- case Some
- with neq hyp and Env Cons show ?thesis by simp
- qed
- qed
- qed
-qed
-
-text {* Environments and code generation *}
-
-lemma [code, code del]:
- "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
-
-lemma equal_env_code [code]:
- fixes x y :: "'a\<Colon>equal"
- and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
- shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
- HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
- of None \<Rightarrow> (case g z
- of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z
- of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
- and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
- and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
- and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
-proof (unfold equal)
- have "f = g \<longleftrightarrow> (\<forall>z. case f z
- of None \<Rightarrow> (case g z
- of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z
- of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
- proof
- assume ?lhs
- then show ?rhs by (auto split: option.splits)
- next
- assume assm: ?rhs (is "\<forall>z. ?prop z")
- show ?lhs
- proof
- fix z
- from assm have "?prop z" ..
- then show "f z = g z" by (auto split: option.splits)
- qed
- qed
- then show "Env x f = Env y g \<longleftrightarrow>
- x = y \<and> (\<forall>z\<in>UNIV. case f z
- of None \<Rightarrow> (case g z
- of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z
- of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
-qed simp_all
-
-lemma [code nbe]:
- "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
- by (fact equal_refl)
-
-lemma [code, code del]:
- "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
-
-end
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Aug 17 18:52:21 2011 +0200
@@ -102,16 +102,16 @@
let
val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
in
- absdummy (@{typ nat}, absdummy (@{typ nat},
- Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
+ absdummy @{typ nat} (absdummy @{typ nat}
+ (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
(@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
Predicate_Compile_Aux.mk_single compfuns
(@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
end
fun enumerate_addups_nat compfuns (_ : typ) =
- absdummy (@{typ nat}, Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
- (absdummy (@{typ code_numeral}, @{term "Pair :: nat => nat => nat * nat"} $
+ absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
+ (absdummy @{typ code_numeral} (@{term "Pair :: nat => nat => nat * nat"} $
(@{term "Code_Numeral.nat_of"} $ Bound 0) $
(@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
@{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
@@ -120,8 +120,8 @@
val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
in
- absdummy(@{typ nat}, absdummy (@{typ nat},
- Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
+ absdummy @{typ nat} (absdummy @{typ nat}
+ (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
(@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
(Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
@{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Aug 17 18:52:21 2011 +0200
@@ -1678,7 +1678,7 @@
fresh_fs @
map (fn (((P, T), (x, U)), Q) =>
(Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
- Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
+ Abs ("z", HOLogic.unitT, absfree (x, U) Q)))
(pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
map (fn (s, T) => (Var ((s, 0), Logic.varifyT_global T), Free (s, T)))
rec_unique_frees)) induct_aux;
@@ -2017,9 +2017,9 @@
(Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
- (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
- Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
- set $ Free ("x", T) $ Free ("y", T'))))))
+ (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T)
+ (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
+ (set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
(* prove characteristic equations for primrec combinators *)
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Aug 17 18:52:21 2011 +0200
@@ -187,7 +187,7 @@
fun mk s =
let
val t = Syntax.read_term ctxt' s;
- val t' = list_abs_free (params, t) |>
+ val t' = fold_rev absfree params t |>
funpow (length params) (fn Abs (_, _, t) => t)
in (t', HOLogic.dest_setT (fastype_of t)) end
handle TERM _ =>
--- a/src/HOL/Nominal/nominal_primrec.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Aug 17 18:52:21 2011 +0200
@@ -163,8 +163,7 @@
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle RecError s => primrec_eq_err lthy s eq
- in (fnames'', fnss'',
- (list_abs_free (cargs' @ subs, rhs'))::fns)
+ in (fnames'', fnss'', fold_rev absfree (cargs' @ subs) rhs' :: fns)
end)
in (case AList.lookup (op =) fnames i of
@@ -209,8 +208,8 @@
val used = map fst (fold Term.add_frees fs []);
val x = (singleton (Name.variant_list used) "x", dummyT);
val frees = ls @ x :: rs;
- val raw_rhs = list_abs_free (frees,
- list_comb (Const (rec_name, dummyT), fs @ [Free x]))
+ val raw_rhs = fold_rev absfree frees
+ (list_comb (Const (rec_name, dummyT), fs @ [Free x]))
val def_name = Thm.def_name (Long_Name.base_name fname);
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
val SOME var = get_first (fn ((b, _), mx) =>
--- a/src/HOL/Set.thy Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Set.thy Wed Aug 17 18:52:21 2011 +0200
@@ -281,7 +281,7 @@
val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
val exP = ex_tr [idts, P];
- in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
+ in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
*}
--- a/src/HOL/Tools/Datatype/datatype.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Aug 17 18:52:21 2011 +0200
@@ -323,7 +323,7 @@
val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []);
val xs = map (uncurry (Datatype_Aux.mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
val ys = map (uncurry (Datatype_Aux.mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
- val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
+ val f = fold_rev (absfree o dest_Free) (xs @ ys) (mk_univ_inj ts n i);
val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []);
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Aug 17 18:52:21 2011 +0200
@@ -201,10 +201,10 @@
let
val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
- absfree ("y", T2, set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
+ absfree ("y", T2) (set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
(rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
val cert = cterm_of thy1
- val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
+ val insts = map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
val induct' = cterm_instantiate ((map cert induct_Ps) ~~
(map cert insts)) induct;
@@ -238,9 +238,9 @@
|> (Global_Theory.add_defs false o map Thm.no_attributes)
(map (fn ((((name, comb), set), T), T') =>
(Binding.name (Long_Name.base_name name ^ "_def"),
- Logic.mk_equals (comb, absfree ("x", T,
- Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
- set $ Free ("x", T) $ Free ("y", T'))))))
+ Logic.mk_equals (comb, absfree ("x", T)
+ (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
+ (set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
||> Sign.parent_path
||> Theory.checkpoint;
@@ -306,8 +306,7 @@
val frees = take (length cargs) frees';
val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j
in
- (free, list_abs_free (map dest_Free frees',
- list_comb (free, frees)))
+ (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
end) (constrs ~~ (1 upto length constrs)));
val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Aug 17 18:52:21 2011 +0200
@@ -145,7 +145,7 @@
(case t1 of
NONE =>
(case flt (Misc_Legacy.term_frees t2) of
- [Free (s, T)] => SOME (absfree (s, T, t2))
+ [Free (s, T)] => SOME (absfree (s, T) t2)
| _ => NONE)
| SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
val insts = map_filter (fn (t, u) =>
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Aug 17 18:52:21 2011 +0200
@@ -56,9 +56,8 @@
val rT = nth (rec_result_Ts) i;
val vs' = filter_out is_unit vs;
val f = Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
- val f' = Envir.eta_contract (list_abs_free
- (map dest_Free vs, if member (op =) is i then list_comb (f, vs')
- else HOLogic.unit));
+ val f' = Envir.eta_contract (fold_rev (absfree o dest_Free) vs
+ (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
(list_comb (Const (cname, Ts ---> T), map Free frees))), f')
end
--- a/src/HOL/Tools/Function/fun.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Function/fun.ML Wed Aug 17 18:52:21 2011 +0200
@@ -7,12 +7,13 @@
signature FUNCTION_FUN =
sig
+ val fun_config : Function_Common.function_config
val add_fun : (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> Function_Common.function_config ->
local_theory -> Proof.context
val add_fun_cmd : (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> Function_Common.function_config ->
- local_theory -> Proof.context
+ bool -> local_theory -> Proof.context
val setup : theory -> theory
end
@@ -149,7 +150,7 @@
val fun_config = FunctionConfig { sequential=true, default=NONE,
domintros=false, partials=false }
-fun gen_add_fun add fixes statements config lthy =
+fun gen_add_fun add lthy =
let
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1
@@ -159,18 +160,18 @@
(Function_Common.get_termination_prover lthy lthy) lthy
in
lthy
- |> add fixes statements config pat_completeness_auto |> snd
+ |> add pat_completeness_auto |> snd
|> Local_Theory.restore
|> prove_termination |> snd
end
-val add_fun = gen_add_fun Function.add_function
-val add_fun_cmd = gen_add_fun Function.add_function_cmd
+fun add_fun a b c = gen_add_fun (Function.add_function a b c)
+fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b c tac int)
val _ =
- Outer_Syntax.local_theory "fun" "define general recursive functions (short version)"
+ Outer_Syntax.local_theory' "fun" "define general recursive functions (short version)"
Keyword.thy_decl
(function_parser fun_config
>> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
--- a/src/HOL/Tools/Function/function.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Function/function.ML Wed Aug 17 18:52:21 2011 +0200
@@ -14,7 +14,7 @@
val add_function_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> Function_Common.function_config ->
- (Proof.context -> tactic) -> local_theory -> info * local_theory
+ (Proof.context -> tactic) -> bool -> local_theory -> info * local_theory
val function: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> Function_Common.function_config ->
@@ -22,7 +22,7 @@
val function_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> Function_Common.function_config ->
- local_theory -> Proof.state
+ bool -> local_theory -> Proof.state
val prove_termination: term option -> tactic -> local_theory ->
info * local_theory
@@ -76,7 +76,7 @@
(saved_simps, fold2 add_for_f fnames simps_by_f lthy)
end
-fun prepare_function is_external prep default_constraint fixspec eqns config lthy =
+fun prepare_function do_print prep default_constraint fixspec eqns config lthy =
let
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
@@ -125,19 +125,19 @@
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
fs=fs, R=R, defname=defname, is_partial=true }
- val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes)
+ val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
in
- (info,
+ (info,
lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
end
in
((goal_state, afterqed), lthy')
end
-fun gen_add_function is_external prep default_constraint fixspec eqns config tac lthy =
+fun gen_add_function do_print prep default_constraint fixspec eqns config tac lthy =
let
val ((goal_state, afterqed), lthy') =
- prepare_function is_external prep default_constraint fixspec eqns config lthy
+ prepare_function do_print prep default_constraint fixspec eqns config lthy
val pattern_thm =
case SINGLE (tac lthy') goal_state of
NONE => error "pattern completeness and compatibility proof failed"
@@ -149,12 +149,12 @@
val add_function =
gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
-val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
+fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d
-fun gen_function is_external prep default_constraint fixspec eqns config lthy =
+fun gen_function do_print prep default_constraint fixspec eqns config lthy =
let
val ((goal_state, afterqed), lthy') =
- prepare_function is_external prep default_constraint fixspec eqns config lthy
+ prepare_function do_print prep default_constraint fixspec eqns config lthy
in
lthy'
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
@@ -163,7 +163,7 @@
val function =
gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
-val function_cmd = gen_function true Specification.read_spec "_::type"
+fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c
fun prepare_termination_proof prep_term raw_term_opt lthy =
let
@@ -277,7 +277,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
+ Outer_Syntax.local_theory_to_proof' "function" "define general recursive functions"
Keyword.thy_goal
(function_parser default_config
>> (fn ((config, fixes), statements) => function_cmd fixes statements config))
--- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Wed Aug 17 18:52:21 2011 +0200
@@ -68,8 +68,8 @@
val args = Misc_Legacy.term_frees body
(* Forms a lambda-abstraction over the formal parameters *)
val rhs =
- list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ beta_eta_in_abs_body body)
+ fold_rev (absfree o dest_Free) args
+ (HOLogic.choice_const T $ beta_eta_in_abs_body body)
|> mk_old_skolem_term_wrapper
val comb = list_comb (rhs, args)
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 17 18:52:21 2011 +0200
@@ -491,7 +491,7 @@
case strip_comb flex of
(Var (z as (_, T)), args) =>
add_terms (Var z,
- fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
+ fold_rev absdummy (take (length args) (binder_types T)) rigid)
| _ => I
fun unify_potential_flex comb atom =
if is_flex comb then unify_flex comb atom
@@ -541,7 +541,7 @@
if k > j then t else t $ u
| (t, u) => t $ u)
| repair t = t
- val t' = t |> repair |> fold (curry absdummy) (map snd params)
+ val t' = t |> repair |> fold (absdummy o snd) params
fun do_instantiate th =
case Term.add_vars (prop_of th) []
|> filter_out ((Meson_Clausify.is_zapped_var_name orf
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Aug 17 18:52:21 2011 +0200
@@ -1555,7 +1555,7 @@
else
fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
end
- |> curry absdummy dataT
+ |> absdummy dataT
fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
@@ -1968,7 +1968,7 @@
discriminate_value hol_ctxt x y_var ::
map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
|> foldr1 s_conj
- in List.foldr absdummy core_t arg_Ts end
+ in fold_rev absdummy arg_Ts core_t end
in
[HOLogic.mk_imp
(HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Aug 17 18:52:21 2011 +0200
@@ -634,7 +634,7 @@
fun app f =
list_comb (f (), map Bound (length arg_Ts - 1 downto 0))
in
- List.foldr absdummy (connective $ app pos $ app neg) arg_Ts
+ fold_rev absdummy arg_Ts (connective $ app pos $ app neg)
end
end
else
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 17 18:52:21 2011 +0200
@@ -1017,7 +1017,7 @@
fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
let
- val t' = list_abs_free (Term.add_frees t [], t)
+ val t' = fold_rev absfree (Term.add_frees t []) t
val options = code_options_of (Proof_Context.theory_of ctxt)
val thy = Theory.copy (Proof_Context.theory_of ctxt)
val ((((full_constname, constT), vs'), intro), thy1) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Aug 17 18:52:21 2011 +0200
@@ -914,7 +914,7 @@
val Ts = binder_types (fastype_of f')
val bs = map Bound ((length Ts - 1) downto 0)
in
- fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
+ fold_rev absdummy Ts (f $ (list_comb (f', bs)))
end
val fs' = map apply_f fs
val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
@@ -949,7 +949,7 @@
val T' = TFree (tname', HOLogic.typeS)
val U = TFree (uname, HOLogic.typeS)
val y = Free (yname, U)
- val f' = absdummy (U --> T', Bound 0 $ y)
+ val f' = absdummy (U --> T') (Bound 0 $ y)
val th' = Thm.certify_instantiate
([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
[((fst (dest_Var f), (U --> T') --> T'), f')]) th
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Aug 17 18:52:21 2011 +0200
@@ -524,7 +524,7 @@
Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
@{typ "Int.int"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))
in
- absdummy (@{typ code_numeral}, small_lazy $ HOLogic.mk_number @{typ int} 3)
+ absdummy @{typ code_numeral} (small_lazy $ HOLogic.mk_number @{typ int} 3)
end
),
modify_funT = I,
@@ -580,27 +580,29 @@
(** specific rpred functions -- move them to the correct place in this file *)
fun mk_Eval_of (P as (Free (f, _)), T) mode =
-let
- fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
- let
- val (bs2, i') = mk_bounds T2 i
- val (bs1, i'') = mk_bounds T1 i'
- in
- (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
- end
- | mk_bounds T i = (Bound i, i + 1)
- fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
- fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
- | mk_tuple tTs = foldr1 mk_prod tTs;
- fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t = absdummy (T, HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
- | mk_split_abs T t = absdummy (T, t)
- val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
- val (inargs, outargs) = split_mode mode args
- val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
- val inner_term = PredicateCompFuns.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
-in
- fold_rev mk_split_abs (binder_types T) inner_term
-end
+ let
+ fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
+ let
+ val (bs2, i') = mk_bounds T2 i
+ val (bs1, i'') = mk_bounds T1 i'
+ in
+ (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
+ end
+ | mk_bounds T i = (Bound i, i + 1)
+ fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
+ fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
+ | mk_tuple tTs = foldr1 mk_prod tTs
+ fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
+ absdummy T
+ (HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
+ | mk_split_abs T t = absdummy T t
+ val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
+ val (inargs, outargs) = split_mode mode args
+ val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
+ val inner_term = PredicateCompFuns.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
+ in
+ fold_rev mk_split_abs (binder_types T) inner_term
+ end
fun compile_arg compilation_modifiers additional_arguments ctxt param_modes arg =
let
@@ -1831,7 +1833,7 @@
val t' =
if stats andalso compilation = New_Pos_Random_DSeq then
mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
- (absdummy (T, HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
+ (absdummy T (HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
@{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
else
mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Aug 17 18:52:21 2011 +0200
@@ -218,7 +218,7 @@
fun compile_term compilation options ctxt t =
let
- val t' = list_abs_free (Term.add_frees t [], t)
+ val t' = fold_rev absfree (Term.add_frees t []) t
val thy = Theory.copy (Proof_Context.theory_of ctxt)
val ((((full_constname, constT), vs'), intro), thy1) =
Predicate_Compile_Aux.define_quickcheck_predicate t' thy
@@ -269,7 +269,7 @@
| Pos_Generator_DSeq => mk_gen_bind (prog,
mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
- | Depth_Limited_Random => fold_rev (curry absdummy)
+ | Depth_Limited_Random => fold_rev absdummy
[@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
@{typ "code_numeral * code_numeral"}]
(mk_bind' (list_comb (prog, map Bound (3 downto 0)),
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Aug 17 18:52:21 2011 +0200
@@ -70,7 +70,7 @@
end
fun mk_unit_let (x, y) =
- Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ (absdummy (@{typ unit}, y))
+ Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ absdummy @{typ unit} y
(* handling inductive datatypes *)
@@ -113,14 +113,14 @@
map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
end
-fun gen_mk_call c T = (T, fn t => c T $ absdummy (T, t) $ size_pred)
+fun gen_mk_call c T = (T, fn t => c T $ absdummy T t $ size_pred)
fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) =
let
val T = Type (tyco, Ts)
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
in
- (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
+ (T, fn t => nth functerms k $ absdummy T t $ size_pred)
end
fun gen_mk_consexpr test_function functerms simpleT (c, xs) =
@@ -184,18 +184,18 @@
Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
full_exhaustiveT T)
in
- (T, (fn t => full_exhaustive $
+ (T, fn t => full_exhaustive $
(HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
- $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
+ $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
end
fun mk_aux_call fTs (k, _) (tyco, Ts) =
let
val T = Type (tyco, Ts)
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
in
- (T, (fn t => nth functerms k $
+ (T, fn t => nth functerms k $
(HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
- $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
+ $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
end
fun mk_consexpr simpleT (c, xs) =
let
@@ -209,7 +209,7 @@
bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
val start_term = test_function simpleT $
(HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
- $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
+ $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
in fold_rev (fn f => fn t => f t) fns start_term end
fun mk_rhs exprs =
@{term "If :: bool => term list option => term list option => term list option"}
@@ -382,7 +382,7 @@
fun mk_parametric_generator_expr mk_generator_expr =
Quickcheck_Common.gen_mk_parametric_generator_expr
- ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
+ ((mk_generator_expr, absdummy @{typ "code_numeral"} @{term "None :: term list option"}),
@{typ "code_numeral => term list option"})
fun mk_validator_expr ctxt t =
@@ -412,9 +412,9 @@
val return = @{term "Some :: term list => term list option"} $
(HOLogic.mk_list @{typ "term"}
(replicate (length frees + length eval_terms) dummy_term))
- val wrap = absdummy (@{typ bool},
- @{term "If :: bool => term list option => term list option => term list option"} $
- Bound 0 $ @{term "None :: term list option"} $ return)
+ val wrap = absdummy @{typ bool}
+ (@{term "If :: bool => term list option => term list option => term list option"} $
+ Bound 0 $ @{term "None :: term list option"} $ return)
in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
(** generator compiliation **)
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Aug 17 18:52:21 2011 +0200
@@ -340,10 +340,11 @@
in
case dT of
Type (@{type_name fun}, _) =>
- (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
- Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
- | _ => (fn t => absdummy (dT, rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
- Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
+ (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
+ Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
+ | _ =>
+ (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
+ Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
end
| eval_function T = (I, T)
val (tt, boundTs') = split_list (map eval_function boundTs)
@@ -432,7 +433,7 @@
end
else
let
- val t' = Term.list_abs_free (Term.add_frees t [], t)
+ val t' = fold_rev absfree (Term.add_frees t []) t
fun wrap f t = list_abs (f (strip_abs t))
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
fun ensure_testable t =
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Aug 17 18:52:21 2011 +0200
@@ -112,7 +112,7 @@
if_t $ (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
(mk_generator_expr ctxt (t, eval_terms)) $ else_t
in
- absdummy (@{typ "code_numeral"}, fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
+ absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
end
(** post-processing of function terms **)
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Aug 17 18:52:21 2011 +0200
@@ -291,7 +291,7 @@
fun mk_generator_expr ctxt (t, eval_terms) =
let
val thy = Proof_Context.theory_of ctxt
- val prop = list_abs_free (Term.add_frees t [], t)
+ val prop = fold_rev absfree (Term.add_frees t []) t
val Ts = (map snd o fst o strip_abs) prop
val bound_max = length Ts - 1;
val bounds = map_index (fn (i, ty) =>
@@ -317,7 +317,7 @@
fun mk_reporting_generator_expr ctxt (t, eval_terms) =
let
val thy = Proof_Context.theory_of ctxt
- val prop = list_abs_free (Term.add_frees t [], t)
+ val prop = fold_rev absfree (Term.add_frees t []) t
val Ts = (map snd o fst o strip_abs) prop
val bound_max = length Ts - 1
val bounds = map_index (fn (i, ty) =>
@@ -360,13 +360,13 @@
val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_generator_expr,
- absdummy (@{typ code_numeral}, @{term "Pair None :: Random.seed => term list option * Random.seed"})),
+ absdummy @{typ code_numeral} @{term "Pair None :: Random.seed => term list option * Random.seed"}),
@{typ "code_numeral => Random.seed => term list option * Random.seed"})
val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_reporting_generator_expr,
- absdummy (@{typ code_numeral},
- @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"})),
+ absdummy @{typ code_numeral}
+ @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"}),
@{typ "code_numeral => Random.seed => (term list option * (bool list * bool)) * Random.seed"})
--- a/src/HOL/Tools/SMT/z3_model.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_model.ML Wed Aug 17 18:52:21 2011 +0200
@@ -156,11 +156,11 @@
val (dT', rT') = Term.dest_funT rT
in
mk_fun_upd dT rT $ f $ t $
- mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
+ mk_update (ts, u) (absdummy dT' (Const ("_", rT')))
end
fun mk_lambda Ts (t, pats) =
- fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
+ fold_rev absdummy Ts t |> fold mk_update pats
fun translate ((t, k), (e, cs)) =
let
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Aug 17 18:52:21 2011 +0200
@@ -145,7 +145,7 @@
val frees = map Free (Term.add_frees t [])
val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs
val vs = map (Term.dest_Free o Thm.term_of) cvs'
- in (Term.list_abs_free (vs, t), cvs') end
+ in (fold_rev absfree vs t, cvs') end
fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) =
let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
--- a/src/HOL/Tools/TFL/tfl.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Aug 17 18:52:21 2011 +0200
@@ -342,8 +342,7 @@
("The following clauses are redundant (covered by preceding clauses): " ^
commas (map (fn i => string_of_int (i + 1)) L))
in {functional = Abs(Long_Name.base_name fname, ftype,
- abstract_over (atom,
- absfree(aname,atype, case_tm))),
+ abstract_over (atom, absfree (aname,atype) case_tm)),
pats = patts2}
end end;
--- a/src/HOL/Tools/hologic.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/hologic.ML Wed Aug 17 18:52:21 2011 +0200
@@ -183,7 +183,7 @@
| dest_set t = raise TERM ("dest_set", [t]);
fun Collect_const T = Const ("Set.Collect", (T --> boolT) --> mk_setT T);
-fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
+fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T) t;
fun mk_mem (x, A) =
let val setT = fastype_of A in
@@ -258,11 +258,11 @@
| dest_eq t = raise TERM ("dest_eq", [t])
fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
-fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
+fun mk_all (x, T, P) = all_const T $ absfree (x, T) P;
fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
fun exists_const T = Const ("HOL.Ex", [T --> boolT] ---> boolT);
-fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
+fun mk_exists (x, T, P) = exists_const T $ absfree (x, T) P;
fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
--- a/src/HOL/Tools/inductive_codegen.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Aug 17 18:52:21 2011 +0200
@@ -871,7 +871,7 @@
fun test_term ctxt [(t, [])] =
let
- val t' = list_abs_free (Term.add_frees t [], t)
+ val t' = fold_rev absfree (Term.add_frees t []) t;
val thy = Proof_Context.theory_of ctxt;
val (xs, p) = strip_abs t';
val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
--- a/src/HOL/Tools/inductive_realizer.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Aug 17 18:52:21 2011 +0200
@@ -190,10 +190,11 @@
| fun_of ts rts args used [] =
let val xs = rev (rts @ ts)
in if conclT = Extraction.nullT
- then list_abs_free (map dest_Free xs, HOLogic.unit)
- else list_abs_free (map dest_Free xs, list_comb
- (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
- map fastype_of (rev args) ---> conclT), rev args))
+ then fold_rev (absfree o dest_Free) xs HOLogic.unit
+ else fold_rev (absfree o dest_Free) xs
+ (list_comb
+ (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
+ map fastype_of (rev args) ---> conclT), rev args))
end
in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
@@ -223,10 +224,11 @@
let
val Type ("fun", [U, _]) = T;
val a :: names' = names
- in (list_abs_free (("x", U) :: map_filter (fn intr =>
- Option.map (pair (name_of_fn intr))
- (AList.lookup (op =) frees (name_of_fn intr))) intrs,
- list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
+ in
+ (fold_rev absfree (("x", U) :: map_filter (fn intr =>
+ Option.map (pair (name_of_fn intr))
+ (AList.lookup (op =) frees (name_of_fn intr))) intrs)
+ (list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
end
end) concls rec_names)
end;
--- a/src/HOL/Tools/list_to_set_comprehension.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/list_to_set_comprehension.ML Wed Aug 17 18:52:21 2011 +0200
@@ -207,7 +207,7 @@
val eqs' = map reverse_bounds eqs
val pat_eq' = reverse_bounds pat_eq
val inner_t =
- fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy (T, t))
+ fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy T t)
(rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
val lhs = term_of redex
val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
--- a/src/HOL/Tools/primrec.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Tools/primrec.ML Wed Aug 17 18:52:21 2011 +0200
@@ -154,8 +154,8 @@
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle PrimrecError (s, NONE) => primrec_error_eqn s eq
- in (fnames'', fnss'',
- (list_abs_free (cargs' @ subs @ ls @ rs, rhs')) :: fns)
+ in
+ (fnames'', fnss'', fold_rev absfree (cargs' @ subs @ ls @ rs) rhs' :: fns)
end)
in
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Unix/Nested_Environment.thy Wed Aug 17 18:52:21 2011 +0200
@@ -0,0 +1,571 @@
+(* Title: HOL/Unix/Nested_Environment.thy
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+header {* Nested environments *}
+
+theory Nested_Environment
+imports Main
+begin
+
+text {*
+ Consider a partial function @{term [source] "e :: 'a => 'b option"};
+ this may be understood as an \emph{environment} mapping indexes
+ @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
+ @{text Map} of Isabelle/HOL). This basic idea is easily generalized
+ to that of a \emph{nested environment}, where entries may be either
+ basic values or again proper environments. Then each entry is
+ accessed by a \emph{path}, i.e.\ a list of indexes leading to its
+ position within the structure.
+*}
+
+datatype ('a, 'b, 'c) env =
+ Val 'a
+ | Env 'b "'c => ('a, 'b, 'c) env option"
+
+text {*
+ \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
+ 'a} refers to basic values (occurring in terminal positions), type
+ @{typ 'b} to values associated with proper (inner) environments, and
+ type @{typ 'c} with the index type for branching. Note that there
+ is no restriction on any of these types. In particular, arbitrary
+ branching may yield rather large (transfinite) tree structures.
+*}
+
+
+subsection {* The lookup operation *}
+
+text {*
+ Lookup in nested environments works by following a given path of
+ index elements, leading to an optional result (a terminal value or
+ nested environment). A \emph{defined position} within a nested
+ environment is one where @{term lookup} at its path does not yield
+ @{term None}.
+*}
+
+primrec
+ lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
+ and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
+ "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
+ | "lookup (Env b es) xs =
+ (case xs of
+ [] => Some (Env b es)
+ | y # ys => lookup_option (es y) ys)"
+ | "lookup_option None xs = None"
+ | "lookup_option (Some e) xs = lookup e xs"
+
+hide_const lookup_option
+
+text {*
+ \medskip The characteristic cases of @{term lookup} are expressed by
+ the following equalities.
+*}
+
+theorem lookup_nil: "lookup e [] = Some e"
+ by (cases e) simp_all
+
+theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"
+ by simp
+
+theorem lookup_env_cons:
+ "lookup (Env b es) (x # xs) =
+ (case es x of
+ None => None
+ | Some e => lookup e xs)"
+ by (cases "es x") simp_all
+
+lemmas lookup_lookup_option.simps [simp del]
+ and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
+
+theorem lookup_eq:
+ "lookup env xs =
+ (case xs of
+ [] => Some env
+ | x # xs =>
+ (case env of
+ Val a => None
+ | Env b es =>
+ (case es x of
+ None => None
+ | Some e => lookup e xs)))"
+ by (simp split: list.split env.split)
+
+text {*
+ \medskip Displaced @{term lookup} operations, relative to a certain
+ base path prefix, may be reduced as follows. There are two cases,
+ depending whether the environment actually extends far enough to
+ follow the base path.
+*}
+
+theorem lookup_append_none:
+ assumes "lookup env xs = None"
+ shows "lookup env (xs @ ys) = None"
+ using assms
+proof (induct xs arbitrary: env)
+ case Nil
+ then have False by simp
+ then show ?case ..
+next
+ case (Cons x xs)
+ show ?case
+ proof (cases env)
+ case Val
+ then show ?thesis by simp
+ next
+ case (Env b es)
+ show ?thesis
+ proof (cases "es x")
+ case None
+ with Env show ?thesis by simp
+ next
+ case (Some e)
+ note es = `es x = Some e`
+ show ?thesis
+ proof (cases "lookup e xs")
+ case None
+ then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)
+ with Env Some show ?thesis by simp
+ next
+ case Some
+ with Env es have False using Cons.prems by simp
+ then show ?thesis ..
+ qed
+ qed
+ qed
+qed
+
+theorem lookup_append_some:
+ assumes "lookup env xs = Some e"
+ shows "lookup env (xs @ ys) = lookup e ys"
+ using assms
+proof (induct xs arbitrary: env e)
+ case Nil
+ then have "env = e" by simp
+ then show "lookup env ([] @ ys) = lookup e ys" by simp
+next
+ case (Cons x xs)
+ note asm = `lookup env (x # xs) = Some e`
+ show "lookup env ((x # xs) @ ys) = lookup e ys"
+ proof (cases env)
+ case (Val a)
+ with asm have False by simp
+ then show ?thesis ..
+ next
+ case (Env b es)
+ show ?thesis
+ proof (cases "es x")
+ case None
+ with asm Env have False by simp
+ then show ?thesis ..
+ next
+ case (Some e')
+ note es = `es x = Some e'`
+ show ?thesis
+ proof (cases "lookup e' xs")
+ case None
+ with asm Env es have False by simp
+ then show ?thesis ..
+ next
+ case Some
+ with asm Env es have "lookup e' xs = Some e"
+ by simp
+ then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)
+ with Env es show ?thesis by simp
+ qed
+ qed
+ qed
+qed
+
+text {*
+ \medskip Successful @{term lookup} deeper down an environment
+ structure means we are able to peek further up as well. Note that
+ this is basically just the contrapositive statement of @{thm
+ [source] lookup_append_none} above.
+*}
+
+theorem lookup_some_append:
+ assumes "lookup env (xs @ ys) = Some e"
+ shows "\<exists>e. lookup env xs = Some e"
+proof -
+ from assms have "lookup env (xs @ ys) \<noteq> None" by simp
+ then have "lookup env xs \<noteq> None"
+ by (rule contrapos_nn) (simp only: lookup_append_none)
+ then show ?thesis by (simp)
+qed
+
+text {*
+ The subsequent statement describes in more detail how a successful
+ @{term lookup} with a non-empty path results in a certain situation
+ at any upper position.
+*}
+
+theorem lookup_some_upper:
+ assumes "lookup env (xs @ y # ys) = Some e"
+ shows "\<exists>b' es' env'.
+ lookup env xs = Some (Env b' es') \<and>
+ es' y = Some env' \<and>
+ lookup env' ys = Some e"
+ using assms
+proof (induct xs arbitrary: env e)
+ case Nil
+ from Nil.prems have "lookup env (y # ys) = Some e"
+ by simp
+ then obtain b' es' env' where
+ env: "env = Env b' es'" and
+ es': "es' y = Some env'" and
+ look': "lookup env' ys = Some e"
+ by (auto simp add: lookup_eq split: option.splits env.splits)
+ from env have "lookup env [] = Some (Env b' es')" by simp
+ with es' look' show ?case by blast
+next
+ case (Cons x xs)
+ from Cons.prems
+ obtain b' es' env' where
+ env: "env = Env b' es'" and
+ es': "es' x = Some env'" and
+ look': "lookup env' (xs @ y # ys) = Some e"
+ by (auto simp add: lookup_eq split: option.splits env.splits)
+ from Cons.hyps [OF look'] obtain b'' es'' env'' where
+ upper': "lookup env' xs = Some (Env b'' es'')" and
+ es'': "es'' y = Some env''" and
+ look'': "lookup env'' ys = Some e"
+ by blast
+ from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
+ by simp
+ with es'' look'' show ?case by blast
+qed
+
+
+subsection {* The update operation *}
+
+text {*
+ Update at a certain position in a nested environment may either
+ delete an existing entry, or overwrite an existing one. Note that
+ update at undefined positions is simple absorbed, i.e.\ the
+ environment is left unchanged.
+*}
+
+primrec
+ update :: "'c list => ('a, 'b, 'c) env option
+ => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
+ and update_option :: "'c list => ('a, 'b, 'c) env option
+ => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
+ "update xs opt (Val a) =
+ (if xs = [] then (case opt of None => Val a | Some e => e)
+ else Val a)"
+ | "update xs opt (Env b es) =
+ (case xs of
+ [] => (case opt of None => Env b es | Some e => e)
+ | y # ys => Env b (es (y := update_option ys opt (es y))))"
+ | "update_option xs opt None =
+ (if xs = [] then opt else None)"
+ | "update_option xs opt (Some e) =
+ (if xs = [] then opt else Some (update xs opt e))"
+
+hide_const update_option
+
+text {*
+ \medskip The characteristic cases of @{term update} are expressed by
+ the following equalities.
+*}
+
+theorem update_nil_none: "update [] None env = env"
+ by (cases env) simp_all
+
+theorem update_nil_some: "update [] (Some e) env = e"
+ by (cases env) simp_all
+
+theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"
+ by simp
+
+theorem update_cons_nil_env:
+ "update [x] opt (Env b es) = Env b (es (x := opt))"
+ by (cases "es x") simp_all
+
+theorem update_cons_cons_env:
+ "update (x # y # ys) opt (Env b es) =
+ Env b (es (x :=
+ (case es x of
+ None => None
+ | Some e => Some (update (y # ys) opt e))))"
+ by (cases "es x") simp_all
+
+lemmas update_update_option.simps [simp del]
+ and update_simps [simp] = update_nil_none update_nil_some
+ update_cons_val update_cons_nil_env update_cons_cons_env
+
+lemma update_eq:
+ "update xs opt env =
+ (case xs of
+ [] =>
+ (case opt of
+ None => env
+ | Some e => e)
+ | x # xs =>
+ (case env of
+ Val a => Val a
+ | Env b es =>
+ (case xs of
+ [] => Env b (es (x := opt))
+ | y # ys =>
+ Env b (es (x :=
+ (case es x of
+ None => None
+ | Some e => Some (update (y # ys) opt e)))))))"
+ by (simp split: list.split env.split option.split)
+
+text {*
+ \medskip The most basic correspondence of @{term lookup} and @{term
+ update} states that after @{term update} at a defined position,
+ subsequent @{term lookup} operations would yield the new value.
+*}
+
+theorem lookup_update_some:
+ assumes "lookup env xs = Some e"
+ shows "lookup (update xs (Some env') env) xs = Some env'"
+ using assms
+proof (induct xs arbitrary: env e)
+ case Nil
+ then have "env = e" by simp
+ then show ?case by simp
+next
+ case (Cons x xs)
+ note hyp = Cons.hyps
+ and asm = `lookup env (x # xs) = Some e`
+ show ?case
+ proof (cases env)
+ case (Val a)
+ with asm have False by simp
+ then show ?thesis ..
+ next
+ case (Env b es)
+ show ?thesis
+ proof (cases "es x")
+ case None
+ with asm Env have False by simp
+ then show ?thesis ..
+ next
+ case (Some e')
+ note es = `es x = Some e'`
+ show ?thesis
+ proof (cases xs)
+ case Nil
+ with Env show ?thesis by simp
+ next
+ case (Cons x' xs')
+ from asm Env es have "lookup e' xs = Some e" by simp
+ then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
+ with Env es Cons show ?thesis by simp
+ qed
+ qed
+ qed
+qed
+
+text {*
+ \medskip The properties of displaced @{term update} operations are
+ analogous to those of @{term lookup} above. There are two cases:
+ below an undefined position @{term update} is absorbed altogether,
+ and below a defined positions @{term update} affects subsequent
+ @{term lookup} operations in the obvious way.
+*}
+
+theorem update_append_none:
+ assumes "lookup env xs = None"
+ shows "update (xs @ y # ys) opt env = env"
+ using assms
+proof (induct xs arbitrary: env)
+ case Nil
+ then have False by simp
+ then show ?case ..
+next
+ case (Cons x xs)
+ note hyp = Cons.hyps
+ and asm = `lookup env (x # xs) = None`
+ show "update ((x # xs) @ y # ys) opt env = env"
+ proof (cases env)
+ case (Val a)
+ then show ?thesis by simp
+ next
+ case (Env b es)
+ show ?thesis
+ proof (cases "es x")
+ case None
+ note es = `es x = None`
+ show ?thesis
+ by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
+ next
+ case (Some e)
+ note es = `es x = Some e`
+ show ?thesis
+ proof (cases xs)
+ case Nil
+ with asm Env Some have False by simp
+ then show ?thesis ..
+ next
+ case (Cons x' xs')
+ from asm Env es have "lookup e xs = None" by simp
+ then have "update (xs @ y # ys) opt e = e" by (rule hyp)
+ with Env es Cons show "update ((x # xs) @ y # ys) opt env = env"
+ by (simp add: fun_upd_idem_iff)
+ qed
+ qed
+ qed
+qed
+
+theorem update_append_some:
+ assumes "lookup env xs = Some e"
+ shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
+ using assms
+proof (induct xs arbitrary: env e)
+ case Nil
+ then have "env = e" by simp
+ then show ?case by simp
+next
+ case (Cons x xs)
+ note hyp = Cons.hyps
+ and asm = `lookup env (x # xs) = Some e`
+ show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
+ Some (update (y # ys) opt e)"
+ proof (cases env)
+ case (Val a)
+ with asm have False by simp
+ then show ?thesis ..
+ next
+ case (Env b es)
+ show ?thesis
+ proof (cases "es x")
+ case None
+ with asm Env have False by simp
+ then show ?thesis ..
+ next
+ case (Some e')
+ note es = `es x = Some e'`
+ show ?thesis
+ proof (cases xs)
+ case Nil
+ with asm Env es have "e = e'" by simp
+ with Env es Nil show ?thesis by simp
+ next
+ case (Cons x' xs')
+ from asm Env es have "lookup e' xs = Some e" by simp
+ then have "lookup (update (xs @ y # ys) opt e') xs =
+ Some (update (y # ys) opt e)" by (rule hyp)
+ with Env es Cons show ?thesis by simp
+ qed
+ qed
+ qed
+qed
+
+text {*
+ \medskip Apparently, @{term update} does not affect the result of
+ subsequent @{term lookup} operations at independent positions, i.e.\
+ in case that the paths for @{term update} and @{term lookup} fork at
+ a certain point.
+*}
+
+theorem lookup_update_other:
+ assumes neq: "y \<noteq> (z::'c)"
+ shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
+ lookup env (xs @ y # ys)"
+proof (induct xs arbitrary: env)
+ case Nil
+ show ?case
+ proof (cases env)
+ case Val
+ then show ?thesis by simp
+ next
+ case Env
+ show ?thesis
+ proof (cases zs)
+ case Nil
+ with neq Env show ?thesis by simp
+ next
+ case Cons
+ with neq Env show ?thesis by simp
+ qed
+ qed
+next
+ case (Cons x xs)
+ note hyp = Cons.hyps
+ show ?case
+ proof (cases env)
+ case Val
+ then show ?thesis by simp
+ next
+ case (Env y es)
+ show ?thesis
+ proof (cases xs)
+ case Nil
+ show ?thesis
+ proof (cases "es x")
+ case None
+ with Env Nil show ?thesis by simp
+ next
+ case Some
+ with neq hyp and Env Nil show ?thesis by simp
+ qed
+ next
+ case (Cons x' xs')
+ show ?thesis
+ proof (cases "es x")
+ case None
+ with Env Cons show ?thesis by simp
+ next
+ case Some
+ with neq hyp and Env Cons show ?thesis by simp
+ qed
+ qed
+ qed
+qed
+
+text {* Environments and code generation *}
+
+lemma [code, code del]:
+ "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
+
+lemma equal_env_code [code]:
+ fixes x y :: "'a\<Colon>equal"
+ and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
+ shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
+ HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
+ of None \<Rightarrow> (case g z
+ of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+ | Some a \<Rightarrow> (case g z
+ of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
+ and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
+ and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
+ and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
+proof (unfold equal)
+ have "f = g \<longleftrightarrow> (\<forall>z. case f z
+ of None \<Rightarrow> (case g z
+ of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+ | Some a \<Rightarrow> (case g z
+ of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
+ proof
+ assume ?lhs
+ then show ?rhs by (auto split: option.splits)
+ next
+ assume assm: ?rhs (is "\<forall>z. ?prop z")
+ show ?lhs
+ proof
+ fix z
+ from assm have "?prop z" ..
+ then show "f z = g z" by (auto split: option.splits)
+ qed
+ qed
+ then show "Env x f = Env y g \<longleftrightarrow>
+ x = y \<and> (\<forall>z\<in>UNIV. case f z
+ of None \<Rightarrow> (case g z
+ of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+ | Some a \<Rightarrow> (case g z
+ of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
+qed simp_all
+
+lemma [code nbe]:
+ "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
+ by (fact equal_refl)
+
+lemma [code, code del]:
+ "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
+
+end
--- a/src/HOL/Unix/Unix.thy Wed Aug 17 18:51:27 2011 +0200
+++ b/src/HOL/Unix/Unix.thy Wed Aug 17 18:52:21 2011 +0200
@@ -6,8 +6,7 @@
theory Unix
imports
- Main
- "~~/src/HOL/Library/Nested_Environment"
+ Nested_Environment
"~~/src/HOL/Library/List_Prefix"
begin
--- a/src/Pure/General/symbol.scala Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Pure/General/symbol.scala Wed Aug 17 18:52:21 2011 +0200
@@ -356,14 +356,15 @@
val ctrl_decoded: Set[Symbol] =
Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
- val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
- val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
-
- val bold_decoded = decode("\\<^bold>")
+ val sub_decoded = decode("\\<^sub>")
+ val sup_decoded = decode("\\<^sup>")
+ val isub_decoded = decode("\\<^isub>")
+ val isup_decoded = decode("\\<^isup>")
val bsub_decoded = decode("\\<^bsub>")
val esub_decoded = decode("\\<^esub>")
val bsup_decoded = decode("\\<^bsup>")
val esup_decoded = decode("\\<^esup>")
+ val bold_decoded = decode("\\<^bold>")
}
@@ -401,11 +402,13 @@
def is_controllable(sym: Symbol): Boolean =
!is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
- def is_subscript_decoded(sym: Symbol): Boolean = symbols.subscript_decoded.contains(sym)
- def is_superscript_decoded(sym: Symbol): Boolean = symbols.superscript_decoded.contains(sym)
- def is_bold_decoded(sym: Symbol): Boolean = sym == symbols.bold_decoded
- def is_bsub_decoded(sym: Symbol): Boolean = sym == symbols.bsub_decoded
- def is_esub_decoded(sym: Symbol): Boolean = sym == symbols.esub_decoded
- def is_bsup_decoded(sym: Symbol): Boolean = sym == symbols.bsup_decoded
- def is_esup_decoded(sym: Symbol): Boolean = sym == symbols.esup_decoded
+ def sub_decoded: Symbol = symbols.sub_decoded
+ def sup_decoded: Symbol = symbols.sup_decoded
+ def isub_decoded: Symbol = symbols.isub_decoded
+ def isup_decoded: Symbol = symbols.isup_decoded
+ def bsub_decoded: Symbol = symbols.bsub_decoded
+ def esub_decoded: Symbol = symbols.esub_decoded
+ def bsup_decoded: Symbol = symbols.bsup_decoded
+ def esup_decoded: Symbol = symbols.esup_decoded
+ def bold_decoded: Symbol = symbols.bold_decoded
}
--- a/src/Pure/Isar/proof_display.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML Wed Aug 17 18:52:21 2011 +0200
@@ -31,14 +31,18 @@
Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
else Pretty.str "<context>");
+fun default_context thy =
+ Context.cases Syntax.init_pretty_global I
+ (the_default (Context.Theory thy) (try ML_Context.the_generic_context ()));
+
fun pp_thm th =
let
- val thy = Thm.theory_of_thm th;
+ val ctxt = default_context (Thm.theory_of_thm th);
val flags = {quote = true, show_hyps = false, show_status = true};
- in Display.pretty_thm_raw (Syntax.init_pretty_global thy) flags th end;
+ in Display.pretty_thm_raw ctxt flags th end;
-val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
-val pp_term = Pretty.quote oo Syntax.pretty_term_global;
+fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
+fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
--- a/src/Pure/Isar/rule_insts.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML Wed Aug 17 18:52:21 2011 +0200
@@ -318,10 +318,9 @@
fun liftvar (Var ((a,j), T)) =
Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
| liftvar t = raise TERM("Variable expected", [t]);
- fun liftterm t = list_abs_free
- (param_names ~~ paramTs, Logic.incr_indexes(paramTs,inc) t)
- fun liftpair (cv,ct) =
- (cterm_fun liftvar cv, cterm_fun liftterm ct)
+ fun liftterm t =
+ fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
+ fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
val rule = Drule.instantiate_normalize
(map lifttvar envT', map liftpair cenv)
--- a/src/Pure/Syntax/syntax_trans.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Wed Aug 17 18:52:21 2011 +0200
@@ -125,13 +125,13 @@
fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
| lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
-fun absfree_proper (x, T, t) =
+fun absfree_proper (x, T) t =
if can Name.dest_internal x
then error ("Illegal internal variable in abstraction: " ^ quote x)
- else Term.absfree (x, T, t);
+ else absfree (x, T) t;
-fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
- | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
+fun abs_tr [Free x, t] = absfree_proper x t
+ | abs_tr [Const ("_idtdummy", T), t] = absdummy T t
| abs_tr [Const ("_constrain", _) $ x $ tT, t] =
Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
| abs_tr ts = raise TERM ("abs_tr", ts);
--- a/src/Pure/Thy/html.scala Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Pure/Thy/html.scala Wed Aug 17 18:52:21 2011 +0200
@@ -83,13 +83,15 @@
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
if (s1 == "\n") add(XML.elem(BR))
- else if (Symbol.is_bsub_decoded(s1)) t ++= s1 // FIXME
- else if (Symbol.is_esub_decoded(s1)) t ++= s1 // FIXME
- else if (Symbol.is_bsup_decoded(s1)) t ++= s1 // FIXME
- else if (Symbol.is_esup_decoded(s1)) t ++= s1 // FIXME
- else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
- else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
- else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
+ else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
+ { add(hidden(s1)); add(sub(s2())) }
+ else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
+ { add(hidden(s1)); add(sup(s2())) }
+ else if (s1 == Symbol.bsub_decoded) t ++= s1 // FIXME
+ else if (s1 == Symbol.esub_decoded) t ++= s1 // FIXME
+ else if (s1 == Symbol.bsup_decoded) t ++= s1 // FIXME
+ else if (s1 == Symbol.esup_decoded) t ++= s1 // FIXME
+ else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
else t ++= s1
}
--- a/src/Pure/primitive_defs.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Pure/primitive_defs.ML Wed Aug 17 18:52:21 2011 +0200
@@ -74,7 +74,7 @@
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
val (lhs', args) = Term.strip_comb lhs;
- val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
+ val rhs' = fold_rev (absfree o dest_Free) args rhs;
in (lhs', rhs') end;
end;
--- a/src/Pure/term.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Pure/term.ML Wed Aug 17 18:52:21 2011 +0200
@@ -95,9 +95,8 @@
val subst_free: (term * term) list -> term -> term
val abstract_over: term * term -> term
val lambda: term -> term -> term
- val absfree: string * typ * term -> term
- val absdummy: typ * term -> term
- val list_abs_free: (string * typ) list * term -> term
+ val absfree: string * typ -> term -> term
+ val absdummy: typ -> term -> term
val list_all_free: (string * typ) list * term -> term
val list_all: (string * typ) list * term -> term
val subst_atomic: (term * term) list -> term -> term
@@ -760,24 +759,18 @@
fun lambda v t = lambda_name ("", v) t;
-(*Form an abstraction over a free variable.*)
-fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
-fun absdummy (T, body) = Abs (Name.uu_, T, body);
-
-(*Abstraction over a list of free variables*)
-fun list_abs_free ([ ] , t) = t
- | list_abs_free ((a,T)::vars, t) =
- absfree(a, T, list_abs_free(vars,t));
+fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
+fun absdummy T body = Abs (Name.uu_, T, body);
(*Quantification over a list of free variables*)
fun list_all_free ([], t: term) = t
| list_all_free ((a,T)::vars, t) =
- (all T) $ (absfree(a, T, list_all_free(vars,t)));
+ all T $ absfree (a, T) (list_all_free (vars, t));
(*Quantification over a list of variables (already bound in body) *)
fun list_all ([], t) = t
| list_all ((a,T)::vars, t) =
- (all T) $ (Abs(a, T, list_all(vars,t)));
+ all T $ Abs (a, T, list_all (vars, t));
(*Replace the ATOMIC term ti by ui; inst = [(t1,u1), ..., (tn,un)].
A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *)
--- a/src/Tools/induct.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Tools/induct.ML Wed Aug 17 18:52:21 2011 +0200
@@ -658,7 +658,7 @@
fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
| goal_concl 0 xs B =
if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
- else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
+ else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
| goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
| goal_concl _ _ _ = NONE;
in
--- a/src/Tools/jEdit/src/Isabelle.props Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Wed Aug 17 18:52:21 2011 +0200
@@ -37,6 +37,11 @@
options.isabelle.auto-start.title=Auto Start
options.isabelle.auto-start=true
+#actions
+isabelle.input-isub.shortcut=C+e DOWN
+isabelle.input-isup.shortcut=C+e UP
+isabelle.input-bold.shortcut=C+e RIGHT
+
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
--- a/src/Tools/jEdit/src/actions.xml Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Tools/jEdit/src/actions.xml Wed Aug 17 18:52:21 2011 +0200
@@ -22,4 +22,40 @@
wm.addDockableWindow("isabelle-protocol");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.input-sub">
+ <CODE>
+ isabelle.jedit.Isabelle.input_sub(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.input-sup">
+ <CODE>
+ isabelle.jedit.Isabelle.input_sup(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.input-isub">
+ <CODE>
+ isabelle.jedit.Isabelle.input_isub(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.input-isup">
+ <CODE>
+ isabelle.jedit.Isabelle.input_isup(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.input-bsub">
+ <CODE>
+ isabelle.jedit.Isabelle.input_bsub(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.input-bsup">
+ <CODE>
+ isabelle.jedit.Isabelle.input_bsup(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.input-bold">
+ <CODE>
+ isabelle.jedit.Isabelle.input_bold(textArea);
+ </CODE>
+ </ACTION>
+
</ACTIONS>
\ No newline at end of file
--- a/src/Tools/jEdit/src/plugin.scala Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 17 18:52:21 2011 +0200
@@ -316,6 +316,24 @@
}
session.start(timeout, modes ::: List(logic))
}
+
+
+ /* convenience actions */
+
+ private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
+ {
+ s1.foreach(text_area.userInput(_))
+ s2.foreach(text_area.userInput(_))
+ s2.foreach(_ => text_area.goToPrevCharacter(false))
+ }
+
+ def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
+ def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
+ def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
+ def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
+ def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
+ def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
+ def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
}
--- a/src/Tools/jEdit/src/token_markup.scala Wed Aug 17 18:51:27 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Aug 17 18:52:21 2011 +0200
@@ -107,11 +107,11 @@
def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
{
- // FIXME Symbol.is_bsub_decoded etc.
+ // FIXME Symbol.bsub_decoded etc.
def ctrl_style(sym: String): Option[Byte => Byte] =
- if (Symbol.is_subscript_decoded(sym)) Some(subscript(_))
- else if (Symbol.is_superscript_decoded(sym)) Some(superscript(_))
- else if (Symbol.is_bold_decoded(sym)) Some(bold(_))
+ if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_))
+ else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_))
+ else if (sym == Symbol.bold_decoded) Some(bold(_))
else None
var result = Map[Text.Offset, Byte => Byte]()
--- a/src/ZF/Tools/datatype_package.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML Wed Aug 17 18:52:21 2011 +0200
@@ -235,7 +235,7 @@
Misc_Legacy.mk_defpair
(recursor_tm,
@{const Univ.Vrecursor} $
- absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
+ absfree ("rec", @{typ i}) (list_comb (case_const, recursor_cases)));
(* Build the new theory *)
--- a/src/ZF/Tools/inductive_package.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Aug 17 18:52:21 2011 +0200
@@ -127,8 +127,8 @@
val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
val fp_abs =
- absfree (X', Ind_Syntax.iT,
- Ind_Syntax.mk_Collect (z', dom_sum,
+ absfree (X', Ind_Syntax.iT)
+ (Ind_Syntax.mk_Collect (z', dom_sum,
Balanced_Tree.make FOLogic.mk_disj part_intrs));
val fp_rhs = Fp.oper $ dom_sum $ fp_abs
--- a/src/ZF/Tools/primrec_package.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/ZF/Tools/primrec_package.ML Wed Aug 17 18:52:21 2011 +0200
@@ -105,8 +105,8 @@
val cnames = map (#1 o dest_Const) constructors
and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites
- fun absterm (Free(a,T), body) = absfree (a,T,body)
- | absterm (t,body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
+ fun absterm (Free x, body) = absfree x body
+ | absterm (t, body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
(*Translate rec equations into function arguments suitable for recursor.
Missing cases are replaced by 0 and all cases are put into order.*)
--- a/src/ZF/ind_syntax.ML Wed Aug 17 18:51:27 2011 +0200
+++ b/src/ZF/ind_syntax.ML Wed Aug 17 18:52:21 2011 +0200
@@ -26,7 +26,7 @@
Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $
Term.betapply(P, Bound 0));
-fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
+fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT) t;
(*simple error-checking in the premises of an inductive definition*)
fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =