re-enable bisim code, now in domain_theorems.ML

--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 04:19:06 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 04:31:50 2010 -0800
@@ -11,14 +11,14 @@
 
   val calc_axioms :
       bool -> string Symtab.table ->
-      string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
+      Domain_Library.eq list -> int -> Domain_Library.eq ->
       string * (string * term) list * (string * term) list
 
   val add_axioms :
       bool ->
       ((string * typ list) *
        (binding * (bool * binding option * typ) list * mixfix) list) list ->
-      bstring -> Domain_Library.eq list -> theory -> theory
+      Domain_Library.eq list -> theory -> theory
 end;
 
 
@@ -51,7 +51,6 @@
 fun calc_axioms
     (definitional : bool)
     (map_tab : string Symtab.table)
-    (comp_dname : string)
     (eqs : eq list)
     (n : int)
     (eqn as ((dname,_),cons) : eq)
@@ -99,61 +98,18 @@
 fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
 
-fun add_axioms definitional eqs' comp_dnam (eqs : eq list) thy' =
+fun add_axioms definitional eqs' (eqs : eq list) thy' =
   let
-    val comp_dname = Sign.full_bname thy' comp_dnam;
     val dnames = map (fst o fst) eqs;
     val x_name = idx_name dnames "x"; 
 
-    fun one_con (con, _, args) =
-      let
-        val nonrec_args = filter_out is_rec args;
-        val    rec_args = filter is_rec args;
-        val    recs_cnt = length rec_args;
-        val allargs     = nonrec_args @ rec_args
-                          @ map (upd_vname (fn s=> s^"'")) rec_args;
-        val allvns      = map vname allargs;
-        fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
-        val vns1        = map (vname_arg "" ) args;
-        val vns2        = map (vname_arg "'") args;
-        val allargs_cnt = length nonrec_args + 2*recs_cnt;
-        val rec_idxs    = (recs_cnt-1) downto 0;
-        val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
-                                               (allargs~~((allargs_cnt-1) downto 0)));
-        fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
-                                Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
-        val capps =
-          List.foldr
-            mk_conj
-            (mk_conj(
-             Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
-             Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
-            (mapn rel_app 1 rec_args);
-      in
-        List.foldr
-          mk_ex
-          (Library.foldr mk_conj
-                         (map (defined o Bound) nonlazy_idxs,capps)) allvns
-      end;
-    fun one_comp n (_,cons) =
-        mk_all (x_name(n+1),
-        mk_all (x_name(n+1)^"'",
-        mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
-        foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
-                        ::map one_con cons))));
-(* TEMPORARILY DISABLED
-    val bisim_def =
-        ("bisim_def", %%:(comp_dname^"_bisim") ==
-                         mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
-TEMPORARILY DISABLED *)
-
     fun add_one (dnam, axs, dfs) =
         Sign.add_path dnam
           #> add_axioms_infer axs
           #> Sign.parent_path;
 
     val map_tab = Domain_Isomorphism.get_map_tab thy';
-    val axs = mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs;
+    val axs = mapn (calc_axioms definitional map_tab eqs) 0 eqs;
     val thy = thy' |> fold add_one axs;
 
     fun get_iso_info ((dname, tyvars), cons') =
@@ -211,11 +167,6 @@
     end;
   in
     thy
-    |> Sign.add_path comp_dnam
-(*
-    |> add_defs_infer [bisim_def]
-*)
-    |> Sign.parent_path
   end; (* let (add_axioms) *)
 
 end; (* struct *)

--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 04:19:06 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 04:31:50 2010 -0800
@@ -150,7 +150,7 @@
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
       check_and_sort_domain false dtnvs' cons'' thy'';
-    val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
+    val thy' = thy'' |> Domain_Syntax.add_syntax false eqs';
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
@@ -164,7 +164,7 @@
         ) : cons;
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-    val thy = thy' |> Domain_Axioms.add_axioms false eqs' comp_dnam eqs;
+    val thy = thy' |> Domain_Axioms.add_axioms false eqs' eqs;
     val ((rewss, take_rews), theorems_thy) =
         thy
           |> fold_map (fn (eq, (x,cs)) =>
@@ -223,7 +223,7 @@
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
              (eqs''' ~~ eqs'))
 
-    val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
+    val thy' = thy'' |> Domain_Syntax.add_syntax true eqs';
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
@@ -237,7 +237,7 @@
         ) : cons;
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-    val thy = thy' |> Domain_Axioms.add_axioms true eqs' comp_dnam eqs;
+    val thy = thy' |> Domain_Axioms.add_axioms true eqs' eqs;
     val ((rewss, take_rews), theorems_thy) =
         thy
           |> fold_map (fn (eq, (x,cs)) =>

--- a/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 04:19:06 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 04:31:50 2010 -0800
@@ -64,6 +64,7 @@
   val mk_return : term -> term;
   val list_ccomb : term * term list -> term;
   val con_app2 : string -> ('a -> term) -> 'a list -> term;
+  val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a
   val proj : term -> 'a list -> int -> term;
   val mk_ctuple_pat : term list -> term;
   val mk_branch : term -> term;

--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 04:19:06 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 04:31:50 2010 -0800
@@ -15,7 +15,6 @@
 
   val add_syntax:
       bool ->
-      string ->
       ((string * typ list) *
        (binding * (bool * binding option * typ) list * mixfix) list) list ->
       theory -> theory
@@ -48,8 +47,6 @@
     val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
     end;
 
-(* ----- constants concerning induction ------------------------------------- *)
-
     val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
 
     val optional_consts =
@@ -62,22 +59,14 @@
 
 fun add_syntax
     (definitional : bool)
-    (comp_dnam : string)
     (eqs' : ((string * typ list) *
              (binding * (bool * binding option * typ) list * mixfix) list) list)
     (thy'' : theory) =
   let
-    val dtypes  = map (Type o fst) eqs';
-    val boolT   = HOLogic.boolT;
-    val relprod =
-        foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
-    val const_bisim =
-        (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
     val ctt : (binding * typ * mixfix) list list =
         map (calc_syntax thy'' definitional) eqs';
   in thy''
-       |> Cont_Consts.add_consts
-           (flat ctt @ [const_bisim])
+       |> Cont_Consts.add_consts (flat ctt)
   end; (* let *)
 
 end; (* struct *)

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 04:19:06 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 04:31:50 2010 -0800
@@ -239,7 +239,6 @@
 
 fun comp_theorems (comp_dnam, eqs: eq list) thy =
 let
-val global_ctxt = ProofContext.init thy;
 val map_tab = Domain_Isomorphism.get_map_tab thy;
 
 val dnames = map (fst o fst) eqs;
@@ -247,6 +246,81 @@
 val comp_dname = Sign.full_bname thy comp_dnam;
 
 val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+
+(* ----- define bisimulation predicate -------------------------------------- *)
+
+local
+  open HOLCF_Library
+  val dtypes  = map (Type o fst) eqs;
+  val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes);
+  val bisim_bind = Binding.name (comp_dnam ^ "_bisim");
+  val bisim_type = relprod --> boolT;
+in
+  val (bisim_const, thy) =
+      Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy;
+end;
+
+local
+
+  fun legacy_infer_term thy t =
+      singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
+  fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+  fun infer_props thy = map (apsnd (legacy_infer_prop thy));
+  fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
+  fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
+
+  val comp_dname = Sign.full_bname thy comp_dnam;
+  val dnames = map (fst o fst) eqs;
+  val x_name = idx_name dnames "x"; 
+
+  fun one_con (con, _, args) =
+    let
+      val nonrec_args = filter_out is_rec args;
+      val    rec_args = filter is_rec args;
+      val    recs_cnt = length rec_args;
+      val allargs     = nonrec_args @ rec_args
+                        @ map (upd_vname (fn s=> s^"'")) rec_args;
+      val allvns      = map vname allargs;
+      fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
+      val vns1        = map (vname_arg "" ) args;
+      val vns2        = map (vname_arg "'") args;
+      val allargs_cnt = length nonrec_args + 2*recs_cnt;
+      val rec_idxs    = (recs_cnt-1) downto 0;
+      val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
+                                             (allargs~~((allargs_cnt-1) downto 0)));
+      fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
+                              Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
+      val capps =
+          List.foldr
+            mk_conj
+            (mk_conj(
+             Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
+             Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
+            (mapn rel_app 1 rec_args);
+    in
+      List.foldr
+        mk_ex
+        (Library.foldr mk_conj
+                       (map (defined o Bound) nonlazy_idxs,capps)) allvns
+    end;
+  fun one_comp n (_,cons) =
+      mk_all (x_name(n+1),
+      mk_all (x_name(n+1)^"'",
+      mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
+      foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
+                      ::map one_con cons))));
+  val bisim_eqn =
+      %%:(comp_dname^"_bisim") ==
+         mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs));
+
+in
+  val ([ax_bisim_def], thy) =
+      thy
+        |> Sign.add_path comp_dnam
+        |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)]
+        ||> Sign.parent_path;
+end; (* local *)
+
 val pg = pg' thy;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
@@ -258,9 +332,6 @@
   val axs_chain_take = map (ga "chain_take") dnames;
   val axs_lub_take   = map (ga "lub_take"  ) dnames;
   val axs_finite_def = map (ga "finite_def") dnames;
-(* TEMPORARILY DISABLED
-  val ax_bisim_def   =      ga "bisim_def" comp_dnam;
-TEMPORARILY DISABLED *)
 end;
 
 local
@@ -385,6 +456,8 @@
 
 (* ----- theorems concerning finiteness and induction ----------------------- *)
 
+  val global_ctxt = ProofContext.init thy;
+
   val _ = trace " Proving finites, ind...";
   val (finites, ind) =
   (
@@ -524,11 +597,10 @@
 
 (* ----- theorem concerning coinduction ------------------------------------- *)
 
-(* COINDUCTION TEMPORARILY DISABLED
 local
   val xs = mapn (fn n => K (x_name n)) 1 dnames;
   fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
-  val take_ss = HOL_ss addsimps take_rews;
+  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
   val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
   val _ = trace " Proving coind_lemma...";
   val coind_lemma =
@@ -575,7 +647,6 @@
         take_lemmas;
     in pg [] goal (K tacs) end;
 end; (* local *)
-COINDUCTION TEMPORARILY DISABLED *)
 
 val inducts = Project_Rule.projections (ProofContext.init thy) ind;
 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
@@ -587,8 +658,8 @@
            ((Binding.name "reach"      , axs_reach   ), []),
            ((Binding.name "finites"    , finites     ), []),
            ((Binding.name "finite_ind" , [finite_ind]), []),
-           ((Binding.name "ind"        , [ind]       ), [])(*,
-           ((Binding.name "coind"      , [coind]     ), [])*)]
+           ((Binding.name "ind"        , [ind]       ), []),
+           ((Binding.name "coind"      , [coind]     ), [])]
        |> (if induct_failed then I
            else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
        |> Sign.parent_path |> pair take_rews

--- a/src/HOLCF/ex/Domain_ex.thy	Tue Mar 02 04:19:06 2010 -0800
+++ b/src/HOLCF/ex/Domain_ex.thy	Tue Mar 02 04:31:50 2010 -0800
@@ -176,11 +176,9 @@
 thm tree.finites
 
 text {* Rules about bisimulation predicate *}
-(* COINDUCTION TEMPORARILY DISABLED
 term tree_bisim
 thm tree.bisim_def
 thm tree.coind
-COINDUCTION TEMPORARILY DISABLED *)
 
 text {* Induction rule *}
 thm tree.ind

--- a/src/HOLCF/ex/Stream.thy	Tue Mar 02 04:19:06 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy	Tue Mar 02 04:31:50 2010 -0800
@@ -266,21 +266,12 @@
 
 section "coinduction"
 
-(* COINDUCTION TEMPORARILY DISABLED
 lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 &  R (rt$s1) (rt$s2) ==> stream_bisim R"
  apply (simp add: stream.bisim_def,clarsimp)
- apply (case_tac "x=UU",clarsimp)
-  apply (erule_tac x="UU" in allE,simp)
-  apply (case_tac "x'=UU",simp)
-  apply (drule stream_exhaust_eq [THEN iffD1],auto)+
- apply (case_tac "x'=UU",auto)
-  apply (erule_tac x="a && y" in allE)
-  apply (erule_tac x="UU" in allE)+
-  apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
- apply (erule_tac x="a && y" in allE)
- apply (erule_tac x="aa && ya" in allE) back
+ apply (drule spec, drule spec, drule (1) mp)
+ apply (case_tac "x", simp)
+ apply (case_tac "x'", simp)
 by auto
-COINDUCTION TEMPORARILY DISABLED *)