--- a/src/HOL/IMP/Natural.thy Sat May 22 11:01:59 2010 +0200
+++ b/src/HOL/IMP/Natural.thy Sat May 22 16:46:18 2010 -0700
@@ -25,6 +25,16 @@
notation (xsymbols)
update ("_/[_ \<mapsto> /_]" [900,0,0] 900)
+text {* Disable conflicting syntax from HOL Map theory. *}
+
+no_syntax
+ "_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _")
+ "_maplets" :: "['a, 'a] => maplet" ("_ /[|->]/ _")
+ "" :: "maplet => maplets" ("_")
+ "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
+ "_MapUpd" :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
+ "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])")
+
text {*
The big-step execution relation @{text evalc} is defined inductively:
*}
@@ -111,7 +121,7 @@
in the same @{text s'}}. Formally:
*}
definition
- equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _") where
+ equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _" [56, 56] 55) where
"c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
text {*
--- a/src/HOLCF/Cfun.thy Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Cfun.thy Sat May 22 16:46:18 2010 -0700
@@ -100,7 +100,7 @@
subsection {* Continuous function space is pointed *}
lemma UU_CFun: "\<bottom> \<in> CFun"
-by (simp add: CFun_def inst_fun_pcpo cont_const)
+by (simp add: CFun_def inst_fun_pcpo)
instance cfun :: (finite_po, finite_po) finite_po
by (rule typedef_finite_po [OF type_definition_CFun])
@@ -139,9 +139,37 @@
lemma Abs_CFun_inverse2: "cont f \<Longrightarrow> Rep_CFun (Abs_CFun f) = f"
by (simp add: Abs_CFun_inverse CFun_def)
-lemma beta_cfun [simp]: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
+lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
by (simp add: Abs_CFun_inverse2)
+text {* Beta-reduction simproc *}
+
+text {*
+ Given the term @{term "(\<Lambda> x. f x)\<cdot>y"}, the procedure tries to
+ construct the theorem @{term "(\<Lambda> x. f x)\<cdot>y == f y"}. If this
+ theorem cannot be completely solved by the cont2cont rules, then
+ the procedure returns the ordinary conditional @{text beta_cfun}
+ rule.
+
+ The simproc does not solve any more goals that would be solved by
+ using @{text beta_cfun} as a simp rule. The advantage of the
+ simproc is that it can avoid deeply-nested calls to the simplifier
+ that would otherwise be caused by large continuity side conditions.
+*}
+
+simproc_setup beta_cfun_proc ("Abs_CFun f\<cdot>x") = {*
+ fn phi => fn ss => fn ct =>
+ let
+ val dest = Thm.dest_comb;
+ val (f, x) = (apfst (snd o dest o snd o dest) o dest) ct;
+ val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
+ val tr = instantiate' [SOME T, SOME U] [SOME f, SOME x]
+ (mk_meta_eq @{thm beta_cfun});
+ val rules = Cont2ContData.get (Simplifier.the_context ss);
+ val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
+ in SOME (perhaps (SINGLE (tac 1)) tr) end
+*}
+
text {* Eta-equality for continuous functions *}
lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f"
@@ -301,7 +329,7 @@
text {* cont2cont lemma for @{term Rep_CFun} *}
-lemma cont2cont_Rep_CFun [cont2cont]:
+lemma cont2cont_Rep_CFun [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes t: "cont (\<lambda>x. t x)"
shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
@@ -341,7 +369,7 @@
has only a single subgoal.
*}
-lemma cont2cont_LAM' [cont2cont]:
+lemma cont2cont_LAM' [simp, cont2cont]:
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
@@ -353,7 +381,7 @@
using f by (rule cont_fst_snd_D1)
qed
-lemma cont2cont_LAM_discrete [cont2cont]:
+lemma cont2cont_LAM_discrete [simp, cont2cont]:
"(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
by (simp add: cont2cont_LAM)
@@ -556,7 +584,7 @@
shows "cont (\<lambda>x. let y = f x in g x y)"
unfolding Let_def using f g2 g1 by (rule cont_apply)
-lemma cont2cont_Let' [cont2cont]:
+lemma cont2cont_Let' [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
shows "cont (\<lambda>x. let y = f x in g x y)"
--- a/src/HOLCF/Cont.thy Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Cont.thy Sat May 22 16:46:18 2010 -0700
@@ -120,7 +120,7 @@
apply (erule ch2ch_monofun [OF mono])
done
-subsection {* Continuity simproc *}
+subsection {* Collection of continuity rules *}
ML {*
structure Cont2ContData = Named_Thms
@@ -132,34 +132,18 @@
setup Cont2ContData.setup
-text {*
- Given the term @{term "cont f"}, the procedure tries to construct the
- theorem @{term "cont f == True"}. If this theorem cannot be completely
- solved by the introduction rules, then the procedure returns a
- conditional rewrite rule with the unsolved subgoals as premises.
-*}
-
-simproc_setup cont_proc ("cont f") = {*
- fn phi => fn ss => fn ct =>
- let
- val tr = instantiate' [] [SOME ct] @{thm Eq_TrueI};
- val rules = Cont2ContData.get (Simplifier.the_context ss);
- val tac = REPEAT_ALL_NEW (match_tac rules);
- in SINGLE (tac 1) tr end
-*}
-
subsection {* Continuity of basic functions *}
text {* The identity function is continuous *}
-lemma cont_id [cont2cont]: "cont (\<lambda>x. x)"
+lemma cont_id [simp, cont2cont]: "cont (\<lambda>x. x)"
apply (rule contI)
apply (erule cpo_lubI)
done
text {* constant functions are continuous *}
-lemma cont_const [cont2cont]: "cont (\<lambda>x. c)"
+lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
apply (rule contI)
apply (rule lub_const)
done
@@ -237,7 +221,7 @@
text {* functions with discrete domain *}
-lemma cont_discrete_cpo [cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
+lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
apply (rule contI)
apply (drule discrete_chain_const, clarify)
apply (simp add: lub_const)
--- a/src/HOLCF/Fixrec.thy Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Fixrec.thy Sat May 22 16:46:18 2010 -0700
@@ -586,23 +586,4 @@
hide_const (open) return fail run cases
-lemmas [fixrec_simp] =
- run_strict run_fail run_return
- mplus_strict mplus_fail mplus_return
- spair_strict_iff
- sinl_defined_iff
- sinr_defined_iff
- up_defined
- ONE_defined
- dist_eq_tr(1,2)
- match_UU_simps
- match_cpair_simps
- match_spair_simps
- match_sinl_simps
- match_sinr_simps
- match_up_simps
- match_ONE_simps
- match_TT_simps
- match_FF_simps
-
end
--- a/src/HOLCF/IMP/Denotational.thy Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/IMP/Denotational.thy Sat May 22 16:46:18 2010 -0700
@@ -7,6 +7,16 @@
theory Denotational imports HOLCF "../../HOL/IMP/Natural" begin
+text {* Disable conflicting syntax from HOL Map theory. *}
+
+no_syntax
+ "_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _")
+ "_maplets" :: "['a, 'a] => maplet" ("_ /[|->]/ _")
+ "" :: "maplet => maplets" ("_")
+ "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
+ "_MapUpd" :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
+ "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])")
+
subsection "Definition"
definition
--- a/src/HOLCF/Product_Cpo.thy Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Product_Cpo.thy Sat May 22 16:46:18 2010 -0700
@@ -221,7 +221,7 @@
apply (erule cpo_lubI [OF ch2ch_snd])
done
-lemma cont2cont_Pair [cont2cont]:
+lemma cont2cont_Pair [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. (f x, g x))"
@@ -230,9 +230,9 @@
apply (rule cont_const)
done
-lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst]
+lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
-lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd]
+lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
lemma cont2cont_split:
assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
@@ -256,7 +256,7 @@
"cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
by (drule cont_compose [OF _ cont_pair2], simp)
-lemma cont2cont_split' [cont2cont]:
+lemma cont2cont_split' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. split (f x) (g x))"
--- a/src/HOLCF/Sum_Cpo.thy Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Sum_Cpo.thy Sat May 22 16:46:18 2010 -0700
@@ -136,8 +136,8 @@
lemma cont_Inr: "cont Inr"
by (intro contI is_lub_Inr cpo_lubI)
-lemmas cont2cont_Inl [cont2cont] = cont_compose [OF cont_Inl]
-lemmas cont2cont_Inr [cont2cont] = cont_compose [OF cont_Inr]
+lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl]
+lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr]
lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
@@ -168,7 +168,7 @@
apply (rule cont_sum_case1 [OF f1 g1])
done
-lemma cont2cont_sum_case' [cont2cont]:
+lemma cont2cont_sum_case' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
assumes h: "cont (\<lambda>x. h x)"
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat May 22 16:46:18 2010 -0700
@@ -42,14 +42,13 @@
(************************** miscellaneous functions ***************************)
-val simple_ss =
- HOL_basic_ss addsimps simp_thms;
+val simple_ss = HOL_basic_ss addsimps simp_thms;
-val beta_ss =
- HOL_basic_ss
- addsimps simp_thms
- addsimps [@{thm beta_cfun}]
- addsimprocs [@{simproc cont_proc}];
+val beta_rules =
+ @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
+
+val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
fun define_consts
(specs : (binding * term * mixfix) list)
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat May 22 16:46:18 2010 -0700
@@ -34,11 +34,11 @@
structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
struct
-val beta_ss =
- HOL_basic_ss
- addsimps simp_thms
- addsimps [@{thm beta_cfun}]
- addsimprocs [@{simproc cont_proc}];
+val beta_rules =
+ @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_split'};
+
+val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
val beta_tac = simp_tac beta_ss;
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat May 22 16:46:18 2010 -0700
@@ -101,11 +101,11 @@
take_induct_thms : thm list
};
-val beta_ss =
- HOL_basic_ss
- addsimps simp_thms
- addsimps [@{thm beta_cfun}]
- addsimprocs [@{simproc cont_proc}];
+val beta_rules =
+ @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
+
+val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
val beta_tac = simp_tac beta_ss;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat May 22 16:46:18 2010 -0700
@@ -198,7 +198,6 @@
fun qualified name = Binding.qualified true name dbind;
val simp = Simplifier.simp_add;
-val fixrec_simp = Fixrec.fixrec_simp_add;
in
thy
@@ -209,7 +208,7 @@
[Rule_Cases.case_names case_ns, Induct.cases_type dname]),
((qualified "when_rews" , when_rews ), [simp]),
((qualified "compacts" , compacts ), [simp]),
- ((qualified "con_rews" , con_rews ), [simp, fixrec_simp]),
+ ((qualified "con_rews" , con_rews ), [simp]),
((qualified "sel_rews" , sel_rews ), [simp]),
((qualified "dis_rews" , dis_rews ), [simp]),
((qualified "pat_rews" , pat_rews ), [simp]),
@@ -218,7 +217,7 @@
((qualified "inverts" , inverts ), [simp]),
((qualified "injects" , injects ), [simp]),
((qualified "take_rews" , take_rews ), [simp]),
- ((qualified "match_rews", mat_rews ), [simp, fixrec_simp])]
+ ((qualified "match_rews", mat_rews ), [simp])]
|> snd
|> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
pat_rews @ dist_les @ dist_eqs)
--- a/src/HOLCF/Tools/fixrec.ML Sat May 22 11:01:59 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Sat May 22 16:46:18 2010 -0700
@@ -13,8 +13,6 @@
val add_fixpat: Thm.binding * term list -> theory -> theory
val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
val add_matchers: (string * string) list -> theory -> theory
- val fixrec_simp_add: attribute
- val fixrec_simp_del: attribute
val fixrec_simp_tac: Proof.context -> int -> tactic
val setup: theory -> theory
end;
@@ -135,7 +133,10 @@
"The error occurred for the goal statement:\n" ^
Syntax.string_of_term lthy prop);
fun check th = case Thm.nprems_of th of 0 => all_tac th | n => err ();
- val tac = simp_tac (simpset_of lthy) 1 THEN check;
+ val rules = Cont2ContData.get lthy;
+ val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
+ val slow_tac = simp_tac (simpset_of lthy);
+ val tac = (fast_tac 1 ORELSE slow_tac 1) THEN check;
in
Goal.prove lthy [] [] prop (K tac)
end;
@@ -304,22 +305,12 @@
(********************** Proving associated theorems **********************)
(*************************************************************************)
-structure FixrecSimpData = Generic_Data
-(
- type T = simpset;
- val empty =
- HOL_basic_ss
- addsimps simp_thms
- addsimps [@{thm beta_cfun}]
- addsimprocs [@{simproc cont_proc}];
- val extend = I;
- val merge = merge_ss;
-);
+fun eta_tac i = CONVERSION Thm.eta_conversion i;
fun fixrec_simp_tac ctxt =
let
val tab = FixrecUnfoldData.get (Context.Proof ctxt);
- val ss = Simplifier.context ctxt (FixrecSimpData.get (Context.Proof ctxt));
+ val ss = Simplifier.simpset_of ctxt;
fun concl t =
if Logic.is_all t then concl (snd (Logic.dest_all t))
else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);
@@ -330,26 +321,18 @@
val unfold_thm = the (Symtab.lookup tab c);
val rule = unfold_thm RS @{thm ssubst_lhs};
in
- CHANGED (rtac rule i THEN asm_simp_tac ss i)
+ CHANGED (rtac rule i THEN eta_tac i THEN asm_simp_tac ss i)
end
in
SUBGOAL (fn ti => the_default no_tac (try tac ti))
end;
-val fixrec_simp_add : attribute =
- Thm.declaration_attribute
- (fn th => FixrecSimpData.map (fn ss => ss addsimps [th]));
-
-val fixrec_simp_del : attribute =
- Thm.declaration_attribute
- (fn th => FixrecSimpData.map (fn ss => ss delsimps [th]));
-
(* proves a block of pattern matching equations as theorems, using unfold *)
fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
let
- val ss = Simplifier.context ctxt (FixrecSimpData.get (Context.Proof ctxt));
+ val ss = Simplifier.simpset_of ctxt;
val rule = unfold_thm RS @{thm ssubst_lhs};
- val tac = rtac rule 1 THEN asm_simp_tac ss 1;
+ val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ss 1;
fun prove_term t = Goal.prove ctxt [] [] t (K tac);
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
in
@@ -463,11 +446,8 @@
(Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
val setup =
- Attrib.setup @{binding fixrec_simp}
- (Attrib.add_del fixrec_simp_add fixrec_simp_del)
- "declaration of fixrec simp rule"
- #> Method.setup @{binding fixrec_simp}
- (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
- "pattern prover for fixrec constants";
+ Method.setup @{binding fixrec_simp}
+ (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
+ "pattern prover for fixrec constants";
end;