diff --git a/src/HOL/HOLCF/Pcpo.thy b/src/HOL/HOLCF/Pcpo.thy --- a/src/HOL/HOLCF/Pcpo.thy +++ b/src/HOL/HOLCF/Pcpo.thy @@ -1,258 +1,258 @@ (* Title: HOL/HOLCF/Pcpo.thy Author: Franz Regensburger *) section \Classes cpo and pcpo\ theory Pcpo imports Porder begin subsection \Complete partial orders\ text \The class cpo of chain complete partial orders\ class cpo = po + assumes cpo: "chain S \ \x. range S <<| x" begin text \in cpo's everthing equal to THE lub has lub properties for every chain\ lemma cpo_lubI: "chain S \ range S <<| (\i. S i)" by (fast dest: cpo elim: is_lub_lub) lemma thelubE: "\chain S; (\i. S i) = l\ \ range S <<| l" by (blast dest: cpo intro: is_lub_lub) text \Properties of the lub\ lemma is_ub_thelub: "chain S \ S x \ (\i. S i)" by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1]) lemma is_lub_thelub: "\chain S; range S <| x\ \ (\i. S i) \ x" by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2]) lemma lub_below_iff: "chain S \ (\i. S i) \ x \ (\i. S i \ x)" by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def) lemma lub_below: "\chain S; \i. S i \ x\ \ (\i. S i) \ x" by (simp add: lub_below_iff) lemma below_lub: "\chain S; x \ S i\ \ x \ (\i. S i)" by (erule below_trans, erule is_ub_thelub) lemma lub_range_mono: "\range X \ range Y; chain Y; chain X\ \ (\i. X i) \ (\i. Y i)" apply (erule lub_below) apply (subgoal_tac "\j. X i = Y j") apply clarsimp apply (erule is_ub_thelub) apply auto done lemma lub_range_shift: "chain Y \ (\i. Y (i + j)) = (\i. Y i)" apply (rule below_antisym) apply (rule lub_range_mono) apply fast apply assumption apply (erule chain_shift) apply (rule lub_below) apply assumption apply (rule_tac i="i" in below_lub) apply (erule chain_shift) apply (erule chain_mono) apply (rule le_add1) done lemma maxinch_is_thelub: "chain Y \ max_in_chain i Y = ((\i. Y i) = Y i)" apply (rule iffI) apply (fast intro!: lub_eqI lub_finch1) apply (unfold max_in_chain_def) apply (safe intro!: below_antisym) apply (fast elim!: chain_mono) apply (drule sym) apply (force elim!: is_ub_thelub) done text \the \\\ relation between two chains is preserved by their lubs\ lemma lub_mono: "\chain X; chain Y; \i. X i \ Y i\ \ (\i. X i) \ (\i. Y i)" by (fast elim: lub_below below_lub) text \the = relation between two chains is preserved by their lubs\ lemma lub_eq: "(\i. X i = Y i) \ (\i. X i) = (\i. Y i)" by simp lemma ch2ch_lub: assumes 1: "\j. chain (\i. Y i j)" assumes 2: "\i. chain (\j. Y i j)" shows "chain (\i. \j. Y i j)" apply (rule chainI) apply (rule lub_mono [OF 2 2]) apply (rule chainE [OF 1]) done lemma diag_lub: assumes 1: "\j. chain (\i. Y i j)" assumes 2: "\i. chain (\j. Y i j)" shows "(\i. \j. Y i j) = (\i. Y i i)" proof (rule below_antisym) have 3: "chain (\i. Y i i)" apply (rule chainI) apply (rule below_trans) apply (rule chainE [OF 1]) apply (rule chainE [OF 2]) done have 4: "chain (\i. \j. Y i j)" by (rule ch2ch_lub [OF 1 2]) show "(\i. \j. Y i j) \ (\i. Y i i)" apply (rule lub_below [OF 4]) apply (rule lub_below [OF 2]) apply (rule below_lub [OF 3]) apply (rule below_trans) apply (rule chain_mono [OF 1 max.cobounded1]) apply (rule chain_mono [OF 2 max.cobounded2]) done show "(\i. Y i i) \ (\i. \j. Y i j)" apply (rule lub_mono [OF 3 4]) apply (rule is_ub_thelub [OF 2]) done qed lemma ex_lub: assumes 1: "\j. chain (\i. Y i j)" assumes 2: "\i. chain (\j. Y i j)" shows "(\i. \j. Y i j) = (\j. \i. Y i j)" by (simp add: diag_lub 1 2) end subsection \Pointed cpos\ text \The class pcpo of pointed cpos\ class pcpo = cpo + assumes least: "\x. \y. x \ y" begin definition bottom :: "'a" ("\") where "bottom = (THE x. \y. x \ y)" lemma minimal [iff]: "\ \ x" unfolding bottom_def apply (rule the1I2) apply (rule ex_ex1I) apply (rule least) apply (blast intro: below_antisym) apply simp done end text \Old "UU" syntax:\ syntax UU :: logic translations "UU" \ "CONST bottom" text \Simproc to rewrite \<^term>\\ = x\ to \<^term>\x = \\.\ -setup \Reorient_Proc.add (fn Const(\<^const_name>\bottom\, _) => true | _ => false)\ +setup \Reorient_Proc.add (fn \<^Const_>\bottom _\ => true | _ => false)\ simproc_setup reorient_bottom ("\ = x") = Reorient_Proc.proc text \useful lemmas about \<^term>\\\\ lemma below_bottom_iff [simp]: "x \ \ \ x = \" by (simp add: po_eq_conv) lemma eq_bottom_iff: "x = \ \ x \ \" by simp lemma bottomI: "x \ \ \ x = \" by (subst eq_bottom_iff) lemma lub_eq_bottom_iff: "chain Y \ (\i. Y i) = \ \ (\i. Y i = \)" by (simp only: eq_bottom_iff lub_below_iff) subsection \Chain-finite and flat cpos\ text \further useful classes for HOLCF domains\ class chfin = po + assumes chfin: "chain Y \ \n. max_in_chain n Y" begin subclass cpo apply standard apply (frule chfin) apply (blast intro: lub_finch1) done lemma chfin2finch: "chain Y \ finite_chain Y" by (simp add: chfin finite_chain_def) end class flat = pcpo + assumes ax_flat: "x \ y \ x = \ \ x = y" begin subclass chfin proof fix Y assume *: "chain Y" show "\n. max_in_chain n Y" apply (unfold max_in_chain_def) apply (cases "\i. Y i = \") apply simp apply simp apply (erule exE) apply (rule_tac x="i" in exI) apply clarify using * apply (blast dest: chain_mono ax_flat) done qed lemma flat_below_iff: "x \ y \ x = \ \ x = y" by (safe dest!: ax_flat) lemma flat_eq: "a \ \ \ a \ b = (a = b)" by (safe dest!: ax_flat) end subsection \Discrete cpos\ class discrete_cpo = below + assumes discrete_cpo [simp]: "x \ y \ x = y" begin subclass po by standard simp_all text \In a discrete cpo, every chain is constant\ lemma discrete_chain_const: assumes S: "chain S" shows "\x. S = (\i. x)" proof (intro exI ext) fix i :: nat from S le0 have "S 0 \ S i" by (rule chain_mono) then have "S 0 = S i" by simp then show "S i = S 0" by (rule sym) qed subclass chfin proof fix S :: "nat \ 'a" assume S: "chain S" then have "\x. S = (\i. x)" by (rule discrete_chain_const) then have "max_in_chain 0 S" by (auto simp: max_in_chain_def) then show "\i. max_in_chain i S" .. qed end end diff --git a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML @@ -1,138 +1,138 @@ (* Title: HOL/HOLCF/Tools/Domain/domain_axioms.ML Author: David von Oheimb Author: Brian Huffman Syntax generator for domain command. *) signature DOMAIN_AXIOMS = sig val axiomatize_isomorphism : binding * (typ * typ) -> theory -> Domain_Take_Proofs.iso_info * theory val axiomatize_lub_take : binding * term -> theory -> thm * theory val add_axioms : (binding * mixfix * (typ * typ)) list -> theory -> (Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info) * theory end structure Domain_Axioms : DOMAIN_AXIOMS = struct open HOLCF_Library infixr 6 ->> infix -->> infix 9 ` fun axiomatize_isomorphism (dbind : binding, (lhsT, rhsT)) (thy : theory) : Domain_Take_Proofs.iso_info * theory = let val abs_bind = Binding.suffix_name "_abs" dbind val rep_bind = Binding.suffix_name "_rep" dbind val (abs_const, thy) = Sign.declare_const_global ((abs_bind, rhsT ->> lhsT), NoSyn) thy val (rep_const, thy) = Sign.declare_const_global ((rep_bind, lhsT ->> rhsT), NoSyn) thy val x = Free ("x", lhsT) val y = Free ("y", rhsT) val abs_iso_eqn = Logic.all y (mk_trp (mk_eq (rep_const ` (abs_const ` y), y))) val rep_iso_eqn = Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x))) val abs_iso_bind = Binding.qualify_name true dbind "abs_iso" val rep_iso_bind = Binding.qualify_name true dbind "rep_iso" val (abs_iso_thm, thy) = Specification.axiom ((abs_iso_bind, []), abs_iso_eqn) thy val (rep_iso_thm, thy) = Specification.axiom ((rep_iso_bind, []), rep_iso_eqn) thy val result = { absT = lhsT, repT = rhsT, abs_const = abs_const, rep_const = rep_const, abs_inverse = Drule.export_without_context abs_iso_thm, rep_inverse = Drule.export_without_context rep_iso_thm } in (result, thy) end fun axiomatize_lub_take (dbind : binding, take_const : term) (thy : theory) : thm * theory = let - val i = Free ("i", natT) + val i = Free ("i", \<^Type>\nat\) val T = (fst o dest_cfunT o range_type o fastype_of) take_const val lub_take_eqn = mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)) val lub_take_bind = Binding.qualify_name true dbind "lub_take" val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy in (lub_take_thm, thy) end fun add_axioms (dom_eqns : (binding * mixfix * (typ * typ)) list) (thy : theory) = let val dbinds = map #1 dom_eqns (* declare new types *) fun thy_type (dbind, mx, (lhsT, _)) = (dbind, (length o snd o dest_Type) lhsT, mx) val thy = Sign.add_types_global (map thy_type dom_eqns) thy (* axiomatize type constructor arities *) fun thy_arity (_, _, (lhsT, _)) = let val (dname, tvars) = dest_Type lhsT in (dname, map (snd o dest_TFree) tvars, \<^sort>\pcpo\) end val thy = fold (Axclass.arity_axiomatization o thy_arity) dom_eqns thy (* declare and axiomatize abs/rep *) val (iso_infos, thy) = fold_map axiomatize_isomorphism (map (fn (dbind, _, eqn) => (dbind, eqn)) dom_eqns) thy (* define take functions *) val (take_info, thy) = Domain_Take_Proofs.define_take_functions (dbinds ~~ iso_infos) thy (* declare lub_take axioms *) val (lub_take_thms, thy) = fold_map axiomatize_lub_take (dbinds ~~ #take_consts take_info) thy (* prove additional take theorems *) val (take_info2, thy) = Domain_Take_Proofs.add_lub_take_theorems (dbinds ~~ iso_infos) take_info lub_take_thms thy (* define map functions *) val (_, thy) = Domain_Isomorphism.define_map_functions (dbinds ~~ iso_infos) thy in ((iso_infos, take_info2), thy) end end (* struct *) diff --git a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML @@ -1,441 +1,441 @@ (* Title: HOL/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 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 + val n' = \<^Const>\Suc for 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 + fun is_ID \<^Const_>\ID _\ = true + | is_ID _ = false in fun map_of_arg thy 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, ...} : Domain_Constructors.constr_info = 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"] (Old_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 thy) 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 fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1 in Goal.prove_global thy [] [] goal (tac o #context) end val take_apps = map prove_take_app con_specs in yield_singleton Global_Theory.add_thmss ((Binding.qualify_name true dbind "take_rews", 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 \ \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 = Old_Datatype_Prop.indexify_names (map (K "P") newTs) val x_names = Old_Datatype_Prop.indexify_names (map (K "x") newTs) - val P_types = map (fn T => T --> HOLogic.boolT) newTs + val P_types = map (fn T => T --> \<^Type>\bool\) newTs val Ps = map Free (P_names ~~ P_types) val xs = map Free (x_names ~~ newTs) - val n = Free ("n", HOLogic.natT) + val n = Free ("n", \<^Type>\nat\) fun con_assm defined p (con, args) = let val Ts = map snd args val ns = Name.variant_list P_names (Old_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) fun quant_tac ctxt i = EVERY (map (fn name => Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), 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 = ctxt} = let val take_ctxt = put_simpset HOL_ss ctxt addsimps (@{thm Rep_cfun_strict1} :: take_rews) (* 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 @ @{thms simp_thms} val simplify = asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) fun arg_tac (lazy, _) = resolve_tac ctxt [if lazy then allI else case_UU_allI] 1 fun tacs ctxt = rewrite_goals_tac ctxt @{thms atomize_all atomize_imp} :: map arg_tac args @ [REPEAT (resolve_tac ctxt [impI] 1), ALLGOALS simplify] in Goal.prove ctxt [] [] subgoal (EVERY o tacs o #context) 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 ctxt 1, simp_tac (put_simpset HOL_ss ctxt) 1, Induct_Tacs.induct_tac ctxt [[SOME "n"]] NONE 1, simp_tac (take_ctxt addsimps prems) 1, TRY (safe_tac (put_claset HOL_cs ctxt))] fun con_tac _ = asm_simp_tac take_ctxt 1 THEN (resolve_tac ctxt prems' THEN_ALL_NEW eresolve_tac ctxt [spec]) 1 fun cases_tacs (cons, exhaust) = Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), "x")] [] exhaust 1 :: asm_simp_tac (take_ctxt 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 = ctxt} = let fun finite_tac (take_induct, fin_ind) = resolve_tac ctxt [take_induct] 1 THEN (if is_finite then all_tac else resolve_tac ctxt prems 1) THEN (resolve_tac ctxt [fin_ind] THEN_ALL_NEW solve_tac ctxt prems) 1 val fin_inds = Project_Rule.projections ctxt finite_ind in TRY (safe_tac (put_claset HOL_cs ctxt)) 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 : Domain_Constructors.constr_info) = let fun name_of (c, _) = 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 (Proof_Context.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.qualify_name true comp_dbind "finite_induct", finite_ind), []), ((Binding.qualify_name true comp_dbind "induct", 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 = Old_Datatype_Prop.indexify_names (map (K "R") newTs) - val R_types = map (fn T => T --> T --> boolT) newTs + val R_types = map (fn T => T --> T --> \<^Type>\bool\) newTs val Rs = map Free (R_names ~~ R_types) - val n = Free ("n", natT) + val n = Free ("n", \<^Type>\nat\) 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_type = R_types ---> \<^Type>\bool\ val (bisim_const, thy) = Sign.declare_const_global ((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 (Old_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.qualify_name true comp_dbind "bisim_def", 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 = ctxt} = let val prem' = rewrite_rule ctxt [bisim_def_thm] (hd prems) val prems' = Project_Rule.projections ctxt prem' val dests = map (fn th => th RS spec RS spec RS mp) prems' fun one_tac (dest, rews) = dresolve_tac ctxt [dest] 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rews)) in resolve_tac ctxt @{thms nat.induct} 1 THEN simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1 THEN safe_tac (put_claset HOL_cs ctxt) 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 = ctxt} = let val rule = hd prems RS coind_lemma in resolve_tac ctxt [take_lemma] 1 THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt 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 (fn b => Binding.qualify_name true b "coinduct") dbinds in thy |> snd o Global_Theory.add_thms (map Thm.no_attributes (coind_binds ~~ coinds)) end (* let *) (******************************************************************************) (******************************* main function ********************************) (******************************************************************************) fun comp_theorems (dbinds : binding list) (take_info : Domain_Take_Proofs.take_induct_info) (constr_infos : Domain_Constructors.constr_info list) (thy : theory) = let val comp_dbind = Binding.conglomerate dbinds 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, nth conss (rec_of arg))) ) o snd) cons fun warn (n,cons) = if rec_to [] false (n,cons) then (warning ("domain " ^ 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_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 --git a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML @@ -1,763 +1,760 @@ (* Title: HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Author: Brian Huffman Defines new types satisfying the given domain equations. *) signature DOMAIN_ISOMORPHISM = sig val domain_isomorphism : (string list * binding * mixfix * typ * (binding * binding) option) list -> theory -> (Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info) * theory val define_map_functions : (binding * Domain_Take_Proofs.iso_info) list -> theory -> { map_consts : term list, map_apply_thms : thm list, map_unfold_thms : thm list, map_cont_thm : thm, deflation_map_thms : thm list } * theory val domain_isomorphism_cmd : (string list * binding * mixfix * string * (binding * binding) option) list -> theory -> theory end structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = struct val beta_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms} addsimprocs [\<^simproc>\beta_cfun_proc\]) fun is_cpo thy T = Sign.of_sort thy (T, \<^sort>\cpo\) (******************************************************************************) (************************** building types and terms **************************) (******************************************************************************) open HOLCF_Library infixr 6 ->> infixr -->> val udomT = \<^typ>\udom\ val deflT = \<^typ>\udom defl\ val udeflT = \<^typ>\udom u defl\ -fun mk_DEFL T = - Const (\<^const_name>\defl\, Term.itselfT T --> deflT) $ Logic.mk_type T +fun mk_DEFL T = \<^Const>\defl T for \Logic.mk_type T\\ -fun dest_DEFL (Const (\<^const_name>\defl\, _) $ t) = Logic.dest_type t +fun dest_DEFL \<^Const_>\defl _ for t\ = Logic.dest_type t | dest_DEFL t = raise TERM ("dest_DEFL", [t]) -fun mk_LIFTDEFL T = - Const (\<^const_name>\liftdefl\, Term.itselfT T --> udeflT) $ Logic.mk_type T +fun mk_LIFTDEFL T = \<^Const>\liftdefl T for \Logic.mk_type T\\ -fun dest_LIFTDEFL (Const (\<^const_name>\liftdefl\, _) $ t) = Logic.dest_type t +fun dest_LIFTDEFL \<^Const_>\liftdefl _ for t\ = Logic.dest_type t | dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t]) -fun mk_u_defl t = mk_capply (\<^const>\u_defl\, t) +fun mk_u_defl t = mk_capply (\<^Const>\u_defl\, t) -fun emb_const T = Const (\<^const_name>\emb\, T ->> udomT) -fun prj_const T = Const (\<^const_name>\prj\, udomT ->> T) +fun emb_const T = \<^Const>\emb T\ +fun prj_const T = \<^Const>\prj 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) +fun isodefl_const T = \<^Const>\isodefl T\ -fun isodefl'_const T = - Const (\<^const_name>\isodefl'\, (T ->> T) --> udeflT --> HOLogic.boolT) +fun isodefl'_const T = \<^Const>\isodefl' T\ fun mk_deflation t = - Const (\<^const_name>\deflation\, Term.fastype_of t --> boolT) $ t + let val T = #1 (dest_cfunT (Term.fastype_of t)) + in \<^Const>\deflation T for t\ end (* splits a cterm into the right and lefthand sides of equality *) fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t) fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) (******************************************************************************) (****************************** isomorphism info ******************************) (******************************************************************************) fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm = let val abs_iso = #abs_inverse info val rep_iso = #rep_inverse info val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso] in Drule.zero_var_indexes thm end (******************************************************************************) (*************** fixed-point definitions and unfolding theorems ***************) (******************************************************************************) fun mk_projs [] _ = [] | mk_projs (x::[]) t = [(x, t)] | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t) fun add_fixdefs (spec : (binding * term) list) (thy : theory) : (thm list * thm list * thm) * theory = let val binds = map fst spec val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec) val functional = lambda_tuple lhss (mk_tuple rhss) val fixpoint = mk_fix (mk_cabs functional) (* project components of fixpoint *) val projs = mk_projs lhss fixpoint (* convert parameters to lambda abstractions *) fun mk_eqn (lhs, rhs) = case lhs of - Const (\<^const_name>\Rep_cfun\, _) $ f $ (x as Free _) => + \<^Const_>\Rep_cfun _ _ for f \x as Free _\\ => mk_eqn (f, big_lambda x rhs) - | f $ Const (\<^const_name>\Pure.type\, T) => - mk_eqn (f, Abs ("t", T, rhs)) + | f $ \<^Const_>\Pure.type T\ => + mk_eqn (f, Abs ("t", \<^Type>\itself T\, rhs)) | Const _ => Logic.mk_equals (lhs, rhs) | _ => raise TERM ("lhs not of correct form", [lhs, rhs]) val eqns = map mk_eqn projs (* register constant definitions *) val (fixdef_thms, thy) = (Global_Theory.add_defs false o map Thm.no_attributes) (map Thm.def_binding binds ~~ eqns) thy (* prove applied version of definitions *) fun prove_proj (lhs, rhs) = let fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN (simp_tac (put_simpset beta_ss ctxt)) 1 val goal = Logic.mk_equals (lhs, rhs) in Goal.prove_global thy [] [] goal (tac o #context) end val proj_thms = map prove_proj projs (* mk_tuple lhss == fixpoint *) fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2] val tuple_fixdef_thm = foldr1 pair_equalI proj_thms val cont_thm = let val prop = mk_trp (mk_cont functional) val rules = Named_Theorems.get (Proof_Context.init_global thy) \<^named_theorems>\cont2cont\ fun tac ctxt = REPEAT_ALL_NEW (match_tac ctxt (rev rules)) 1 in Goal.prove_global thy [] [] prop (tac o #context) end val tuple_unfold_thm = (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) |> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv} fun mk_unfold_thms [] _ = [] | mk_unfold_thms (n::[]) thm = [(n, thm)] | mk_unfold_thms (n::ns) thm = let val thmL = thm RS @{thm Pair_eqD1} val thmR = thm RS @{thm Pair_eqD2} in (n, thmL) :: mk_unfold_thms ns thmR end val unfold_binds = map (Binding.suffix_name "_unfold") binds (* register unfold theorems *) val (unfold_thms, thy) = (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (mk_unfold_thms unfold_binds tuple_unfold_thm) thy in ((proj_thms, unfold_thms, cont_thm), thy) end (******************************************************************************) (****************** deflation combinators and map functions *******************) (******************************************************************************) fun defl_of_typ (thy : theory) (tab1 : (typ * term) list) (tab2 : (typ * term) list) (T : typ) : term = let val defl_simps = Named_Theorems.get (Proof_Context.init_global thy) \<^named_theorems>\domain_defl_simps\ val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) (rev defl_simps) val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2 fun proc1 t = (case dest_DEFL t of TFree (a, _) => SOME (Free ("d" ^ Library.unprefix "'" a, deflT)) | _ => NONE) handle TERM _ => NONE fun proc2 t = (case dest_LIFTDEFL t of TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, udeflT)) | _ => NONE) handle TERM _ => NONE in Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T) end (******************************************************************************) (********************* declaring definitions and theorems *********************) (******************************************************************************) fun define_const (bind : binding, rhs : term) (thy : theory) : (term * thm) * theory = let val typ = Term.fastype_of rhs val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy val eqn = Logic.mk_equals (const, rhs) val def = Thm.no_attributes (Thm.def_binding bind, eqn) val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy in ((const, def_thm), thy) end fun add_qualified_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms ((Binding.qualify_name true dbind name, thm), []) (******************************************************************************) (*************************** defining map functions ***************************) (******************************************************************************) fun define_map_functions (spec : (binding * Domain_Take_Proofs.iso_info) list) (thy : theory) = let (* retrieve components of spec *) val dbinds = map fst spec val iso_infos = map snd spec val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos fun mapT (T as Type (_, Ts)) = (map (fn T => T ->> T) (filter (is_cpo thy) Ts)) -->> (T ->> T) | mapT T = T ->> T (* declare map functions *) fun declare_map_const (tbind, (lhsT, _)) thy = let val map_type = mapT lhsT val map_bind = Binding.suffix_name "_map" tbind in Sign.declare_const_global ((map_bind, map_type), NoSyn) thy end val (map_consts, thy) = thy |> fold_map declare_map_const (dbinds ~~ dom_eqns) (* defining equations for map functions *) local fun unprime a = Library.unprefix "'" a fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T) fun map_lhs (map_const, lhsT) = (lhsT, list_ccomb (map_const, map mapvar (filter (is_cpo thy) (snd (dest_Type lhsT))))) val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns) val Ts = (snd o dest_Type o fst o hd) dom_eqns val tab = (Ts ~~ map mapvar Ts) @ tab1 fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) = let val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT val body = Domain_Take_Proofs.map_of_typ thy tab rhsT val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)) in mk_eqs (lhs, rhs) end in val map_specs = map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns) end (* register recursive definition of map functions *) val map_binds = map (Binding.suffix_name "_map") dbinds val ((map_apply_thms, map_unfold_thms, map_cont_thm), thy) = add_fixdefs (map_binds ~~ map_specs) thy (* prove deflation theorems for map functions *) val deflation_abs_rep_thms = map deflation_abs_rep iso_infos val deflation_map_thm = let fun unprime a = Library.unprefix "'" a fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T) fun mk_assm T = mk_trp (mk_deflation (mk_f T)) fun mk_goal (map_const, (lhsT, _)) = let val (_, Ts) = dest_Type lhsT val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts)) in mk_deflation map_term end val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns val goals = map mk_goal (map_consts ~~ dom_eqns) val goal = mk_trp (foldr1 HOLogic.mk_conj goals) val adm_rules = @{thms adm_conj adm_subst [OF _ adm_deflation] cont2cont_fst cont2cont_snd cont_id} val bottom_rules = @{thms fst_strict snd_strict deflation_bottom simp_thms} val tuple_rules = @{thms split_def fst_conv snd_conv} val deflation_rules = @{thms conjI deflation_ID} @ deflation_abs_rep_thms @ Domain_Take_Proofs.get_deflation_thms thy in Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} => EVERY [rewrite_goals_tac ctxt map_apply_thms, resolve_tac ctxt [map_cont_thm RS @{thm cont_fix_ind}] 1, REPEAT (resolve_tac ctxt adm_rules 1), simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1, REPEAT (eresolve_tac ctxt @{thms conjE} 1), REPEAT (resolve_tac ctxt (deflation_rules @ prems) 1 ORELSE assume_tac ctxt 1)]) end fun conjuncts [] _ = [] | conjuncts (n::[]) thm = [(n, thm)] | conjuncts (n::ns) thm = let val thmL = thm RS @{thm conjunct1} val thmR = thm RS @{thm conjunct2} in (n, thmL):: conjuncts ns thmR end val deflation_map_binds = dbinds |> map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map") val (deflation_map_thms, thy) = thy |> (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (conjuncts deflation_map_binds deflation_map_thm) (* register indirect recursion in theory data *) local fun register_map (dname, args) = Domain_Take_Proofs.add_rec_type (dname, args) val dnames = map (fst o dest_Type o fst) dom_eqns fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => [] val argss = map args dom_eqns in val thy = fold register_map (dnames ~~ argss) thy end (* register deflation theorems *) val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy val result = { map_consts = map_consts, map_apply_thms = map_apply_thms, map_unfold_thms = map_unfold_thms, map_cont_thm = map_cont_thm, deflation_map_thms = deflation_map_thms } in (result, thy) end (******************************************************************************) (******************************* main function ********************************) (******************************************************************************) fun read_typ thy str sorts = let val ctxt = Proof_Context.init_global thy |> fold (Variable.declare_typ o TFree) sorts val T = Syntax.read_typ ctxt str in (T, Term.add_tfreesT T sorts) end fun cert_typ sign raw_T sorts = 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, sorts') end fun gen_domain_isomorphism (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list) (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list) (thy: theory) : (Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info) * theory = let (* this theory is used just for parsing *) val tmp_thy = thy |> Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) => (tbind, length tvs, mx)) doms_raw) fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts = let val (typ, sorts') = prep_typ thy typ_raw sorts in ((vs, t, mx, typ, morphs), sorts') end val (doms : (string list * binding * mixfix * typ * (binding * binding) option) list, sorts : (string * sort) list) = fold_map (prep_dom tmp_thy) doms_raw [] (* lookup function for sorts of type variables *) fun the_sort v = the (AList.lookup (op =) sorts v) (* declare arities in temporary theory *) val tmp_thy = let fun arity (vs, tbind, _, _, _) = (Sign.full_name thy tbind, map the_sort vs, \<^sort>\domain\) in fold Axclass.arity_axiomatization (map arity doms) tmp_thy end (* check bifiniteness of right-hand sides *) fun check_rhs (_, _, _, rhs, _) = if Sign.of_sort tmp_thy (rhs, \<^sort>\domain\) then () else error ("Type not of sort domain: " ^ quote (Syntax.string_of_typ_global tmp_thy rhs)) val _ = map check_rhs doms (* domain equations *) fun mk_dom_eqn (vs, tbind, _, rhs, _) = let fun arg v = TFree (v, the_sort v) in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end val dom_eqns = map mk_dom_eqn doms (* check for valid type parameters *) val (tyvars, _, _, _, _) = hd doms val _ = map (fn (tvs, tname, _, _, _) => let val full_tname = Sign.full_name tmp_thy tname in (case duplicates (op =) tvs of [] => if eq_set (op =) (tyvars, tvs) then (full_tname, tvs) else error ("Mutually recursive domains must have same type parameters") | dups => error ("Duplicate parameter(s) for domain " ^ Binding.print tname ^ " : " ^ commas dups)) end) doms val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms val morphs = map (fn (_, _, _, _, morphs) => morphs) doms (* determine deflation combinator arguments *) val lhsTs : typ list = map fst dom_eqns val defl_rec = Free ("t", mk_tupleT (map (K deflT) lhsTs)) val defl_recs = mk_projs lhsTs defl_rec val defl_recs' = map (apsnd mk_u_defl) defl_recs fun defl_body (_, _, _, rhsT, _) = defl_of_typ tmp_thy defl_recs defl_recs' rhsT val functional = Term.lambda defl_rec (mk_tuple (map defl_body doms)) val tfrees = map fst (Term.add_tfrees functional []) val frees = map fst (Term.add_frees functional []) fun get_defl_flags (vs, _, _, _, _) = let fun argT v = TFree (v, the_sort v) fun mk_d v = "d" ^ Library.unprefix "'" v fun mk_p v = "p" ^ Library.unprefix "'" v val args = maps (fn v => [(mk_d v, mk_DEFL (argT v)), (mk_p v, mk_LIFTDEFL (argT v))]) vs val typeTs = map argT (filter (member (op =) tfrees) vs) val defl_args = map snd (filter (member (op =) frees o fst) args) in (typeTs, defl_args) end val defl_flagss = map get_defl_flags doms (* declare deflation combinator constants *) fun declare_defl_const ((typeTs, defl_args), (_, tbind, _, _, _)) thy = let val defl_bind = Binding.suffix_name "_defl" tbind val defl_type = map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT in Sign.declare_const_global ((defl_bind, defl_type), NoSyn) thy end val (defl_consts, thy) = fold_map declare_defl_const (defl_flagss ~~ doms) thy (* defining equations for type combinators *) fun mk_defl_term (defl_const, (typeTs, defl_args)) = let val type_args = map Logic.mk_type typeTs in list_ccomb (list_comb (defl_const, type_args), defl_args) end val defl_terms = map mk_defl_term (defl_consts ~~ defl_flagss) val defl_tab = map fst dom_eqns ~~ defl_terms val defl_tab' = map fst dom_eqns ~~ map mk_u_defl defl_terms fun mk_defl_spec (lhsT, rhsT) = mk_eqs (defl_of_typ tmp_thy defl_tab defl_tab' lhsT, defl_of_typ tmp_thy defl_tab defl_tab' rhsT) val defl_specs = map mk_defl_spec dom_eqns (* register recursive definition of deflation combinators *) val defl_binds = map (Binding.suffix_name "_defl") dbinds val ((defl_apply_thms, defl_unfold_thms, defl_cont_thm), thy) = add_fixdefs (defl_binds ~~ defl_specs) thy (* define types using deflation combinators *) fun make_repdef ((vs, tbind, mx, _, _), defl) thy = let val spec = (tbind, map (rpair dummyS) vs, mx) val ((_, _, _, {DEFL, ...}), thy) = Domaindef.add_domaindef spec defl NONE thy (* declare domain_defl_simps rules *) val thy = Context.theory_map (Named_Theorems.add_thm \<^named_theorems>\domain_defl_simps\ DEFL) thy in (DEFL, thy) end val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) thy (* prove DEFL equations *) fun mk_DEFL_eq_thm (lhsT, rhsT) = let val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT) val DEFL_simps = Named_Theorems.get (Proof_Context.init_global thy) \<^named_theorems>\domain_defl_simps\ fun tac ctxt = rewrite_goals_tac ctxt (map mk_meta_eq (rev DEFL_simps)) THEN TRY (resolve_tac ctxt defl_unfold_thms 1) in Goal.prove_global thy [] [] goal (tac o #context) end val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns (* register DEFL equations *) val DEFL_eq_binds = map (Binding.prefix_name "DEFL_eq_") dbinds val (_, thy) = thy |> (Global_Theory.add_thms o map Thm.no_attributes) (DEFL_eq_binds ~~ DEFL_eq_thms) (* define rep/abs functions *) fun mk_rep_abs ((tbind, _), (lhsT, rhsT)) thy = let 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 val ((abs_const, abs_def), thy) = define_const (abs_bind, coerce_const (rhsT, lhsT)) thy in (((rep_const, abs_const), (rep_def, abs_def)), thy) end val ((rep_abs_consts, rep_abs_defs), thy) = thy |> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns) |>> ListPair.unzip (* prove isomorphism and isodefl rules *) fun mk_iso_thms ((tbind, DEFL_eq), (rep_def, abs_def)) thy = let fun make thm = Drule.zero_var_indexes (thm OF [DEFL_eq, abs_def, rep_def]) val rep_iso_thm = make @{thm domain_rep_iso} val abs_iso_thm = make @{thm domain_abs_iso} val isodefl_thm = make @{thm isodefl_abs_rep} val thy = thy |> snd o add_qualified_thm "rep_iso" (tbind, rep_iso_thm) |> snd o add_qualified_thm "abs_iso" (tbind, abs_iso_thm) |> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm) in (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) end val ((iso_thms, isodefl_abs_rep_thms), thy) = thy |> fold_map mk_iso_thms (dbinds ~~ DEFL_eq_thms ~~ rep_abs_defs) |>> ListPair.unzip (* collect info about rep/abs *) val iso_infos : Domain_Take_Proofs.iso_info list = let fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) = { repT = rhsT, absT = lhsT, rep_const = repC, abs_const = absC, rep_inverse = rep_iso, abs_inverse = abs_iso } in map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms) end (* definitions and proofs related to map functions *) val (map_info, thy) = define_map_functions (dbinds ~~ iso_infos) thy val { map_consts, map_apply_thms, map_cont_thm, ...} = map_info (* prove isodefl rules for map functions *) val isodefl_thm = let fun unprime a = Library.unprefix "'" a fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT) fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), udeflT) fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T) fun mk_assm t = case try dest_LIFTDEFL t of SOME T => mk_trp (isodefl'_const T $ mk_f T $ mk_p T) | NONE => let val T = dest_DEFL t in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end fun mk_goal (map_const, (T, _)) = let val (_, Ts) = dest_Type T val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts)) val defl_term = defl_of_typ thy (Ts ~~ map mk_d Ts) (Ts ~~ map mk_p Ts) T in isodefl_const T $ map_term $ defl_term end val assms = (map mk_assm o snd o hd) defl_flagss val goals = map mk_goal (map_consts ~~ dom_eqns) val goal = mk_trp (foldr1 HOLogic.mk_conj goals) val adm_rules = @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id} val bottom_rules = @{thms fst_strict snd_strict isodefl_bottom simp_thms} val tuple_rules = @{thms split_def fst_conv snd_conv} val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy val map_ID_simps = map (fn th => th RS sym) map_ID_thms val isodefl_rules = @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL} @ isodefl_abs_rep_thms @ rev (Named_Theorems.get (Proof_Context.init_global thy) \<^named_theorems>\domain_isodefl\) in Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} => EVERY [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms), resolve_tac ctxt [@{thm cont_parallel_fix_ind} OF [defl_cont_thm, map_cont_thm]] 1, REPEAT (resolve_tac ctxt adm_rules 1), simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1, REPEAT (eresolve_tac ctxt @{thms conjE} 1), REPEAT (resolve_tac ctxt (isodefl_rules @ prems) 1 ORELSE assume_tac ctxt 1)]) end val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds fun conjuncts [] _ = [] | conjuncts (n::[]) thm = [(n, thm)] | conjuncts (n::ns) thm = let val thmL = thm RS @{thm conjunct1} val thmR = thm RS @{thm conjunct2} in (n, thmL):: conjuncts ns thmR end val (isodefl_thms, thy) = thy |> (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (conjuncts isodefl_binds isodefl_thm) val thy = fold (Context.theory_map o Named_Theorems.add_thm \<^named_theorems>\domain_isodefl\) isodefl_thms thy (* prove map_ID theorems *) fun prove_map_ID_thm (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) = let val Ts = snd (dest_Type lhsT) fun is_cpo T = Sign.of_sort thy (T, \<^sort>\cpo\) val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts)) val goal = mk_eqs (lhs, mk_ID lhsT) fun tac ctxt = EVERY [resolve_tac ctxt @{thms isodefl_DEFL_imp_ID} 1, stac ctxt DEFL_thm 1, resolve_tac ctxt [isodefl_thm] 1, REPEAT (resolve_tac ctxt @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)] in Goal.prove_global thy [] [] goal (tac o #context) end val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds val map_ID_thms = map prove_map_ID_thm (map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms) val (_, thy) = thy |> (Global_Theory.add_thms o map (rpair [Domain_Take_Proofs.map_ID_add])) (map_ID_binds ~~ map_ID_thms) (* definitions and proofs related to take functions *) val (take_info, thy) = Domain_Take_Proofs.define_take_functions (dbinds ~~ iso_infos) thy val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info (* least-upper-bound lemma for take functions *) val lub_take_lemma = let val lhs = mk_tuple (map mk_lub take_consts) fun is_cpo T = Sign.of_sort thy (T, \<^sort>\cpo\) fun mk_map_ID (map_const, (lhsT, _)) = list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT)))) val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns)) val goal = mk_trp (mk_eq (lhs, rhs)) val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy val start_rules = @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms @ @{thms prod.collapse split_def} @ map_apply_thms @ map_ID_thms val rules0 = @{thms iterate_0 Pair_strict} @ take_0_thms val rules1 = @{thms iterate_Suc prod_eq_iff fst_conv snd_conv} @ take_Suc_thms fun tac ctxt = EVERY [simp_tac (put_simpset HOL_basic_ss ctxt addsimps start_rules) 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms fix_def2}) 1, resolve_tac ctxt @{thms lub_eq} 1, resolve_tac ctxt @{thms nat.induct} 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules0) 1, asm_full_simp_tac (put_simpset beta_ss ctxt addsimps rules1) 1] in Goal.prove_global thy [] [] goal (tac o #context) end (* prove lub of take equals ID *) fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy = let - val n = Free ("n", natT) + val n = Free ("n", \<^Type>\nat\) val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT) fun tac ctxt = EVERY [resolve_tac ctxt @{thms trans} 1, resolve_tac ctxt [map_ID_thm] 2, cut_tac lub_take_lemma 1, REPEAT (eresolve_tac ctxt @{thms Pair_inject} 1), assume_tac ctxt 1] val lub_take_thm = Goal.prove_global thy [] [] goal (tac o #context) in add_qualified_thm "lub_take" (dbind, lub_take_thm) thy end val (lub_take_thms, thy) = fold_map prove_lub_take (dbinds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy (* prove additional take theorems *) val (take_info2, thy) = Domain_Take_Proofs.add_lub_take_theorems (dbinds ~~ iso_infos) take_info lub_take_thms thy in ((iso_infos, take_info2), thy) end val domain_isomorphism = gen_domain_isomorphism cert_typ val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ (******************************************************************************) (******************************** outer syntax ********************************) (******************************************************************************) local val parse_domain_iso : (string list * binding * mixfix * string * (binding * binding) option) parser = (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (\<^keyword>\=\ |-- Parse.typ) -- Scan.option (\<^keyword>\morphisms\ |-- Parse.!!! (Parse.binding -- Parse.binding))) >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)) val parse_domain_isos = Parse.and_list1 parse_domain_iso in val _ = Outer_Syntax.command \<^command_keyword>\domain_isomorphism\ "define domain isomorphisms (HOLCF)" (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd)) end end diff --git a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML @@ -1,585 +1,587 @@ (* Title: HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Author: Brian Huffman Defines take functions for the given domain equation and proves related theorems. *) signature DOMAIN_TAKE_PROOFS = sig type iso_info = { absT : typ, repT : typ, abs_const : term, rep_const : term, abs_inverse : thm, rep_inverse : thm } type take_info = { take_consts : term list, take_defs : thm list, chain_take_thms : thm list, take_0_thms : thm list, take_Suc_thms : thm list, deflation_take_thms : thm list, take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list } type take_induct_info = { take_consts : term list, take_defs : thm list, chain_take_thms : thm list, take_0_thms : thm list, take_Suc_thms : thm list, deflation_take_thms : thm list, take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list, lub_take_thms : thm list, reach_thms : thm list, take_lemma_thms : thm list, is_finite : bool, take_induct_thms : thm list } val define_take_functions : (binding * iso_info) list -> theory -> take_info * theory val add_lub_take_theorems : (binding * iso_info) list -> take_info -> thm list -> theory -> take_induct_info * theory val map_of_typ : theory -> (typ * term) list -> typ -> term val add_rec_type : (string * bool list) -> theory -> theory val get_rec_tab : theory -> (bool list) Symtab.table val add_deflation_thm : thm -> theory -> theory val get_deflation_thms : theory -> thm list val map_ID_add : attribute val get_map_ID_thms : theory -> thm list end structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS = struct type iso_info = { absT : typ, repT : typ, abs_const : term, rep_const : term, abs_inverse : thm, rep_inverse : thm } type take_info = { take_consts : term list, take_defs : thm list, chain_take_thms : thm list, take_0_thms : thm list, take_Suc_thms : thm list, deflation_take_thms : thm list, take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list } type take_induct_info = { take_consts : term list, take_defs : thm list, chain_take_thms : thm list, take_0_thms : thm list, take_Suc_thms : thm list, deflation_take_thms : thm list, take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list, lub_take_thms : thm list, reach_thms : thm list, take_lemma_thms : thm list, is_finite : bool, take_induct_thms : thm list } val beta_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms} addsimprocs [\<^simproc>\beta_cfun_proc\]) (******************************************************************************) (******************************** theory data *********************************) (******************************************************************************) structure Rec_Data = Theory_Data ( (* list indicates which type arguments allow indirect recursion *) type T = (bool list) Symtab.table val empty = Symtab.empty val extend = I fun merge data = Symtab.merge (K true) data ) fun add_rec_type (tname, bs) = Rec_Data.map (Symtab.insert (K true) (tname, bs)) fun add_deflation_thm thm = Context.theory_map (Named_Theorems.add_thm \<^named_theorems>\domain_deflation\ thm) val get_rec_tab = Rec_Data.get fun get_deflation_thms thy = rev (Named_Theorems.get (Proof_Context.init_global thy) \<^named_theorems>\domain_deflation\) val map_ID_add = Named_Theorems.add \<^named_theorems>\domain_map_ID\ fun get_map_ID_thms thy = rev (Named_Theorems.get (Proof_Context.init_global thy) \<^named_theorems>\domain_map_ID\) (******************************************************************************) (************************** building types and terms **************************) (******************************************************************************) open HOLCF_Library infixr 6 ->> infix -->> infix 9 ` fun mk_deflation t = - Const (\<^const_name>\deflation\, Term.fastype_of t --> boolT) $ t + let val T = #1 (dest_cfunT (Term.fastype_of t)) + in \<^Const>\deflation T for t\ end fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) (******************************************************************************) (****************************** isomorphism info ******************************) (******************************************************************************) fun deflation_abs_rep (info : iso_info) : thm = let val abs_iso = #abs_inverse info val rep_iso = #rep_inverse info val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso] in Drule.zero_var_indexes thm end (******************************************************************************) (********************* building map functions over types **********************) (******************************************************************************) fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term = let val thms = get_map_ID_thms thy val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) thms val rules' = map (apfst mk_ID) sub @ map swap rules in mk_ID T |> Pattern.rewrite_term thy rules' [] |> Pattern.rewrite_term thy rules [] end (******************************************************************************) (********************* declaring definitions and theorems *********************) (******************************************************************************) fun add_qualified_def name (dbind, eqn) = yield_singleton (Global_Theory.add_defs false) ((Binding.qualify_name true dbind name, eqn), []) fun add_qualified_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms ((Binding.qualify_name true dbind name, thm), []) fun add_qualified_simp_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms ((Binding.qualify_name true dbind name, thm), [Simplifier.simp_add]) (******************************************************************************) (************************** defining take functions ***************************) (******************************************************************************) fun define_take_functions (spec : (binding * iso_info) list) (thy : theory) = let (* retrieve components of spec *) val dbinds = map fst spec val iso_infos = map snd spec val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos fun mk_projs [] _ = [] | mk_projs (x::[]) t = [(x, t)] | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t) fun mk_cfcomp2 ((rep_const, abs_const), f) = mk_cfcomp (abs_const, mk_cfcomp (f, rep_const)) (* define take functional *) val newTs : typ list = map fst dom_eqns val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs) val copy_arg = Free ("f", copy_arg_type) val copy_args = map snd (mk_projs dbinds copy_arg) fun one_copy_rhs (rep_abs, (_, rhsT)) = let val body = map_of_typ thy (newTs ~~ copy_args) rhsT in mk_cfcomp2 (rep_abs, body) end val take_functional = big_lambda copy_arg (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))) val take_rhss = let - val n = Free ("n", HOLogic.natT) + val n = Free ("n", \<^Type>\nat\) val rhs = mk_iterate (n, take_functional) in map (lambda n o snd) (mk_projs dbinds rhs) end (* define take constants *) fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy = let - val take_type = HOLogic.natT --> lhsT ->> lhsT + val take_type = \<^Type>\nat\ --> lhsT ->> lhsT val take_bind = Binding.suffix_name "_take" dbind val (take_const, thy) = Sign.declare_const_global ((take_bind, take_type), NoSyn) thy val take_eqn = Logic.mk_equals (take_const, take_rhs) val (take_def_thm, thy) = add_qualified_def "take_def" (dbind, take_eqn) thy in ((take_const, take_def_thm), thy) end val ((take_consts, take_defs), thy) = thy |> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns) |>> ListPair.unzip (* prove chain_take lemmas *) fun prove_chain_take (take_const, dbind) thy = let val goal = mk_trp (mk_chain take_const) val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd} fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1 val thm = Goal.prove_global thy [] [] goal (tac o #context) in add_qualified_simp_thm "chain_take" (dbind, thm) thy end val (chain_take_thms, thy) = fold_map prove_chain_take (take_consts ~~ dbinds) thy (* prove take_0 lemmas *) fun prove_take_0 ((take_const, dbind), (lhsT, _)) thy = let val lhs = take_const $ \<^term>\0::nat\ val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)) val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict} fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1 val take_0_thm = Goal.prove_global thy [] [] goal (tac o #context) in add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy end val (take_0_thms, thy) = fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy (* prove take_Suc lemmas *) - val n = Free ("n", natT) + val n = Free ("n", \<^Type>\nat\) val take_is = map (fn t => t $ n) take_consts fun prove_take_Suc (((take_const, rep_abs), dbind), (_, rhsT)) thy = let val lhs = take_const $ (\<^term>\Suc\ $ n) val body = map_of_typ thy (newTs ~~ take_is) rhsT val rhs = mk_cfcomp2 (rep_abs, body) val goal = mk_eqs (lhs, rhs) val simps = @{thms iterate_Suc fst_conv snd_conv} val rules = take_defs @ simps fun tac ctxt = simp_tac (put_simpset beta_ss ctxt addsimps rules) 1 val take_Suc_thm = Goal.prove_global thy [] [] goal (tac o #context) in add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy end val (take_Suc_thms, thy) = fold_map prove_take_Suc (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy (* prove deflation theorems for take functions *) val deflation_abs_rep_thms = map deflation_abs_rep iso_infos val deflation_take_thm = let - val n = Free ("n", natT) + val n = Free ("n", \<^Type>\nat\) fun mk_goal take_const = mk_deflation (take_const $ n) val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)) val bottom_rules = take_0_thms @ @{thms deflation_bottom simp_thms} val deflation_rules = @{thms conjI deflation_ID} @ deflation_abs_rep_thms @ get_deflation_thms thy in Goal.prove_global thy [] [] goal (fn {context = ctxt, ...} => EVERY [resolve_tac ctxt @{thms nat.induct} 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps take_Suc_thms) 1, REPEAT (eresolve_tac ctxt @{thms conjE} 1 ORELSE resolve_tac ctxt deflation_rules 1 ORELSE assume_tac ctxt 1)]) end fun conjuncts [] _ = [] | conjuncts (n::[]) thm = [(n, thm)] | conjuncts (n::ns) thm = let val thmL = thm RS @{thm conjunct1} val thmR = thm RS @{thm conjunct2} in (n, thmL):: conjuncts ns thmR end val (deflation_take_thms, thy) = fold_map (add_qualified_thm "deflation_take") (map (apsnd Drule.zero_var_indexes) (conjuncts dbinds deflation_take_thm)) thy (* prove strictness of take functions *) fun prove_take_strict (deflation_take, dbind) thy = let val take_strict_thm = Drule.zero_var_indexes (@{thm deflation_strict} OF [deflation_take]) in add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy end val (take_strict_thms, thy) = fold_map prove_take_strict (deflation_take_thms ~~ dbinds) thy (* prove take/take rules *) fun prove_take_take ((chain_take, deflation_take), dbind) thy = let val take_take_thm = Drule.zero_var_indexes (@{thm deflation_chain_min} OF [chain_take, deflation_take]) in add_qualified_thm "take_take" (dbind, take_take_thm) thy end val (_, thy) = fold_map prove_take_take (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy (* prove take_below rules *) fun prove_take_below (deflation_take, dbind) thy = let val take_below_thm = Drule.zero_var_indexes (@{thm deflation.below} OF [deflation_take]) in add_qualified_thm "take_below" (dbind, take_below_thm) thy end val (_, thy) = fold_map prove_take_below (deflation_take_thms ~~ dbinds) thy (* define finiteness predicates *) fun define_finite_const ((dbind, take_const), (lhsT, _)) thy = let - val finite_type = lhsT --> boolT + val finite_type = lhsT --> \<^Type>\bool\ val finite_bind = Binding.suffix_name "_finite" dbind val (finite_const, thy) = Sign.declare_const_global ((finite_bind, finite_type), NoSyn) thy val x = Free ("x", lhsT) - val n = Free ("n", natT) + val n = Free ("n", \<^Type>\nat\) val finite_rhs = - lambda x (HOLogic.exists_const natT $ + lambda x (HOLogic.exists_const \<^Type>\nat\ $ (lambda n (mk_eq (mk_capply (take_const $ n, x), x)))) val finite_eqn = Logic.mk_equals (finite_const, finite_rhs) val (finite_def_thm, thy) = add_qualified_def "finite_def" (dbind, finite_eqn) thy in ((finite_const, finite_def_thm), thy) end val ((finite_consts, finite_defs), thy) = thy |> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns) |>> ListPair.unzip val result = { take_consts = take_consts, take_defs = take_defs, chain_take_thms = chain_take_thms, take_0_thms = take_0_thms, take_Suc_thms = take_Suc_thms, deflation_take_thms = deflation_take_thms, take_strict_thms = take_strict_thms, finite_consts = finite_consts, finite_defs = finite_defs } in (result, thy) end fun prove_finite_take_induct (spec : (binding * iso_info) list) (take_info : take_info) (lub_take_thms : thm list) (thy : theory) = let val dbinds = map fst spec val iso_infos = map snd spec val absTs = map #absT iso_infos val {take_consts, ...} = take_info val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info val {finite_consts, finite_defs, ...} = take_info val decisive_lemma = let fun iso_locale (info : iso_info) = @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info] val iso_locale_thms = map iso_locale iso_infos val decisive_abs_rep_thms = map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms val n = Free ("n", \<^typ>\nat\) fun mk_decisive t = - Const (\<^const_name>\decisive\, fastype_of t --> boolT) $ t + let val T = #1 (dest_cfunT (fastype_of t)) + in \<^Const>\decisive T for t\ end fun f take_const = mk_decisive (take_const $ n) val goal = mk_trp (foldr1 mk_conj (map f take_consts)) val rules0 = @{thm decisive_bottom} :: take_0_thms val rules1 = take_Suc_thms @ decisive_abs_rep_thms @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map} fun tac ctxt = EVERY [ resolve_tac ctxt @{thms nat.induct} 1, simp_tac (put_simpset HOL_ss ctxt addsimps rules0) 1, asm_simp_tac (put_simpset HOL_ss ctxt addsimps rules1) 1] in Goal.prove_global thy [] [] goal (tac o #context) end fun conjuncts 1 thm = [thm] | conjuncts n thm = let val thmL = thm RS @{thm conjunct1} val thmR = thm RS @{thm conjunct2} in thmL :: conjuncts (n-1) thmR end val decisive_thms = conjuncts (length spec) decisive_lemma fun prove_finite_thm (absT, finite_const) = let val goal = mk_trp (finite_const $ Free ("x", absT)) fun tac ctxt = EVERY [ rewrite_goals_tac ctxt finite_defs, resolve_tac ctxt @{thms lub_ID_finite} 1, resolve_tac ctxt chain_take_thms 1, resolve_tac ctxt lub_take_thms 1, resolve_tac ctxt decisive_thms 1] in Goal.prove_global thy [] [] goal (tac o #context) end val finite_thms = map prove_finite_thm (absTs ~~ finite_consts) fun prove_take_induct ((ch_take, lub_take), decisive) = Drule.export_without_context (@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]) val take_induct_thms = map prove_take_induct (chain_take_thms ~~ lub_take_thms ~~ decisive_thms) val thy = thy |> fold (snd oo add_qualified_thm "finite") (dbinds ~~ finite_thms) |> fold (snd oo add_qualified_thm "take_induct") (dbinds ~~ take_induct_thms) in ((finite_thms, take_induct_thms), thy) end fun add_lub_take_theorems (spec : (binding * iso_info) list) (take_info : take_info) (lub_take_thms : thm list) (thy : theory) = let (* retrieve components of spec *) val dbinds = map fst spec val iso_infos = map snd spec val absTs = map #absT iso_infos val repTs = map #repT iso_infos val {chain_take_thms, ...} = take_info (* prove take lemmas *) fun prove_take_lemma ((chain_take, lub_take), dbind) thy = let val take_lemma = Drule.export_without_context (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]) in add_qualified_thm "take_lemma" (dbind, take_lemma) thy end val (take_lemma_thms, thy) = fold_map prove_take_lemma (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy (* prove reach lemmas *) fun prove_reach_lemma ((chain_take, lub_take), dbind) thy = let val thm = Drule.export_without_context (@{thm lub_ID_reach} OF [chain_take, lub_take]) in add_qualified_thm "reach" (dbind, thm) thy end val (reach_thms, thy) = fold_map prove_reach_lemma (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy (* test for finiteness of domain definitions *) local val types = [\<^type_name>\ssum\, \<^type_name>\sprod\] fun finite d T = if member (op =) absTs T then d else finite' d T and finite' d (Type (c, Ts)) = let val d' = d andalso member (op =) types c in forall (finite d') Ts end | finite' _ _ = true in val is_finite = forall (finite true) repTs end val ((_, take_induct_thms), thy) = if is_finite then let val ((finites, take_inducts), thy) = prove_finite_take_induct spec take_info lub_take_thms thy in ((SOME finites, take_inducts), thy) end else let fun prove_take_induct (chain_take, lub_take) = Drule.export_without_context (@{thm lub_ID_take_induct} OF [chain_take, lub_take]) val take_inducts = map prove_take_induct (chain_take_thms ~~ lub_take_thms) val thy = fold (snd oo add_qualified_thm "take_induct") (dbinds ~~ take_inducts) thy in ((NONE, take_inducts), thy) end val result = { take_consts = #take_consts take_info, take_defs = #take_defs take_info, chain_take_thms = #chain_take_thms take_info, take_0_thms = #take_0_thms take_info, take_Suc_thms = #take_Suc_thms take_info, deflation_take_thms = #deflation_take_thms take_info, take_strict_thms = #take_strict_thms take_info, finite_consts = #finite_consts take_info, finite_defs = #finite_defs take_info, lub_take_thms = lub_take_thms, reach_thms = reach_thms, take_lemma_thms = take_lemma_thms, is_finite = is_finite, take_induct_thms = take_induct_thms } in (result, thy) end end diff --git a/src/HOL/HOLCF/Tools/cont_consts.ML b/src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML +++ b/src/HOL/HOLCF/Tools/cont_consts.ML @@ -1,94 +1,94 @@ (* Title: HOL/HOLCF/Tools/cont_consts.ML Author: Tobias Mayr, David von Oheimb, and Markus Wenzel HOLCF version of consts: handle continuous function types in mixfix syntax. *) signature CONT_CONSTS = sig val add_consts: (binding * typ * mixfix) list -> theory -> theory val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory end structure Cont_Consts: CONT_CONSTS = struct (* misc utils *) fun change_arrow 0 T = T - | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T]) + | change_arrow n (Type (_, [S, T])) = \<^Type>\fun S \change_arrow (n - 1) T\\ | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) fun trans_rules name2 name1 n mx = let val vnames = Name.invent Name.context "a" n val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1) in [Syntax.Parse_Print_Rule (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames), fold (fn a => fn t => Ast.mk_appl (Ast.Constant \<^const_syntax>\Rep_cfun\) [t, Ast.Variable a]) vnames (Ast.Constant name1))] @ (case mx of Infix _ => [extra_parse_rule] | Infixl _ => [extra_parse_rule] | Infixr _ => [extra_parse_rule] | _ => []) end (* transforming infix/mixfix declarations of constants with type ...->... a declaration of such a constant is transformed to a normal declaration with an internal name, the same type, and nofix. Additionally, a purely syntactic declaration with the original name, type ...=>..., and the original mixfix is generated and connected to the other declaration via some translation. *) fun transform thy (c, T, mx) = let fun syntax b = Lexicon.mark_const (Sign.full_bname thy b) val c1 = Binding.name_of c val c2 = c1 ^ "_cont_syntax" val n = Mixfix.mixfix_args mx in ((c, T, NoSyn), (Binding.name c2, change_arrow n T, mx), trans_rules (syntax c2) (syntax c1) n mx) end fun cfun_arity (Type (n, [_, T])) = if n = \<^type_name>\cfun\ then 1 + cfun_arity T else 0 | cfun_arity _ = 0 fun is_contconst (_, _, NoSyn) = false | is_contconst (_, _, Binder _) = false (* FIXME ? *) | is_contconst (c, T, mx) = let val n = Mixfix.mixfix_args mx handle ERROR msg => cat_error msg ("in mixfix annotation for " ^ Binding.print c) in cfun_arity T >= n end (* add_consts *) local fun gen_add_consts prep_typ raw_decls thy = let val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls val (contconst_decls, normal_decls) = List.partition is_contconst decls val transformed_decls = map (transform thy) contconst_decls in thy |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) |> Sign.add_trrules (maps #3 transformed_decls) end in val add_consts = gen_add_consts Sign.certify_typ val add_consts_cmd = gen_add_consts Syntax.read_typ_global end end diff --git a/src/HOL/HOLCF/Tools/cont_proc.ML b/src/HOL/HOLCF/Tools/cont_proc.ML --- a/src/HOL/HOLCF/Tools/cont_proc.ML +++ b/src/HOL/HOLCF/Tools/cont_proc.ML @@ -1,135 +1,132 @@ (* Title: HOL/HOLCF/Tools/cont_proc.ML Author: Brian Huffman *) signature CONT_PROC = sig val is_lcf_term: term -> bool val cont_thms: term -> thm list val all_cont_thms: term -> thm list val cont_tac: Proof.context -> int -> tactic val cont_proc: simproc val setup: theory -> theory end structure ContProc : CONT_PROC = struct (** theory context references **) val cont_K = @{thm cont_const} val cont_I = @{thm cont_id} val cont_A = @{thm cont2cont_APP} val cont_L = @{thm cont2cont_LAM} val cont_R = @{thm cont_Rep_cfun2} (* checks whether a term is written entirely in the LCF sublanguage *) -fun is_lcf_term (Const (\<^const_name>\Rep_cfun\, _) $ t $ u) = - is_lcf_term t andalso is_lcf_term u - | is_lcf_term (Const (\<^const_name>\Abs_cfun\, _) $ Abs (_, _, t)) = - is_lcf_term t - | is_lcf_term (Const (\<^const_name>\Abs_cfun\, _) $ t) = - is_lcf_term (Term.incr_boundvars 1 t $ Bound 0) +fun is_lcf_term \<^Const_>\Rep_cfun _ _ for t u\ = is_lcf_term t andalso is_lcf_term u + | is_lcf_term \<^Const_>\Abs_cfun _ _ for \Abs (_, _, t)\\ = is_lcf_term t + | is_lcf_term \<^Const_>\Abs_cfun _ _ for t\ = is_lcf_term (Term.incr_boundvars 1 t $ Bound 0) | is_lcf_term (Bound _) = true | is_lcf_term t = not (Term.is_open t) (* efficiently generates a cont thm for every LAM abstraction in a term, using forward proof and reusing common subgoals *) local fun var 0 = [SOME cont_I] | var n = NONE :: var (n-1) fun k NONE = cont_K | k (SOME x) = x fun ap NONE NONE = NONE | ap x y = SOME (k y RS (k x RS cont_A)) fun zip [] [] = [] | zip [] (y::ys) = (ap NONE y ) :: zip [] ys | zip (x::xs) [] = (ap x NONE) :: zip xs [] | zip (x::xs) (y::ys) = (ap x y ) :: zip xs ys fun lam [] = ([], cont_K) | lam (x::ys) = let (* should use "close_derivation" for thms that are used multiple times *) (* it seems to allow for sharing in explicit proof objects *) val x' = Thm.close_derivation \<^here> (k x) val Lx = x' RS cont_L in (map (fn y => SOME (k y RS Lx)) ys, x') end (* first list: cont thm for each dangling bound variable *) (* second list: cont thm for each LAM in t *) (* if b = false, only return cont thm for outermost LAMs *) - fun cont_thms1 b (Const (\<^const_name>\Rep_cfun\, _) $ f $ t) = + fun cont_thms1 b \<^Const_>\Rep_cfun _ _ for f t\ = let val (cs1,ls1) = cont_thms1 b f val (cs2,ls2) = cont_thms1 b t in (zip cs1 cs2, if b then ls1 @ ls2 else []) end - | cont_thms1 b (Const (\<^const_name>\Abs_cfun\, _) $ Abs (_, _, t)) = + | cont_thms1 b \<^Const_>\Abs_cfun _ _ for \Abs (_, _, t)\\ = let val (cs, ls) = cont_thms1 b t val (cs', l) = lam cs in (cs', l::ls) end - | cont_thms1 b (Const (\<^const_name>\Abs_cfun\, _) $ t) = + | cont_thms1 b \<^Const_>\Abs_cfun _ _ for t\ = let val t' = Term.incr_boundvars 1 t $ Bound 0 val (cs, ls) = cont_thms1 b t' val (cs', l) = lam cs in (cs', l::ls) end | cont_thms1 _ (Bound n) = (var n, []) | cont_thms1 _ _ = ([], []) in (* precondition: is_lcf_term t = true *) fun cont_thms t = snd (cont_thms1 false t) fun all_cont_thms t = snd (cont_thms1 true t) end (* Given the term "cont f", the procedure tries to construct the theorem "cont f == True". If this theorem cannot be completely solved by the introduction rules, then the procedure returns a conditional rewrite rule with the unsolved subgoals as premises. *) fun cont_tac ctxt = let val rules = [cont_K, cont_I, cont_R, cont_A, cont_L] fun new_cont_tac f' i = case all_cont_thms f' of [] => no_tac | (c::_) => resolve_tac ctxt [c] i - fun cont_tac_of_term (Const (\<^const_name>\cont\, _) $ f) = + fun cont_tac_of_term \<^Const_>\cont _ _ for f\ = let - val f' = Const (\<^const_name>\Abs_cfun\, dummyT) $ f + val f' = \<^Const>\Abs_cfun dummyT dummyT for f\ in if is_lcf_term f' then new_cont_tac f' else REPEAT_ALL_NEW (resolve_tac ctxt rules) end | cont_tac_of_term _ = K no_tac in SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i) end local fun solve_cont ctxt ct = let val t = Thm.term_of ct val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI} in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end in val cont_proc = Simplifier.make_simproc \<^context> "cont_proc" {lhss = [\<^term>\cont f\], proc = K solve_cont} end val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc]) end diff --git a/src/HOL/HOLCF/Tools/cpodef.ML b/src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML +++ b/src/HOL/HOLCF/Tools/cpodef.ML @@ -1,349 +1,349 @@ (* Title: HOL/HOLCF/Tools/cpodef.ML Author: Brian Huffman Primitive domain definitions for HOLCF, similar to Gordon/HOL-style typedef (see also ~~/src/HOL/Tools/typedef.ML). *) signature CPODEF = sig type cpo_info = { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, lub: thm, compact: thm } type pcpo_info = { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm } val add_podef: binding * (string * sort) list * mixfix -> term -> Typedef.bindings option -> (Proof.context -> tactic) -> theory -> (Typedef.info * thm) * theory val add_cpodef: binding * (string * sort) list * mixfix -> term -> Typedef.bindings option -> (Proof.context -> tactic) * (Proof.context -> tactic) -> theory -> (Typedef.info * cpo_info) * theory val add_pcpodef: binding * (string * sort) list * mixfix -> term -> Typedef.bindings option -> (Proof.context -> tactic) * (Proof.context -> tactic) -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory val cpodef_proof: (binding * (string * sort) list * mixfix) * term * Typedef.bindings option -> theory -> Proof.state val cpodef_proof_cmd: (binding * (string * string option) list * mixfix) * string * Typedef.bindings option -> theory -> Proof.state val pcpodef_proof: (binding * (string * sort) list * mixfix) * term * Typedef.bindings option -> theory -> Proof.state val pcpodef_proof_cmd: (binding * (string * string option) list * mixfix) * string * Typedef.bindings option -> theory -> Proof.state end structure Cpodef : CPODEF = struct (** type definitions **) type cpo_info = { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, lub: thm, compact: thm } type pcpo_info = { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm } (* building terms *) -fun adm_const T = Const (\<^const_name>\adm\, (T --> HOLogic.boolT) --> HOLogic.boolT) +fun adm_const T = \<^Const>\adm T\ fun mk_adm (x, T, P) = adm_const T $ absfree (x, T) P -fun below_const T = Const (\<^const_name>\below\, T --> T --> HOLogic.boolT) +fun below_const T = \<^Const>\below T\ (* proving class instances *) fun prove_cpo (name: binding) (newT: typ) opt_bindings (type_definition: thm) (* type_definition Rep Abs A *) (below_def: thm) (* op << == %x y. Rep x << Rep y *) (admissible: thm) (* adm (%x. x : set) *) (thy: theory) = let val {Rep_name, Abs_name, ...} = Typedef.make_bindings name opt_bindings; val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible] val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts fun tac ctxt = resolve_tac ctxt [@{thm typedef_cpo} OF cpo_thms] 1 val thy = Axclass.prove_arity (full_tname, lhs_sorts, \<^sort>\cpo\) tac thy (* transfer thms so that they will know about the new cpo instance *) val cpo_thms' = map (Thm.transfer thy) cpo_thms fun make thm = Drule.zero_var_indexes (thm OF cpo_thms') val cont_Rep = make @{thm typedef_cont_Rep} val cont_Abs = make @{thm typedef_cont_Abs} val lub = make @{thm typedef_lub} val compact = make @{thm typedef_compact} val (_, thy) = thy |> Sign.add_path (Binding.name_of name) |> Global_Theory.add_thms ([((Binding.prefix_name "adm_" name, admissible), []), ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), ((Binding.prefix_name "lub_" name, lub ), []), ((Binding.prefix_name "compact_" name, compact ), [])]) ||> Sign.parent_path val cpo_info : cpo_info = { below_def = below_def, adm = admissible, cont_Rep = cont_Rep, cont_Abs = cont_Abs, lub = lub, compact = compact } in (cpo_info, thy) end fun prove_pcpo (name: binding) (newT: typ) opt_bindings (type_definition: thm) (* type_definition Rep Abs A *) (below_def: thm) (* op << == %x y. Rep x << Rep y *) (bottom_mem: thm) (* bottom : set *) (thy: theory) = let val {Rep_name, Abs_name, ...} = Typedef.make_bindings name opt_bindings; val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem] val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts fun tac ctxt = resolve_tac ctxt [@{thm typedef_pcpo} OF pcpo_thms] 1 val thy = Axclass.prove_arity (full_tname, lhs_sorts, \<^sort>\pcpo\) tac thy val pcpo_thms' = map (Thm.transfer thy) pcpo_thms fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms') val Rep_strict = make @{thm typedef_Rep_strict} val Abs_strict = make @{thm typedef_Abs_strict} val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff} val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff} val (_, thy) = thy |> Sign.add_path (Binding.name_of name) |> Global_Theory.add_thms ([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []), ((Binding.suffix_name "_strict" Abs_name, Abs_strict), []), ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []), ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), [])]) ||> Sign.parent_path val pcpo_info = { Rep_strict = Rep_strict, Abs_strict = Abs_strict, Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff } in (pcpo_info, thy) end (* prepare_cpodef *) fun prepare prep_term name (tname, raw_args, _) raw_set thy = let (*rhs*) val tmp_ctxt = Proof_Context.init_global thy |> fold (Variable.declare_typ o TFree) raw_args val set = prep_term tmp_ctxt raw_set val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set val setT = Term.fastype_of set val oldT = HOLogic.dest_setT setT handle TYPE _ => error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT)) (*lhs*) val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt') raw_args val full_tname = Sign.full_name thy tname val newT = Type (full_tname, map TFree lhs_tfrees) in (newT, oldT, set) end fun add_podef typ set opt_bindings tac thy = let val name = #1 typ val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy |> Named_Target.theory_map_result (apsnd o Typedef.transform_info) (Typedef.add_typedef {overloaded = false} typ set opt_bindings tac) val oldT = #rep_type (#1 info) val newT = #abs_type (#1 info) val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) val RepC = Const (Rep_name, newT --> oldT) val below_eqn = Logic.mk_equals (below_const newT, Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))) val ((_, (_, below_ldef)), lthy) = thy |> Class.instantiation ([full_tname], lhs_tfrees, \<^sort>\po\) |> Specification.definition NONE [] [] ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn) val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef val thy = lthy |> Class.prove_instantiation_exit (fn ctxt => resolve_tac ctxt [@{thm typedef_po} OF [type_definition, below_def]] 1) in ((info, below_def), thy) end fun prepare_cpodef (prep_term: Proof.context -> 'a -> term) (typ: binding * (string * sort) list * mixfix) (raw_set: 'a) opt_bindings (thy: theory) : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = let val name = #1 typ val (newT, oldT, set) = prepare prep_term name typ raw_set thy val goal_nonempty = HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) val goal_admissible = HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) fun cpodef_result nonempty admissible thy = let val ((info as (_, {type_definition, ...}), below_def), thy) = thy |> add_podef typ set opt_bindings (fn ctxt => resolve_tac ctxt [nonempty] 1) val (cpo_info, thy) = thy |> prove_cpo name newT opt_bindings type_definition below_def admissible in ((info, cpo_info), thy) end in (goal_nonempty, goal_admissible, cpodef_result) end handle ERROR msg => cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print (#1 typ)) fun prepare_pcpodef (prep_term: Proof.context -> 'a -> term) (typ: binding * (string * sort) list * mixfix) (raw_set: 'a) opt_bindings (thy: theory) : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = let val name = #1 typ val (newT, oldT, set) = prepare prep_term name typ raw_set thy val goal_bottom_mem = - HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (\<^const_name>\bottom\, oldT), set)) + HOLogic.mk_Trueprop (HOLogic.mk_mem (\<^Const>\bottom oldT\, set)) val goal_admissible = HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) fun pcpodef_result bottom_mem admissible thy = let fun tac ctxt = resolve_tac ctxt [exI] 1 THEN resolve_tac ctxt [bottom_mem] 1 val ((info as (_, {type_definition, ...}), below_def), thy) = thy |> add_podef typ set opt_bindings tac val (cpo_info, thy) = thy |> prove_cpo name newT opt_bindings type_definition below_def admissible val (pcpo_info, thy) = thy |> prove_pcpo name newT opt_bindings type_definition below_def bottom_mem in ((info, cpo_info, pcpo_info), thy) end in (goal_bottom_mem, goal_admissible, pcpodef_result) end handle ERROR msg => cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print (#1 typ)) (* tactic interface *) fun add_cpodef typ set opt_bindings (tac1, tac2) thy = let val (goal1, goal2, cpodef_result) = prepare_cpodef Syntax.check_term typ set opt_bindings thy val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context) handle ERROR msg => cat_error msg ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) in cpodef_result thm1 thm2 thy end fun add_pcpodef typ set opt_bindings (tac1, tac2) thy = let val (goal1, goal2, pcpodef_result) = prepare_pcpodef Syntax.check_term typ set opt_bindings thy val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context) handle ERROR msg => cat_error msg ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) in pcpodef_result thm1 thm2 thy end (* proof interface *) local fun gen_cpodef_proof prep_term prep_constraint ((b, raw_args, mx), set, opt_bindings) thy = let val ctxt = Proof_Context.init_global thy val args = map (apsnd (prep_constraint ctxt)) raw_args val (goal1, goal2, make_result) = prepare_cpodef prep_term (b, args, mx) set opt_bindings thy fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) | after_qed _ = raise Fail "cpodef_proof" in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end fun gen_pcpodef_proof prep_term prep_constraint ((b, raw_args, mx), set, opt_bindings) thy = let val ctxt = Proof_Context.init_global thy val args = map (apsnd (prep_constraint ctxt)) raw_args val (goal1, goal2, make_result) = prepare_pcpodef prep_term (b, args, mx) set opt_bindings thy fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) | after_qed _ = raise Fail "pcpodef_proof" in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end in fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x end (** outer syntax **) local fun cpodef pcpo = (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- (\<^keyword>\=\ |-- Parse.term) -- Scan.option (\<^keyword>\morphisms\ |-- Parse.!!! (Parse.binding -- Parse.binding)) >> (fn ((((args, t), mx), A), morphs) => Toplevel.theory_to_proof ((if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) ((t, args, mx), A, SOME (Typedef.make_morphisms t morphs)))) in val _ = Outer_Syntax.command \<^command_keyword>\pcpodef\ "HOLCF type definition (requires admissibility proof)" (cpodef true) val _ = Outer_Syntax.command \<^command_keyword>\cpodef\ "HOLCF type definition (requires admissibility proof)" (cpodef false) end end diff --git a/src/HOL/HOLCF/Tools/domaindef.ML b/src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML +++ b/src/HOL/HOLCF/Tools/domaindef.ML @@ -1,207 +1,205 @@ (* Title: HOL/HOLCF/Tools/domaindef.ML Author: Brian Huffman Defining representable domains using algebraic deflations. *) signature DOMAINDEF = sig type rep_info = { emb_def : thm, prj_def : thm, defl_def : thm, liftemb_def : thm, liftprj_def : thm, liftdefl_def : thm, DEFL : thm } val add_domaindef: binding * (string * sort) list * mixfix -> term -> Typedef.bindings option -> theory -> (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory val domaindef_cmd: (binding * (string * string option) list * mixfix) * string * Typedef.bindings option -> theory -> theory end structure Domaindef : DOMAINDEF = struct open HOLCF_Library infixr 6 ->> infix -->> (** type definitions **) type rep_info = { emb_def : thm, prj_def : thm, defl_def : thm, liftemb_def : thm, liftprj_def : thm, liftdefl_def : thm, DEFL : thm } (* building types and terms *) val udomT = \<^typ>\udom\ val deflT = \<^typ>\udom defl\ -val udeflT = \<^typ>\udom u defl\ -fun emb_const T = Const (\<^const_name>\emb\, T ->> udomT) -fun prj_const T = Const (\<^const_name>\prj\, udomT ->> T) -fun defl_const T = Const (\<^const_name>\defl\, Term.itselfT T --> deflT) -fun liftemb_const T = Const (\<^const_name>\liftemb\, mk_upT T ->> mk_upT udomT) -fun liftprj_const T = Const (\<^const_name>\liftprj\, mk_upT udomT ->> mk_upT T) -fun liftdefl_const T = Const (\<^const_name>\liftdefl\, Term.itselfT T --> udeflT) +fun emb_const T = \<^Const>\emb T\ +fun prj_const T = \<^Const>\prj T\ +fun defl_const T = \<^Const>\defl T\ +fun liftemb_const T = \<^Const>\liftemb T\ +fun liftprj_const T = \<^Const>\liftprj T\ +fun liftdefl_const T = \<^Const>\liftdefl T\ fun mk_u_map t = let val (T, U) = dest_cfunT (fastype_of t) - val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U) - val u_map_const = Const (\<^const_name>\u_map\, u_map_type) + val u_map_const = \<^Const>\u_map T U\ in mk_capply (u_map_const, t) end fun mk_cast (t, x) = capply_const (udomT, udomT) $ (capply_const (deflT, udomT ->> udomT) $ \<^term>\cast :: udom defl -> udom -> udom\ $ t) $ x (* manipulating theorems *) (* proving class instances *) fun gen_add_domaindef (prep_term: Proof.context -> 'a -> term) (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix) (raw_defl: 'a) (opt_bindings: Typedef.bindings option) (thy: theory) : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory = let (*rhs*) val tmp_ctxt = Proof_Context.init_global thy |> fold (Variable.declare_typ o TFree) raw_args val defl = prep_term tmp_ctxt raw_defl val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl val deflT = Term.fastype_of defl val _ = if deflT = \<^typ>\udom defl\ then () else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT)) (*lhs*) val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt) raw_args val full_tname = Sign.full_name thy tname val newT = Type (full_tname, map TFree lhs_tfrees) (*set*) val set = \<^term>\defl_set :: udom defl => udom set\ $ defl (*pcpodef*) fun tac1 ctxt = resolve_tac ctxt @{thms defl_set_bottom} 1 fun tac2 ctxt = resolve_tac ctxt @{thms adm_defl_set} 1 val ((info, cpo_info, pcpo_info), thy) = thy |> Cpodef.add_pcpodef typ set opt_bindings (tac1, tac2) (*definitions*) val Rep_const = Const (#Rep_name (#1 info), newT --> udomT) val Abs_const = Const (#Abs_name (#1 info), udomT --> newT) val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const) val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $ Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))) val defl_eqn = Logic.mk_equals (defl_const newT, Abs ("x", Term.itselfT newT, defl)) val liftemb_eqn = Logic.mk_equals (liftemb_const newT, mk_u_map (emb_const newT)) val liftprj_eqn = Logic.mk_equals (liftprj_const newT, mk_u_map (prj_const newT)) val liftdefl_eqn = Logic.mk_equals (liftdefl_const newT, Abs ("t", Term.itselfT newT, - mk_capply (\<^const>\liftdefl_of\, defl_const newT $ Logic.mk_type newT))) + mk_capply (\<^Const>\liftdefl_of\, defl_const newT $ Logic.mk_type newT))) val name_def = Thm.def_binding tname val emb_bind = (Binding.prefix_name "emb_" name_def, []) val prj_bind = (Binding.prefix_name "prj_" name_def, []) val defl_bind = (Binding.prefix_name "defl_" name_def, []) val liftemb_bind = (Binding.prefix_name "liftemb_" name_def, []) val liftprj_bind = (Binding.prefix_name "liftprj_" name_def, []) val liftdefl_bind = (Binding.prefix_name "liftdefl_" name_def, []) (*instantiate class rep*) val lthy = thy |> Class.instantiation ([full_tname], lhs_tfrees, \<^sort>\domain\) val ((_, (_, emb_ldef)), lthy) = Specification.definition NONE [] [] (emb_bind, emb_eqn) lthy val ((_, (_, prj_ldef)), lthy) = Specification.definition NONE [] [] (prj_bind, prj_eqn) lthy val ((_, (_, defl_ldef)), lthy) = Specification.definition NONE [] [] (defl_bind, defl_eqn) lthy val ((_, (_, liftemb_ldef)), lthy) = Specification.definition NONE [] [] (liftemb_bind, liftemb_eqn) lthy val ((_, (_, liftprj_ldef)), lthy) = Specification.definition NONE [] [] (liftprj_bind, liftprj_eqn) lthy val ((_, (_, liftdefl_ldef)), lthy) = Specification.definition NONE [] [] (liftdefl_bind, liftdefl_eqn) lthy val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef val defl_def = singleton (Proof_Context.export lthy ctxt_thy) defl_ldef val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef val liftprj_def = singleton (Proof_Context.export lthy ctxt_thy) liftprj_ldef val liftdefl_def = singleton (Proof_Context.export lthy ctxt_thy) liftdefl_ldef val typedef_thms = [#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def, liftemb_def, liftprj_def, liftdefl_def] val thy = lthy |> Class.prove_instantiation_instance (fn ctxt => resolve_tac ctxt [@{thm typedef_domain_class} OF typedef_thms] 1) |> Local_Theory.exit_global (*other theorems*) val defl_thm' = Thm.transfer thy defl_def val (DEFL_thm, thy) = thy |> Sign.add_path (Binding.name_of tname) |> Global_Theory.add_thm ((Binding.prefix_name "DEFL_" tname, Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), []) ||> Sign.restore_naming thy val rep_info = { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def, liftemb_def = liftemb_def, liftprj_def = liftprj_def, liftdefl_def = liftdefl_def, DEFL = DEFL_thm } in ((info, cpo_info, pcpo_info, rep_info), thy) end handle ERROR msg => cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print tname) fun add_domaindef typ defl opt_bindings thy = gen_add_domaindef Syntax.check_term typ defl opt_bindings thy fun domaindef_cmd ((b, raw_args, mx), A, morphs) thy = let val ctxt = Proof_Context.init_global thy val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args in snd (gen_add_domaindef Syntax.read_term (b, args, mx) A morphs thy) end (** outer syntax **) val _ = Outer_Syntax.command \<^command_keyword>\domaindef\ "HOLCF definition of domains from deflations" ((Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- (\<^keyword>\=\ |-- Parse.term) -- Scan.option (\<^keyword>\morphisms\ |-- Parse.!!! (Parse.binding -- Parse.binding)) >> (fn (((((args, t)), mx), A), morphs) => Toplevel.theory (domaindef_cmd ((t, args, mx), A, SOME (Typedef.make_morphisms t morphs))))); end diff --git a/src/HOL/HOLCF/Tools/fixrec.ML b/src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML +++ b/src/HOL/HOLCF/Tools/fixrec.ML @@ -1,406 +1,405 @@ (* Title: HOL/HOLCF/Tools/fixrec.ML Author: Amber Telfer and Brian Huffman Recursive function definition package for HOLCF. *) signature FIXREC = sig 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 end structure Fixrec : FIXREC = struct open HOLCF_Library infixr 6 ->> infix -->> infix 9 ` val def_cont_fix_eq = @{thm def_cont_fix_eq} val def_cont_fix_ind = @{thm def_cont_fix_ind} fun fixrec_err s = error ("fixrec definition error:\n" ^ s) (*************************************************************************) (***************************** building types ****************************) (*************************************************************************) local -fun binder_cfun (Type(\<^type_name>\cfun\,[T, U])) = T :: binder_cfun U - | binder_cfun (Type(\<^type_name>\fun\,[T, U])) = T :: binder_cfun U +fun binder_cfun \<^Type>\cfun T U\ = T :: binder_cfun U + | binder_cfun \<^Type>\fun T U\ = T :: binder_cfun U | binder_cfun _ = [] -fun body_cfun (Type(\<^type_name>\cfun\,[_, U])) = body_cfun U - | body_cfun (Type(\<^type_name>\fun\,[_, U])) = body_cfun U +fun body_cfun \<^Type>\cfun _ U\ = body_cfun U + | body_cfun \<^Type>\fun _ U\ = body_cfun U | body_cfun T = T in fun matcherT (T, U) = body_cfun T ->> (binder_cfun T -->> U) ->> U end (*************************************************************************) (***************************** building terms ****************************) (*************************************************************************) val mk_trp = HOLogic.mk_Trueprop (* splits a cterm into the right and lefthand sides of equality *) fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t) (* similar to Thm.head_of, but for continuous application *) -fun chead_of (Const(\<^const_name>\Rep_cfun\,_)$f$_) = chead_of f +fun chead_of \<^Const_>\Rep_cfun _ _ for f _\ = chead_of f | chead_of u = u infix 1 === val (op ===) = HOLogic.mk_eq fun mk_mplus (t, u) = - let val mT = Term.fastype_of t - in Const(\<^const_name>\Fixrec.mplus\, mT ->> mT ->> mT) ` t ` u end + let val T = dest_matchT (Term.fastype_of t) + in \<^Const>\Fixrec.mplus T\ ` t ` u end fun mk_run t = let val mT = Term.fastype_of t val T = dest_matchT mT - val run = Const(\<^const_name>\Fixrec.run\, mT ->> T) + val run = \<^Const>\Fixrec.run T\ in case t of - Const(\<^const_name>\Rep_cfun\, _) $ - Const(\<^const_name>\Fixrec.succeed\, _) $ u => u + \<^Const_>\Rep_cfun _ _\ $ \<^Const_>\Fixrec.succeed _\ $ u => u | _ => run ` t end (*************************************************************************) (************* fixed-point definitions and unfolding theorems ************) (*************************************************************************) structure FixrecUnfoldData = Generic_Data ( type T = thm Symtab.table val empty = Symtab.empty val extend = I fun merge data : T = Symtab.merge (K true) data ) local fun name_of (Const (n, _)) = n | name_of (Free (n, _)) = n | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t]) val lhs_name = name_of o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of in val add_unfold : attribute = Thm.declaration_attribute (fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th))) end fun add_fixdefs (fixes : ((binding * typ) * mixfix) list) (spec : (Attrib.binding * term) list) (lthy : local_theory) = let val thy = Proof_Context.theory_of lthy val names = map (Binding.name_of o fst o fst) fixes val all_names = space_implode "_" names val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec) val functional = lambda_tuple lhss (mk_tuple rhss) val fixpoint = mk_fix (mk_cabs functional) val cont_thm = let val prop = mk_trp (mk_cont functional) fun err _ = error ( "Continuity proof failed please check that cont2cont rules\n" ^ "or simp rules are configured for all non-HOLCF constants.\n" ^ "The error occurred for the goal statement:\n" ^ Syntax.string_of_term lthy prop) val rules = Named_Theorems.get lthy \<^named_theorems>\cont2cont\ val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac lthy (rev rules))) val slow_tac = SOLVED' (simp_tac lthy) val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err in Goal.prove lthy [] [] prop (K tac) end fun one_def (Free(n,_)) r = let val b = Long_Name.base_name n in ((Binding.name (Thm.def_name b), []), r) end | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form" fun defs [] _ = [] | defs (l::[]) r = [one_def l r] | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r) val fixdefs = defs lhss fixpoint val (fixdef_thms : (term * (string * thm)) list, lthy) = lthy |> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs) fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2] val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms) - val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT) + val P = Var (("P", 0), map Term.fastype_of lhss ---> \<^Type>\bool\) val predicate = lambda_tuple lhss (list_comb (P, lhss)) val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm]) |> Thm.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)] |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict} val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm]) |> Local_Defs.unfold lthy @{thms split_conv} fun unfolds [] _ = [] | unfolds (n::[]) thm = [(n, thm)] | unfolds (n::ns) thm = let val thmL = thm RS @{thm Pair_eqD1} val thmR = thm RS @{thm Pair_eqD2} in (n, thmL) :: unfolds ns thmR end val unfold_thms = unfolds names tuple_unfold_thm val induct_note : Attrib.binding * Thm.thm list = let val thm_name = Binding.qualify true all_names (Binding.name "induct") in ((thm_name, []), [tuple_induct_thm]) end fun unfold_note (name, thm) : Attrib.binding * Thm.thm list = let val thm_name = Binding.qualify true name (Binding.name "unfold") val src = Attrib.internal (K add_unfold) in ((thm_name, [src]), [thm]) end val (_, lthy) = lthy |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms) in (lthy, names, fixdef_thms, map snd unfold_thms) end (*************************************************************************) (*********** monadic notation and pattern matching compilation ***********) (*************************************************************************) structure FixrecMatchData = Theory_Data ( type T = string Symtab.table val empty = Symtab.empty val extend = I fun merge data = Symtab.merge (K true) data ) (* associate match functions with pattern constants *) fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms) fun taken_names (t : term) : bstring list = let fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs | taken (Free(a,_) , bs) = insert (op =) a bs | taken (f $ u , bs) = taken (f, taken (u, bs)) | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) | taken (_ , bs) = bs in taken (t, []) end (* builds a monadic term for matching a pattern *) (* returns (rhs, free variable, used varnames) *) fun compile_pat match_name pat rhs taken = let fun comp_pat p rhs taken = if is_Free p then (rhs, p, taken) else comp_con (fastype_of p) p rhs [] taken (* compiles a monadic term for a constructor pattern *) and comp_con T p rhs vs taken = case p of - Const(\<^const_name>\Rep_cfun\,_) $ f $ x => + \<^Const_>\Rep_cfun _ _ for f x\ => let val (rhs', v, taken') = comp_pat x rhs taken in comp_con T f rhs' (v::vs) taken' end | f $ x => let val (rhs', v, taken') = comp_pat x rhs taken in comp_con T f rhs' (v::vs) taken' end | Const (c, cT) => let val n = singleton (Name.variant_list taken) "v" val v = Free(n, T) val m = Const(match_name c, matcherT (cT, fastype_of rhs)) val k = big_lambdas vs rhs in (m`v`k, v, n::taken) end | _ => raise TERM ("fixrec: invalid pattern ", [p]) in comp_pat pat rhs taken end (* builds a monadic term for matching a function definition pattern *) (* returns (constant, (vars, matcher)) *) fun compile_lhs match_name pat rhs vs taken = case pat of - Const(\<^const_name>\Rep_cfun\, _) $ f $ x => + \<^Const_>\Rep_cfun _ _ for 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, (vs, rhs)) | Const(_,_) => (pat, (vs, rhs)) | _ => fixrec_err ("invalid function pattern: " ^ ML_Syntax.print_term pat) fun strip_alls t = (case try Logic.dest_all t of SOME (_, u) => strip_alls u | NONE => t) fun compile_eq match_name eq = let val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq)) in compile_lhs match_name lhs (mk_succeed rhs) [] (taken_names eq) end (* this is the pattern-matching compiler function *) fun compile_eqs match_name eqs = let val (consts, matchers) = ListPair.unzip (map (compile_eq match_name) eqs) val const = case distinct (op =) consts of [n] => n | [] => fixrec_err "no defining equations for function" | _ => fixrec_err "all equations in block must define the same function" val vars = case distinct (op = o apply2 length) (map fst matchers) of [vars] => vars | _ => fixrec_err "all equations in block must have the same arity" (* 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 (const === rhs) end (*************************************************************************) (********************** Proving associated theorems **********************) (*************************************************************************) fun eta_tac i = CONVERSION Thm.eta_conversion i fun fixrec_simp_tac ctxt = let val tab = FixrecUnfoldData.get (Context.Proof ctxt) val concl = HOLogic.dest_Trueprop o Logic.strip_imp_concl o strip_alls fun tac (t, i) = let val (c, _) = (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t val unfold_thm = the (Symtab.lookup tab c) val rule = unfold_thm RS @{thm ssubst_lhs} in CHANGED (resolve_tac ctxt [rule] i THEN eta_tac i THEN asm_simp_tac ctxt i) end in SUBGOAL (fn ti => the_default no_tac (try tac ti)) end (* proves a block of pattern matching equations as theorems, using unfold *) fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) = let val rule = unfold_thm RS @{thm ssubst_lhs} val tac = resolve_tac ctxt [rule] 1 THEN eta_tac 1 THEN asm_simp_tac ctxt 1 fun prove_term t = Goal.prove ctxt [] [] t (K tac) fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t) in map prove_eqn eqns end (*************************************************************************) (************************* Main fixrec function **************************) (*************************************************************************) local (* code adapted from HOL/Tools/Datatype/primrec.ML *) fun gen_fixrec prep_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 (map (fn s => (s, [], [])) raw_spec) lthy) val names = map (Binding.name_of o fst o fst) fixes fun check_head name = member (op =) names name orelse fixrec_err ("Illegal equation head. Expected " ^ commas_quote names) val chead_of_spec = chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd fun name_of (Free (n, _)) = tap check_head n | name_of _ = fixrec_err ("unknown term") val all_names = map (name_of o chead_of_spec) spec fun block_of_name n = map_filter (fn (m,eq) => if m = n then SOME eq else NONE) (all_names ~~ (spec ~~ skips)) val blocks = map block_of_name names val matcher_tab = FixrecMatchData.get (Proof_Context.theory_of lthy) fun match_name c = 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 o fst)) blocks) val spec' = map (pair Binding.empty_atts) matches val (lthy, _, _, 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"), @{attributes [simp]}) 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 in val add_fixrec = gen_fixrec Specification.check_multi_specs val add_fixrec_cmd = gen_fixrec Specification.read_multi_specs end (* local *) (*************************************************************************) (******************************** Parsers ********************************) (*************************************************************************) val opt_thm_name' : (bool * Attrib.binding) parser = \<^keyword>\(\ -- \<^keyword>\unchecked\ -- \<^keyword>\)\ >> K (true, Binding.empty_atts) || Parse_Spec.opt_thm_name ":" >> pair false val spec' : (bool * (Attrib.binding * string)) parser = opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c))) val multi_specs' : (bool * (Attrib.binding * string)) list parser = let val unexpected = Scan.ahead (Parse.name || \<^keyword>\[\ || \<^keyword>\(\) in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! \<^keyword>\|\)) end val _ = Outer_Syntax.local_theory \<^command_keyword>\fixrec\ "define recursive functions (HOLCF)" (Parse.vars -- (Parse.where_ |-- Parse.!!! multi_specs') >> (fn (vars, specs) => add_fixrec_cmd vars specs)) end diff --git a/src/HOL/HOLCF/Tools/holcf_library.ML b/src/HOL/HOLCF/Tools/holcf_library.ML --- a/src/HOL/HOLCF/Tools/holcf_library.ML +++ b/src/HOL/HOLCF/Tools/holcf_library.ML @@ -1,290 +1,272 @@ (* Title: HOL/HOLCF/Tools/holcf_library.ML Author: Brian Huffman Functions for constructing HOLCF types and terms. *) structure HOLCF_Library = struct infixr 6 ->> infixr -->> infix 9 ` (*** Operations from Isabelle/HOL ***) -val boolT = HOLogic.boolT -val natT = HOLogic.natT -val mk_setT = HOLogic.mk_setT - val mk_equals = Logic.mk_equals val mk_eq = HOLogic.mk_eq val mk_trp = HOLogic.mk_Trueprop val mk_fst = HOLogic.mk_fst val mk_snd = HOLogic.mk_snd val mk_not = HOLogic.mk_not val mk_conj = HOLogic.mk_conj val mk_disj = HOLogic.mk_disj val mk_imp = HOLogic.mk_imp fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t (*** Basic HOLCF concepts ***) -fun mk_bottom T = Const (\<^const_name>\bottom\, T) +fun mk_bottom T = \<^Const>\bottom T\ -fun below_const T = Const (\<^const_name>\below\, [T, T] ---> boolT) +fun below_const T = \<^Const>\below T\ fun mk_below (t, u) = below_const (fastype_of t) $ t $ u fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t)) fun mk_defined t = mk_not (mk_undef t) fun mk_adm t = - Const (\<^const_name>\adm\, fastype_of t --> boolT) $ t + let val T = Term.domain_type (fastype_of t) + in \<^Const>\adm T for t\ end fun mk_compact t = - Const (\<^const_name>\compact\, fastype_of t --> boolT) $ t + let val T = fastype_of t + in \<^Const>\compact T for t\ end fun mk_cont t = - Const (\<^const_name>\cont\, fastype_of t --> boolT) $ t + let val \<^Type>\fun A B\ = fastype_of t + in \<^Const>\cont A B for t\ end fun mk_chain t = - Const (\<^const_name>\chain\, Term.fastype_of t --> boolT) $ t + let val T = Term.range_type (Term.fastype_of t) + in \<^Const>\chain T for t\ end fun mk_lub t = let val T = Term.range_type (Term.fastype_of t) - val lub_const = Const (\<^const_name>\lub\, mk_setT T --> T) val UNIV_const = \<^term>\UNIV :: nat set\ - val image_type = (natT --> T) --> mk_setT natT --> mk_setT T - val image_const = Const (\<^const_name>\image\, image_type) - in - lub_const $ (image_const $ t $ UNIV_const) - end + in \<^Const>\lub T for \\<^Const>\image \\<^Type>\nat\\ T for t UNIV_const\\\ end (*** Continuous function space ***) -fun mk_cfunT (T, U) = Type(\<^type_name>\cfun\, [T, U]) +fun mk_cfunT (T, U) = \<^Type>\cfun T U\ val (op ->>) = mk_cfunT val (op -->>) = Library.foldr mk_cfunT -fun dest_cfunT (Type(\<^type_name>\cfun\, [T, U])) = (T, U) +fun dest_cfunT \<^Type>\cfun T U\ = (T, U) | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []) -fun capply_const (S, T) = - Const(\<^const_name>\Rep_cfun\, (S ->> T) --> (S --> T)) - -fun cabs_const (S, T) = - Const(\<^const_name>\Abs_cfun\, (S --> T) --> (S ->> T)) +fun capply_const (S, T) = \<^Const>\Rep_cfun S T\ +fun cabs_const (S, T) = \<^Const>\Abs_cfun S T\ fun mk_cabs t = let val T = fastype_of t in cabs_const (Term.dest_funT T) $ t end (* builds the expression (% v1 v2 .. vn. rhs) *) fun lambdas [] rhs = rhs | lambdas (v::vs) rhs = Term.lambda v (lambdas vs rhs) (* builds the expression (LAM v. rhs) *) fun big_lambda v rhs = cabs_const (fastype_of v, fastype_of rhs) $ Term.lambda v rhs (* builds the expression (LAM v1 v2 .. vn. rhs) *) fun big_lambdas [] rhs = rhs | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs) fun mk_capply (t, u) = let val (S, T) = case fastype_of t of - Type(\<^type_name>\cfun\, [S, T]) => (S, T) + \<^Type>\cfun S T\ => (S, T) | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]) in capply_const (S, T) $ t $ u end val (op `) = mk_capply val list_ccomb : term * term list -> term = Library.foldl mk_capply -fun mk_ID T = Const (\<^const_name>\ID\, T ->> T) - -fun cfcomp_const (T, U, V) = - Const (\<^const_name>\cfcomp\, (U ->> V) ->> (T ->> U) ->> (T ->> V)) +fun mk_ID T = \<^Const>\ID T\ fun mk_cfcomp (f, g) = let val (U, V) = dest_cfunT (fastype_of f) val (T, U') = dest_cfunT (fastype_of g) in if U = U' - then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g) + then mk_capply (mk_capply (\<^Const>\cfcomp U V T\, f), g) else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) end -fun strictify_const T = Const (\<^const_name>\strictify\, T ->> T) -fun mk_strictify t = strictify_const (fastype_of t) ` t +fun mk_strictify t = + let val (T, U) = dest_cfunT (fastype_of t) + in \<^Const>\strictify T U\ ` t end; fun mk_strict t = let val (T, U) = dest_cfunT (fastype_of t) in mk_eq (t ` mk_bottom T, mk_bottom U) end (*** Product type ***) val mk_prodT = HOLogic.mk_prodT fun mk_tupleT [] = HOLogic.unitT | mk_tupleT [T] = T | mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts) (* builds the expression (v1,v2,..,vn) *) fun mk_tuple [] = HOLogic.unit | mk_tuple (t::[]) = t | mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts) (* builds the expression (%(v1,v2,..,vn). rhs) *) fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs | lambda_tuple (v::[]) rhs = Term.lambda v rhs | lambda_tuple (v::vs) rhs = HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs)) (*** Lifted cpo type ***) -fun mk_upT T = Type(\<^type_name>\u\, [T]) +fun mk_upT T = \<^Type>\u T\ -fun dest_upT (Type(\<^type_name>\u\, [T])) = T +fun dest_upT \<^Type>\u T\ = T | dest_upT T = raise TYPE ("dest_upT", [T], []) -fun up_const T = Const(\<^const_name>\up\, T ->> mk_upT T) +fun up_const T = \<^Const>\up T\ fun mk_up t = up_const (fastype_of t) ` t -fun fup_const (T, U) = - Const(\<^const_name>\fup\, (T ->> U) ->> mk_upT T ->> U) +fun fup_const (T, U) = \<^Const>\fup T U\ fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t fun from_up T = fup_const (T, T) ` mk_ID T (*** Lifted unit type ***) val oneT = \<^typ>\one\ -fun one_case_const T = Const (\<^const_name>\one_case\, T ->> oneT ->> T) +fun one_case_const T = \<^Const>\one_case T\ fun mk_one_case t = one_case_const (fastype_of t) ` t (*** Strict product type ***) -fun mk_sprodT (T, U) = Type(\<^type_name>\sprod\, [T, U]) +fun mk_sprodT (T, U) = \<^Type>\sprod T U\ -fun dest_sprodT (Type(\<^type_name>\sprod\, [T, U])) = (T, U) +fun dest_sprodT \<^Type>\sprod T U\ = (T, U) | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []) -fun spair_const (T, U) = - Const(\<^const_name>\spair\, T ->> U ->> mk_sprodT (T, U)) +fun spair_const (T, U) = \<^Const>\spair T U\ (* builds the expression (:t, u:) *) fun mk_spair (t, u) = spair_const (fastype_of t, fastype_of u) ` t ` u (* builds the expression (:t1,t2,..,tn:) *) fun mk_stuple [] = \<^term>\ONE\ | mk_stuple (t::[]) = t | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts) -fun sfst_const (T, U) = - Const(\<^const_name>\sfst\, mk_sprodT (T, U) ->> T) +fun sfst_const (T, U) = \<^Const>\sfst T U\ -fun ssnd_const (T, U) = - Const(\<^const_name>\ssnd\, mk_sprodT (T, U) ->> U) +fun ssnd_const (T, U) = \<^Const>\ssnd T U\ -fun ssplit_const (T, U, V) = - Const (\<^const_name>\ssplit\, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V) +fun ssplit_const (T, U, V) = \<^Const>\ssplit T U V\ fun mk_ssplit t = let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t)) in ssplit_const (T, U, V) ` t end (*** Strict sum type ***) -fun mk_ssumT (T, U) = Type(\<^type_name>\ssum\, [T, U]) +fun mk_ssumT (T, U) = \<^Type>\ssum T U\ -fun dest_ssumT (Type(\<^type_name>\ssum\, [T, U])) = (T, U) +fun dest_ssumT \<^Type>\ssum T U\ = (T, U) | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []) -fun sinl_const (T, U) = Const(\<^const_name>\sinl\, T ->> mk_ssumT (T, U)) -fun sinr_const (T, U) = Const(\<^const_name>\sinr\, U ->> mk_ssumT (T, U)) +fun sinl_const (T, U) = \<^Const>\sinl T U\ +fun sinr_const (T, U) = \<^Const>\sinr U T\ (* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) fun mk_sinjects ts = let val Ts = map fastype_of ts fun combine (t, T) (us, U) = let val v = sinl_const (T, U) ` t val vs = map (fn u => sinr_const (T, U) ` u) us in (v::vs, mk_ssumT (T, U)) end fun inj [] = raise Fail "mk_sinjects: empty list" | inj ((t, T)::[]) = ([t], T) | inj ((t, T)::ts) = combine (t, T) (inj ts) in fst (inj (ts ~~ Ts)) end -fun sscase_const (T, U, V) = - Const(\<^const_name>\sscase\, - (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V) +fun sscase_const (T, U, V) = \<^Const>\sscase T V U\ fun mk_sscase (t, u) = let val (T, _) = dest_cfunT (fastype_of t) val (U, V) = dest_cfunT (fastype_of u) in sscase_const (T, U, V) ` t ` u end fun from_sinl (T, U) = sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T) fun from_sinr (T, U) = sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U (*** pattern match monad type ***) -fun mk_matchT T = Type (\<^type_name>\match\, [T]) +fun mk_matchT T = \<^Type>\match T\ -fun dest_matchT (Type(\<^type_name>\match\, [T])) = T +fun dest_matchT \<^Type>\match T\ = T | dest_matchT T = raise TYPE ("dest_matchT", [T], []) -fun mk_fail T = Const (\<^const_name>\Fixrec.fail\, mk_matchT T) +fun mk_fail T = \<^Const>\Fixrec.fail T\ -fun succeed_const T = Const (\<^const_name>\Fixrec.succeed\, T ->> mk_matchT T) +fun succeed_const T = \<^Const>\Fixrec.succeed T\ fun mk_succeed t = succeed_const (fastype_of t) ` t (*** lifted boolean type ***) val trT = \<^typ>\tr\ (*** theory of fixed points ***) fun mk_fix t = let val (T, _) = dest_cfunT (fastype_of t) - in mk_capply (Const(\<^const_name>\fix\, (T ->> T) ->> T), t) end + in mk_capply (\<^Const>\fix T\, t) end -fun iterate_const T = - Const (\<^const_name>\iterate\, natT --> (T ->> T) ->> (T ->> T)) +fun iterate_const T = \<^Const>\iterate T\ fun mk_iterate (n, f) = let val (T, _) = dest_cfunT (Term.fastype_of f) in (iterate_const T $ n) ` f ` mk_bottom T end end diff --git a/src/HOL/HOLCF/ex/Pattern_Match.thy b/src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy @@ -1,609 +1,606 @@ (* Title: HOL/HOLCF/ex/Pattern_Match.thy Author: Brian Huffman *) section \An experimental pattern-matching notation\ theory Pattern_Match imports HOLCF begin default_sort pcpo text \FIXME: Find a proper way to un-hide constants.\ abbreviation fail :: "'a match" where "fail \ Fixrec.fail" abbreviation succeed :: "'a \ 'a match" where "succeed \ Fixrec.succeed" abbreviation run :: "'a match \ 'a" where "run \ Fixrec.run" subsection \Fatbar combinator\ definition fatbar :: "('a \ 'b match) \ ('a \ 'b match) \ ('a \ 'b match)" where "fatbar = (\ a b x. a\x +++ b\x)" abbreviation fatbar_syn :: "['a \ 'b match, 'a \ 'b match] \ 'a \ 'b match" (infixr "\" 60) where "m1 \ m2 == fatbar\m1\m2" lemma fatbar1: "m\x = \ \ (m \ ms)\x = \" by (simp add: fatbar_def) lemma fatbar2: "m\x = fail \ (m \ ms)\x = ms\x" by (simp add: fatbar_def) lemma fatbar3: "m\x = succeed\y \ (m \ ms)\x = succeed\y" by (simp add: fatbar_def) lemmas fatbar_simps = fatbar1 fatbar2 fatbar3 lemma run_fatbar1: "m\x = \ \ run\((m \ ms)\x) = \" by (simp add: fatbar_def) lemma run_fatbar2: "m\x = fail \ run\((m \ ms)\x) = run\(ms\x)" by (simp add: fatbar_def) lemma run_fatbar3: "m\x = succeed\y \ run\((m \ ms)\x) = y" by (simp add: fatbar_def) lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3 subsection \Bind operator for match monad\ definition match_bind :: "'a match \ ('a \ 'b match) \ 'b match" where "match_bind = (\ m k. sscase\(\ _. fail)\(fup\k)\(Rep_match m))" lemma match_bind_simps [simp]: "match_bind\\\k = \" "match_bind\fail\k = fail" "match_bind\(succeed\x)\k = k\x" unfolding match_bind_def fail_def succeed_def by (simp_all add: cont_Rep_match cont_Abs_match Rep_match_strict Abs_match_inverse) subsection \Case branch combinator\ definition branch :: "('a \ 'b match) \ ('b \ 'c) \ ('a \ 'c match)" where "branch p \ \ r x. match_bind\(p\x)\(\ y. succeed\(r\y))" lemma branch_simps: "p\x = \ \ branch p\r\x = \" "p\x = fail \ branch p\r\x = fail" "p\x = succeed\y \ branch p\r\x = succeed\(r\y)" by (simp_all add: branch_def) lemma branch_succeed [simp]: "branch succeed\r\x = succeed\(r\x)" by (simp add: branch_def) subsection \Cases operator\ definition cases :: "'a match \ 'a::pcpo" where "cases = Fixrec.run" text \rewrite rules for cases\ lemma cases_strict [simp]: "cases\\ = \" by (simp add: cases_def) lemma cases_fail [simp]: "cases\fail = \" by (simp add: cases_def) lemma cases_succeed [simp]: "cases\(succeed\x) = x" by (simp add: cases_def) subsection \Case syntax\ nonterminal Case_pat and Case_syn and Cases_syn syntax "_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10) "_Case1" :: "[Case_pat, 'b] => Case_syn" ("(2_ \/ _)" 10) "" :: "Case_syn => Cases_syn" ("_") "_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" ("_/ | _") "_strip_positions" :: "'a => Case_pat" ("_") syntax (ASCII) "_Case1" :: "[Case_pat, 'b] => Case_syn" ("(2_ =>/ _)" 10) translations "_Case_syntax x ms" == "CONST cases\(ms\x)" "_Case2 m ms" == "m \ ms" text \Parsing Case expressions\ syntax "_pat" :: "'a" "_variable" :: "'a" "_noargs" :: "'a" translations "_Case1 p r" => "CONST branch (_pat p)\(_variable p r)" "_variable (_args x y) r" => "CONST csplit\(_variable x (_variable y r))" "_variable _noargs r" => "CONST unit_when\r" parse_translation \ (* rewrite (_pat x) => (succeed) *) (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *) [(\<^syntax_const>\_pat\, fn _ => fn _ => Syntax.const \<^const_syntax>\Fixrec.succeed\), Syntax_Trans.mk_binder_tr (\<^syntax_const>\_variable\, \<^const_syntax>\Abs_cfun\)] \ text \Printing Case expressions\ syntax "_match" :: "'a" print_translation \ let fun dest_LAM (Const (\<^const_syntax>\Rep_cfun\,_) $ Const (\<^const_syntax>\unit_when\,_) $ t) = (Syntax.const \<^syntax_const>\_noargs\, t) | dest_LAM (Const (\<^const_syntax>\Rep_cfun\,_) $ Const (\<^const_syntax>\csplit\,_) $ t) = let val (v1, t1) = dest_LAM t; val (v2, t2) = dest_LAM t1; in (Syntax.const \<^syntax_const>\_args\ $ v1 $ v2, t2) end | dest_LAM (Const (\<^const_syntax>\Abs_cfun\,_) $ t) = let val abs = case t of Abs abs => abs | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); val (x, t') = Syntax_Trans.atomic_abs_tr' abs; in (Syntax.const \<^syntax_const>\_variable\ $ x, t') end | dest_LAM _ = raise Match; (* too few vars: abort translation *) fun Case1_tr' [Const(\<^const_syntax>\branch\,_) $ p, r] = let val (v, t) = dest_LAM r in Syntax.const \<^syntax_const>\_Case1\ $ (Syntax.const \<^syntax_const>\_match\ $ p $ v) $ t end; in [(\<^const_syntax>\Rep_cfun\, K Case1_tr')] end \ translations "x" <= "_match (CONST succeed) (_variable x)" subsection \Pattern combinators for data constructors\ type_synonym ('a, 'b) pat = "'a \ 'b match" definition cpair_pat :: "('a, 'c) pat \ ('b, 'd) pat \ ('a \ 'b, 'c \ 'd) pat" where "cpair_pat p1 p2 = (\(x, y). match_bind\(p1\x)\(\ a. match_bind\(p2\y)\(\ b. succeed\(a, b))))" definition spair_pat :: "('a, 'c) pat \ ('b, 'd) pat \ ('a::pcpo \ 'b::pcpo, 'c \ 'd) pat" where "spair_pat p1 p2 = (\(:x, y:). cpair_pat p1 p2\(x, y))" definition sinl_pat :: "('a, 'c) pat \ ('a::pcpo \ 'b::pcpo, 'c) pat" where "sinl_pat p = sscase\p\(\ x. fail)" definition sinr_pat :: "('b, 'c) pat \ ('a::pcpo \ 'b::pcpo, 'c) pat" where "sinr_pat p = sscase\(\ x. fail)\p" definition up_pat :: "('a, 'b) pat \ ('a u, 'b) pat" where "up_pat p = fup\p" definition TT_pat :: "(tr, unit) pat" where "TT_pat = (\ b. If b then succeed\() else fail)" definition FF_pat :: "(tr, unit) pat" where "FF_pat = (\ b. If b then fail else succeed\())" definition ONE_pat :: "(one, unit) pat" where "ONE_pat = (\ ONE. succeed\())" text \Parse translations (patterns)\ translations "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)" "_pat (XCONST spair\x\y)" => "CONST spair_pat (_pat x) (_pat y)" "_pat (XCONST sinl\x)" => "CONST sinl_pat (_pat x)" "_pat (XCONST sinr\x)" => "CONST sinr_pat (_pat x)" "_pat (XCONST up\x)" => "CONST up_pat (_pat x)" "_pat (XCONST TT)" => "CONST TT_pat" "_pat (XCONST FF)" => "CONST FF_pat" "_pat (XCONST ONE)" => "CONST ONE_pat" text \CONST version is also needed for constructors with special syntax\ translations "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)" "_pat (CONST spair\x\y)" => "CONST spair_pat (_pat x) (_pat y)" text \Parse translations (variables)\ translations "_variable (XCONST Pair x y) r" => "_variable (_args x y) r" "_variable (XCONST spair\x\y) r" => "_variable (_args x y) r" "_variable (XCONST sinl\x) r" => "_variable x r" "_variable (XCONST sinr\x) r" => "_variable x r" "_variable (XCONST up\x) r" => "_variable x r" "_variable (XCONST TT) r" => "_variable _noargs r" "_variable (XCONST FF) r" => "_variable _noargs r" "_variable (XCONST ONE) r" => "_variable _noargs r" translations "_variable (CONST Pair x y) r" => "_variable (_args x y) r" "_variable (CONST spair\x\y) r" => "_variable (_args x y) r" text \Print translations\ translations "CONST Pair (_match p1 v1) (_match p2 v2)" <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)" "CONST spair\(_match p1 v1)\(_match p2 v2)" <= "_match (CONST spair_pat p1 p2) (_args v1 v2)" "CONST sinl\(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1" "CONST sinr\(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1" "CONST up\(_match p1 v1)" <= "_match (CONST up_pat p1) v1" "CONST TT" <= "_match (CONST TT_pat) _noargs" "CONST FF" <= "_match (CONST FF_pat) _noargs" "CONST ONE" <= "_match (CONST ONE_pat) _noargs" lemma cpair_pat1: "branch p\r\x = \ \ branch (cpair_pat p q)\(csplit\r)\(x, y) = \" apply (simp add: branch_def cpair_pat_def) apply (cases "p\x", simp_all) done lemma cpair_pat2: "branch p\r\x = fail \ branch (cpair_pat p q)\(csplit\r)\(x, y) = fail" apply (simp add: branch_def cpair_pat_def) apply (cases "p\x", simp_all) done lemma cpair_pat3: "branch p\r\x = succeed\s \ branch (cpair_pat p q)\(csplit\r)\(x, y) = branch q\s\y" apply (simp add: branch_def cpair_pat_def) apply (cases "p\x", simp_all) apply (cases "q\y", simp_all) done lemmas cpair_pat [simp] = cpair_pat1 cpair_pat2 cpair_pat3 lemma spair_pat [simp]: "branch (spair_pat p1 p2)\r\\ = \" "\x \ \; y \ \\ \ branch (spair_pat p1 p2)\r\(:x, y:) = branch (cpair_pat p1 p2)\r\(x, y)" by (simp_all add: branch_def spair_pat_def) lemma sinl_pat [simp]: "branch (sinl_pat p)\r\\ = \" "x \ \ \ branch (sinl_pat p)\r\(sinl\x) = branch p\r\x" "y \ \ \ branch (sinl_pat p)\r\(sinr\y) = fail" by (simp_all add: branch_def sinl_pat_def) lemma sinr_pat [simp]: "branch (sinr_pat p)\r\\ = \" "x \ \ \ branch (sinr_pat p)\r\(sinl\x) = fail" "y \ \ \ branch (sinr_pat p)\r\(sinr\y) = branch p\r\y" by (simp_all add: branch_def sinr_pat_def) lemma up_pat [simp]: "branch (up_pat p)\r\\ = \" "branch (up_pat p)\r\(up\x) = branch p\r\x" by (simp_all add: branch_def up_pat_def) lemma TT_pat [simp]: "branch TT_pat\(unit_when\r)\\ = \" "branch TT_pat\(unit_when\r)\TT = succeed\r" "branch TT_pat\(unit_when\r)\FF = fail" by (simp_all add: branch_def TT_pat_def) lemma FF_pat [simp]: "branch FF_pat\(unit_when\r)\\ = \" "branch FF_pat\(unit_when\r)\TT = fail" "branch FF_pat\(unit_when\r)\FF = succeed\r" by (simp_all add: branch_def FF_pat_def) lemma ONE_pat [simp]: "branch ONE_pat\(unit_when\r)\\ = \" "branch ONE_pat\(unit_when\r)\ONE = succeed\r" by (simp_all add: branch_def ONE_pat_def) subsection \Wildcards, as-patterns, and lazy patterns\ definition wild_pat :: "'a \ unit match" where "wild_pat = (\ x. succeed\())" definition as_pat :: "('a \ 'b match) \ 'a \ ('a \ 'b) match" where "as_pat p = (\ x. match_bind\(p\x)\(\ a. succeed\(x, a)))" definition lazy_pat :: "('a \ 'b::pcpo match) \ ('a \ 'b match)" where "lazy_pat p = (\ x. succeed\(cases\(p\x)))" text \Parse translations (patterns)\ translations "_pat _" => "CONST wild_pat" text \Parse translations (variables)\ translations "_variable _ r" => "_variable _noargs r" text \Print translations\ translations "_" <= "_match (CONST wild_pat) _noargs" lemma wild_pat [simp]: "branch wild_pat\(unit_when\r)\x = succeed\r" by (simp add: branch_def wild_pat_def) lemma as_pat [simp]: "branch (as_pat p)\(csplit\r)\x = branch p\(r\x)\x" apply (simp add: branch_def as_pat_def) apply (cases "p\x", simp_all) done lemma lazy_pat [simp]: "branch p\r\x = \ \ branch (lazy_pat p)\r\x = succeed\(r\\)" "branch p\r\x = fail \ branch (lazy_pat p)\r\x = succeed\(r\\)" "branch p\r\x = succeed\s \ branch (lazy_pat p)\r\x = succeed\s" apply (simp_all add: branch_def lazy_pat_def) apply (cases "p\x", simp_all)+ done subsection \Examples\ term "Case t of (:up\(sinl\x), sinr\y:) \ (x, y)" term "\ t. Case t of up\(sinl\a) \ a | up\(sinr\b) \ b" term "\ t. Case t of (:up\(sinl\_), sinr\x:) \ x" subsection \ML code for generating definitions\ ML \ local open HOLCF_Library in infixr 6 ->>; infix 9 ` ; val beta_rules = @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; val beta_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps (@{thms simp_thms} @ beta_rules)); fun define_consts (specs : (binding * term * mixfix) list) (thy : theory) : (term list * thm list) * theory = let fun mk_decl (b, t, mx) = (b, fastype_of t, mx); val decls = map mk_decl specs; val thy = Cont_Consts.add_consts decls thy; fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T); val consts = map mk_const decls; fun mk_def c (b, t, mx) = (Thm.def_binding b, Logic.mk_equals (c, t)); val defs = map2 mk_def consts specs; val (def_thms, thy) = Global_Theory.add_defs false (map Thm.no_attributes defs) thy; in ((consts, def_thms), thy) end; fun prove (thy : theory) (defs : thm list) (goal : term) (tacs : {prems: thm list, context: Proof.context} -> tactic list) : thm = let fun tac {prems, context} = rewrite_goals_tac context defs THEN EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context}) in Goal.prove_global thy [] [] goal tac end; fun get_vars_avoiding (taken : string list) (args : (bool * typ) list) : (term list * term list) = let val Ts = map snd args; val ns = Name.variant_list taken (Old_Datatype_Prop.make_tnames Ts); val vs = map Free (ns ~~ Ts); val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); in (vs, nonlazy) end; (******************************************************************************) (************** definitions and theorems for pattern combinators **************) (******************************************************************************) fun add_pattern_combinators (bindings : binding list) (spec : (term * (bool * typ) list) list) (lhsT : typ) (exhaust : thm) (case_const : typ -> term) (case_rews : thm list) (thy : theory) = let (* utility functions *) fun mk_pair_pat (p1, p2) = let val T1 = fastype_of p1; val T2 = fastype_of p2; val (U1, V1) = apsnd dest_matchT (dest_cfunT T1); val (U2, V2) = apsnd dest_matchT (dest_cfunT T2); val pat_typ = [T1, T2] ---> (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2))); val pat_const = Const (\<^const_name>\cpair_pat\, pat_typ); in pat_const $ p1 $ p2 end; - fun mk_tuple_pat [] = succeed_const HOLogic.unitT + fun mk_tuple_pat [] = succeed_const \<^Type>\unit\ | mk_tuple_pat ps = foldr1 mk_pair_pat ps; - fun branch_const (T,U,V) = - Const (\<^const_name>\branch\, - (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V); (* define pattern combinators *) local val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix = let val pat_bind = Binding.suffix_name "_pat" bind; val Ts = map snd args; val Vs = (map (K "'t") args) |> Old_Datatype_Prop.indexify_names |> Name.variant_list tns |> map (fn t => TFree (t, \<^sort>\pcpo\)); val patNs = Old_Datatype_Prop.indexify_names (map (K "pat") args); val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs; val pats = map Free (patNs ~~ patTs); val fail = mk_fail (mk_tupleT Vs); val (vs, nonlazy) = get_vars_avoiding patNs args; val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs); fun one_fun (j, (_, args')) = let val (vs', nonlazy) = get_vars_avoiding patNs args'; in if i = j then rhs else big_lambdas vs' fail end; val funs = map_index one_fun spec; val body = list_ccomb (case_const (mk_matchT (mk_tupleT Vs)), funs); in (pat_bind, lambdas pats body, NoSyn) end; in val ((pat_consts, pat_defs), thy) = define_consts (map_index pat_eqn (bindings ~~ spec)) thy end; (* syntax translations for pattern combinators *) local fun syntax c = Lexicon.mark_const (fst (dest_Const c)); fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r]; val capp = app \<^const_syntax>\Rep_cfun\; val capps = Library.foldl capp fun app_var x = Ast.mk_appl (Ast.Constant "_variable") [x, Ast.Variable "rhs"]; fun app_pat x = Ast.mk_appl (Ast.Constant "_pat") [x]; fun args_list [] = Ast.Constant "_noargs" | args_list xs = foldr1 (app "_args") xs; fun one_case_trans (pat, (con, args)) = let val cname = Ast.Constant (syntax con); val pname = Ast.Constant (syntax pat); val ns = 1 upto length args; val xs = map (fn n => Ast.Variable ("x"^(string_of_int n))) ns; val ps = map (fn n => Ast.Variable ("p"^(string_of_int n))) ns; val vs = map (fn n => Ast.Variable ("v"^(string_of_int n))) ns; in [Syntax.Parse_Rule (app_pat (capps (cname, xs)), Ast.mk_appl pname (map app_pat xs)), Syntax.Parse_Rule (app_var (capps (cname, xs)), app_var (args_list xs)), Syntax.Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)), app "_match" (Ast.mk_appl pname ps, args_list vs))] end; val trans_rules : Ast.ast Syntax.trrule list = maps one_case_trans (pat_consts ~~ spec); in val thy = Sign.add_trrules trans_rules thy; end; (* prove strictness and reduction rules of pattern combinators *) local val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); val rn = singleton (Name.variant_list tns) "'r"; val R = TFree (rn, \<^sort>\pcpo\); fun pat_lhs (pat, args) = let val Ts = map snd args; val Vs = (map (K "'t") args) |> Old_Datatype_Prop.indexify_names |> Name.variant_list (rn::tns) |> map (fn t => TFree (t, \<^sort>\pcpo\)); val patNs = Old_Datatype_Prop.indexify_names (map (K "pat") args); val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs; val pats = map Free (patNs ~~ patTs); val k = Free ("rhs", mk_tupleT Vs ->> R); - val branch1 = branch_const (lhsT, mk_tupleT Vs, R); + val branch1 = \<^Const>\branch lhsT \mk_tupleT Vs\ R\; val fun1 = (branch1 $ list_comb (pat, pats)) ` k; - val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R); + val branch2 = \<^Const>\branch \mk_tupleT Ts\ \mk_tupleT Vs\ R\; val fun2 = (branch2 $ mk_tuple_pat pats) ` k; val taken = "rhs" :: patNs; in (fun1, fun2, taken) end; fun pat_strict (pat, (con, args)) = let val (fun1, fun2, taken) = pat_lhs (pat, args); val defs = @{thm branch_def} :: pat_defs; val goal = mk_trp (mk_strict fun1); val rules = @{thms match_bind_simps} @ case_rews; fun tacs ctxt = [simp_tac (put_simpset beta_ss ctxt addsimps rules) 1]; in prove thy defs goal (tacs o #context) end; fun pat_apps (i, (pat, (con, args))) = let val (fun1, fun2, taken) = pat_lhs (pat, args); fun pat_app (j, (con', args')) = let val (vs, nonlazy) = get_vars_avoiding taken args'; val con_app = list_ccomb (con', vs); val assms = map (mk_trp o mk_defined) nonlazy; val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R; val concl = mk_trp (mk_eq (fun1 ` con_app, rhs)); val goal = Logic.list_implies (assms, concl); val defs = @{thm branch_def} :: pat_defs; val rules = @{thms match_bind_simps} @ case_rews; fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps rules) 1]; in prove thy defs goal (tacs o #context) end; in map_index pat_app spec end; in val pat_stricts = map pat_strict (pat_consts ~~ spec); val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec)); end; in (pat_stricts @ pat_apps, thy) end end \ (* Cut from HOLCF/Tools/domain_constructors.ML in function add_domain_constructors: ( * define and prove theorems for pattern combinators * ) val (pat_thms : thm list, thy : theory) = let val bindings = map #1 spec; fun prep_arg (lazy, sel, T) = (lazy, T); fun prep_con c (b, args, mx) = (c, map prep_arg args); val pat_spec = map2 prep_con con_consts spec; in add_pattern_combinators bindings pat_spec lhsT exhaust case_const cases thy end *) end