re-enable bisim code, now in domain_theorems.ML
authorhuffman
Tue Mar 02 04:31:50 2010 -0800 (2010-03-02)
changeset 35497979706bd5c16
parent 35496 9ed6a6d6615b
child 35498 5c70de748522
re-enable bisim code, now in domain_theorems.ML
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/Domain/domain_syntax.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/ex/Domain_ex.thy
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 04:19:06 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 04:31:50 2010 -0800
     1.3 @@ -11,14 +11,14 @@
     1.4  
     1.5    val calc_axioms :
     1.6        bool -> string Symtab.table ->
     1.7 -      string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
     1.8 +      Domain_Library.eq list -> int -> Domain_Library.eq ->
     1.9        string * (string * term) list * (string * term) list
    1.10  
    1.11    val add_axioms :
    1.12        bool ->
    1.13        ((string * typ list) *
    1.14         (binding * (bool * binding option * typ) list * mixfix) list) list ->
    1.15 -      bstring -> Domain_Library.eq list -> theory -> theory
    1.16 +      Domain_Library.eq list -> theory -> theory
    1.17  end;
    1.18  
    1.19  
    1.20 @@ -51,7 +51,6 @@
    1.21  fun calc_axioms
    1.22      (definitional : bool)
    1.23      (map_tab : string Symtab.table)
    1.24 -    (comp_dname : string)
    1.25      (eqs : eq list)
    1.26      (n : int)
    1.27      (eqn as ((dname,_),cons) : eq)
    1.28 @@ -99,61 +98,18 @@
    1.29  fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
    1.30  fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
    1.31  
    1.32 -fun add_axioms definitional eqs' comp_dnam (eqs : eq list) thy' =
    1.33 +fun add_axioms definitional eqs' (eqs : eq list) thy' =
    1.34    let
    1.35 -    val comp_dname = Sign.full_bname thy' comp_dnam;
    1.36      val dnames = map (fst o fst) eqs;
    1.37      val x_name = idx_name dnames "x"; 
    1.38  
    1.39 -    fun one_con (con, _, args) =
    1.40 -      let
    1.41 -        val nonrec_args = filter_out is_rec args;
    1.42 -        val    rec_args = filter is_rec args;
    1.43 -        val    recs_cnt = length rec_args;
    1.44 -        val allargs     = nonrec_args @ rec_args
    1.45 -                          @ map (upd_vname (fn s=> s^"'")) rec_args;
    1.46 -        val allvns      = map vname allargs;
    1.47 -        fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
    1.48 -        val vns1        = map (vname_arg "" ) args;
    1.49 -        val vns2        = map (vname_arg "'") args;
    1.50 -        val allargs_cnt = length nonrec_args + 2*recs_cnt;
    1.51 -        val rec_idxs    = (recs_cnt-1) downto 0;
    1.52 -        val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
    1.53 -                                               (allargs~~((allargs_cnt-1) downto 0)));
    1.54 -        fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
    1.55 -                                Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
    1.56 -        val capps =
    1.57 -          List.foldr
    1.58 -            mk_conj
    1.59 -            (mk_conj(
    1.60 -             Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
    1.61 -             Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
    1.62 -            (mapn rel_app 1 rec_args);
    1.63 -      in
    1.64 -        List.foldr
    1.65 -          mk_ex
    1.66 -          (Library.foldr mk_conj
    1.67 -                         (map (defined o Bound) nonlazy_idxs,capps)) allvns
    1.68 -      end;
    1.69 -    fun one_comp n (_,cons) =
    1.70 -        mk_all (x_name(n+1),
    1.71 -        mk_all (x_name(n+1)^"'",
    1.72 -        mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
    1.73 -        foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
    1.74 -                        ::map one_con cons))));
    1.75 -(* TEMPORARILY DISABLED
    1.76 -    val bisim_def =
    1.77 -        ("bisim_def", %%:(comp_dname^"_bisim") ==
    1.78 -                         mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
    1.79 -TEMPORARILY DISABLED *)
    1.80 -
    1.81      fun add_one (dnam, axs, dfs) =
    1.82          Sign.add_path dnam
    1.83            #> add_axioms_infer axs
    1.84            #> Sign.parent_path;
    1.85  
    1.86      val map_tab = Domain_Isomorphism.get_map_tab thy';
    1.87 -    val axs = mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs;
    1.88 +    val axs = mapn (calc_axioms definitional map_tab eqs) 0 eqs;
    1.89      val thy = thy' |> fold add_one axs;
    1.90  
    1.91      fun get_iso_info ((dname, tyvars), cons') =
    1.92 @@ -211,11 +167,6 @@
    1.93      end;
    1.94    in
    1.95      thy
    1.96 -    |> Sign.add_path comp_dnam
    1.97 -(*
    1.98 -    |> add_defs_infer [bisim_def]
    1.99 -*)
   1.100 -    |> Sign.parent_path
   1.101    end; (* let (add_axioms) *)
   1.102  
   1.103  end; (* struct *)
     2.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 04:19:06 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 04:31:50 2010 -0800
     2.3 @@ -150,7 +150,7 @@
     2.4      val eqs' : ((string * typ list) *
     2.5          (binding * (bool * binding option * typ) list * mixfix) list) list =
     2.6        check_and_sort_domain false dtnvs' cons'' thy'';
     2.7 -    val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
     2.8 +    val thy' = thy'' |> Domain_Syntax.add_syntax false eqs';
     2.9      val dts  = map (Type o fst) eqs';
    2.10      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
    2.11      fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
    2.12 @@ -164,7 +164,7 @@
    2.13          ) : cons;
    2.14      val eqs : eq list =
    2.15          map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
    2.16 -    val thy = thy' |> Domain_Axioms.add_axioms false eqs' comp_dnam eqs;
    2.17 +    val thy = thy' |> Domain_Axioms.add_axioms false eqs' eqs;
    2.18      val ((rewss, take_rews), theorems_thy) =
    2.19          thy
    2.20            |> fold_map (fn (eq, (x,cs)) =>
    2.21 @@ -223,7 +223,7 @@
    2.22                   (map fst vs, dname, mx, mk_eq_typ eq, NONE))
    2.23               (eqs''' ~~ eqs'))
    2.24  
    2.25 -    val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
    2.26 +    val thy' = thy'' |> Domain_Syntax.add_syntax true eqs';
    2.27      val dts  = map (Type o fst) eqs';
    2.28      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
    2.29      fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
    2.30 @@ -237,7 +237,7 @@
    2.31          ) : cons;
    2.32      val eqs : eq list =
    2.33          map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
    2.34 -    val thy = thy' |> Domain_Axioms.add_axioms true eqs' comp_dnam eqs;
    2.35 +    val thy = thy' |> Domain_Axioms.add_axioms true eqs' eqs;
    2.36      val ((rewss, take_rews), theorems_thy) =
    2.37          thy
    2.38            |> fold_map (fn (eq, (x,cs)) =>
     3.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 04:19:06 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 04:31:50 2010 -0800
     3.3 @@ -64,6 +64,7 @@
     3.4    val mk_return : term -> term;
     3.5    val list_ccomb : term * term list -> term;
     3.6    val con_app2 : string -> ('a -> term) -> 'a list -> term;
     3.7 +  val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a
     3.8    val proj : term -> 'a list -> int -> term;
     3.9    val mk_ctuple_pat : term list -> term;
    3.10    val mk_branch : term -> term;
     4.1 --- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 04:19:06 2010 -0800
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 04:31:50 2010 -0800
     4.3 @@ -15,7 +15,6 @@
     4.4  
     4.5    val add_syntax:
     4.6        bool ->
     4.7 -      string ->
     4.8        ((string * typ list) *
     4.9         (binding * (bool * binding option * typ) list * mixfix) list) list ->
    4.10        theory -> theory
    4.11 @@ -48,8 +47,6 @@
    4.12      val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
    4.13      end;
    4.14  
    4.15 -(* ----- constants concerning induction ------------------------------------- *)
    4.16 -
    4.17      val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
    4.18  
    4.19      val optional_consts =
    4.20 @@ -62,22 +59,14 @@
    4.21  
    4.22  fun add_syntax
    4.23      (definitional : bool)
    4.24 -    (comp_dnam : string)
    4.25      (eqs' : ((string * typ list) *
    4.26               (binding * (bool * binding option * typ) list * mixfix) list) list)
    4.27      (thy'' : theory) =
    4.28    let
    4.29 -    val dtypes  = map (Type o fst) eqs';
    4.30 -    val boolT   = HOLogic.boolT;
    4.31 -    val relprod =
    4.32 -        foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
    4.33 -    val const_bisim =
    4.34 -        (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
    4.35      val ctt : (binding * typ * mixfix) list list =
    4.36          map (calc_syntax thy'' definitional) eqs';
    4.37    in thy''
    4.38 -       |> Cont_Consts.add_consts
    4.39 -           (flat ctt @ [const_bisim])
    4.40 +       |> Cont_Consts.add_consts (flat ctt)
    4.41    end; (* let *)
    4.42  
    4.43  end; (* struct *)
     5.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 04:19:06 2010 -0800
     5.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 04:31:50 2010 -0800
     5.3 @@ -239,7 +239,6 @@
     5.4  
     5.5  fun comp_theorems (comp_dnam, eqs: eq list) thy =
     5.6  let
     5.7 -val global_ctxt = ProofContext.init thy;
     5.8  val map_tab = Domain_Isomorphism.get_map_tab thy;
     5.9  
    5.10  val dnames = map (fst o fst) eqs;
    5.11 @@ -247,6 +246,81 @@
    5.12  val comp_dname = Sign.full_bname thy comp_dnam;
    5.13  
    5.14  val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
    5.15 +
    5.16 +(* ----- define bisimulation predicate -------------------------------------- *)
    5.17 +
    5.18 +local
    5.19 +  open HOLCF_Library
    5.20 +  val dtypes  = map (Type o fst) eqs;
    5.21 +  val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes);
    5.22 +  val bisim_bind = Binding.name (comp_dnam ^ "_bisim");
    5.23 +  val bisim_type = relprod --> boolT;
    5.24 +in
    5.25 +  val (bisim_const, thy) =
    5.26 +      Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy;
    5.27 +end;
    5.28 +
    5.29 +local
    5.30 +
    5.31 +  fun legacy_infer_term thy t =
    5.32 +      singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
    5.33 +  fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
    5.34 +  fun infer_props thy = map (apsnd (legacy_infer_prop thy));
    5.35 +  fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
    5.36 +  fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
    5.37 +
    5.38 +  val comp_dname = Sign.full_bname thy comp_dnam;
    5.39 +  val dnames = map (fst o fst) eqs;
    5.40 +  val x_name = idx_name dnames "x"; 
    5.41 +
    5.42 +  fun one_con (con, _, args) =
    5.43 +    let
    5.44 +      val nonrec_args = filter_out is_rec args;
    5.45 +      val    rec_args = filter is_rec args;
    5.46 +      val    recs_cnt = length rec_args;
    5.47 +      val allargs     = nonrec_args @ rec_args
    5.48 +                        @ map (upd_vname (fn s=> s^"'")) rec_args;
    5.49 +      val allvns      = map vname allargs;
    5.50 +      fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
    5.51 +      val vns1        = map (vname_arg "" ) args;
    5.52 +      val vns2        = map (vname_arg "'") args;
    5.53 +      val allargs_cnt = length nonrec_args + 2*recs_cnt;
    5.54 +      val rec_idxs    = (recs_cnt-1) downto 0;
    5.55 +      val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
    5.56 +                                             (allargs~~((allargs_cnt-1) downto 0)));
    5.57 +      fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
    5.58 +                              Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
    5.59 +      val capps =
    5.60 +          List.foldr
    5.61 +            mk_conj
    5.62 +            (mk_conj(
    5.63 +             Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
    5.64 +             Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
    5.65 +            (mapn rel_app 1 rec_args);
    5.66 +    in
    5.67 +      List.foldr
    5.68 +        mk_ex
    5.69 +        (Library.foldr mk_conj
    5.70 +                       (map (defined o Bound) nonlazy_idxs,capps)) allvns
    5.71 +    end;
    5.72 +  fun one_comp n (_,cons) =
    5.73 +      mk_all (x_name(n+1),
    5.74 +      mk_all (x_name(n+1)^"'",
    5.75 +      mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
    5.76 +      foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
    5.77 +                      ::map one_con cons))));
    5.78 +  val bisim_eqn =
    5.79 +      %%:(comp_dname^"_bisim") ==
    5.80 +         mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs));
    5.81 +
    5.82 +in
    5.83 +  val ([ax_bisim_def], thy) =
    5.84 +      thy
    5.85 +        |> Sign.add_path comp_dnam
    5.86 +        |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)]
    5.87 +        ||> Sign.parent_path;
    5.88 +end; (* local *)
    5.89 +
    5.90  val pg = pg' thy;
    5.91  
    5.92  (* ----- getting the composite axiom and definitions ------------------------ *)
    5.93 @@ -258,9 +332,6 @@
    5.94    val axs_chain_take = map (ga "chain_take") dnames;
    5.95    val axs_lub_take   = map (ga "lub_take"  ) dnames;
    5.96    val axs_finite_def = map (ga "finite_def") dnames;
    5.97 -(* TEMPORARILY DISABLED
    5.98 -  val ax_bisim_def   =      ga "bisim_def" comp_dnam;
    5.99 -TEMPORARILY DISABLED *)
   5.100  end;
   5.101  
   5.102  local
   5.103 @@ -385,6 +456,8 @@
   5.104  
   5.105  (* ----- theorems concerning finiteness and induction ----------------------- *)
   5.106  
   5.107 +  val global_ctxt = ProofContext.init thy;
   5.108 +
   5.109    val _ = trace " Proving finites, ind...";
   5.110    val (finites, ind) =
   5.111    (
   5.112 @@ -524,11 +597,10 @@
   5.113  
   5.114  (* ----- theorem concerning coinduction ------------------------------------- *)
   5.115  
   5.116 -(* COINDUCTION TEMPORARILY DISABLED
   5.117  local
   5.118    val xs = mapn (fn n => K (x_name n)) 1 dnames;
   5.119    fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
   5.120 -  val take_ss = HOL_ss addsimps take_rews;
   5.121 +  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
   5.122    val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
   5.123    val _ = trace " Proving coind_lemma...";
   5.124    val coind_lemma =
   5.125 @@ -575,7 +647,6 @@
   5.126          take_lemmas;
   5.127      in pg [] goal (K tacs) end;
   5.128  end; (* local *)
   5.129 -COINDUCTION TEMPORARILY DISABLED *)
   5.130  
   5.131  val inducts = Project_Rule.projections (ProofContext.init thy) ind;
   5.132  fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
   5.133 @@ -587,8 +658,8 @@
   5.134             ((Binding.name "reach"      , axs_reach   ), []),
   5.135             ((Binding.name "finites"    , finites     ), []),
   5.136             ((Binding.name "finite_ind" , [finite_ind]), []),
   5.137 -           ((Binding.name "ind"        , [ind]       ), [])(*,
   5.138 -           ((Binding.name "coind"      , [coind]     ), [])*)]
   5.139 +           ((Binding.name "ind"        , [ind]       ), []),
   5.140 +           ((Binding.name "coind"      , [coind]     ), [])]
   5.141         |> (if induct_failed then I
   5.142             else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
   5.143         |> Sign.parent_path |> pair take_rews
     6.1 --- a/src/HOLCF/ex/Domain_ex.thy	Tue Mar 02 04:19:06 2010 -0800
     6.2 +++ b/src/HOLCF/ex/Domain_ex.thy	Tue Mar 02 04:31:50 2010 -0800
     6.3 @@ -176,11 +176,9 @@
     6.4  thm tree.finites
     6.5  
     6.6  text {* Rules about bisimulation predicate *}
     6.7 -(* COINDUCTION TEMPORARILY DISABLED
     6.8  term tree_bisim
     6.9  thm tree.bisim_def
    6.10  thm tree.coind
    6.11 -COINDUCTION TEMPORARILY DISABLED *)
    6.12  
    6.13  text {* Induction rule *}
    6.14  thm tree.ind
     7.1 --- a/src/HOLCF/ex/Stream.thy	Tue Mar 02 04:19:06 2010 -0800
     7.2 +++ b/src/HOLCF/ex/Stream.thy	Tue Mar 02 04:31:50 2010 -0800
     7.3 @@ -266,21 +266,12 @@
     7.4  
     7.5  section "coinduction"
     7.6  
     7.7 -(* COINDUCTION TEMPORARILY DISABLED
     7.8  lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 &  R (rt$s1) (rt$s2) ==> stream_bisim R"
     7.9   apply (simp add: stream.bisim_def,clarsimp)
    7.10 - apply (case_tac "x=UU",clarsimp)
    7.11 -  apply (erule_tac x="UU" in allE,simp)
    7.12 -  apply (case_tac "x'=UU",simp)
    7.13 -  apply (drule stream_exhaust_eq [THEN iffD1],auto)+
    7.14 - apply (case_tac "x'=UU",auto)
    7.15 -  apply (erule_tac x="a && y" in allE)
    7.16 -  apply (erule_tac x="UU" in allE)+
    7.17 -  apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
    7.18 - apply (erule_tac x="a && y" in allE)
    7.19 - apply (erule_tac x="aa && ya" in allE) back
    7.20 + apply (drule spec, drule spec, drule (1) mp)
    7.21 + apply (case_tac "x", simp)
    7.22 + apply (case_tac "x'", simp)
    7.23  by auto
    7.24 -COINDUCTION TEMPORARILY DISABLED *)
    7.25  
    7.26  
    7.27