--- a/Admin/makedist Wed Nov 17 17:27:25 2010 +0100
+++ b/Admin/makedist Wed Nov 17 23:20:26 2010 +0100
@@ -108,7 +108,7 @@
if [ -z "$RELEASE" ]; then
DISTNAME="Isabelle_$DATE"
- DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
+ DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
else
DISTNAME="$RELEASE"
DISTVERSION="$DISTNAME: $DISTDATE"
--- a/Isabelle Wed Nov 17 17:27:25 2010 +0100
+++ b/Isabelle Wed Nov 17 23:20:26 2010 +0100
@@ -24,6 +24,6 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars
CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$ISABELLE_JAVA" \
+exec "$ISABELLE_TOOL" java \
"-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
-jar "$(jvmpath "$ISABELLE_HOME/lib/classes/isabelle-scala.jar")" "$@"
--- a/doc-src/System/Thy/Basics.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/doc-src/System/Thy/Basics.thy Wed Nov 17 23:20:26 2010 +0100
@@ -309,12 +309,18 @@
The root of component initialization is @{setting ISABELLE_HOME}
itself. After initializing all of its sub-components recursively,
@{setting ISABELLE_HOME_USER} is included in the same manner (if
- that directory exists). Thus users can easily add private
- components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}.
-
- It is also possible to initialize components programmatically via
- the \verb,init_component, shell function, say within the
- \verb,settings, script of another component.
+ that directory exists). This allows to install private components
+ via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+ often more convenient to do that programmatically via the
+ \verb,init_component, shell function in the \verb,etc/settings,
+ script of \verb,$ISABELLE_HOME_USER, (or any other component
+ directory). For example:
+ \begin{verbatim}
+ if [ -d "$HOME/screwdriver-2.0" ]
+ then
+ init_component "$HOME/screwdriver-2.0"
+ else
+ \end{verbatim}
*}
--- a/doc-src/System/Thy/document/Basics.tex Wed Nov 17 17:27:25 2010 +0100
+++ b/doc-src/System/Thy/document/Basics.tex Wed Nov 17 23:20:26 2010 +0100
@@ -318,12 +318,18 @@
The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}
itself. After initializing all of its sub-components recursively,
\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} is included in the same manner (if
- that directory exists). Thus users can easily add private
- components to \verb|$ISABELLE_HOME_USER/etc/components|.
-
- It is also possible to initialize components programmatically via
- the \verb,init_component, shell function, say within the
- \verb,settings, script of another component.%
+ that directory exists). This allows to install private components
+ via \verb|$ISABELLE_HOME_USER/etc/components|, although it is
+ often more convenient to do that programmatically via the
+ \verb,init_component, shell function in the \verb,etc/settings,
+ script of \verb,$ISABELLE_HOME_USER, (or any other component
+ directory). For example:
+ \begin{verbatim}
+ if [ -d "$HOME/screwdriver-2.0" ]
+ then
+ init_component "$HOME/screwdriver-2.0"
+ else
+ \end{verbatim}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/etc/settings Wed Nov 17 17:27:25 2010 +0100
+++ b/etc/settings Wed Nov 17 23:20:26 2010 +0100
@@ -55,7 +55,11 @@
### JVM components (Scala or Java)
###
-ISABELLE_JAVA="java"
+if [ -n "$JAVA_HOME" ]; then
+ ISABELLE_JAVA="$JAVA_HOME/bin/java"
+else
+ ISABELLE_JAVA="java"
+fi
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/lib/scripts/getsettings Wed Nov 17 17:27:25 2010 +0100
+++ b/lib/scripts/getsettings Wed Nov 17 23:20:26 2010 +0100
@@ -72,6 +72,7 @@
CLASSPATH="$CLASSPATH:$X"
fi
done
+ export CLASSPATH
}
#arrays
@@ -90,6 +91,13 @@
function init_component ()
{
local COMPONENT="$1"
+ case "$COMPONENT" in
+ /*) ;;
+ *)
+ echo >&2 "Absolute component path required: \"$COMPONENT\""
+ exit 2
+ ;;
+ esac
if [ ! -d "$COMPONENT" ]; then
echo >&2 "Bad Isabelle component: \"$COMPONENT\""
--- a/src/HOL/List.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOL/List.thy Wed Nov 17 23:20:26 2010 +0100
@@ -214,11 +214,10 @@
sublist :: "'a list => nat set => 'a list" where
"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
-primrec
- splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "splice [] ys = ys"
- | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))"
- -- {*Warning: simpset does not contain the second eqn but a derived one. *}
+fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"splice [] ys = ys" |
+"splice xs [] = xs" |
+"splice (x#xs) (y#ys) = x # y # splice xs ys"
text{*
\begin{figure}[htbp]
@@ -3477,21 +3476,14 @@
subsubsection {* @{const splice} *}
-lemma splice_Nil2 [simp, code]:
- "splice xs [] = xs"
+lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
by (cases xs) simp_all
-lemma splice_Cons_Cons [simp, code]:
- "splice (x#xs) (y#ys) = x # y # splice xs ys"
-by simp
-
-declare splice.simps(2) [simp del, code del]
+declare splice.simps(1,3)[code]
+declare splice.simps(2)[simp del]
lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
-apply(induct xs arbitrary: ys) apply simp
-apply(case_tac ys)
- apply auto
-done
+by (induct xs ys rule: splice.induct) auto
subsubsection {* Transpose *}
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 17 23:20:26 2010 +0100
@@ -89,7 +89,7 @@
lemma "Rep_unit () = True"
nitpick [expect = none]
-by (insert Rep_unit) (simp add: unit_def)
+by (insert Rep_unit) simp
lemma "Rep_unit () = False"
nitpick [expect = genuine]
--- a/src/HOL/Product_Type.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOL/Product_Type.thy Wed Nov 17 23:20:26 2010 +0100
@@ -37,7 +37,7 @@
subsection {* The @{text unit} type *}
-typedef unit = "{True}"
+typedef (open) unit = "{True}"
proof
show "True : ?unit" ..
qed
@@ -48,7 +48,7 @@
"() = Abs_unit True"
lemma unit_eq [no_atp]: "u = ()"
- by (induct u) (simp add: unit_def Unity_def)
+ by (induct u) (simp add: Unity_def)
text {*
Simplification procedure for @{thm [source] unit_eq}. Cannot use
--- a/src/HOLCF/Bifinite.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/Bifinite.thy Wed Nov 17 23:20:26 2010 +0100
@@ -88,8 +88,8 @@
definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
-definition cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
- where "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+definition sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
+ where "sfun_approx = (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
definition prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
where "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
@@ -119,9 +119,9 @@
using u_map_ID finite_deflation_u_map
unfolding u_approx_def by (rule approx_chain_lemma1)
-lemma cfun_approx: "approx_chain cfun_approx"
-using cfun_map_ID finite_deflation_cfun_map
-unfolding cfun_approx_def by (rule approx_chain_lemma2)
+lemma sfun_approx: "approx_chain sfun_approx"
+using sfun_map_ID finite_deflation_sfun_map
+unfolding sfun_approx_def by (rule approx_chain_lemma2)
lemma prod_approx: "approx_chain prod_approx"
using cprod_map_ID finite_deflation_cprod_map
@@ -211,8 +211,8 @@
definition u_defl :: "defl \<rightarrow> defl"
where "u_defl = defl_fun1 u_approx u_map"
-definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
- where "cfun_defl = defl_fun2 cfun_approx cfun_map"
+definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+ where "sfun_defl = defl_fun2 sfun_approx sfun_map"
definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
where "prod_defl = defl_fun2 prod_approx cprod_map"
@@ -229,11 +229,11 @@
using u_approx finite_deflation_u_map
unfolding u_defl_def by (rule cast_defl_fun1)
-lemma cast_cfun_defl:
- "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
- udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
-using cfun_approx finite_deflation_cfun_map
-unfolding cfun_defl_def by (rule cast_defl_fun2)
+lemma cast_sfun_defl:
+ "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
+ udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
+using sfun_approx finite_deflation_sfun_map
+unfolding sfun_defl_def by (rule cast_defl_fun2)
lemma cast_prod_defl:
"cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
@@ -393,21 +393,80 @@
lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
by (rule defl_u_def)
-subsubsection {* Continuous function space *}
+subsubsection {* Strict function space *}
-text {* TODO: Allow argument type to be a predomain. *}
-
-instantiation cfun :: ("domain", "domain") liftdomain
+instantiation sfun :: ("domain", "domain") liftdomain
begin
definition
- "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
+ "emb = udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb"
+
+definition
+ "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
+
+definition
+ "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+
+definition
+ "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
definition
- "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
+ "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)"
+
+instance
+using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def
+proof (rule liftdomain_class_intro)
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
+ unfolding emb_sfun_def prj_sfun_def
+ using ep_pair_udom [OF sfun_approx]
+ by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
+ show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
+ unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
+ by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)
+qed
+
+end
+
+lemma DEFL_sfun:
+ "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_sfun_def)
+
+subsubsection {* Continuous function space *}
+
+text {*
+ Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
+*}
definition
- "defl (t::('a \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
+
+definition
+ "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
+
+lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
+unfolding encode_cfun_def decode_cfun_def
+by (simp add: eta_cfun)
+
+lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
+unfolding encode_cfun_def decode_cfun_def
+apply (simp add: sfun_eq_iff strictify_cancel)
+apply (rule cfun_eqI, case_tac x, simp_all)
+done
+
+instantiation cfun :: (predomain, "domain") liftdomain
+begin
+
+definition
+ "emb = (udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb) oo encode_cfun"
+
+definition
+ "prj = decode_cfun oo (sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx)"
+
+definition
+ "defl (t::('a \<rightarrow> 'b) itself) = sfun_defl\<cdot>DEFL('a u)\<cdot>DEFL('b)"
definition
"(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
@@ -421,19 +480,24 @@
instance
using liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def
proof (rule liftdomain_class_intro)
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
+ have "ep_pair encode_cfun decode_cfun"
+ by (rule ep_pair.intro, simp_all)
+ thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
unfolding emb_cfun_def prj_cfun_def
- using ep_pair_udom [OF cfun_approx]
- by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
+ apply (rule ep_pair_comp)
+ apply (rule ep_pair_comp)
+ apply (intro ep_pair_sfun_map ep_pair_emb_prj)
+ apply (rule ep_pair_udom [OF sfun_approx])
+ done
show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
- unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map)
+ unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_sfun_defl
+ by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
qed
end
lemma DEFL_cfun:
- "DEFL('a::domain \<rightarrow> 'b::domain) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::predomain \<rightarrow> 'b::domain) = sfun_defl\<cdot>DEFL('a u)\<cdot>DEFL('b)"
by (rule defl_cfun_def)
subsubsection {* Cartesian product *}
--- a/src/HOLCF/ConvexPD.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy Wed Nov 17 23:20:26 2010 +0100
@@ -360,6 +360,11 @@
lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
+lemma convex_bind_bind:
+ "convex_bind\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>g =
+ convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}
--- a/src/HOLCF/Domain.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/Domain.thy Wed Nov 17 23:20:26 2010 +0100
@@ -237,13 +237,13 @@
unfolding isodefl_def
by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
-lemma isodefl_cfun:
+lemma isodefl_sfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
+ isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_cfun_defl cast_isodefl)
-apply (simp add: emb_cfun_def prj_cfun_def)
-apply (simp add: cfun_map_map cfcomp1)
+apply (simp add: cast_sfun_defl cast_isodefl)
+apply (simp add: emb_sfun_def prj_sfun_def)
+apply (simp add: sfun_map_map isodefl_strict)
done
lemma isodefl_ssum:
@@ -299,6 +299,23 @@
apply (simp add: cfcomp1 encode_prod_u_map cast_sprod_defl sprod_map_map)
done
+lemma encode_cfun_map:
+ "encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x))
+ = sfun_map\<cdot>(u_map\<cdot>f)\<cdot>g\<cdot>x"
+unfolding encode_cfun_def decode_cfun_def
+apply (simp add: sfun_eq_iff cfun_map_def sfun_map_def)
+apply (rule cfun_eqI, rename_tac y, case_tac y, simp_all)
+done
+
+lemma isodefl_cfun:
+ "isodefl (u_map\<cdot>d1) t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+ isodefl (cfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_sfun_defl cast_isodefl)
+apply (simp add: emb_cfun_def prj_cfun_def encode_cfun_map)
+apply (simp add: sfun_map_map isodefl_strict)
+done
+
subsection {* Setting up the domain package *}
use "Tools/Domain/domain_isomorphism.ML"
@@ -308,23 +325,24 @@
setup Domain_Isomorphism.setup
lemmas [domain_defl_simps] =
- DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
+ DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
liftdefl_eq LIFTDEFL_prod
lemmas [domain_map_ID] =
- cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
+ cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
lemmas [domain_isodefl] =
- isodefl_u isodefl_cfun isodefl_ssum isodefl_sprod
- isodefl_cprod isodefl_cprod_u
+ isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
+ isodefl_cfun isodefl_cprod isodefl_cprod_u
lemmas [domain_deflation] =
- deflation_cfun_map deflation_ssum_map deflation_sprod_map
- deflation_cprod_map deflation_u_map
+ deflation_cfun_map deflation_sfun_map deflation_ssum_map
+ deflation_sprod_map deflation_cprod_map deflation_u_map
setup {*
fold Domain_Take_Proofs.add_map_function
[(@{type_name cfun}, @{const_name cfun_map}, [true, true]),
+ (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]),
(@{type_name ssum}, @{const_name ssum_map}, [true, true]),
(@{type_name sprod}, @{const_name sprod_map}, [true, true]),
(@{type_name prod}, @{const_name cprod_map}, [true, true]),
--- a/src/HOLCF/IsaMakefile Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/IsaMakefile Wed Nov 17 23:20:26 2010 +0100
@@ -62,6 +62,7 @@
Porder.thy \
Powerdomains.thy \
Product_Cpo.thy \
+ Sfun.thy \
Sprod.thy \
Ssum.thy \
Tr.thy \
@@ -105,7 +106,6 @@
Library/Defl_Bifinite.thy \
Library/List_Cpo.thy \
Library/Stream.thy \
- Library/Strict_Fun.thy \
Library/Sum_Cpo.thy \
Library/HOLCF_Library.thy \
Library/ROOT.ML
--- a/src/HOLCF/Library/HOLCF_Library.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/Library/HOLCF_Library.thy Wed Nov 17 23:20:26 2010 +0100
@@ -3,7 +3,6 @@
Defl_Bifinite
List_Cpo
Stream
- Strict_Fun
Sum_Cpo
begin
--- a/src/HOLCF/Library/Strict_Fun.thy Wed Nov 17 17:27:25 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-(* Title: HOLCF/Library/Strict_Fun.thy
- Author: Brian Huffman
-*)
-
-header {* The Strict Function Type *}
-
-theory Strict_Fun
-imports HOLCF
-begin
-
-pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
- = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
-by simp_all
-
-type_notation (xsymbols)
- sfun (infixr "\<rightarrow>!" 0)
-
-text {* TODO: Define nice syntax for abstraction, application. *}
-
-definition
- sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
-where
- "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
-
-definition
- sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
-where
- "sfun_rep = (\<Lambda> f. Rep_sfun f)"
-
-lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
- unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
-
-lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
- unfolding sfun_rep_beta by (rule Rep_sfun_strict)
-
-lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
- unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
-
-lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
- by (simp add: cfun_eq_iff strictify_conv_if)
-
-lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
- unfolding sfun_abs_def sfun_rep_def
- apply (simp add: cont_Abs_sfun cont_Rep_sfun)
- apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
- apply (simp add: cfun_eq_iff strictify_conv_if)
- apply (simp add: Rep_sfun [simplified])
- done
-
-lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
- unfolding sfun_abs_def sfun_rep_def
- apply (simp add: cont_Abs_sfun cont_Rep_sfun)
- apply (simp add: Abs_sfun_inverse)
- done
-
-lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
-apply default
-apply (rule sfun_abs_sfun_rep)
-apply (simp add: cfun_below_iff strictify_conv_if)
-done
-
-interpretation sfun: ep_pair sfun_rep sfun_abs
- by (rule ep_pair_sfun)
-
-subsection {* Map functional for strict function space *}
-
-definition
- sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
-where
- "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
-
-lemma sfun_map_ID [domain_map_ID]: "sfun_map\<cdot>ID\<cdot>ID = ID"
- unfolding sfun_map_def
- by (simp add: cfun_map_ID cfun_eq_iff)
-
-lemma sfun_map_map:
- assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
- "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
- sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-unfolding sfun_map_def
-by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
-
-lemma ep_pair_sfun_map:
- assumes 1: "ep_pair e1 p1"
- assumes 2: "ep_pair e2 p2"
- shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)"
-proof
- interpret e1p1: pcpo_ep_pair e1 p1
- unfolding pcpo_ep_pair_def by fact
- interpret e2p2: pcpo_ep_pair e2 p2
- unfolding pcpo_ep_pair_def by fact
- fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
- unfolding sfun_map_def
- apply (simp add: sfun.e_eq_iff [symmetric] strictify_cancel)
- apply (rule ep_pair.e_inverse)
- apply (rule ep_pair_cfun_map [OF 1 2])
- done
- fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
- unfolding sfun_map_def
- apply (simp add: sfun.e_below_iff [symmetric] strictify_cancel)
- apply (rule ep_pair.e_p_below)
- apply (rule ep_pair_cfun_map [OF 1 2])
- done
-qed
-
-lemma deflation_sfun_map [domain_deflation]:
- assumes 1: "deflation d1"
- assumes 2: "deflation d2"
- shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
-apply (simp add: sfun_map_def)
-apply (rule deflation.intro)
-apply simp
-apply (subst strictify_cancel)
-apply (simp add: cfun_map_def deflation_strict 1 2)
-apply (simp add: cfun_map_def deflation.idem 1 2)
-apply (simp add: sfun.e_below_iff [symmetric])
-apply (subst strictify_cancel)
-apply (simp add: cfun_map_def deflation_strict 1 2)
-apply (rule deflation.below)
-apply (rule deflation_cfun_map [OF 1 2])
-done
-
-lemma finite_deflation_sfun_map:
- assumes 1: "finite_deflation d1"
- assumes 2: "finite_deflation d2"
- shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)"
-proof (intro finite_deflation.intro finite_deflation_axioms.intro)
- interpret d1: finite_deflation d1 by fact
- interpret d2: finite_deflation d2 by fact
- have "deflation d1" and "deflation d2" by fact+
- thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
- from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
- by (rule finite_deflation_cfun_map)
- then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
- by (rule finite_deflation.finite_fixes)
- moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
- by (rule inj_onI, simp)
- ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
- by (rule finite_vimageI)
- then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
- unfolding sfun_map_def sfun.e_eq_iff [symmetric]
- by (simp add: strictify_cancel
- deflation_strict `deflation d1` `deflation d2`)
-qed
-
-subsection {* Strict function space is a bifinite domain *}
-
-definition
- sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
-where
- "sfun_approx = (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma sfun_approx: "approx_chain sfun_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. sfun_approx i)"
- unfolding sfun_approx_def by simp
- show "(\<Squnion>i. sfun_approx i) = ID"
- unfolding sfun_approx_def
- by (simp add: lub_distribs sfun_map_ID)
- show "\<And>i. finite_deflation (sfun_approx i)"
- unfolding sfun_approx_def
- by (intro finite_deflation_sfun_map finite_deflation_udom_approx)
-qed
-
-definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
-where "sfun_defl = defl_fun2 sfun_approx sfun_map"
-
-lemma cast_sfun_defl:
- "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
- udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
-unfolding sfun_defl_def
-apply (rule cast_defl_fun2 [OF sfun_approx])
-apply (erule (1) finite_deflation_sfun_map)
-done
-
-instantiation sfun :: ("domain", "domain") liftdomain
-begin
-
-definition
- "emb = udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb"
-
-definition
- "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
-
-definition
- "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-
-definition
- "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
- "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
- "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)"
-
-instance
-using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def
-proof (rule liftdomain_class_intro)
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
- unfolding emb_sfun_def prj_sfun_def
- using ep_pair_udom [OF sfun_approx]
- by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
-next
- show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
- unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
- by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
-qed
-
-end
-
-lemma DEFL_sfun [domain_defl_simps]:
- "DEFL('a \<rightarrow>! 'b) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
-by (rule defl_sfun_def)
-
-lemma isodefl_sfun [domain_isodefl]:
- "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
-apply (rule isodeflI)
-apply (simp add: cast_sfun_defl cast_isodefl)
-apply (simp add: emb_sfun_def prj_sfun_def)
-apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation])
-done
-
-setup {*
- Domain_Take_Proofs.add_map_function
- (@{type_name "sfun"}, @{const_name sfun_map}, [true, true])
-*}
-
-end
--- a/src/HOLCF/LowerPD.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/LowerPD.thy Wed Nov 17 23:20:26 2010 +0100
@@ -353,6 +353,10 @@
lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)
+lemma lower_bind_bind:
+ "lower_bind\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>g = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}
--- a/src/HOLCF/Map_Functions.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/Map_Functions.thy Wed Nov 17 23:20:26 2010 +0100
@@ -380,4 +380,85 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
+subsection {* Map operator for strict function space *}
+
+definition
+ sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
+where
+ "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
+
+lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
+ unfolding sfun_map_def
+ by (simp add: cfun_map_ID cfun_eq_iff)
+
+lemma sfun_map_map:
+ assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
+ "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+unfolding sfun_map_def
+by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
+
+lemma ep_pair_sfun_map:
+ assumes 1: "ep_pair e1 p1"
+ assumes 2: "ep_pair e2 p2"
+ shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)"
+proof
+ interpret e1p1: pcpo_ep_pair e1 p1
+ unfolding pcpo_ep_pair_def by fact
+ interpret e2p2: pcpo_ep_pair e2 p2
+ unfolding pcpo_ep_pair_def by fact
+ fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
+ unfolding sfun_map_def
+ apply (simp add: sfun_eq_iff strictify_cancel)
+ apply (rule ep_pair.e_inverse)
+ apply (rule ep_pair_cfun_map [OF 1 2])
+ done
+ fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
+ unfolding sfun_map_def
+ apply (simp add: sfun_below_iff strictify_cancel)
+ apply (rule ep_pair.e_p_below)
+ apply (rule ep_pair_cfun_map [OF 1 2])
+ done
+qed
+
+lemma deflation_sfun_map:
+ assumes 1: "deflation d1"
+ assumes 2: "deflation d2"
+ shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
+apply (simp add: sfun_map_def)
+apply (rule deflation.intro)
+apply simp
+apply (subst strictify_cancel)
+apply (simp add: cfun_map_def deflation_strict 1 2)
+apply (simp add: cfun_map_def deflation.idem 1 2)
+apply (simp add: sfun_below_iff)
+apply (subst strictify_cancel)
+apply (simp add: cfun_map_def deflation_strict 1 2)
+apply (rule deflation.below)
+apply (rule deflation_cfun_map [OF 1 2])
+done
+
+lemma finite_deflation_sfun_map:
+ assumes 1: "finite_deflation d1"
+ assumes 2: "finite_deflation d2"
+ shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation_intro)
+ interpret d1: finite_deflation d1 by fact
+ interpret d2: finite_deflation d2 by fact
+ have "deflation d1" and "deflation d2" by fact+
+ thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
+ from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
+ by (rule finite_deflation_cfun_map)
+ then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+ by (rule finite_deflation.finite_fixes)
+ moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
+ by (rule inj_onI, simp add: sfun_eq_iff)
+ ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
+ by (rule finite_vimageI)
+ then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+ unfolding sfun_map_def sfun_eq_iff
+ by (simp add: strictify_cancel
+ deflation_strict `deflation d1` `deflation d2`)
+qed
+
end
--- a/src/HOLCF/Plain_HOLCF.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/Plain_HOLCF.thy Wed Nov 17 23:20:26 2010 +0100
@@ -5,7 +5,7 @@
header {* Plain HOLCF *}
theory Plain_HOLCF
-imports Cfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
+imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Sfun.thy Wed Nov 17 23:20:26 2010 +0100
@@ -0,0 +1,62 @@
+(* Title: HOLCF/Sfun.thy
+ Author: Brian Huffman
+*)
+
+header {* The Strict Function Type *}
+
+theory Sfun
+imports Cfun
+begin
+
+pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
+ = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
+by simp_all
+
+type_notation (xsymbols)
+ sfun (infixr "\<rightarrow>!" 0)
+
+text {* TODO: Define nice syntax for abstraction, application. *}
+
+definition
+ sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
+where
+ "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
+
+definition
+ sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
+where
+ "sfun_rep = (\<Lambda> f. Rep_sfun f)"
+
+lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
+ unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
+
+lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
+ unfolding sfun_rep_beta by (rule Rep_sfun_strict)
+
+lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
+ unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
+
+lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
+ by (simp add: cfun_eq_iff strictify_conv_if)
+
+lemma sfun_abs_sfun_rep [simp]: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
+ unfolding sfun_abs_def sfun_rep_def
+ apply (simp add: cont_Abs_sfun cont_Rep_sfun)
+ apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
+ apply (simp add: cfun_eq_iff strictify_conv_if)
+ apply (simp add: Rep_sfun [simplified])
+ done
+
+lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
+ unfolding sfun_abs_def sfun_rep_def
+ apply (simp add: cont_Abs_sfun cont_Rep_sfun)
+ apply (simp add: Abs_sfun_inverse)
+ done
+
+lemma sfun_eq_iff: "f = g \<longleftrightarrow> sfun_rep\<cdot>f = sfun_rep\<cdot>g"
+by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)
+
+lemma sfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> sfun_rep\<cdot>f \<sqsubseteq> sfun_rep\<cdot>g"
+by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)
+
+end
--- a/src/HOLCF/UpperPD.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/UpperPD.thy Wed Nov 17 23:20:26 2010 +0100
@@ -348,6 +348,10 @@
lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)
+lemma upper_bind_bind:
+ "upper_bind\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}
--- a/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 17 17:27:25 2010 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 17 23:20:26 2010 +0100
@@ -34,14 +34,14 @@
where
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3).
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
- , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
- , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
+ , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
+ , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
lemma foo_bar_baz_deflF_beta:
"foo_bar_baz_deflF\<cdot>a\<cdot>t =
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
- , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>DEFL(tr))
- , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>DEFL(tr)))"
+ , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
+ , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
unfolding foo_bar_baz_deflF_def
by (simp add: split_def)
@@ -68,10 +68,10 @@
"foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>DEFL(tr))"
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>DEFL(tr))"
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
text "The automation for the previous steps will be quite similar to
--- a/src/Pure/PIDE/command.scala Wed Nov 17 17:27:25 2010 +0100
+++ b/src/Pure/PIDE/command.scala Wed Nov 17 23:20:26 2010 +0100
@@ -54,7 +54,9 @@
val props = Position.purge(atts)
val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
state.add_markup(info)
- case _ => System.err.println("Ignored report message: " + msg); state
+ case _ =>
+ // FIXME System.err.println("Ignored report message: " + msg)
+ state
})
case XML.Elem(Markup(name, atts), body) =>
atts match {
--- a/src/Pure/System/gui_setup.scala Wed Nov 17 17:27:25 2010 +0100
+++ b/src/Pure/System/gui_setup.scala Wed Nov 17 23:20:26 2010 +0100
@@ -39,6 +39,7 @@
// values
if (Platform.is_windows)
text.append("Cygwin root: " + Cygwin.check_root() + "\n")
+ text.append("JVM name: " + System.getProperty("java.vm.name") + "\n")
text.append("JVM platform: " + Platform.jvm_platform + "\n")
try {
val isabelle_system = new Isabelle_System
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Nov 17 17:27:25 2010 +0100
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Nov 17 23:20:26 2010 +0100
@@ -24,7 +24,6 @@
echo " -m MODE add print mode for output"
echo
echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
- echo "(default ~/Scratch.thy)."
echo
exit 1
}
@@ -93,14 +92,10 @@
# args
-if [ "$#" -eq 0 ]; then
- ARGS["${#ARGS[@]}"]="Scratch.thy"
-else
- while [ "$#" -gt 0 ]; do
- ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
- shift
- done
-fi
+while [ "$#" -gt 0 ]; do
+ ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+ shift
+done
## default perspective