# HG changeset patch # User huffman # Date 1267533110 28800 # Node ID 979706bd5c16e1de1195ae2fc36222da6f3a6839 # Parent 9ed6a6d6615bd1092755231675eae0f8e80f2d41 re-enable bisim code, now in domain_theorems.ML diff -r 9ed6a6d6615b -r 979706bd5c16 src/HOLCF/Tools/Domain/domain_axioms.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 *) diff -r 9ed6a6d6615b -r 979706bd5c16 src/HOLCF/Tools/Domain/domain_extender.ML --- 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)) => diff -r 9ed6a6d6615b -r 979706bd5c16 src/HOLCF/Tools/Domain/domain_library.ML --- 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; diff -r 9ed6a6d6615b -r 979706bd5c16 src/HOLCF/Tools/Domain/domain_syntax.ML --- 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 *) diff -r 9ed6a6d6615b -r 979706bd5c16 src/HOLCF/Tools/Domain/domain_theorems.ML --- 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 diff -r 9ed6a6d6615b -r 979706bd5c16 src/HOLCF/ex/Domain_ex.thy --- 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 diff -r 9ed6a6d6615b -r 979706bd5c16 src/HOLCF/ex/Stream.thy --- 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 *)