# HG changeset patch # User huffman # Date 1287635211 25200 # Node ID 6547d0f079ed8d5608150f95b90282d1c969d266 # Parent ba2e41c8b725abcb54c9c02e160e9e9d25672315# Parent 767a28027b685981aee27d2988938d98879edc0c merged diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Algebraic.thy --- a/src/HOLCF/Algebraic.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Algebraic.thy Wed Oct 20 21:26:51 2010 -0700 @@ -211,43 +211,4 @@ lemma cast_strict2 [simp]: "cast\A\\ = \" by (rule cast.below [THEN UU_I]) -subsection {* Deflation membership relation *} - -definition - in_defl :: "udom \ defl \ bool" (infixl ":::" 50) -where - "x ::: A \ cast\A\x = x" - -lemma adm_in_defl: "adm (\x. x ::: A)" -unfolding in_defl_def by simp - -lemma in_deflI: "cast\A\x = x \ x ::: A" -unfolding in_defl_def . - -lemma cast_fixed: "x ::: A \ cast\A\x = x" -unfolding in_defl_def . - -lemma cast_in_defl [simp]: "cast\A\x ::: A" -unfolding in_defl_def by (rule cast.idem) - -lemma bottom_in_defl [simp]: "\ ::: A" -unfolding in_defl_def by (rule cast_strict2) - -lemma defl_belowD: "A \ B \ x ::: A \ x ::: B" -unfolding in_defl_def - apply (rule deflation.belowD) - apply (rule deflation_cast) - apply (erule monofun_cfun_arg) - apply assumption -done - -lemma rev_defl_belowD: "x ::: A \ A \ B \ x ::: B" -by (rule defl_belowD) - -lemma defl_belowI: "(\x. x ::: A \ x ::: B) \ A \ B" -apply (rule cast_below_imp_below) -apply (rule cast.belowI) -apply (simp add: in_defl_def) -done - end diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Cfun.thy Wed Oct 20 21:26:51 2010 -0700 @@ -534,32 +534,28 @@ default_sort pcpo definition - strictify :: "('a \ 'b) \ 'a \ 'b" where - "strictify = (\ f x. if x = \ then \ else f\x)" + strict :: "'a \ 'b \ 'b" where + "strict = (\ x. if x = \ then \ else ID)" -text {* results about strictify *} +lemma cont_strict: "cont (\x. if x = \ then \ else y)" +unfolding cont_def is_lub_def is_ub_def ball_simps +by (simp add: lub_eq_bottom_iff) -lemma cont_strictify1: "cont (\f. if x = \ then \ else f\x)" -by simp +lemma strict_conv_if: "strict\x = (if x = \ then \ else ID)" +unfolding strict_def by (simp add: cont_strict) -lemma monofun_strictify2: "monofun (\x. if x = \ then \ else f\x)" -apply (rule monofunI) -apply (auto simp add: monofun_cfun_arg) -done +lemma strict1 [simp]: "strict\\ = \" +by (simp add: strict_conv_if) -lemma cont_strictify2: "cont (\x. if x = \ then \ else f\x)" -apply (rule contI2) -apply (rule monofun_strictify2) -apply (case_tac "(\i. Y i) = \", simp) -apply (simp add: contlub_cfun_arg del: if_image_distrib) -apply (drule chain_UU_I_inverse2, clarify, rename_tac j) -apply (rule lub_mono2, rule_tac x=j in exI, simp_all) -apply (auto dest!: chain_mono_less) -done +lemma strict2 [simp]: "x \ \ \ strict\x = ID" +by (simp add: strict_conv_if) + + definition + strictify :: "('a \ 'b) \ 'a \ 'b" where + "strictify = (\ f x. strict\x\(f\x))" lemma strictify_conv_if: "strictify\f\x = (if x = \ then \ else f\x)" - unfolding strictify_def - by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM) +unfolding strictify_def by simp lemma strictify1 [simp]: "strictify\f\\ = \" by (simp add: strictify_conv_if) diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Domain.thy Wed Oct 20 21:26:51 2010 -0700 @@ -11,8 +11,8 @@ ("Tools/cont_proc.ML") ("Tools/Domain/domain_constructors.ML") ("Tools/Domain/domain_axioms.ML") - ("Tools/Domain/domain_theorems.ML") - ("Tools/Domain/domain_extender.ML") + ("Tools/Domain/domain_induction.ML") + ("Tools/Domain/domain.ML") begin default_sort pcpo @@ -20,61 +20,31 @@ subsection {* Casedist *} +text {* Lemmas for proving nchotomy rule: *} + lemma ex_one_defined_iff: "(\x. P x \ x \ \) = P ONE" - apply safe - apply (rule_tac p=x in oneE) - apply simp - apply simp - apply force - done +by simp lemma ex_up_defined_iff: "(\x. P x \ x \ \) = (\x. P (up\x))" - apply safe - apply (rule_tac p=x in upE) - apply simp - apply fast - apply (force intro!: up_defined) - done +by (safe, case_tac x, auto) lemma ex_sprod_defined_iff: "(\y. P y \ y \ \) = (\x y. (P (:x, y:) \ x \ \) \ y \ \)" - apply safe - apply (rule_tac p=y in sprodE) - apply simp - apply fast - apply (force intro!: spair_defined) - done +by (safe, case_tac y, auto) lemma ex_sprod_up_defined_iff: "(\y. P y \ y \ \) = (\x y. P (:up\x, y:) \ y \ \)" - apply safe - apply (rule_tac p=y in sprodE) - apply simp - apply (rule_tac p=x in upE) - apply simp - apply fast - apply (force intro!: spair_defined) - done +by (safe, case_tac y, simp, case_tac x, auto) lemma ex_ssum_defined_iff: "(\x. P x \ x \ \) = ((\x. P (sinl\x) \ x \ \) \ (\x. P (sinr\x) \ x \ \))" - apply (rule iffI) - apply (erule exE) - apply (erule conjE) - apply (rule_tac p=x in ssumE) - apply simp - apply (rule disjI1, fast) - apply (rule disjI2, fast) - apply (erule disjE) - apply force - apply force - done +by (safe, case_tac x, auto) lemma exh_start: "p = \ \ (\x. p = x \ x \ \)" by auto @@ -86,7 +56,7 @@ ex_up_defined_iff ex_one_defined_iff -text {* Rules for turning exh into casedist *} +text {* Rules for turning nchotomy into exhaust: *} lemma exh_casedist0: "\R; R \ P\ \ P" (* like make_elim *) by auto @@ -103,23 +73,11 @@ lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3 -subsection {* Combinators for building copy functions *} - -lemmas domain_map_stricts = - ssum_map_strict sprod_map_strict u_map_strict - -lemmas domain_map_simps = - ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up - - subsection {* Installing the domain package *} lemmas con_strict_rules = sinl_strict sinr_strict spair_strict1 spair_strict2 -lemmas con_defin_rules = - sinl_defined sinr_defined spair_defined up_defined ONE_defined - lemmas con_defined_iff_rules = sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined @@ -155,7 +113,7 @@ use "Tools/cont_proc.ML" use "Tools/Domain/domain_axioms.ML" use "Tools/Domain/domain_constructors.ML" -use "Tools/Domain/domain_theorems.ML" -use "Tools/Domain/domain_extender.ML" +use "Tools/Domain/domain_induction.ML" +use "Tools/Domain/domain.ML" end diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Fixrec.thy Wed Oct 20 21:26:51 2010 -0700 @@ -115,7 +115,7 @@ definition match_UU :: "'a \ 'c match \ 'c match" where - "match_UU = strictify\(\ x k. fail)" + "match_UU = (\ x k. strict\x\fail)" definition match_Pair :: "'a::cpo \ 'b::cpo \ ('a \ 'b \ 'c match) \ 'c match" diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/IsaMakefile Wed Oct 20 21:26:51 2010 -0700 @@ -70,12 +70,12 @@ Tools/cont_consts.ML \ Tools/cont_proc.ML \ Tools/holcf_library.ML \ - Tools/Domain/domain_extender.ML \ + Tools/Domain/domain.ML \ Tools/Domain/domain_axioms.ML \ Tools/Domain/domain_constructors.ML \ + Tools/Domain/domain_induction.ML \ Tools/Domain/domain_isomorphism.ML \ Tools/Domain/domain_take_proofs.ML \ - Tools/Domain/domain_theorems.ML \ Tools/fixrec.ML \ Tools/pcpodef.ML \ Tools/repdef.ML \ diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/One.thy --- a/src/HOLCF/One.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/One.thy Wed Oct 20 21:26:51 2010 -0700 @@ -54,7 +54,7 @@ definition one_when :: "'a::pcpo \ one \ 'a" where - "one_when = (\ a. strictify\(\ _. a))" + "one_when = (\ a x. strict\x\a)" translations "case x of XCONST ONE \ t" == "CONST one_when\t\x" diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Pcpo.thy --- a/src/HOLCF/Pcpo.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Pcpo.thy Wed Oct 20 21:26:51 2010 -0700 @@ -223,18 +223,14 @@ lemma UU_I: "x \ \ \ x = \" by (subst eq_UU_iff) +lemma lub_eq_bottom_iff: "chain Y \ (\i. Y i) = \ \ (\i. Y i = \)" +by (simp only: eq_UU_iff lub_below_iff) + lemma chain_UU_I: "\chain Y; (\i. Y i) = \\ \ \i. Y i = \" -apply (rule allI) -apply (rule UU_I) -apply (erule subst) -apply (erule is_ub_thelub) -done +by (simp add: lub_eq_bottom_iff) lemma chain_UU_I_inverse: "\i::nat. Y i = \ \ (\i. Y i) = \" -apply (rule lub_chain_maxelem) -apply (erule spec) -apply simp -done +by simp lemma chain_UU_I_inverse2: "(\i. Y i) \ \ \ \i::nat. Y i \ \" by (blast intro: chain_UU_I_inverse) diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Pcpodef.thy --- a/src/HOLCF/Pcpodef.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Pcpodef.thy Wed Oct 20 21:26:51 2010 -0700 @@ -57,13 +57,10 @@ subsection {* Proving a subtype is chain-finite *} -lemma monofun_Rep: +lemma ch2ch_Rep: assumes below: "op \ \ \x y. Rep x \ Rep y" - shows "monofun Rep" -by (rule monofunI, unfold below) - -lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep] -lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep] + shows "chain S \ chain (\i. Rep (S i))" +unfolding chain_def below . theorem typedef_chfin: fixes Abs :: "'a::chfin \ 'b::po" @@ -87,6 +84,11 @@ admissible predicate. *} +lemma typedef_is_lubI: + assumes below: "op \ \ \x y. Rep x \ Rep y" + shows "range (\i. Rep (S i)) <<| Rep x \ range S <<| x" +unfolding is_lub_def is_ub_def below by simp + lemma Abs_inverse_lub_Rep: fixes Abs :: "'a::cpo \ 'b::po" assumes type: "type_definition Rep Abs A" @@ -104,15 +106,15 @@ and below: "op \ \ \x y. Rep x \ Rep y" and adm: "adm (\x. x \ A)" shows "chain S \ range S <<| Abs (\i. Rep (S i))" - apply (frule ch2ch_Rep [OF below]) - apply (rule is_lubI) - apply (rule ub_rangeI) - apply (simp only: below Abs_inverse_lub_Rep [OF type below adm]) - apply (erule is_ub_thelub) - apply (simp only: below Abs_inverse_lub_Rep [OF type below adm]) - apply (erule is_lub_thelub) - apply (erule ub2ub_Rep [OF below]) -done +proof - + assume S: "chain S" + hence "chain (\i. Rep (S i))" by (rule ch2ch_Rep [OF below]) + hence "range (\i. Rep (S i)) <<| (\i. Rep (S i))" by (rule cpo_lubI) + hence "range (\i. Rep (S i)) <<| Rep (Abs (\i. Rep (S i)))" + by (simp only: Abs_inverse_lub_Rep [OF type below adm S]) + thus "range S <<| Abs (\i. Rep (S i))" + by (rule typedef_is_lubI [OF below]) +qed lemmas typedef_thelub = typedef_lub [THEN thelubI, standard] @@ -152,18 +154,6 @@ composing it with another continuous function. *} -theorem typedef_is_lubI: - assumes below: "op \ \ \x y. Rep x \ Rep y" - shows "range (\i. Rep (S i)) <<| Rep x \ range S <<| x" - apply (rule is_lubI) - apply (rule ub_rangeI) - apply (subst below) - apply (erule is_ub_lub) - apply (subst below) - apply (erule is_lub_lub) - apply (erule ub2ub_Rep [OF below]) -done - theorem typedef_cont_Abs: fixes Abs :: "'a::cpo \ 'b::cpo" fixes f :: "'c::cpo \ 'a::cpo" diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Representable.thy Wed Oct 20 21:26:51 2010 -0700 @@ -18,80 +18,25 @@ lemma emb_prj: "emb\((prj\x)::'a) = cast\DEFL('a)\x" by (simp add: cast_DEFL) -lemma in_DEFL_iff: - "x ::: DEFL('a) \ emb\((prj\x)::'a) = x" -by (simp add: in_defl_def cast_DEFL) - -lemma prj_inverse: - "x ::: DEFL('a) \ emb\((prj\x)::'a) = x" -by (simp only: in_DEFL_iff) - -lemma emb_in_DEFL [simp]: - "emb\(x::'a) ::: DEFL('a)" -by (simp add: in_DEFL_iff) - -subsection {* Coerce operator *} - -definition coerce :: "'a \ 'b" -where "coerce = prj oo emb" - -lemma beta_coerce: "coerce\x = prj\(emb\x)" -by (simp add: coerce_def) - -lemma prj_emb: "prj\(emb\x) = coerce\x" -by (simp add: coerce_def) - -lemma coerce_strict [simp]: "coerce\\ = \" -by (simp add: coerce_def) - -lemma coerce_eq_ID [simp]: "(coerce :: 'a \ 'a) = ID" -by (rule cfun_eqI, simp add: beta_coerce) - -lemma emb_coerce: - "DEFL('a) \ DEFL('b) - \ emb\((coerce::'a \ 'b)\x) = emb\x" - apply (simp add: beta_coerce) - apply (rule prj_inverse) - apply (erule defl_belowD) - apply (rule emb_in_DEFL) +lemma emb_prj_emb: + fixes x :: "'a" + assumes "DEFL('a) \ DEFL('b)" + shows "emb\(prj\(emb\x) :: 'b) = emb\x" +unfolding emb_prj +apply (rule cast.belowD) +apply (rule monofun_cfun_arg [OF assms]) +apply (simp add: cast_DEFL) done -lemma coerce_prj: - "DEFL('a) \ DEFL('b) - \ (coerce::'b \ 'a)\(prj\x) = prj\x" - apply (simp add: coerce_def) +lemma prj_emb_prj: + assumes "DEFL('a) \ DEFL('b)" + shows "prj\(emb\(prj\x :: 'b)) = (prj\x :: 'a)" apply (rule emb_eq_iff [THEN iffD1]) apply (simp only: emb_prj) apply (rule deflation_below_comp1) apply (rule deflation_cast) apply (rule deflation_cast) - apply (erule monofun_cfun_arg) -done - -lemma coerce_coerce [simp]: - "DEFL('a) \ DEFL('b) - \ coerce\((coerce::'a \ 'b)\x) = coerce\x" -by (simp add: beta_coerce prj_inverse defl_belowD) - -lemma coerce_inverse: - "emb\(x::'a) ::: DEFL('b) \ coerce\(coerce\x :: 'b) = x" -by (simp only: beta_coerce prj_inverse emb_inverse) - -lemma coerce_type: - "DEFL('a) \ DEFL('b) - \ emb\((coerce::'a \ 'b)\x) ::: DEFL('a)" -by (simp add: beta_coerce prj_inverse defl_belowD) - -lemma ep_pair_coerce: - "DEFL('a) \ DEFL('b) - \ ep_pair (coerce::'a \ 'b) (coerce::'b \ 'a)" - apply (rule ep_pair.intro) - apply simp - apply (simp only: beta_coerce) - apply (rule below_trans) - apply (rule monofun_cfun_arg) - apply (rule emb_prj_below) - apply simp + apply (rule monofun_cfun_arg [OF assms]) done text {* Isomorphism lemmas used internally by the domain package: *} @@ -99,67 +44,79 @@ lemma domain_abs_iso: fixes abs and rep assumes DEFL: "DEFL('b) = DEFL('a)" - assumes abs_def: "abs \ (coerce :: 'a \ 'b)" - assumes rep_def: "rep \ (coerce :: 'b \ 'a)" + assumes abs_def: "(abs :: 'a \ 'b) \ prj oo emb" + assumes rep_def: "(rep :: 'b \ 'a) \ prj oo emb" shows "rep\(abs\x) = x" -unfolding abs_def rep_def by (simp add: DEFL) +unfolding abs_def rep_def +by (simp add: emb_prj_emb DEFL) lemma domain_rep_iso: fixes abs and rep assumes DEFL: "DEFL('b) = DEFL('a)" - assumes abs_def: "abs \ (coerce :: 'a \ 'b)" - assumes rep_def: "rep \ (coerce :: 'b \ 'a)" + assumes abs_def: "(abs :: 'a \ 'b) \ prj oo emb" + assumes rep_def: "(rep :: 'b \ 'a) \ prj oo emb" shows "abs\(rep\x) = x" -unfolding abs_def rep_def by (simp add: DEFL [symmetric]) +unfolding abs_def rep_def +by (simp add: emb_prj_emb DEFL) + +subsection {* Deflations as sets *} + +definition defl_set :: "defl \ udom set" +where "defl_set A = {x. cast\A\x = x}" + +lemma adm_defl_set: "adm (\x. x \ defl_set A)" +unfolding defl_set_def by simp +lemma defl_set_bottom: "\ \ defl_set A" +unfolding defl_set_def by simp + +lemma defl_set_cast [simp]: "cast\A\x \ defl_set A" +unfolding defl_set_def by simp + +lemma defl_set_subset_iff: "defl_set A \ defl_set B \ A \ B" +apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric]) +apply (auto simp add: cast.belowI cast.belowD) +done subsection {* Proving a subtype is representable *} text {* - Temporarily relax type constraints for @{term emb}, and @{term prj}. + Temporarily relax type constraints for @{term emb} and @{term prj}. *} -setup {* Sign.add_const_constraint - (@{const_name defl}, SOME @{typ "'a::pcpo itself \ defl"}) *} - -setup {* Sign.add_const_constraint - (@{const_name emb}, SOME @{typ "'a::pcpo \ udom"}) *} - -setup {* Sign.add_const_constraint - (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) *} +setup {* + fold Sign.add_const_constraint + [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \ defl"}) + , (@{const_name emb}, SOME @{typ "'a::pcpo \ udom"}) + , (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) ] +*} lemma typedef_rep_class: fixes Rep :: "'a::pcpo \ udom" fixes Abs :: "udom \ 'a::pcpo" fixes t :: defl - assumes type: "type_definition Rep Abs {x. x ::: t}" + assumes type: "type_definition Rep Abs (defl_set t)" assumes below: "op \ \ \x y. Rep x \ Rep y" assumes emb: "emb \ (\ x. Rep x)" assumes prj: "prj \ (\ x. Abs (cast\t\x))" assumes defl: "defl \ (\ a::'a itself. t)" shows "OFCLASS('a, bifinite_class)" proof - have adm: "adm (\x. x \ {x. x ::: t})" - by (simp add: adm_in_defl) have emb_beta: "\x. emb\x = Rep x" unfolding emb apply (rule beta_cfun) - apply (rule typedef_cont_Rep [OF type below adm]) + apply (rule typedef_cont_Rep [OF type below adm_defl_set]) done have prj_beta: "\y. prj\y = Abs (cast\t\y)" unfolding prj apply (rule beta_cfun) - apply (rule typedef_cont_Abs [OF type below adm]) + apply (rule typedef_cont_Abs [OF type below adm_defl_set]) apply simp_all done - have emb_in_defl: "\x::'a. emb\x ::: t" + have prj_emb: "\x::'a. prj\(emb\x) = x" using type_definition.Rep [OF type] - by (simp add: emb_beta) - have prj_emb: "\x::'a. prj\(emb\x) = x" - unfolding prj_beta - apply (simp add: cast_fixed [OF emb_in_defl]) - apply (simp add: emb_beta type_definition.Rep_inverse [OF type]) - done + unfolding prj_beta emb_beta defl_set_def + by (simp add: type_definition.Rep_inverse [OF type]) have emb_prj: "\y. emb\(prj\y :: 'a) = cast\t\y" unfolding prj_beta emb_beta by (simp add: type_definition.Abs_inverse [OF type]) @@ -177,19 +134,14 @@ shows "DEFL('a::pcpo) = t" unfolding assms .. -text {* Restore original typing constraints *} - -setup {* Sign.add_const_constraint - (@{const_name defl}, SOME @{typ "'a::bifinite itself \ defl"}) *} +text {* Restore original typing constraints. *} -setup {* Sign.add_const_constraint - (@{const_name emb}, SOME @{typ "'a::bifinite \ udom"}) *} - -setup {* Sign.add_const_constraint - (@{const_name prj}, SOME @{typ "udom \ 'a::bifinite"}) *} - -lemma adm_mem_Collect_in_defl: "adm (\x. x \ {x. x ::: A})" -unfolding mem_Collect_eq by (rule adm_in_defl) +setup {* + fold Sign.add_const_constraint + [ (@{const_name defl}, SOME @{typ "'a::bifinite itself \ defl"}) + , (@{const_name emb}, SOME @{typ "'a::bifinite \ udom"}) + , (@{const_name prj}, SOME @{typ "udom \ 'a::bifinite"}) ] +*} use "Tools/repdef.ML" @@ -258,22 +210,14 @@ apply (simp add: assms) done -lemma isodefl_coerce: - fixes d :: "'a \ 'a" - assumes DEFL: "DEFL('b) = DEFL('a)" - shows "isodefl d t \ isodefl (coerce oo d oo coerce :: 'b \ 'b) t" -unfolding isodefl_def -apply (simp add: cfun_eq_iff) -apply (simp add: emb_coerce coerce_prj DEFL) -done - lemma isodefl_abs_rep: fixes abs and rep and d assumes DEFL: "DEFL('b) = DEFL('a)" - assumes abs_def: "abs \ (coerce :: 'a \ 'b)" - assumes rep_def: "rep \ (coerce :: 'b \ 'a)" + assumes abs_def: "(abs :: 'a \ 'b) \ prj oo emb" + assumes rep_def: "(rep :: 'b \ 'a) \ prj oo emb" shows "isodefl d t \ isodefl (abs oo d oo rep) t" -unfolding abs_def rep_def using DEFL by (rule isodefl_coerce) +unfolding isodefl_def +by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb) lemma isodefl_cfun: "isodefl d1 t1 \ isodefl d2 t2 \ diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Sprod.thy Wed Oct 20 21:26:51 2010 -0700 @@ -27,9 +27,8 @@ type_notation (HTML output) sprod ("(_ \/ _)" [21,20] 20) -lemma spair_lemma: - "(strictify\(\ b. a)\b, strictify\(\ a. b)\a) \ Sprod" -by (simp add: Sprod_def strictify_conv_if) +lemma spair_lemma: "(strict\b\a, strict\a\b) \ Sprod" +by (simp add: Sprod_def strict_conv_if) subsection {* Definitions of constants *} @@ -43,12 +42,11 @@ definition spair :: "'a \ 'b \ ('a ** 'b)" where - "spair = (\ a b. Abs_Sprod - (strictify\(\ b. a)\b, strictify\(\ a. b)\a))" + "spair = (\ a b. Abs_Sprod (strict\b\a, strict\a\b))" definition ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" where - "ssplit = (\ f. strictify\(\ p. f\(sfst\p)\(ssnd\p)))" + "ssplit = (\ f p. strict\p\(f\(sfst\p)\(ssnd\p)))" syntax "_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") @@ -62,7 +60,7 @@ subsection {* Case analysis *} lemma Rep_Sprod_spair: - "Rep_Sprod (:a, b:) = (strictify\(\ b. a)\b, strictify\(\ a. b)\a)" + "Rep_Sprod (:a, b:) = (strict\b\a, strict\a\b)" unfolding spair_def by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma) @@ -76,7 +74,7 @@ apply (simp add: Rep_Sprod_simps Pair_fst_snd_eq) apply (simp add: Sprod_def) apply (erule disjE, simp) -apply (simp add: strictify_conv_if) +apply (simp add: strict_conv_if) apply fast done @@ -91,22 +89,22 @@ subsection {* Properties of \emph{spair} *} lemma spair_strict1 [simp]: "(:\, y:) = \" -by (simp add: Rep_Sprod_simps strictify_conv_if) +by (simp add: Rep_Sprod_simps strict_conv_if) lemma spair_strict2 [simp]: "(:x, \:) = \" -by (simp add: Rep_Sprod_simps strictify_conv_if) +by (simp add: Rep_Sprod_simps strict_conv_if) lemma spair_strict_iff [simp]: "((:x, y:) = \) = (x = \ \ y = \)" -by (simp add: Rep_Sprod_simps strictify_conv_if) +by (simp add: Rep_Sprod_simps strict_conv_if) lemma spair_below_iff: "((:a, b:) \ (:c, d:)) = (a = \ \ b = \ \ (a \ c \ b \ d))" -by (simp add: Rep_Sprod_simps strictify_conv_if) +by (simp add: Rep_Sprod_simps strict_conv_if) lemma spair_eq_iff: "((:a, b:) = (:c, d:)) = (a = c \ b = d \ (a = \ \ b = \) \ (c = \ \ d = \))" -by (simp add: Rep_Sprod_simps strictify_conv_if) +by (simp add: Rep_Sprod_simps strict_conv_if) lemma spair_strict: "x = \ \ y = \ \ (:x, y:) = \" by simp @@ -197,7 +195,7 @@ by (rule compactI, simp add: ssnd_below_iff) lemma compact_spair: "\compact x; compact y\ \ compact (:x, y:)" -by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if) +by (rule compact_Sprod, simp add: Rep_Sprod_spair strict_conv_if) lemma compact_spair_iff: "compact (:x, y:) = (x = \ \ y = \ \ (compact x \ compact y))" diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Ssum.thy Wed Oct 20 21:26:51 2010 -0700 @@ -34,28 +34,28 @@ definition sinl :: "'a \ ('a ++ 'b)" where - "sinl = (\ a. Abs_Ssum (strictify\(\ _. TT)\a, a, \))" + "sinl = (\ a. Abs_Ssum (strict\a\TT, a, \))" definition sinr :: "'b \ ('a ++ 'b)" where - "sinr = (\ b. Abs_Ssum (strictify\(\ _. FF)\b, \, b))" + "sinr = (\ b. Abs_Ssum (strict\b\FF, \, b))" -lemma sinl_Ssum: "(strictify\(\ _. TT)\a, a, \) \ Ssum" -by (simp add: Ssum_def strictify_conv_if) +lemma sinl_Ssum: "(strict\a\TT, a, \) \ Ssum" +by (simp add: Ssum_def strict_conv_if) -lemma sinr_Ssum: "(strictify\(\ _. FF)\b, \, b) \ Ssum" -by (simp add: Ssum_def strictify_conv_if) +lemma sinr_Ssum: "(strict\b\FF, \, b) \ Ssum" +by (simp add: Ssum_def strict_conv_if) -lemma sinl_Abs_Ssum: "sinl\a = Abs_Ssum (strictify\(\ _. TT)\a, a, \)" +lemma sinl_Abs_Ssum: "sinl\a = Abs_Ssum (strict\a\TT, a, \)" by (unfold sinl_def, simp add: cont_Abs_Ssum sinl_Ssum) -lemma sinr_Abs_Ssum: "sinr\b = Abs_Ssum (strictify\(\ _. FF)\b, \, b)" +lemma sinr_Abs_Ssum: "sinr\b = Abs_Ssum (strict\b\FF, \, b)" by (unfold sinr_def, simp add: cont_Abs_Ssum sinr_Ssum) -lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\a) = (strictify\(\ _. TT)\a, a, \)" +lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\a) = (strict\a\TT, a, \)" by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum) -lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\b) = (strictify\(\ _. FF)\b, \, b)" +lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\b) = (strict\b\FF, \, b)" by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum) subsection {* Properties of \emph{sinl} and \emph{sinr} *} @@ -63,16 +63,16 @@ text {* Ordering *} lemma sinl_below [simp]: "(sinl\x \ sinl\y) = (x \ y)" -by (simp add: below_Ssum_def Rep_Ssum_sinl strictify_conv_if) +by (simp add: below_Ssum_def Rep_Ssum_sinl strict_conv_if) lemma sinr_below [simp]: "(sinr\x \ sinr\y) = (x \ y)" -by (simp add: below_Ssum_def Rep_Ssum_sinr strictify_conv_if) +by (simp add: below_Ssum_def Rep_Ssum_sinr strict_conv_if) lemma sinl_below_sinr [simp]: "(sinl\x \ sinr\y) = (x = \)" -by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if) +by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if) lemma sinr_below_sinl [simp]: "(sinr\x \ sinl\y) = (x = \)" -by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if) +by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if) text {* Equality *} @@ -117,10 +117,10 @@ text {* Compactness *} lemma compact_sinl: "compact x \ compact (sinl\x)" -by (rule compact_Ssum, simp add: Rep_Ssum_sinl strictify_conv_if) +by (rule compact_Ssum, simp add: Rep_Ssum_sinl strict_conv_if) lemma compact_sinr: "compact x \ compact (sinr\x)" -by (rule compact_Ssum, simp add: Rep_Ssum_sinr strictify_conv_if) +by (rule compact_Ssum, simp add: Rep_Ssum_sinr strict_conv_if) lemma compact_sinlD: "compact (sinl\x) \ compact x" unfolding compact_def diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Tools/Domain/domain.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain.ML Wed Oct 20 21:26:51 2010 -0700 @@ -0,0 +1,274 @@ +(* Title: HOLCF/Tools/Domain/domain.ML + Author: David von Oheimb + Author: Brian Huffman + +Theory extender for domain command, including theory syntax. +*) + +signature DOMAIN = +sig + val add_domain_cmd: + binding -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory + + val add_domain: + binding -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory + + val add_new_domain_cmd: + binding -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory + + val add_new_domain: + binding -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory +end; + +structure Domain :> DOMAIN = +struct + +open HOLCF_Library; + +fun first (x,_,_) = x; +fun second (_,x,_) = x; +fun third (_,_,x) = x; + +(* ----- calls for building new thy and thms -------------------------------- *) + +type info = + Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info; + +fun gen_add_domain + (prep_typ : theory -> (string * sort) list -> 'a -> typ) + (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory) + (arg_sort : bool -> sort) + (comp_dbind : binding) + (raw_specs : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * 'a) list * mixfix) list) list) + (thy : theory) = + let + val dtnvs : (binding * typ list * mixfix) list = + let + fun readS (SOME s) = Syntax.read_sort_global thy s + | readS NONE = Sign.defaultS thy; + fun readTFree (a, s) = TFree (a, readS s); + in + map (fn (vs, dbind, mx, _) => + (dbind, map readTFree vs, mx)) raw_specs + end; + + fun thy_type (dbind, tvars, mx) = (dbind, length tvars, mx); + fun thy_arity (dbind, tvars, mx) = + (Sign.full_name thy dbind, map (snd o dest_TFree) tvars, arg_sort false); + + (* this theory is used just for parsing and error checking *) + val tmp_thy = thy + |> Theory.copy + |> Sign.add_types (map thy_type dtnvs) + |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; + + val dbinds : binding list = + map (fn (_,dbind,_,_) => dbind) raw_specs; + val raw_rhss : + (binding * (bool * binding option * 'a) list * mixfix) list list = + map (fn (_,_,_,cons) => cons) raw_specs; + val dtnvs' : (string * typ list) list = + map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs; + + val all_cons = map (Binding.name_of o first) (flat raw_rhss); + val test_dupl_cons = + case duplicates (op =) all_cons of + [] => false | dups => error ("Duplicate constructors: " + ^ commas_quote dups); + val all_sels = + (map Binding.name_of o map_filter second o maps second) (flat raw_rhss); + val test_dupl_sels = + case duplicates (op =) all_sels of + [] => false | dups => error("Duplicate selectors: "^commas_quote dups); + + fun test_dupl_tvars s = + case duplicates (op =) (map(fst o dest_TFree)s) of + [] => false | dups => error("Duplicate type arguments: " + ^commas_quote dups); + val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs'); + + val sorts : (string * sort) list = + let val all_sorts = map (map dest_TFree o snd) dtnvs'; + in + case distinct (eq_set (op =)) all_sorts of + [sorts] => sorts + | _ => error "Mutually recursive domains must have same type parameters" + end; + + (* a lazy argument may have an unpointed type *) + (* unless the argument has a selector function *) + fun check_pcpo (lazy, sel, T) = + let val sort = arg_sort (lazy andalso is_none sel) in + if Sign.of_sort tmp_thy (T, sort) then () + else error ("Constructor argument type is not of sort " ^ + Syntax.string_of_sort_global tmp_thy sort ^ ": " ^ + Syntax.string_of_typ_global tmp_thy T) + end; + + (* 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; + 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; + in Type (s, map (check_rec rec_ok') Ts) end + | SOME typevars => + if typevars <> Ts + then error ("Recursion of type " ^ + quote (Syntax.string_of_typ_global tmp_thy T) ^ + " with different arguments") + else if rec_ok then T + else error ("Illegal indirect recursion of type " ^ + quote (Syntax.string_of_typ_global tmp_thy T))) + | check_rec rec_ok (TVar _) = error "extender:check_rec"; + + fun prep_arg (lazy, sel, raw_T) = + let + val T = prep_typ tmp_thy sorts raw_T; + val _ = check_rec true T; + val _ = check_pcpo (lazy, sel, T); + in (lazy, sel, T) end; + fun prep_con (b, args, mx) = (b, map prep_arg args, mx); + fun prep_rhs cons = map prep_con cons; + val rhss : (binding * (bool * binding option * typ) list * mixfix) list list = + map prep_rhs raw_rhss; + + fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T; + fun mk_con_typ (bind, args, mx) = + if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); + fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons); + + val absTs : typ list = map Type dtnvs'; + val repTs : typ list = map mk_rhs_typ rhss; + + val iso_spec : (binding * mixfix * (typ * typ)) list = + map (fn ((dbind, _, mx), eq) => (dbind, mx, eq)) + (dtnvs ~~ (absTs ~~ repTs)); + + val ((iso_infos, take_info), thy) = add_isos iso_spec thy; + + val (constr_infos, thy) = + thy + |> fold_map (fn ((dbind, cons), info) => + Domain_Constructors.add_domain_constructors dbind cons info) + (dbinds ~~ rhss ~~ iso_infos); + + val (take_rews, thy) = + Domain_Induction.comp_theorems comp_dbind + dbinds take_info constr_infos thy; + in + thy + end; + +fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = + let + fun prep (dbind, mx, (lhsT, rhsT)) = + let val (dname, vs) = dest_Type lhsT; + in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end; + in + Domain_Isomorphism.domain_isomorphism (map prep spec) + end; + +fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo}; +fun rep_arg lazy = @{sort bifinite}; + +(* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *) +fun read_typ thy sorts str = + let + val ctxt = ProofContext.init_global thy + |> fold (Variable.declare_typ o TFree) sorts; + in Syntax.read_typ ctxt str end; + +fun cert_typ sign sorts raw_T = + let + val T = Type.no_tvars (Sign.certify_typ sign raw_T) + handle TYPE (msg, _, _) => error msg; + val sorts' = Term.add_tfreesT T sorts; + val _ = + case duplicates (op =) (map fst sorts') of + [] => () + | dups => error ("Inconsistent sort constraints for " ^ commas dups) + in T end; + +val add_domain = + gen_add_domain cert_typ Domain_Axioms.add_axioms pcpo_arg; + +val add_new_domain = + gen_add_domain cert_typ define_isos rep_arg; + +val add_domain_cmd = + gen_add_domain read_typ Domain_Axioms.add_axioms pcpo_arg; + +val add_new_domain_cmd = + gen_add_domain read_typ define_isos rep_arg; + + +(** outer syntax **) + +val _ = Keyword.keyword "lazy"; + +val dest_decl : (bool * binding option * string) parser = + Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false -- + (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1 + || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")" + >> (fn t => (true,NONE,t)) + || Parse.typ >> (fn t => (false,NONE,t)); + +val cons_decl = + Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix; + +val domain_decl = + (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) -- + (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl); + +val domains_decl = + Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") -- + Parse.and_list1 domain_decl; + +fun mk_domain + (definitional : bool) + (opt_name : binding option, + doms : ((((string * string option) list * binding) * mixfix) * + ((binding * (bool * binding option * string) list) * mixfix) list) list ) = + let + val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; + val specs : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list = + map (fn (((vs, t), mx), cons) => + (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; + val comp_dbind = + case opt_name of NONE => Binding.name (space_implode "_" names) + | SOME s => s; + in + if definitional + then add_new_domain_cmd comp_dbind specs + else add_domain_cmd comp_dbind specs + end; + +val _ = + Outer_Syntax.command "domain" "define recursive domains (HOLCF)" + Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false)); + +val _ = + Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)" + Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true)); + +end; diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Oct 19 15:13:35 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,278 +0,0 @@ -(* Title: HOLCF/Tools/Domain/domain_extender.ML - Author: David von Oheimb - Author: Brian Huffman - -Theory extender for domain command, including theory syntax. -*) - -signature DOMAIN_EXTENDER = -sig - val add_domain_cmd: - binding -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list - -> theory -> theory - - val add_domain: - binding -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * typ) list * mixfix) list) list - -> theory -> theory - - val add_new_domain_cmd: - binding -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list - -> theory -> theory - - val add_new_domain: - binding -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * typ) list * mixfix) list) list - -> theory -> theory -end; - -structure Domain_Extender :> DOMAIN_EXTENDER = -struct - -open HOLCF_Library; - -fun first (x,_,_) = x; -fun second (_,x,_) = x; -fun third (_,_,x) = x; - -fun upd_first f (x,y,z) = (f x, y, z); -fun upd_second f (x,y,z) = ( x, f y, z); -fun upd_third f (x,y,z) = ( x, y, f z); - -(* ----- general testing and preprocessing of constructor list -------------- *) -fun check_and_sort_domain - (arg_sort : bool -> sort) - (dtnvs : (string * typ list) list) - (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) - (thy : theory) - : ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list = - let - val defaultS = Sign.defaultS thy; - - val test_dupl_typs = - case duplicates (op =) (map fst dtnvs) of - [] => false | dups => error ("Duplicate types: " ^ commas_quote dups); - - val all_cons = map (Binding.name_of o first) (flat cons''); - val test_dupl_cons = - case duplicates (op =) all_cons of - [] => false | dups => error ("Duplicate constructors: " - ^ commas_quote dups); - val all_sels = - (map Binding.name_of o map_filter second o maps second) (flat cons''); - val test_dupl_sels = - case duplicates (op =) all_sels of - [] => false | dups => error("Duplicate selectors: "^commas_quote dups); - - fun test_dupl_tvars s = - case duplicates (op =) (map(fst o dest_TFree)s) of - [] => false | dups => error("Duplicate type arguments: " - ^commas_quote dups); - val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs); - - (* 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 *) - fun analyse_equation ((dname,typevars),cons') = - let - val tvars = map dest_TFree typevars; - val distinct_typevars = map TFree tvars; - fun rm_sorts (TFree(s,_)) = TFree(s,[]) - | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) - | rm_sorts (TVar(s,_)) = TVar(s,[]) - and remove_sorts l = map rm_sorts l; - fun analyse indirect (TFree(v,s)) = - (case AList.lookup (op =) tvars v of - NONE => error ("Free type variable " ^ quote v ^ " on rhs.") - | SOME sort => if eq_set (op =) (s, defaultS) orelse - eq_set (op =) (s, sort) - then TFree(v,sort) - else error ("Inconsistent sort constraint" ^ - " for type variable " ^ quote v)) - | analyse indirect (t as Type(s,typl)) = - (case AList.lookup (op =) dtnvs s of - NONE => Type (s, map (analyse false) typl) - | SOME typevars => - if indirect - then error ("Indirect recursion of type " ^ - quote (Syntax.string_of_typ_global thy t)) - else if dname <> s orelse - (** BUG OR FEATURE?: - mutual recursion may use different arguments **) - remove_sorts typevars = remove_sorts typl - then Type(s,map (analyse true) typl) - else error ("Direct recursion of type " ^ - quote (Syntax.string_of_typ_global thy t) ^ - " with different arguments")) - | analyse indirect (TVar _) = error "extender:analyse"; - fun check_pcpo lazy T = - let val sort = arg_sort lazy in - if Sign.of_sort thy (T, sort) then T - else error ("Constructor argument type is not of sort " ^ - Syntax.string_of_sort_global thy sort ^ ": " ^ - Syntax.string_of_typ_global thy T) - end; - fun analyse_arg (lazy, sel, T) = - (lazy, sel, check_pcpo lazy (analyse false T)); - fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); - in ((dname,distinct_typevars), map analyse_con cons') end; - in ListPair.map analyse_equation (dtnvs,cons'') - end; (* let *) - -(* ----- calls for building new thy and thms -------------------------------- *) - -type info = - Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info; - -fun gen_add_domain - (prep_typ : theory -> 'a -> typ) - (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory) - (arg_sort : bool -> sort) - (comp_dbind : binding) - (eqs''' : ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * 'a) list * mixfix) list) list) - (thy : theory) = - let - val dtnvs : (binding * typ list * mixfix) list = - let - fun readS (SOME s) = Syntax.read_sort_global thy s - | readS NONE = Sign.defaultS thy; - fun readTFree (a, s) = TFree (a, readS s); - in - map (fn (vs,dname:binding,mx,_) => - (dname, map readTFree vs, mx)) eqs''' - end; - - fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); - fun thy_arity (dname,tvars,mx) = - (Sign.full_name thy dname, map (snd o dest_TFree) tvars, arg_sort false); - - (* this theory is used just for parsing and error checking *) - val tmp_thy = thy - |> Theory.copy - |> Sign.add_types (map thy_type dtnvs) - |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; - - val dbinds : binding list = - map (fn (_,dbind,_,_) => dbind) eqs'''; - val cons''' : - (binding * (bool * binding option * 'a) list * mixfix) list list = - map (fn (_,_,_,cons) => cons) eqs'''; - val cons'' : - (binding * (bool * binding option * typ) list * mixfix) list list = - map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons'''; - val dtnvs' : (string * typ list) list = - map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs; - val eqs' : ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list = - check_and_sort_domain arg_sort dtnvs' cons'' tmp_thy; - val dts : typ list = map (Type o fst) eqs'; - - fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T; - fun mk_con_typ (bind, args, mx) = - if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); - fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); - val repTs : typ list = map mk_eq_typ eqs'; - - val iso_spec : (binding * mixfix * (typ * typ)) list = - map (fn ((dbind, _, mx), eq) => (dbind, mx, eq)) - (dtnvs ~~ (dts ~~ repTs)); - - val ((iso_infos, take_info), thy) = add_isos iso_spec thy; - - val (constr_infos, thy) = - thy - |> fold_map (fn ((dbind, (_,cs)), info) => - Domain_Constructors.add_domain_constructors dbind cs info) - (dbinds ~~ eqs' ~~ iso_infos); - - val (take_rews, thy) = - Domain_Theorems.comp_theorems comp_dbind - dbinds take_info constr_infos thy; - in - thy - end; - -fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = - let - fun prep (dbind, mx, (lhsT, rhsT)) = - let val (dname, vs) = dest_Type lhsT; - in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end; - in - Domain_Isomorphism.domain_isomorphism (map prep spec) - end; - -fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo}; -fun rep_arg lazy = @{sort bifinite}; - -val add_domain = - gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg; - -val add_new_domain = - gen_add_domain Sign.certify_typ define_isos rep_arg; - -val add_domain_cmd = - gen_add_domain Syntax.read_typ_global Domain_Axioms.add_axioms pcpo_arg; - -val add_new_domain_cmd = - gen_add_domain Syntax.read_typ_global define_isos rep_arg; - - -(** outer syntax **) - -val _ = Keyword.keyword "lazy"; - -val dest_decl : (bool * binding option * string) parser = - Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false -- - (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1 - || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")" - >> (fn t => (true,NONE,t)) - || Parse.typ >> (fn t => (false,NONE,t)); - -val cons_decl = - Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix; - -val domain_decl = - (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) -- - (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl); - -val domains_decl = - Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") -- - Parse.and_list1 domain_decl; - -fun mk_domain - (definitional : bool) - (opt_name : binding option, - doms : ((((string * string option) list * binding) * mixfix) * - ((binding * (bool * binding option * string) list) * mixfix) list) list ) = - let - val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; - val specs : ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list = - map (fn (((vs, t), mx), cons) => - (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; - val comp_dbind = - case opt_name of NONE => Binding.name (space_implode "_" names) - | SOME s => s; - in - if definitional - then add_new_domain_cmd comp_dbind specs - else add_domain_cmd comp_dbind specs - end; - -val _ = - Outer_Syntax.command "domain" "define recursive domains (HOLCF)" - Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false)); - -val _ = - Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)" - Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true)); - -end; diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Tools/Domain/domain_induction.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_induction.ML Wed Oct 20 21:26:51 2010 -0700 @@ -0,0 +1,438 @@ +(* Title: HOLCF/Tools/Domain/domain_induction.ML + Author: David von Oheimb + Author: Brian Huffman + +Proofs of high-level (co)induction rules for domain command. +*) + +signature DOMAIN_INDUCTION = +sig + val comp_theorems : + binding -> binding list -> + Domain_Take_Proofs.take_induct_info -> + Domain_Constructors.constr_info list -> + theory -> thm list * theory + + val quiet_mode: bool Unsynchronized.ref; + val trace_domain: bool Unsynchronized.ref; +end; + +structure Domain_Induction :> DOMAIN_INDUCTION = +struct + +val quiet_mode = Unsynchronized.ref false; +val trace_domain = Unsynchronized.ref false; + +fun message s = if !quiet_mode then () else writeln s; +fun trace s = if !trace_domain then tracing s else (); + +open HOLCF_Library; + +(******************************************************************************) +(***************************** proofs about take ******************************) +(******************************************************************************) + +fun take_theorems + (dbinds : binding list) + (take_info : Domain_Take_Proofs.take_induct_info) + (constr_infos : Domain_Constructors.constr_info list) + (thy : theory) : thm list list * theory = +let + val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info; + val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy; + + val n = Free ("n", @{typ nat}); + val n' = @{const Suc} $ n; + + local + val newTs = map (#absT o #iso_info) constr_infos; + val subs = newTs ~~ map (fn t => t $ n) take_consts; + fun is_ID (Const (c, _)) = (c = @{const_name ID}) + | is_ID _ = false; + in + fun map_of_arg v T = + let val m = Domain_Take_Proofs.map_of_typ thy subs T; + in if is_ID m then v else mk_capply (m, v) end; + end + + fun prove_take_apps + ((dbind, take_const), constr_info) thy = + let + val {iso_info, con_specs, con_betas, ...} = constr_info; + val {abs_inverse, ...} = iso_info; + fun prove_take_app (con_const, args) = + let + val Ts = map snd args; + val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)); + val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts); + val goal = mk_trp (mk_eq (lhs, rhs)); + val rules = + [abs_inverse] @ con_betas @ @{thms take_con_rules} + @ take_Suc_thms @ deflation_thms @ deflation_take_thms; + val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + in + Goal.prove_global thy [] [] goal (K tac) + end; + val take_apps = map prove_take_app con_specs; + in + yield_singleton Global_Theory.add_thmss + ((Binding.qualified true "take_rews" dbind, take_apps), + [Simplifier.simp_add]) thy + end; +in + fold_map prove_take_apps + (dbinds ~~ take_consts ~~ constr_infos) thy +end; + +(******************************************************************************) +(****************************** induction rules *******************************) +(******************************************************************************) + +val case_UU_allI = + @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}; + +fun prove_induction + (comp_dbind : binding) + (constr_infos : Domain_Constructors.constr_info list) + (take_info : Domain_Take_Proofs.take_induct_info) + (take_rews : thm list) + (thy : theory) = +let + val comp_dname = Binding.name_of comp_dbind; + + val iso_infos = map #iso_info constr_infos; + val exhausts = map #exhaust constr_infos; + val con_rews = maps #con_rews constr_infos; + val {take_consts, take_induct_thms, ...} = take_info; + + val newTs = map #absT iso_infos; + val P_names = Datatype_Prop.indexify_names (map (K "P") newTs); + val x_names = Datatype_Prop.indexify_names (map (K "x") newTs); + val P_types = map (fn T => T --> HOLogic.boolT) newTs; + val Ps = map Free (P_names ~~ P_types); + val xs = map Free (x_names ~~ newTs); + val n = Free ("n", HOLogic.natT); + + fun con_assm defined p (con, args) = + let + val Ts = map snd args; + val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + fun ind_hyp (v, T) t = + case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t + | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t); + val t1 = mk_trp (p $ list_ccomb (con, vs)); + val t2 = fold_rev ind_hyp (vs ~~ Ts) t1; + val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2); + in fold_rev Logic.all vs (if defined then t3 else t2) end; + fun eq_assms ((p, T), cons) = + mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons; + val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos); + + val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); + fun quant_tac ctxt i = EVERY + (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names); + + (* FIXME: move this message to domain_take_proofs.ML *) + val is_finite = #is_finite take_info; + val _ = if is_finite + then message ("Proving finiteness rule for domain "^comp_dname^" ...") + else (); + + val _ = trace " Proving finite_ind..."; + val finite_ind = + let + val concls = + map (fn ((P, t), x) => P $ mk_capply (t $ n, x)) + (Ps ~~ take_consts ~~ xs); + val goal = mk_trp (foldr1 mk_conj concls); + + fun tacf {prems, context} = + let + (* Prove stronger prems, without definedness side conditions *) + fun con_thm p (con, args) = + let + val subgoal = con_assm false p (con, args); + val rules = prems @ con_rews @ simp_thms; + val simplify = asm_simp_tac (HOL_basic_ss addsimps rules); + fun arg_tac (lazy, _) = + rtac (if lazy then allI else case_UU_allI) 1; + val tacs = + rewrite_goals_tac @{thms atomize_all atomize_imp} :: + map arg_tac args @ + [REPEAT (rtac impI 1), ALLGOALS simplify]; + in + Goal.prove context [] [] subgoal (K (EVERY tacs)) + end; + fun eq_thms (p, cons) = map (con_thm p) cons; + val conss = map #con_specs constr_infos; + val prems' = maps eq_thms (Ps ~~ conss); + + val tacs1 = [ + quant_tac context 1, + simp_tac HOL_ss 1, + InductTacs.induct_tac context [[SOME "n"]] 1, + simp_tac (take_ss addsimps prems) 1, + TRY (safe_tac HOL_cs)]; + fun con_tac _ = + asm_simp_tac take_ss 1 THEN + (resolve_tac prems' THEN_ALL_NEW etac spec) 1; + fun cases_tacs (cons, exhaust) = + res_inst_tac context [(("y", 0), "x")] exhaust 1 :: + asm_simp_tac (take_ss addsimps prems) 1 :: + map con_tac cons; + val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts) + in + EVERY (map DETERM tacs) + end; + in Goal.prove_global thy [] assms goal tacf end; + + val _ = trace " Proving ind..."; + val ind = + let + val concls = map (op $) (Ps ~~ xs); + val goal = mk_trp (foldr1 mk_conj concls); + val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps; + fun tacf {prems, context} = + let + fun finite_tac (take_induct, fin_ind) = + rtac take_induct 1 THEN + (if is_finite then all_tac else resolve_tac prems 1) THEN + (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1; + val fin_inds = Project_Rule.projections context finite_ind; + in + TRY (safe_tac HOL_cs) THEN + EVERY (map finite_tac (take_induct_thms ~~ fin_inds)) + end; + in Goal.prove_global thy [] (adms @ assms) goal tacf end + + (* case names for induction rules *) + val dnames = map (fst o dest_Type) newTs; + val case_ns = + let + val adms = + if is_finite then [] else + if length dnames = 1 then ["adm"] else + map (fn s => "adm_" ^ Long_Name.base_name s) dnames; + val bottoms = + if length dnames = 1 then ["bottom"] else + map (fn s => "bottom_" ^ Long_Name.base_name s) dnames; + fun one_eq bot constr_info = + let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c)); + in bot :: map name_of (#con_specs constr_info) end; + in adms @ flat (map2 one_eq bottoms constr_infos) end; + + val inducts = Project_Rule.projections (ProofContext.init_global thy) ind; + fun ind_rule (dname, rule) = + ((Binding.empty, rule), + [Rule_Cases.case_names case_ns, Induct.induct_type dname]); + +in + thy + |> snd o Global_Theory.add_thms [ + ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), + ((Binding.qualified true "induct" comp_dbind, ind ), [])] + |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) +end; (* prove_induction *) + +(******************************************************************************) +(************************ bisimulation and coinduction ************************) +(******************************************************************************) + +fun prove_coinduction + (comp_dbind : binding, dbinds : binding list) + (constr_infos : Domain_Constructors.constr_info list) + (take_info : Domain_Take_Proofs.take_induct_info) + (take_rews : thm list list) + (thy : theory) : theory = +let + val iso_infos = map #iso_info constr_infos; + val newTs = map #absT iso_infos; + + val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info; + + val R_names = Datatype_Prop.indexify_names (map (K "R") newTs); + val R_types = map (fn T => T --> T --> boolT) newTs; + val Rs = map Free (R_names ~~ R_types); + val n = Free ("n", natT); + val reserved = "x" :: "y" :: R_names; + + (* declare bisimulation predicate *) + val bisim_bind = Binding.suffix_name "_bisim" comp_dbind; + val bisim_type = R_types ---> boolT; + val (bisim_const, thy) = + Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; + + (* define bisimulation predicate *) + local + fun one_con T (con, args) = + let + val Ts = map snd args; + val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts); + val ns2 = map (fn n => n^"'") ns1; + val vs1 = map Free (ns1 ~~ Ts); + val vs2 = map Free (ns2 ~~ Ts); + val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1)); + val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2)); + fun rel ((v1, v2), T) = + case AList.lookup (op =) (newTs ~~ Rs) T of + NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2; + val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]); + in + Library.foldr mk_ex (vs1 @ vs2, eqs) + end; + fun one_eq ((T, R), cons) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T)); + val disjs = disj1 :: map (one_con T) cons; + in + mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs))) + end; + val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos); + val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs); + val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs); + in + val (bisim_def_thm, thy) = thy |> + yield_singleton (Global_Theory.add_defs false) + ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []); + end (* local *) + + (* prove coinduction lemma *) + val coind_lemma = + let + val assm = mk_trp (list_comb (bisim_const, Rs)); + fun one ((T, R), take_const) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val lhs = mk_capply (take_const $ n, x); + val rhs = mk_capply (take_const $ n, y); + in + mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs)))) + end; + val goal = + mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts))); + val rules = @{thm Rep_CFun_strict1} :: take_0_thms; + fun tacf {prems, context} = + let + val prem' = rewrite_rule [bisim_def_thm] (hd prems); + val prems' = Project_Rule.projections context prem'; + val dests = map (fn th => th RS spec RS spec RS mp) prems'; + fun one_tac (dest, rews) = + dtac dest 1 THEN safe_tac HOL_cs THEN + ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews)); + in + rtac @{thm nat.induct} 1 THEN + simp_tac (HOL_ss addsimps rules) 1 THEN + safe_tac HOL_cs THEN + EVERY (map one_tac (dests ~~ take_rews)) + end + in + Goal.prove_global thy [] [assm] goal tacf + end; + + (* prove individual coinduction rules *) + fun prove_coind ((T, R), take_lemma) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val assm1 = mk_trp (list_comb (bisim_const, Rs)); + val assm2 = mk_trp (R $ x $ y); + val goal = mk_trp (mk_eq (x, y)); + fun tacf {prems, context} = + let + val rule = hd prems RS coind_lemma; + in + rtac take_lemma 1 THEN + asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1 + end; + in + Goal.prove_global thy [] [assm1, assm2] goal tacf + end; + val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms); + val coind_binds = map (Binding.qualified true "coinduct") dbinds; + +in + thy |> snd o Global_Theory.add_thms + (map Thm.no_attributes (coind_binds ~~ coinds)) +end; (* let *) + +(******************************************************************************) +(******************************* main function ********************************) +(******************************************************************************) + +fun comp_theorems + (comp_dbind : binding) + (dbinds : binding list) + (take_info : Domain_Take_Proofs.take_induct_info) + (constr_infos : Domain_Constructors.constr_info list) + (thy : theory) = +let +val comp_dname = Binding.name_of comp_dbind; + +(* Test for emptiness *) +(* FIXME: reimplement emptiness test +local + open Domain_Library; + val dnames = map (fst o fst) eqs; + val conss = map snd eqs; + fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => + is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso + ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse + rec_of arg <> n andalso rec_to (rec_of arg::ns) + (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) + ) o snd) cons; + fun warn (n,cons) = + if rec_to [] false (n,cons) + then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) + else false; +in + val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; + val is_emptys = map warn n__eqs; +end; +*) + +(* Test for indirect recursion *) +local + val newTs = map (#absT o #iso_info) constr_infos; + fun indirect_typ (Type (_, Ts)) = + exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts + | indirect_typ _ = false; + fun indirect_arg (_, T) = indirect_typ T; + fun indirect_con (_, args) = exists indirect_arg args; + fun indirect_eq cons = exists indirect_con cons; +in + val is_indirect = exists indirect_eq (map #con_specs constr_infos); + val _ = + if is_indirect + then message "Indirect recursion detected, skipping proofs of (co)induction rules" + else message ("Proving induction properties of domain "^comp_dname^" ..."); +end; + +(* theorems about take *) + +val (take_rewss, thy) = + take_theorems dbinds take_info constr_infos thy; + +val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info; + +val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss; + +(* prove induction rules, unless definition is indirect recursive *) +val thy = + if is_indirect then thy else + prove_induction comp_dbind constr_infos take_info take_rews thy; + +val thy = + if is_indirect then thy else + prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy; + +in + (take_rews, thy) +end; (* let *) +end; (* struct *) diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Oct 20 21:26:51 2010 -0700 @@ -104,6 +104,7 @@ infixr 6 ->>; infix -->>; +val udomT = @{typ udom}; val deflT = @{typ "defl"}; fun mapT (T as Type (_, Ts)) = @@ -113,7 +114,9 @@ fun mk_DEFL T = Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T; -fun coerce_const T = Const (@{const_name coerce}, T); +fun emb_const T = Const (@{const_name emb}, T ->> udomT); +fun prj_const T = Const (@{const_name prj}, udomT ->> T); +fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T); fun isodefl_const T = Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); @@ -505,9 +508,9 @@ val rep_bind = Binding.suffix_name "_rep" tbind; val abs_bind = Binding.suffix_name "_abs" tbind; val ((rep_const, rep_def), thy) = - define_const (rep_bind, coerce_const (lhsT ->> rhsT)) thy; + define_const (rep_bind, coerce_const (lhsT, rhsT)) thy; val ((abs_const, abs_def), thy) = - define_const (abs_bind, coerce_const (rhsT ->> lhsT)) thy; + define_const (abs_bind, coerce_const (rhsT, lhsT)) thy; in (((rep_const, abs_const), (rep_def, abs_def)), thy) end; diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Oct 19 15:13:35 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,438 +0,0 @@ -(* Title: HOLCF/Tools/Domain/domain_theorems.ML - Author: David von Oheimb - Author: Brian Huffman - -Proof generator for domain command. -*) - -signature DOMAIN_THEOREMS = -sig - val comp_theorems : - binding -> binding list -> - Domain_Take_Proofs.take_induct_info -> - Domain_Constructors.constr_info list -> - theory -> thm list * theory - - val quiet_mode: bool Unsynchronized.ref; - val trace_domain: bool Unsynchronized.ref; -end; - -structure Domain_Theorems :> DOMAIN_THEOREMS = -struct - -val quiet_mode = Unsynchronized.ref false; -val trace_domain = Unsynchronized.ref false; - -fun message s = if !quiet_mode then () else writeln s; -fun trace s = if !trace_domain then tracing s else (); - -open HOLCF_Library; - -(******************************************************************************) -(***************************** proofs about take ******************************) -(******************************************************************************) - -fun take_theorems - (dbinds : binding list) - (take_info : Domain_Take_Proofs.take_induct_info) - (constr_infos : Domain_Constructors.constr_info list) - (thy : theory) : thm list list * theory = -let - val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info; - val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy; - - val n = Free ("n", @{typ nat}); - val n' = @{const Suc} $ n; - - local - val newTs = map (#absT o #iso_info) constr_infos; - val subs = newTs ~~ map (fn t => t $ n) take_consts; - fun is_ID (Const (c, _)) = (c = @{const_name ID}) - | is_ID _ = false; - in - fun map_of_arg v T = - let val m = Domain_Take_Proofs.map_of_typ thy subs T; - in if is_ID m then v else mk_capply (m, v) end; - end - - fun prove_take_apps - ((dbind, take_const), constr_info) thy = - let - val {iso_info, con_specs, con_betas, ...} = constr_info; - val {abs_inverse, ...} = iso_info; - fun prove_take_app (con_const, args) = - let - val Ts = map snd args; - val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts); - val vs = map Free (ns ~~ Ts); - val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)); - val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts); - val goal = mk_trp (mk_eq (lhs, rhs)); - val rules = - [abs_inverse] @ con_betas @ @{thms take_con_rules} - @ take_Suc_thms @ deflation_thms @ deflation_take_thms; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; - in - Goal.prove_global thy [] [] goal (K tac) - end; - val take_apps = map prove_take_app con_specs; - in - yield_singleton Global_Theory.add_thmss - ((Binding.qualified true "take_rews" dbind, take_apps), - [Simplifier.simp_add]) thy - end; -in - fold_map prove_take_apps - (dbinds ~~ take_consts ~~ constr_infos) thy -end; - -(******************************************************************************) -(****************************** induction rules *******************************) -(******************************************************************************) - -val case_UU_allI = - @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}; - -fun prove_induction - (comp_dbind : binding) - (constr_infos : Domain_Constructors.constr_info list) - (take_info : Domain_Take_Proofs.take_induct_info) - (take_rews : thm list) - (thy : theory) = -let - val comp_dname = Binding.name_of comp_dbind; - - val iso_infos = map #iso_info constr_infos; - val exhausts = map #exhaust constr_infos; - val con_rews = maps #con_rews constr_infos; - val {take_consts, take_induct_thms, ...} = take_info; - - val newTs = map #absT iso_infos; - val P_names = Datatype_Prop.indexify_names (map (K "P") newTs); - val x_names = Datatype_Prop.indexify_names (map (K "x") newTs); - val P_types = map (fn T => T --> HOLogic.boolT) newTs; - val Ps = map Free (P_names ~~ P_types); - val xs = map Free (x_names ~~ newTs); - val n = Free ("n", HOLogic.natT); - - fun con_assm defined p (con, args) = - let - val Ts = map snd args; - val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts); - val vs = map Free (ns ~~ Ts); - val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); - fun ind_hyp (v, T) t = - case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t - | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t); - val t1 = mk_trp (p $ list_ccomb (con, vs)); - val t2 = fold_rev ind_hyp (vs ~~ Ts) t1; - val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2); - in fold_rev Logic.all vs (if defined then t3 else t2) end; - fun eq_assms ((p, T), cons) = - mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons; - val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos); - - val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); - fun quant_tac ctxt i = EVERY - (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names); - - (* FIXME: move this message to domain_take_proofs.ML *) - val is_finite = #is_finite take_info; - val _ = if is_finite - then message ("Proving finiteness rule for domain "^comp_dname^" ...") - else (); - - val _ = trace " Proving finite_ind..."; - val finite_ind = - let - val concls = - map (fn ((P, t), x) => P $ mk_capply (t $ n, x)) - (Ps ~~ take_consts ~~ xs); - val goal = mk_trp (foldr1 mk_conj concls); - - fun tacf {prems, context} = - let - (* Prove stronger prems, without definedness side conditions *) - fun con_thm p (con, args) = - let - val subgoal = con_assm false p (con, args); - val rules = prems @ con_rews @ simp_thms; - val simplify = asm_simp_tac (HOL_basic_ss addsimps rules); - fun arg_tac (lazy, _) = - rtac (if lazy then allI else case_UU_allI) 1; - val tacs = - rewrite_goals_tac @{thms atomize_all atomize_imp} :: - map arg_tac args @ - [REPEAT (rtac impI 1), ALLGOALS simplify]; - in - Goal.prove context [] [] subgoal (K (EVERY tacs)) - end; - fun eq_thms (p, cons) = map (con_thm p) cons; - val conss = map #con_specs constr_infos; - val prems' = maps eq_thms (Ps ~~ conss); - - val tacs1 = [ - quant_tac context 1, - simp_tac HOL_ss 1, - InductTacs.induct_tac context [[SOME "n"]] 1, - simp_tac (take_ss addsimps prems) 1, - TRY (safe_tac HOL_cs)]; - fun con_tac _ = - asm_simp_tac take_ss 1 THEN - (resolve_tac prems' THEN_ALL_NEW etac spec) 1; - fun cases_tacs (cons, exhaust) = - res_inst_tac context [(("y", 0), "x")] exhaust 1 :: - asm_simp_tac (take_ss addsimps prems) 1 :: - map con_tac cons; - val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts) - in - EVERY (map DETERM tacs) - end; - in Goal.prove_global thy [] assms goal tacf end; - - val _ = trace " Proving ind..."; - val ind = - let - val concls = map (op $) (Ps ~~ xs); - val goal = mk_trp (foldr1 mk_conj concls); - val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps; - fun tacf {prems, context} = - let - fun finite_tac (take_induct, fin_ind) = - rtac take_induct 1 THEN - (if is_finite then all_tac else resolve_tac prems 1) THEN - (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1; - val fin_inds = Project_Rule.projections context finite_ind; - in - TRY (safe_tac HOL_cs) THEN - EVERY (map finite_tac (take_induct_thms ~~ fin_inds)) - end; - in Goal.prove_global thy [] (adms @ assms) goal tacf end - - (* case names for induction rules *) - val dnames = map (fst o dest_Type) newTs; - val case_ns = - let - val adms = - if is_finite then [] else - if length dnames = 1 then ["adm"] else - map (fn s => "adm_" ^ Long_Name.base_name s) dnames; - val bottoms = - if length dnames = 1 then ["bottom"] else - map (fn s => "bottom_" ^ Long_Name.base_name s) dnames; - fun one_eq bot constr_info = - let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c)); - in bot :: map name_of (#con_specs constr_info) end; - in adms @ flat (map2 one_eq bottoms constr_infos) end; - - val inducts = Project_Rule.projections (ProofContext.init_global thy) ind; - fun ind_rule (dname, rule) = - ((Binding.empty, rule), - [Rule_Cases.case_names case_ns, Induct.induct_type dname]); - -in - thy - |> snd o Global_Theory.add_thms [ - ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), - ((Binding.qualified true "induct" comp_dbind, ind ), [])] - |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) -end; (* prove_induction *) - -(******************************************************************************) -(************************ bisimulation and coinduction ************************) -(******************************************************************************) - -fun prove_coinduction - (comp_dbind : binding, dbinds : binding list) - (constr_infos : Domain_Constructors.constr_info list) - (take_info : Domain_Take_Proofs.take_induct_info) - (take_rews : thm list list) - (thy : theory) : theory = -let - val iso_infos = map #iso_info constr_infos; - val newTs = map #absT iso_infos; - - val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info; - - val R_names = Datatype_Prop.indexify_names (map (K "R") newTs); - val R_types = map (fn T => T --> T --> boolT) newTs; - val Rs = map Free (R_names ~~ R_types); - val n = Free ("n", natT); - val reserved = "x" :: "y" :: R_names; - - (* declare bisimulation predicate *) - val bisim_bind = Binding.suffix_name "_bisim" comp_dbind; - val bisim_type = R_types ---> boolT; - val (bisim_const, thy) = - Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; - - (* define bisimulation predicate *) - local - fun one_con T (con, args) = - let - val Ts = map snd args; - val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts); - val ns2 = map (fn n => n^"'") ns1; - val vs1 = map Free (ns1 ~~ Ts); - val vs2 = map Free (ns2 ~~ Ts); - val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1)); - val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2)); - fun rel ((v1, v2), T) = - case AList.lookup (op =) (newTs ~~ Rs) T of - NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2; - val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]); - in - Library.foldr mk_ex (vs1 @ vs2, eqs) - end; - fun one_eq ((T, R), cons) = - let - val x = Free ("x", T); - val y = Free ("y", T); - val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T)); - val disjs = disj1 :: map (one_con T) cons; - in - mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs))) - end; - val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos); - val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs); - val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs); - in - val (bisim_def_thm, thy) = thy |> - yield_singleton (Global_Theory.add_defs false) - ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []); - end (* local *) - - (* prove coinduction lemma *) - val coind_lemma = - let - val assm = mk_trp (list_comb (bisim_const, Rs)); - fun one ((T, R), take_const) = - let - val x = Free ("x", T); - val y = Free ("y", T); - val lhs = mk_capply (take_const $ n, x); - val rhs = mk_capply (take_const $ n, y); - in - mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs)))) - end; - val goal = - mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts))); - val rules = @{thm Rep_CFun_strict1} :: take_0_thms; - fun tacf {prems, context} = - let - val prem' = rewrite_rule [bisim_def_thm] (hd prems); - val prems' = Project_Rule.projections context prem'; - val dests = map (fn th => th RS spec RS spec RS mp) prems'; - fun one_tac (dest, rews) = - dtac dest 1 THEN safe_tac HOL_cs THEN - ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews)); - in - rtac @{thm nat.induct} 1 THEN - simp_tac (HOL_ss addsimps rules) 1 THEN - safe_tac HOL_cs THEN - EVERY (map one_tac (dests ~~ take_rews)) - end - in - Goal.prove_global thy [] [assm] goal tacf - end; - - (* prove individual coinduction rules *) - fun prove_coind ((T, R), take_lemma) = - let - val x = Free ("x", T); - val y = Free ("y", T); - val assm1 = mk_trp (list_comb (bisim_const, Rs)); - val assm2 = mk_trp (R $ x $ y); - val goal = mk_trp (mk_eq (x, y)); - fun tacf {prems, context} = - let - val rule = hd prems RS coind_lemma; - in - rtac take_lemma 1 THEN - asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1 - end; - in - Goal.prove_global thy [] [assm1, assm2] goal tacf - end; - val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms); - val coind_binds = map (Binding.qualified true "coinduct") dbinds; - -in - thy |> snd o Global_Theory.add_thms - (map Thm.no_attributes (coind_binds ~~ coinds)) -end; (* let *) - -(******************************************************************************) -(******************************* main function ********************************) -(******************************************************************************) - -fun comp_theorems - (comp_dbind : binding) - (dbinds : binding list) - (take_info : Domain_Take_Proofs.take_induct_info) - (constr_infos : Domain_Constructors.constr_info list) - (thy : theory) = -let -val comp_dname = Binding.name_of comp_dbind; - -(* Test for emptiness *) -(* FIXME: reimplement emptiness test -local - open Domain_Library; - val dnames = map (fst o fst) eqs; - val conss = map snd eqs; - fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => - is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso - ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse - rec_of arg <> n andalso rec_to (rec_of arg::ns) - (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) - ) o snd) cons; - fun warn (n,cons) = - if rec_to [] false (n,cons) - then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) - else false; -in - val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; - val is_emptys = map warn n__eqs; -end; -*) - -(* Test for indirect recursion *) -local - val newTs = map (#absT o #iso_info) constr_infos; - fun indirect_typ (Type (_, Ts)) = - exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts - | indirect_typ _ = false; - fun indirect_arg (_, T) = indirect_typ T; - fun indirect_con (_, args) = exists indirect_arg args; - fun indirect_eq cons = exists indirect_con cons; -in - val is_indirect = exists indirect_eq (map #con_specs constr_infos); - val _ = - if is_indirect - then message "Indirect recursion detected, skipping proofs of (co)induction rules" - else message ("Proving induction properties of domain "^comp_dname^" ..."); -end; - -(* theorems about take *) - -val (take_rewss, thy) = - take_theorems dbinds take_info constr_infos thy; - -val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info; - -val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss; - -(* prove induction rules, unless definition is indirect recursive *) -val thy = - if is_indirect then thy else - prove_induction comp_dbind constr_infos take_info take_rews thy; - -val thy = - if is_indirect then thy else - prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy; - -in - (take_rews, thy) -end; (* let *) -end; (* struct *) diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Tools/fixrec.ML Wed Oct 20 21:26:51 2010 -0700 @@ -6,10 +6,10 @@ signature FIXREC = sig - val add_fixrec: bool -> (binding * typ option * mixfix) list - -> (Attrib.binding * term) list -> local_theory -> local_theory - val add_fixrec_cmd: bool -> (binding * string option * mixfix) list - -> (Attrib.binding * string) list -> local_theory -> local_theory + val add_fixrec: (binding * typ option * mixfix) list + -> (bool * (Attrib.binding * term)) list -> local_theory -> local_theory + val add_fixrec_cmd: (binding * string option * mixfix) list + -> (bool * (Attrib.binding * string)) list -> local_theory -> local_theory val add_matchers: (string * string) list -> theory -> theory val fixrec_simp_tac: Proof.context -> int -> tactic val setup: theory -> theory @@ -247,15 +247,15 @@ end; (* builds a monadic term for matching a function definition pattern *) -(* returns (name, arity, matcher) *) +(* returns (constant, (vars, matcher)) *) fun compile_lhs match_name pat rhs vs taken = case pat of Const(@{const_name Rep_CFun}, _) $ f $ x => let val (rhs', v, taken') = compile_pat match_name x rhs taken; in compile_lhs match_name f rhs' (v::vs) taken' end - | Free(_,_) => ((pat, length vs), big_lambdas vs rhs) - | Const(_,_) => ((pat, length vs), big_lambdas vs rhs) - | _ => fixrec_err ("function is not declared as constant in theory: " + | Free(_,_) => (pat, (vs, rhs)) + | Const(_,_) => (pat, (vs, rhs)) + | _ => fixrec_err ("invalid function pattern: " ^ ML_Syntax.print_term pat); fun strip_alls t = @@ -268,41 +268,24 @@ compile_lhs match_name lhs (mk_succeed rhs) [] (taken_names eq) end; -(* returns the sum (using +++) of the terms in ms *) -(* also applies "run" to the result! *) -fun fatbar arity ms = - let - fun LAM_Ts 0 t = ([], Term.fastype_of t) - | LAM_Ts n (_ $ Abs(_,T,t)) = - let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end - | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; - fun unLAM 0 t = t - | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t - | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; - fun reLAM ([], U) t = t - | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t)); - val msum = foldr1 mk_mplus (map (unLAM arity) ms); - val (Ts, U) = LAM_Ts arity (hd ms) - in - reLAM (rev Ts, dest_matchT U) (mk_run msum) - end; - (* this is the pattern-matching compiler function *) fun compile_eqs match_name eqs = let - val ((names, arities), mats) = - apfst ListPair.unzip (ListPair.unzip (map (compile_eq match_name) eqs)); - val cname = - case distinct (op =) names of + val (consts, matchers) = + ListPair.unzip (map (compile_eq match_name) eqs); + val const = + case distinct (op =) consts of [n] => n | _ => fixrec_err "all equations in block must define the same function"; - val arity = - case distinct (op =) arities of - [a] => a + val vars = + case distinct (op = o pairself length) (map fst matchers) of + [vars] => vars | _ => fixrec_err "all equations in block must have the same arity"; - val rhs = fatbar arity mats; + (* rename so all matchers use same free variables *) + fun rename (vs, t) = Term.subst_free (filter_out (op =) (vs ~~ vars)) t; + val rhs = big_lambdas vars (mk_run (foldr1 mk_mplus (map rename matchers))); in - mk_trp (cname === rhs) + mk_trp (const === rhs) end; (*************************************************************************) @@ -352,11 +335,11 @@ fun gen_fixrec prep_spec - (strict : bool) - raw_fixes - raw_spec + (raw_fixes : (binding * 'a option * mixfix) list) + (raw_spec' : (bool * (Attrib.binding * 'b)) list) (lthy : local_theory) = let + val (skips, raw_spec) = ListPair.unzip raw_spec'; val (fixes : ((binding * typ) * mixfix) list, spec : (Attrib.binding * term) list) = fst (prep_spec raw_fixes raw_spec lthy); @@ -369,7 +352,7 @@ fun block_of_name n = map_filter (fn (m,eq) => if m = n then SOME eq else NONE) - (all_names ~~ spec); + (all_names ~~ (spec ~~ skips)); val blocks = map block_of_name names; val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy); @@ -377,27 +360,25 @@ case Symtab.lookup matcher_tab c of SOME m => m | NONE => fixrec_err ("unknown pattern constructor: " ^ c); - val matches = map (compile_eqs match_name) (map (map snd) blocks); + val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks); val spec' = map (pair Attrib.empty_binding) matches; val (lthy, cnames, fixdef_thms, unfold_thms) = add_fixdefs fixes spec' lthy; + + val blocks' = map (map fst o filter_out snd) blocks; + val simps : (Attrib.binding * thm) list list = + map (make_simps lthy) (unfold_thms ~~ blocks'); + fun mk_bind n : Attrib.binding = + (Binding.qualify true n (Binding.name "simps"), + [Attrib.internal (K Simplifier.simp_add)]); + val simps1 : (Attrib.binding * thm list) list = + map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps); + val simps2 : (Attrib.binding * thm list) list = + map (apsnd (fn thm => [thm])) (flat simps); + val (_, lthy) = lthy + |> fold_map Local_Theory.note (simps1 @ simps2); in - if strict then let (* only prove simp rules if strict = true *) - val simps : (Attrib.binding * thm) list list = - map (make_simps lthy) (unfold_thms ~~ blocks); - fun mk_bind n : Attrib.binding = - (Binding.qualify true n (Binding.name "simps"), - [Attrib.internal (K Simplifier.simp_add)]); - val simps1 : (Attrib.binding * thm list) list = - map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps); - val simps2 : (Attrib.binding * thm list) list = - map (apsnd (fn thm => [thm])) (flat simps); - val (_, lthy) = lthy - |> fold_map Local_Theory.note (simps1 @ simps2); - in - lthy - end - else lthy + lthy end; in @@ -412,10 +393,15 @@ (******************************** Parsers ********************************) (*************************************************************************) +val alt_specs' : (bool * (Attrib.binding * string)) list parser = + Parse.enum1 "|" + (Parse.opt_keyword "unchecked" -- Parse_Spec.spec --| + Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|"))); + val _ = Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl - ((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs - >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs)); + (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs') + >> (fn (fixes, specs) => add_fixrec_cmd fixes specs)); val setup = Method.setup @{binding fixrec_simp} diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Tools/repdef.ML Wed Oct 20 21:26:51 2010 -0700 @@ -84,12 +84,11 @@ |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); (*set*) - val in_defl = @{term "in_defl :: udom => defl => bool"}; - val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); + val set = @{const defl_set} $ defl; (*pcpodef*) - val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_defl} 1; - val tac2 = rtac @{thm adm_mem_Collect_in_defl} 1; + val tac1 = rtac @{thm defl_set_bottom} 1; + val tac2 = rtac @{thm adm_defl_set} 1; val ((info, cpo_info, pcpo_info), thy) = thy |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/Tutorial/Fixrec_ex.thy --- a/src/HOLCF/Tutorial/Fixrec_ex.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/Tutorial/Fixrec_ex.thy Wed Oct 20 21:26:51 2010 -0700 @@ -115,22 +115,21 @@ because it only applies when the first pattern fails. *} -fixrec (permissive) +fixrec lzip2 :: "'a llist \ 'b llist \ ('a \ 'b) llist" where - "lzip2\(lCons\x\xs)\(lCons\y\ys) = lCons\(x, y)\(lzip\xs\ys)" -| "lzip2\xs\ys = lNil" + "lzip2\(lCons\x\xs)\(lCons\y\ys) = lCons\(x, y)\(lzip2\xs\ys)" +| (unchecked) "lzip2\xs\ys = lNil" text {* Usually fixrec tries to prove all equations as theorems. - The "permissive" option overrides this behavior, so fixrec - does not produce any simp rules. + The "unchecked" option overrides this behavior, so fixrec + does not attempt to prove that particular equation. *} text {* Simp rules can be generated later using @{text fixrec_simp}. *} lemma lzip2_simps [simp]: - "lzip2\(lCons\x\xs)\(lCons\y\ys) = lCons\(x, y)\(lzip\xs\ys)" "lzip2\(lCons\x\xs)\lNil = lNil" "lzip2\lNil\(lCons\y\ys) = lNil" "lzip2\lNil\lNil = lNil" diff -r 767a28027b68 -r 6547d0f079ed src/HOLCF/ex/Domain_Proofs.thy --- a/src/HOLCF/ex/Domain_Proofs.thy Tue Oct 19 15:13:35 2010 +0100 +++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Oct 20 21:26:51 2010 -0700 @@ -82,14 +82,14 @@ text {* Use @{text pcpodef} with the appropriate type combinator. *} -pcpodef (open) 'a foo = "{x. x ::: foo_defl\DEFL('a)}" -by (simp_all add: adm_in_defl) +pcpodef (open) 'a foo = "defl_set (foo_defl\DEFL('a))" +by (rule defl_set_bottom, rule adm_defl_set) -pcpodef (open) 'a bar = "{x. x ::: bar_defl\DEFL('a)}" -by (simp_all add: adm_in_defl) +pcpodef (open) 'a bar = "defl_set (bar_defl\DEFL('a))" +by (rule defl_set_bottom, rule adm_defl_set) -pcpodef (open) 'a baz = "{x. x ::: baz_defl\DEFL('a)}" -by (simp_all add: adm_in_defl) +pcpodef (open) 'a baz = "defl_set (baz_defl\DEFL('a))" +by (rule defl_set_bottom, rule adm_defl_set) text {* Prove rep instance using lemma @{text typedef_rep_class}. *} @@ -200,25 +200,25 @@ subsection {* Step 3: Define rep and abs functions *} -text {* Define them all using @{text coerce}! *} +text {* Define them all using @{text prj} and @{text emb}! *} definition foo_rep :: "'a foo \ one \ ('a\<^sub>\ \ ('a bar)\<^sub>\)" -where "foo_rep \ coerce" +where "foo_rep \ prj oo emb" definition foo_abs :: "one \ ('a\<^sub>\ \ ('a bar)\<^sub>\) \ 'a foo" -where "foo_abs \ coerce" +where "foo_abs \ prj oo emb" definition bar_rep :: "'a bar \ ('a baz \ tr)\<^sub>\" -where "bar_rep \ coerce" +where "bar_rep \ prj oo emb" definition bar_abs :: "('a baz \ tr)\<^sub>\ \ 'a bar" -where "bar_abs \ coerce" +where "bar_abs \ prj oo emb" definition baz_rep :: "'a baz \ ('a foo convex_pd \ tr)\<^sub>\" -where "baz_rep \ coerce" +where "baz_rep \ prj oo emb" definition baz_abs :: "('a foo convex_pd \ tr)\<^sub>\ \ 'a baz" -where "baz_abs \ coerce" +where "baz_abs \ prj oo emb" text {* Prove isomorphism rules. *}