# HG changeset patch
# User huffman
# Date 1290815399 28800
# Node ID 35781a159d1cc9bf06e119caf589e5aeb84b28f9
# Parent  2037021f034f1cb75f7a5c8aa570bf1ab0b55e19# Parent  a71f786d20da9103006db08007a36bef2e3f37c3
merged

diff -r a71f786d20da -r 35781a159d1c src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/Cont.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -97,22 +97,26 @@
 done
 
 lemma contI2:
+  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
   assumes mono: "monofun f"
   assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
      \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
   shows "cont f"
-apply (rule contI)
-apply (rule thelubE)
-apply (erule ch2ch_monofun [OF mono])
-apply (rule below_antisym)
-apply (rule is_lub_thelub)
-apply (erule ch2ch_monofun [OF mono])
-apply (rule ub2ub_monofun [OF mono])
-apply (rule is_lubD1)
-apply (erule cpo_lubI)
-apply (rule below, assumption)
-apply (erule ch2ch_monofun [OF mono])
-done
+proof (rule contI)
+  fix Y :: "nat \<Rightarrow> 'a"
+  assume Y: "chain Y"
+  with mono have fY: "chain (\<lambda>i. f (Y i))"
+    by (rule ch2ch_monofun)
+  have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)"
+    apply (rule below_antisym)
+    apply (rule lub_below [OF fY])
+    apply (rule monofunE [OF mono])
+    apply (rule is_ub_thelub [OF Y])
+    apply (rule below [OF Y fY])
+    done
+  with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
+    by (rule thelubE)
+qed
 
 subsection {* Collection of continuity rules *}
 
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/Domain.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -340,13 +340,13 @@
   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]),
-     (@{type_name "u"}, @{const_name u_map}, [true])]
+  fold Domain_Take_Proofs.add_rec_type
+    [(@{type_name cfun}, [true, true]),
+     (@{type_name "sfun"}, [true, true]),
+     (@{type_name ssum}, [true, true]),
+     (@{type_name sprod}, [true, true]),
+     (@{type_name prod}, [true, true]),
+     (@{type_name "u"}, [true])]
 *}
 
 end
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/Fixrec.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -26,10 +26,6 @@
   succeed :: "'a \<rightarrow> 'a match" where
   "succeed = (\<Lambda> x. Abs_match (sinr\<cdot>(up\<cdot>x)))"
 
-definition
-  match_case :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a match \<rightarrow> 'b::pcpo" where
-  "match_case = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_match m))"
-
 lemma matchE [case_names bottom fail succeed, cases type: match]:
   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = succeed\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 unfolding fail_def succeed_def
@@ -52,40 +48,31 @@
   "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x"
 by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)
 
-lemma match_case_simps [simp]:
-  "match_case\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
-  "match_case\<cdot>f\<cdot>r\<cdot>fail = f"
-  "match_case\<cdot>f\<cdot>r\<cdot>(succeed\<cdot>x) = r\<cdot>x"
-by (simp_all add: succeed_def fail_def match_case_def cont_Rep_match
-                  cont2cont_LAM
-                  cont_Abs_match Abs_match_inverse Rep_match_strict)
-
-translations
-  "case m of XCONST fail \<Rightarrow> t1 | XCONST succeed\<cdot>x \<Rightarrow> t2"
-    == "CONST match_case\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
-
 subsubsection {* Run operator *}
 
 definition
   run :: "'a match \<rightarrow> 'a::pcpo" where
-  "run = match_case\<cdot>\<bottom>\<cdot>ID"
+  "run = (\<Lambda> m. sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)\<cdot>(Rep_match m))"
 
 text {* rewrite rules for run *}
 
 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
-by (simp add: run_def)
+unfolding run_def
+by (simp add: cont_Rep_match Rep_match_strict)
 
 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
-by (simp add: run_def)
+unfolding run_def fail_def
+by (simp add: cont_Rep_match Abs_match_inverse)
 
 lemma run_succeed [simp]: "run\<cdot>(succeed\<cdot>x) = x"
-by (simp add: run_def)
+unfolding run_def succeed_def
+by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
 
 subsubsection {* Monad plus operator *}
 
 definition
   mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where
-  "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | succeed\<cdot>x \<Rightarrow> m1)"
+  "mplus = (\<Lambda> m1 m2. sscase\<cdot>(\<Lambda> _. m2)\<cdot>(\<Lambda> _. m1)\<cdot>(Rep_match m1))"
 
 abbreviation
   mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match"  (infixr "+++" 65)  where
@@ -93,14 +80,19 @@
 
 text {* rewrite rules for mplus *}
 
+lemmas cont2cont_Rep_match = cont_Rep_match [THEN cont_compose]
+
 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
-by (simp add: mplus_def)
+unfolding mplus_def
+by (simp add: cont2cont_Rep_match Rep_match_strict)
 
 lemma mplus_fail [simp]: "fail +++ m = m"
-by (simp add: mplus_def)
+unfolding mplus_def fail_def
+by (simp add: cont2cont_Rep_match Abs_match_inverse)
 
 lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x"
-by (simp add: mplus_def)
+unfolding mplus_def succeed_def
+by (simp add: cont2cont_Rep_match cont_Abs_match Abs_match_inverse)
 
 lemma mplus_fail2 [simp]: "m +++ fail = m"
 by (cases m, simp_all)
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/LowerPD.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -195,7 +195,7 @@
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
-lemma lower_plus_below_iff:
+lemma lower_plus_below_iff [simp]:
   "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
 apply safe
 apply (erule below_trans [OF lower_plus_below1])
@@ -203,7 +203,7 @@
 apply (erule (1) lower_plus_least)
 done
 
-lemma lower_unit_below_plus_iff:
+lemma lower_unit_below_plus_iff [simp]:
   "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
 apply (induct x rule: compact_basis.principal_induct, simp)
 apply (induct ys rule: lower_pd.principal_induct, simp)
@@ -328,7 +328,7 @@
 apply (erule lower_le_induct, safe)
 apply (simp add: monofun_cfun)
 apply (simp add: rev_below_trans [OF lower_plus_below1])
-apply (simp add: lower_plus_below_iff)
+apply simp
 done
 
 definition
@@ -389,14 +389,14 @@
 apply default
 apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
 apply (induct_tac y rule: lower_pd_induct)
-apply (simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
 done
 
 lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
 apply default
 apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
 apply (induct_tac x rule: lower_pd_induct)
-apply (simp_all add: deflation.below monofun_cfun)
+apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)
 done
 
 (* FIXME: long proof! *)
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/Powerdomains.thy
--- a/src/HOLCF/Powerdomains.thy	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/Powerdomains.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -42,10 +42,10 @@
   deflation_upper_map deflation_lower_map deflation_convex_map
 
 setup {*
-  fold Domain_Take_Proofs.add_map_function
-    [(@{type_name "upper_pd"}, @{const_name upper_map}, [true]),
-     (@{type_name "lower_pd"}, @{const_name lower_map}, [true]),
-     (@{type_name "convex_pd"}, @{const_name convex_map}, [true])]
+  fold Domain_Take_Proofs.add_rec_type
+    [(@{type_name "upper_pd"}, [true]),
+     (@{type_name "lower_pd"}, [true]),
+     (@{type_name "convex_pd"}, [true])]
 *}
 
 end
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/Tools/Domain/domain.ML
--- a/src/HOLCF/Tools/Domain/domain.ML	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -118,14 +118,14 @@
     (* test for free type variables, illegal sort constraints on rhs,
        non-pcpo-types and invalid use of recursive type;
        replace sorts in type variables on rhs *)
-    val map_tab = Domain_Take_Proofs.get_map_tab thy;
+    val rec_tab = Domain_Take_Proofs.get_rec_tab thy;
     fun check_rec rec_ok (T as TFree (v,_))  =
         if AList.defined (op =) sorts v then T
         else error ("Free type variable " ^ quote v ^ " on rhs.")
       | check_rec rec_ok (T as Type (s, Ts)) =
         (case AList.lookup (op =) dtnvs' s of
           NONE =>
-            let val rec_ok' = rec_ok andalso Symtab.defined map_tab s;
+            let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s;
             in Type (s, map (check_rec rec_ok') Ts) end
         | SOME typevars =>
           if typevars <> Ts
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -350,17 +350,17 @@
       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
         (conjuncts deflation_map_binds deflation_map_thm);
 
-    (* register map functions in theory data *)
+    (* register indirect recursion in theory data *)
     local
-      fun register_map ((dname, map_name), args) =
-          Domain_Take_Proofs.add_map_function (dname, map_name, args);
+      fun register_map (dname, args) =
+        Domain_Take_Proofs.add_rec_type (dname, args);
       val dnames = map (fst o dest_Type o fst) dom_eqns;
       val map_names = map (fst o dest_Const) map_consts;
       fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => [];
       val argss = map args dom_eqns;
     in
       val thy =
-          fold register_map (dnames ~~ map_names ~~ argss) thy;
+          fold register_map (dnames ~~ argss) thy;
     end;
 
     (* register deflation theorems *)
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Nov 26 15:49:59 2010 -0800
@@ -55,8 +55,8 @@
   val map_of_typ :
     theory -> (typ * term) list -> typ -> term
 
-  val add_map_function : (string * string * bool list) -> theory -> theory
-  val get_map_tab : theory -> (string * bool list) Symtab.table
+  val add_rec_type : (string * bool list) -> theory -> theory
+  val get_rec_tab : theory -> (bool list) Symtab.table
   val add_deflation_thm : thm -> theory -> theory
   val get_deflation_thms : theory -> thm list
   val map_ID_add : attribute
@@ -119,12 +119,10 @@
 (******************************** theory data *********************************)
 (******************************************************************************)
 
-structure MapData = Theory_Data
+structure Rec_Data = Theory_Data
 (
-  (* constant names like "foo_map" *)
-  (* list indicates which type arguments correspond to map arguments *)
-  (* alternatively, which type arguments allow indirect recursion *)
-  type T = (string * bool list) Symtab.table;
+  (* list indicates which type arguments allow indirect recursion *)
+  type T = (bool list) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
@@ -142,13 +140,13 @@
   val description = "theorems like foo_map$ID = ID"
 );
 
-fun add_map_function (tname, map_name, bs) =
-    MapData.map (Symtab.insert (K true) (tname, (map_name, bs)));
+fun add_rec_type (tname, bs) =
+    Rec_Data.map (Symtab.insert (K true) (tname, bs));
 
 fun add_deflation_thm thm =
     Context.theory_map (DeflMapData.add_thm thm);
 
-val get_map_tab = MapData.get;
+val get_rec_tab = Rec_Data.get;
 fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
 
 val map_ID_add = Map_Id_Data.add;
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/UpperPD.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -193,7 +193,7 @@
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
-lemma upper_below_plus_iff:
+lemma upper_below_plus_iff [simp]:
   "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
 apply safe
 apply (erule below_trans [OF _ upper_plus_below1])
@@ -201,7 +201,7 @@
 apply (erule (1) upper_plus_greatest)
 done
 
-lemma upper_plus_below_unit_iff:
+lemma upper_plus_below_unit_iff [simp]:
   "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
 apply (induct xs rule: upper_pd.principal_induct, simp)
 apply (induct ys rule: upper_pd.principal_induct, simp)
@@ -323,7 +323,7 @@
 apply (erule upper_le_induct, safe)
 apply (simp add: monofun_cfun)
 apply (simp add: below_trans [OF upper_plus_below1])
-apply (simp add: upper_below_plus_iff)
+apply simp
 done
 
 definition
@@ -384,14 +384,14 @@
 apply default
 apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
 apply (induct_tac y rule: upper_pd_induct)
-apply (simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff)
 done
 
 lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
 apply default
 apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
 apply (induct_tac x rule: upper_pd_induct)
-apply (simp_all add: deflation.below monofun_cfun)
+apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff)
 done
 
 (* FIXME: long proof! *)
diff -r a71f786d20da -r 35781a159d1c src/HOLCF/ex/Pattern_Match.thy
--- a/src/HOLCF/ex/Pattern_Match.thy	Sat Nov 27 00:00:54 2010 +0100
+++ b/src/HOLCF/ex/Pattern_Match.thy	Fri Nov 26 15:49:59 2010 -0800
@@ -53,11 +53,24 @@
 
 lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
 
+subsection {* Bind operator for match monad *}
+
+definition match_bind :: "'a match \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> 'b match" where
+  "match_bind = (\<Lambda> m k. sscase\<cdot>(\<Lambda> _. fail)\<cdot>(fup\<cdot>k)\<cdot>(Rep_match m))"
+
+lemma match_bind_simps [simp]:
+  "match_bind\<cdot>\<bottom>\<cdot>k = \<bottom>"
+  "match_bind\<cdot>fail\<cdot>k = fail"
+  "match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
+unfolding match_bind_def fail_def succeed_def
+by (simp_all add: cont2cont_Rep_match cont_Abs_match
+  Rep_match_strict Abs_match_inverse)
+
 subsection {* Case branch combinator *}
 
 definition
   branch :: "('a \<rightarrow> 'b match) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c match)" where
-  "branch p \<equiv> \<Lambda> r x. match_case\<cdot>fail\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
+  "branch p \<equiv> \<Lambda> r x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))"
 
 lemma branch_simps:
   "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
@@ -72,7 +85,7 @@
 
 definition
   cases :: "'a match \<rightarrow> 'a::pcpo" where
-  "cases = match_case\<cdot>\<bottom>\<cdot>ID"
+  "cases = Fixrec.run"
 
 text {* rewrite rules for cases *}
 
@@ -165,7 +178,7 @@
 definition
   cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
   "cpair_pat p1 p2 = (\<Lambda>(x, y).
-    match_case\<cdot>fail\<cdot>(\<Lambda> a. match_case\<cdot>fail\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))\<cdot>(p2\<cdot>y))\<cdot>(p1\<cdot>x))"
+    match_bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. match_bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))))"
 
 definition
   spair_pat ::
@@ -313,7 +326,7 @@
 
 definition
   as_pat :: "('a \<rightarrow> 'b match) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) match" where
-  "as_pat p = (\<Lambda> x. match_case\<cdot>fail\<cdot>(\<Lambda> a. succeed\<cdot>(x, a))\<cdot>(p\<cdot>x))"
+  "as_pat p = (\<Lambda> x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. succeed\<cdot>(x, a)))"
 
 definition
   lazy_pat :: "('a \<rightarrow> 'b::pcpo match) \<Rightarrow> ('a \<rightarrow> 'b match)" where
@@ -544,7 +557,7 @@
           val (fun1, fun2, taken) = pat_lhs (pat, args);
           val defs = @{thm branch_def} :: pat_defs;
           val goal = mk_trp (mk_strict fun1);
-          val rules = @{thms match_case_simps} @ case_rews;
+          val rules = @{thms match_bind_simps} @ case_rews;
           val tacs = [simp_tac (beta_ss addsimps rules) 1];
         in prove thy defs goal (K tacs) end;
       fun pat_apps (i, (pat, (con, args))) =
@@ -559,7 +572,7 @@
               val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
               val goal = Logic.list_implies (assms, concl);
               val defs = @{thm branch_def} :: pat_defs;
-              val rules = @{thms match_case_simps} @ case_rews;
+              val rules = @{thms match_bind_simps} @ case_rews;
               val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
             in prove thy defs goal (K tacs) end;
         in map_index pat_app spec end;