# HG changeset patch # User huffman # Date 1291155717 28800 # Node ID 4352ca878c41ad0890feb708269514233d6440f8 # Parent 10aeee1d5b711cb238bd614855bdbb9e76280e09 remove gratuitous semicolons from ML code diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/Domain/domain.ML --- a/src/HOL/HOLCF/Tools/Domain/domain.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Tue Nov 30 14:21:57 2010 -0800 @@ -26,26 +26,26 @@ ((string * sort) list * binding * mixfix * (binding * (bool * binding option * typ) list * mixfix) list) list -> theory -> theory -end; +end structure Domain :> DOMAIN = struct -open HOLCF_Library; +open HOLCF_Library -fun first (x,_,_) = x; -fun second (_,x,_) = x; -fun third (_,_,x) = x; +fun first (x,_,_) = x +fun second (_,x,_) = x +fun third (_,_,x) = x (* ----- calls for building new thy and thms -------------------------------- *) type info = - Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info; + Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info fun add_arity ((b, sorts, mx), sort) thy : theory = thy |> Sign.add_types [(b, length sorts, mx)] - |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort); + |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort) fun gen_add_domain (prep_sort : theory -> 'a -> sort) @@ -58,52 +58,52 @@ let val dtnvs : (binding * typ list * mixfix) list = let - fun prep_tvar (a, s) = TFree (a, prep_sort thy s); + fun prep_tvar (a, s) = TFree (a, prep_sort thy s) in map (fn (vs, dbind, mx, _) => (dbind, map prep_tvar vs, mx)) raw_specs - end; + end fun thy_arity (dbind, tvars, mx) = - ((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false); + ((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false) (* this theory is used just for parsing and error checking *) val tmp_thy = thy |> Theory.copy - |> fold (add_arity o thy_arity) dtnvs; + |> fold (add_arity o thy_arity) dtnvs val dbinds : binding list = - map (fn (_,dbind,_,_) => dbind) raw_specs; + map (fn (_,dbind,_,_) => dbind) raw_specs val raw_rhss : (binding * (bool * binding option * 'b) list * mixfix) list list = - map (fn (_,_,_,cons) => cons) raw_specs; + map (fn (_,_,_,cons) => cons) raw_specs val dtnvs' : (string * typ list) list = - map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs; + map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs - val all_cons = map (Binding.name_of o first) (flat raw_rhss); + val all_cons = map (Binding.name_of o first) (flat raw_rhss) val test_dupl_cons = case duplicates (op =) all_cons of [] => false | dups => error ("Duplicate constructors: " - ^ commas_quote dups); + ^ commas_quote dups) val all_sels = - (map Binding.name_of o map_filter second o maps second) (flat raw_rhss); + (map Binding.name_of o map_filter second o maps second) (flat raw_rhss) val test_dupl_sels = case duplicates (op =) all_sels of - [] => false | dups => error("Duplicate selectors: "^commas_quote dups); + [] => false | dups => error("Duplicate selectors: "^commas_quote dups) fun test_dupl_tvars s = case duplicates (op =) (map(fst o dest_TFree)s) of [] => false | dups => error("Duplicate type arguments: " - ^commas_quote dups); - val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs'); + ^commas_quote dups) + val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs') val sorts : (string * sort) list = - let val all_sorts = map (map dest_TFree o snd) dtnvs'; + let val all_sorts = map (map dest_TFree o snd) dtnvs' in case distinct (eq_set (op =)) all_sorts of [sorts] => sorts | _ => error "Mutually recursive domains must have same type parameters" - end; + end (* a lazy argument may have an unpointed type *) (* unless the argument has a selector function *) @@ -113,19 +113,19 @@ else error ("Constructor argument type is not of sort " ^ Syntax.string_of_sort_global tmp_thy sort ^ ": " ^ Syntax.string_of_typ_global tmp_thy T) - end; + end (* test for free type variables, illegal sort constraints on rhs, - non-pcpo-types and invalid use of recursive type; + non-pcpo-types and invalid use of recursive type replace sorts in type variables on rhs *) - val rec_tab = Domain_Take_Proofs.get_rec_tab thy; + val rec_tab = Domain_Take_Proofs.get_rec_tab thy fun check_rec rec_ok (T as TFree (v,_)) = if AList.defined (op =) sorts v then T else error ("Free type variable " ^ quote v ^ " on rhs.") | check_rec rec_ok (T as Type (s, Ts)) = (case AList.lookup (op =) dtnvs' s of NONE => - let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s; + let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s in Type (s, map (check_rec rec_ok') Ts) end | SOME typevars => if typevars <> Ts @@ -135,114 +135,114 @@ else if rec_ok then T else error ("Illegal indirect recursion of type " ^ quote (Syntax.string_of_typ_global tmp_thy T))) - | check_rec rec_ok (TVar _) = error "extender:check_rec"; + | check_rec rec_ok (TVar _) = error "extender:check_rec" fun prep_arg (lazy, sel, raw_T) = let - val T = prep_typ tmp_thy sorts raw_T; - val _ = check_rec true T; - val _ = check_pcpo (lazy, sel, T); - in (lazy, sel, T) end; - fun prep_con (b, args, mx) = (b, map prep_arg args, mx); - fun prep_rhs cons = map prep_con cons; + val T = prep_typ tmp_thy sorts raw_T + val _ = check_rec true T + val _ = check_pcpo (lazy, sel, T) + in (lazy, sel, T) end + fun prep_con (b, args, mx) = (b, map prep_arg args, mx) + fun prep_rhs cons = map prep_con cons val rhss : (binding * (bool * binding option * typ) list * mixfix) list list = - map prep_rhs raw_rhss; + map prep_rhs raw_rhss - fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T; + fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T fun mk_con_typ (bind, args, mx) = - if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); - fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons); + if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args) + fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons) - val absTs : typ list = map Type dtnvs'; - val repTs : typ list = map mk_rhs_typ rhss; + val absTs : typ list = map Type dtnvs' + val repTs : typ list = map mk_rhs_typ rhss val iso_spec : (binding * mixfix * (typ * typ)) list = map (fn ((dbind, _, mx), eq) => (dbind, mx, eq)) - (dtnvs ~~ (absTs ~~ repTs)); + (dtnvs ~~ (absTs ~~ repTs)) - val ((iso_infos, take_info), thy) = add_isos iso_spec thy; + val ((iso_infos, take_info), thy) = add_isos iso_spec thy val (constr_infos, thy) = thy |> fold_map (fn ((dbind, cons), info) => Domain_Constructors.add_domain_constructors dbind cons info) - (dbinds ~~ rhss ~~ iso_infos); + (dbinds ~~ rhss ~~ iso_infos) val (take_rews, thy) = Domain_Induction.comp_theorems - dbinds take_info constr_infos thy; + dbinds take_info constr_infos thy in thy - end; + end fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = let fun prep (dbind, mx, (lhsT, rhsT)) = - let val (dname, vs) = dest_Type lhsT; - in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end; + let val (dname, vs) = dest_Type lhsT + in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end in Domain_Isomorphism.domain_isomorphism (map prep spec) - end; + end -fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo}; -fun rep_arg lazy = if lazy then @{sort predomain} else @{sort "domain"}; +fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo} +fun rep_arg lazy = if lazy then @{sort predomain} else @{sort "domain"} fun read_sort thy (SOME s) = Syntax.read_sort_global thy s - | read_sort thy NONE = Sign.defaultS thy; + | read_sort thy NONE = Sign.defaultS thy (* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *) fun read_typ thy sorts str = let val ctxt = ProofContext.init_global thy - |> fold (Variable.declare_typ o TFree) sorts; - in Syntax.read_typ ctxt str end; + |> fold (Variable.declare_typ o TFree) sorts + in Syntax.read_typ ctxt str end fun cert_typ sign sorts raw_T = let val T = Type.no_tvars (Sign.certify_typ sign raw_T) - handle TYPE (msg, _, _) => error msg; - val sorts' = Term.add_tfreesT T sorts; + handle TYPE (msg, _, _) => error msg + val sorts' = Term.add_tfreesT T sorts val _ = case duplicates (op =) (map fst sorts') of [] => () | dups => error ("Inconsistent sort constraints for " ^ commas dups) - in T end; + in T end val add_domain = - gen_add_domain (K I) cert_typ Domain_Axioms.add_axioms pcpo_arg; + gen_add_domain (K I) cert_typ Domain_Axioms.add_axioms pcpo_arg val add_new_domain = - gen_add_domain (K I) cert_typ define_isos rep_arg; + gen_add_domain (K I) cert_typ define_isos rep_arg val add_domain_cmd = - gen_add_domain read_sort read_typ Domain_Axioms.add_axioms pcpo_arg; + gen_add_domain read_sort read_typ Domain_Axioms.add_axioms pcpo_arg val add_new_domain_cmd = - gen_add_domain read_sort read_typ define_isos rep_arg; + gen_add_domain read_sort read_typ define_isos rep_arg (** outer syntax **) -val _ = Keyword.keyword "lazy"; -val _ = Keyword.keyword "unsafe"; +val _ = Keyword.keyword "lazy" +val _ = Keyword.keyword "unsafe" val dest_decl : (bool * binding option * string) parser = Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false -- (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1 || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")" >> (fn t => (true,NONE,t)) - || Parse.typ >> (fn t => (false,NONE,t)); + || Parse.typ >> (fn t => (false,NONE,t)) val cons_decl = - Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix; + Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix val domain_decl = (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) -- - (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl); + (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl) val domains_decl = Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false -- - Parse.and_list1 domain_decl; + Parse.and_list1 domain_decl fun mk_domain (unsafe : bool, @@ -252,15 +252,15 @@ val specs : ((string * string option) list * binding * mixfix * (binding * (bool * binding option * string) list * mixfix) list) list = map (fn (((vs, t), mx), cons) => - (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; + (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms in if unsafe then add_domain_cmd specs else add_new_domain_cmd specs - end; + end val _ = Outer_Syntax.command "domain" "define recursive domains (HOLCF)" - Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain)); + Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain)) -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Tue Nov 30 14:21:57 2010 -0800 @@ -18,44 +18,44 @@ (binding * mixfix * (typ * typ)) list -> theory -> (Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info) * theory -end; +end structure Domain_Axioms : DOMAIN_AXIOMS = struct -open HOLCF_Library; +open HOLCF_Library -infixr 6 ->>; -infix -->>; -infix 9 `; +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_bind = Binding.suffix_name "_abs" dbind + val rep_bind = Binding.suffix_name "_rep" dbind val (abs_const, thy) = - Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy; + Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy val (rep_const, thy) = - Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy; + Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy - val x = Free ("x", lhsT); - val y = Free ("y", rhsT); + 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))); + 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))); + Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x))) - val abs_iso_bind = Binding.qualified true "abs_iso" dbind; - val rep_iso_bind = Binding.qualified true "rep_iso" dbind; + val abs_iso_bind = Binding.qualified true "abs_iso" dbind + val rep_iso_bind = Binding.qualified true "rep_iso" dbind - 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 (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 = { @@ -65,74 +65,74 @@ 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; + end fun axiomatize_lub_take (dbind : binding, take_const : term) (thy : theory) : thm * theory = let - val i = Free ("i", natT); - val T = (fst o dest_cfunT o range_type o fastype_of) take_const; + val i = Free ("i", natT) + 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)); + mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)) - val lub_take_bind = Binding.qualified true "lub_take" dbind; + val lub_take_bind = Binding.qualified true "lub_take" dbind - val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy; + val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy in (lub_take_thm, thy) - end; + end fun add_axioms (dom_eqns : (binding * mixfix * (typ * typ)) list) (thy : theory) = let - val dbinds = map #1 dom_eqns; + 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 (map thy_type dom_eqns) thy; + (dbind, (length o snd o dest_Type) lhsT, mx) + val thy = Sign.add_types (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.axiomatize_arity o thy_arity) dom_eqns thy; + let val (dname, tvars) = dest_Type lhsT + in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end + val thy = fold (AxClass.axiomatize_arity 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; + (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; + (dbinds ~~ iso_infos) thy (* declare lub_take axioms *) val (lub_take_thms, thy) = fold_map axiomatize_lub_take - (dbinds ~~ #take_consts take_info) thy; + (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; + (dbinds ~~ iso_infos) take_info lub_take_thms thy (* define map functions *) val (map_info, thy) = Domain_Isomorphism.define_map_functions - (dbinds ~~ iso_infos) thy; + (dbinds ~~ iso_infos) thy in ((iso_infos, take_info2), thy) - end; + end -end; (* struct *) +end (* struct *) diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Nov 30 14:21:57 2010 -0800 @@ -30,18 +30,18 @@ -> (binding * (bool * binding option * typ) list * mixfix) list -> Domain_Take_Proofs.iso_info -> theory - -> constr_info * theory; -end; + -> constr_info * theory +end structure Domain_Constructors :> DOMAIN_CONSTRUCTORS = struct -open HOLCF_Library; +open HOLCF_Library -infixr 6 ->>; -infix -->>; -infix 9 `; +infixr 6 ->> +infix -->> +infix 9 ` type constr_info = { @@ -64,32 +64,32 @@ (************************** miscellaneous functions ***************************) -val simple_ss = HOL_basic_ss addsimps simp_thms; +val simple_ss = HOL_basic_ss addsimps simp_thms val beta_rules = @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ - @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; + @{thms cont2cont_fst cont2cont_snd cont2cont_Pair} -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); +val beta_ss = HOL_basic_ss addsimps (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_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) = - (Binding.suffix_name "_def" b, Logic.mk_equals (c, t)); - val defs = map2 mk_def consts specs; + (Binding.suffix_name "_def" 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; + Global_Theory.add_defs false (map Thm.no_attributes defs) thy in ((consts, def_thms), thy) - end; + end fun prove (thy : theory) @@ -103,45 +103,45 @@ EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context}) in Goal.prove_global thy [] [] goal tac - end; + 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 (Datatype_Prop.make_tnames Ts); - val vs = map Free (ns ~~ Ts); - val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + val Ts = map snd args + val ns = Name.variant_list taken (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; + end -fun get_vars args = get_vars_avoiding [] args; +fun get_vars args = get_vars_avoiding [] args (************** generating beta reduction rules from definitions **************) local fun arglist (Const _ $ Abs (s, T, t)) = let - val arg = Free (s, T); - val (args, body) = arglist (subst_bound (arg, t)); + val arg = Free (s, T) + val (args, body) = arglist (subst_bound (arg, t)) in (arg :: args, body) end - | arglist t = ([], t); + | arglist t = ([], t) in fun beta_of_def thy def_thm = let - val (con, lam) = Logic.dest_equals (concl_of def_thm); - val (args, rhs) = arglist lam; - val lhs = list_ccomb (con, args); - val goal = mk_equals (lhs, rhs); - val cs = ContProc.cont_thms lam; - val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs; + val (con, lam) = Logic.dest_equals (concl_of def_thm) + val (args, rhs) = arglist lam + val lhs = list_ccomb (con, args) + val goal = mk_equals (lhs, rhs) + val cs = ContProc.cont_thms lam + val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs in prove thy (def_thm::betas) goal (K [rtac reflexive_thm 1]) - end; -end; + end +end (******************************************************************************) (************* definitions and theorems for constructor functions *************) @@ -156,213 +156,213 @@ let (* get theorems about rep and abs *) - val abs_strict = iso_locale RS @{thm iso.abs_strict}; + val abs_strict = iso_locale RS @{thm iso.abs_strict} (* get types of type isomorphism *) - val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const); + val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const) fun vars_of args = let - val Ts = map snd args; - val ns = Datatype_Prop.make_tnames Ts; + val Ts = map snd args + val ns = Datatype_Prop.make_tnames Ts in map Free (ns ~~ Ts) - end; + end (* define constructor functions *) val ((con_consts, con_defs), thy) = let - fun one_arg (lazy, T) var = if lazy then mk_up var else var; - fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args)); - fun mk_abs t = abs_const ` t; - val rhss = map mk_abs (mk_sinjects (map one_con spec)); + fun one_arg (lazy, T) var = if lazy then mk_up var else var + fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args)) + fun mk_abs t = abs_const ` t + val rhss = map mk_abs (mk_sinjects (map one_con spec)) fun mk_def (bind, args, mx) rhs = - (bind, big_lambdas (vars_of args) rhs, mx); + (bind, big_lambdas (vars_of args) rhs, mx) in define_consts (map2 mk_def spec rhss) thy - end; + end (* prove beta reduction rules for constructors *) - val con_betas = map (beta_of_def thy) con_defs; + val con_betas = map (beta_of_def thy) con_defs (* replace bindings with terms in constructor spec *) val spec' : (term * (bool * typ) list) list = - let fun one_con con (b, args, mx) = (con, args); - in map2 one_con con_consts spec end; + let fun one_con con (b, args, mx) = (con, args) + in map2 one_con con_consts spec end (* prove exhaustiveness of constructors *) local fun arg2typ n (true, T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo}))) - | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo})); + | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo})) fun args2typ n [] = (n, oneT) | args2typ n [arg] = arg2typ n arg | args2typ n (arg::args) = let - val (n1, t1) = arg2typ n arg; + val (n1, t1) = arg2typ n arg val (n2, t2) = args2typ n1 args - in (n2, mk_sprodT (t1, t2)) end; + in (n2, mk_sprodT (t1, t2)) end fun cons2typ n [] = (n, oneT) | cons2typ n [con] = args2typ n (snd con) | cons2typ n (con::cons) = let - val (n1, t1) = args2typ n (snd con); + val (n1, t1) = args2typ n (snd con) val (n2, t2) = cons2typ n1 cons - in (n2, mk_ssumT (t1, t2)) end; - val ct = ctyp_of thy (snd (cons2typ 1 spec')); - val thm1 = instantiate' [SOME ct] [] @{thm exh_start}; - val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1; - val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2; + in (n2, mk_ssumT (t1, t2)) end + val ct = ctyp_of thy (snd (cons2typ 1 spec')) + val thm1 = instantiate' [SOME ct] [] @{thm exh_start} + val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1 + val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2 - val y = Free ("y", lhsT); + val y = Free ("y", lhsT) fun one_con (con, args) = let - val (vs, nonlazy) = get_vars_avoiding ["y"] args; - val eqn = mk_eq (y, list_ccomb (con, vs)); - val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy); - in Library.foldr mk_ex (vs, conj) end; - val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec')); + val (vs, nonlazy) = get_vars_avoiding ["y"] args + val eqn = mk_eq (y, list_ccomb (con, vs)) + val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy) + in Library.foldr mk_ex (vs, conj) end + val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec')) (* first rules replace "y = UU \/ P" with "rep$y = UU \/ P" *) val tacs = [ rtac (iso_locale RS @{thm iso.casedist_rule}) 1, rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})], - rtac thm3 1]; + rtac thm3 1] in - val nchotomy = prove thy con_betas goal (K tacs); + val nchotomy = prove thy con_betas goal (K tacs) val exhaust = (nchotomy RS @{thm exh_casedist0}) |> rewrite_rule @{thms exh_casedists} - |> Drule.zero_var_indexes; - end; + |> Drule.zero_var_indexes + end (* prove compactness rules for constructors *) val compacts = let val rules = @{thms compact_sinl compact_sinr compact_spair - compact_up compact_ONE}; + compact_up compact_ONE} val tacs = [rtac (iso_locale RS @{thm iso.compact_abs}) 1, - REPEAT (resolve_tac rules 1 ORELSE atac 1)]; + REPEAT (resolve_tac rules 1 ORELSE atac 1)] fun con_compact (con, args) = let - val vs = vars_of args; - val con_app = list_ccomb (con, vs); - val concl = mk_trp (mk_compact con_app); - val assms = map (mk_trp o mk_compact) vs; - val goal = Logic.list_implies (assms, concl); + val vs = vars_of args + val con_app = list_ccomb (con, vs) + val concl = mk_trp (mk_compact con_app) + val assms = map (mk_trp o mk_compact) vs + val goal = Logic.list_implies (assms, concl) in prove thy con_betas goal (K tacs) - end; + end in map con_compact spec' - end; + end (* prove strictness rules for constructors *) local fun con_strict (con, args) = let - val rules = abs_strict :: @{thms con_strict_rules}; - val (vs, nonlazy) = get_vars args; + val rules = abs_strict :: @{thms con_strict_rules} + val (vs, nonlazy) = get_vars args fun one_strict v' = let - val UU = mk_bottom (fastype_of v'); - val vs' = map (fn v => if v = v' then UU else v) vs; - val goal = mk_trp (mk_undef (list_ccomb (con, vs'))); - val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; - in prove thy con_betas goal (K tacs) end; - in map one_strict nonlazy end; + val UU = mk_bottom (fastype_of v') + val vs' = map (fn v => if v = v' then UU else v) vs + val goal = mk_trp (mk_undef (list_ccomb (con, vs'))) + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1] + in prove thy con_betas goal (K tacs) end + in map one_strict nonlazy end fun con_defin (con, args) = let fun iff_disj (t, []) = HOLogic.mk_not t - | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts); - val (vs, nonlazy) = get_vars args; - val lhs = mk_undef (list_ccomb (con, vs)); - val rhss = map mk_undef nonlazy; - val goal = mk_trp (iff_disj (lhs, rhss)); - val rule1 = iso_locale RS @{thm iso.abs_bottom_iff}; - val rules = rule1 :: @{thms con_bottom_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in prove thy con_betas goal (K tacs) end; + | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts) + val (vs, nonlazy) = get_vars args + val lhs = mk_undef (list_ccomb (con, vs)) + val rhss = map mk_undef nonlazy + val goal = mk_trp (iff_disj (lhs, rhss)) + val rule1 = iso_locale RS @{thm iso.abs_bottom_iff} + val rules = rule1 :: @{thms con_bottom_iff_rules} + val tacs = [simp_tac (HOL_ss addsimps rules) 1] + in prove thy con_betas goal (K tacs) end in - val con_stricts = maps con_strict spec'; - val con_defins = map con_defin spec'; - val con_rews = con_stricts @ con_defins; - end; + val con_stricts = maps con_strict spec' + val con_defins = map con_defin spec' + val con_rews = con_stricts @ con_defins + end (* prove injectiveness of constructors *) local fun pgterm rel (con, args) = let fun prime (Free (n, T)) = Free (n^"'", T) - | prime t = t; - val (xs, nonlazy) = get_vars args; - val ys = map prime xs; - val lhs = rel (list_ccomb (con, xs), list_ccomb (con, ys)); - val rhs = foldr1 mk_conj (ListPair.map rel (xs, ys)); - val concl = mk_trp (mk_eq (lhs, rhs)); - val zs = case args of [_] => [] | _ => nonlazy; - val assms = map (mk_trp o mk_defined) zs; - val goal = Logic.list_implies (assms, concl); - in prove thy con_betas goal end; - val cons' = filter (fn (_, args) => not (null args)) spec'; + | prime t = t + val (xs, nonlazy) = get_vars args + val ys = map prime xs + val lhs = rel (list_ccomb (con, xs), list_ccomb (con, ys)) + val rhs = foldr1 mk_conj (ListPair.map rel (xs, ys)) + val concl = mk_trp (mk_eq (lhs, rhs)) + val zs = case args of [_] => [] | _ => nonlazy + val assms = map (mk_trp o mk_defined) zs + val goal = Logic.list_implies (assms, concl) + in prove thy con_betas goal end + val cons' = filter (fn (_, args) => not (null args)) spec' in val inverts = let - val abs_below = iso_locale RS @{thm iso.abs_below}; - val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below}; + val abs_below = iso_locale RS @{thm iso.abs_below} + val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below} val rules2 = @{thms up_defined spair_defined ONE_defined} - val rules = rules1 @ rules2; - val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; - in map (fn c => pgterm mk_below c (K tacs)) cons' end; + val rules = rules1 @ rules2 + val tacs = [asm_simp_tac (simple_ss addsimps rules) 1] + in map (fn c => pgterm mk_below c (K tacs)) cons' end val injects = let - val abs_eq = iso_locale RS @{thm iso.abs_eq}; - val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq}; + val abs_eq = iso_locale RS @{thm iso.abs_eq} + val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq} val rules2 = @{thms up_defined spair_defined ONE_defined} - val rules = rules1 @ rules2; - val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; - in map (fn c => pgterm mk_eq c (K tacs)) cons' end; - end; + val rules = rules1 @ rules2 + val tacs = [asm_simp_tac (simple_ss addsimps rules) 1] + in map (fn c => pgterm mk_eq c (K tacs)) cons' end + end (* prove distinctness of constructors *) local fun map_dist (f : 'a -> 'a -> 'b) (xs : 'a list) : 'b list = - flat (map_index (fn (i, x) => map (f x) (nth_drop i xs)) xs); + flat (map_index (fn (i, x) => map (f x) (nth_drop i xs)) xs) fun prime (Free (n, T)) = Free (n^"'", T) - | prime t = t; + | prime t = t fun iff_disj (t, []) = mk_not t - | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts); + | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts) fun iff_disj2 (t, [], us) = mk_not t | iff_disj2 (t, ts, []) = mk_not t | iff_disj2 (t, ts, us) = - mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us)); + mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us)) fun dist_le (con1, args1) (con2, args2) = let - val (vs1, zs1) = get_vars args1; - val (vs2, zs2) = get_vars args2 |> pairself (map prime); - val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2)); - val rhss = map mk_undef zs1; - val goal = mk_trp (iff_disj (lhs, rhss)); - val rule1 = iso_locale RS @{thm iso.abs_below}; - val rules = rule1 :: @{thms con_below_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in prove thy con_betas goal (K tacs) end; + val (vs1, zs1) = get_vars args1 + val (vs2, zs2) = get_vars args2 |> pairself (map prime) + val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2)) + val rhss = map mk_undef zs1 + val goal = mk_trp (iff_disj (lhs, rhss)) + val rule1 = iso_locale RS @{thm iso.abs_below} + val rules = rule1 :: @{thms con_below_iff_rules} + val tacs = [simp_tac (HOL_ss addsimps rules) 1] + in prove thy con_betas goal (K tacs) end fun dist_eq (con1, args1) (con2, args2) = let - val (vs1, zs1) = get_vars args1; - val (vs2, zs2) = get_vars args2 |> pairself (map prime); - val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2)); - val rhss1 = map mk_undef zs1; - val rhss2 = map mk_undef zs2; - val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2)); - val rule1 = iso_locale RS @{thm iso.abs_eq}; - val rules = rule1 :: @{thms con_eq_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in prove thy con_betas goal (K tacs) end; + val (vs1, zs1) = get_vars args1 + val (vs2, zs2) = get_vars args2 |> pairself (map prime) + val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2)) + val rhss1 = map mk_undef zs1 + val rhss2 = map mk_undef zs2 + val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2)) + val rule1 = iso_locale RS @{thm iso.abs_eq} + val rules = rule1 :: @{thms con_eq_iff_rules} + val tacs = [simp_tac (HOL_ss addsimps rules) 1] + in prove thy con_betas goal (K tacs) end in - val dist_les = map_dist dist_le spec'; - val dist_eqs = map_dist dist_eq spec'; - end; + val dist_les = map_dist dist_le spec' + val dist_eqs = map_dist dist_eq spec' + end val result = { @@ -376,10 +376,10 @@ injects = injects, dist_les = dist_les, dist_eqs = dist_eqs - }; + } in (result, thy) - end; + end (******************************************************************************) (**************** definition and theorems for case combinator *****************) @@ -398,121 +398,121 @@ let (* prove rep/abs rules *) - val rep_strict = iso_locale RS @{thm iso.rep_strict}; - val abs_inverse = iso_locale RS @{thm iso.abs_iso}; + val rep_strict = iso_locale RS @{thm iso.rep_strict} + val abs_inverse = iso_locale RS @{thm iso.abs_iso} (* calculate function arguments of case combinator *) - val tns = map fst (Term.add_tfreesT lhsT []); - val resultT = TFree (Name.variant tns "'t", @{sort pcpo}); - fun fTs T = map (fn (_, args) => map snd args -->> T) spec; - val fns = Datatype_Prop.indexify_names (map (K "f") spec); - val fs = map Free (fns ~~ fTs resultT); - fun caseT T = fTs T -->> (lhsT ->> T); + val tns = map fst (Term.add_tfreesT lhsT []) + val resultT = TFree (Name.variant tns "'t", @{sort pcpo}) + fun fTs T = map (fn (_, args) => map snd args -->> T) spec + val fns = Datatype_Prop.indexify_names (map (K "f") spec) + val fs = map Free (fns ~~ fTs resultT) + fun caseT T = fTs T -->> (lhsT ->> T) (* definition of case combinator *) local - val case_bind = Binding.suffix_name "_case" dbind; + val case_bind = Binding.suffix_name "_case" dbind fun lambda_arg (lazy, v) t = - (if lazy then mk_fup else I) (big_lambda v t); + (if lazy then mk_fup else I) (big_lambda v t) fun lambda_args [] t = mk_one_case t | lambda_args (x::[]) t = lambda_arg x t - | lambda_args (x::xs) t = mk_ssplit (lambda_arg x (lambda_args xs t)); + | lambda_args (x::xs) t = mk_ssplit (lambda_arg x (lambda_args xs t)) fun one_con f (_, args) = let - val Ts = map snd args; - val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts); - val vs = map Free (ns ~~ Ts); + val Ts = map snd args + val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts) + val vs = map Free (ns ~~ Ts) in lambda_args (map fst args ~~ vs) (list_ccomb (f, vs)) - end; + end fun mk_sscases [t] = mk_strictify t - | mk_sscases ts = foldr1 mk_sscase ts; - val body = mk_sscases (map2 one_con fs spec); - val rhs = big_lambdas fs (mk_cfcomp (body, rep_const)); + | mk_sscases ts = foldr1 mk_sscase ts + val body = mk_sscases (map2 one_con fs spec) + val rhs = big_lambdas fs (mk_cfcomp (body, rep_const)) val ((case_consts, case_defs), thy) = - define_consts [(case_bind, rhs, NoSyn)] thy; - val case_name = Sign.full_name thy case_bind; + define_consts [(case_bind, rhs, NoSyn)] thy + val case_name = Sign.full_name thy case_bind in - val case_def = hd case_defs; - fun case_const T = Const (case_name, caseT T); - val case_app = list_ccomb (case_const resultT, fs); - val thy = thy; - end; + val case_def = hd case_defs + fun case_const T = Const (case_name, caseT T) + val case_app = list_ccomb (case_const resultT, fs) + val thy = thy + end (* define syntax for case combinator *) (* TODO: re-implement case syntax using a parse translation *) local open Syntax - fun syntax c = Syntax.mark_const (fst (dest_Const c)); - fun xconst c = Long_Name.base_name (fst (dest_Const c)); + fun syntax c = Syntax.mark_const (fst (dest_Const c)) + fun xconst c = Long_Name.base_name (fst (dest_Const c)) fun c_ast authentic con = - Constant (if authentic then syntax con else xconst con); - fun showint n = string_of_int (n+1); - fun expvar n = Variable ("e" ^ showint n); - fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m); - fun argvars n args = map_index (argvar n) args; - fun app s (l, r) = mk_appl (Constant s) [l, r]; - val cabs = app "_cabs"; - val capp = app @{const_syntax Rep_cfun}; + Constant (if authentic then syntax con else xconst con) + fun showint n = string_of_int (n+1) + fun expvar n = Variable ("e" ^ showint n) + fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m) + fun argvars n args = map_index (argvar n) args + fun app s (l, r) = mk_appl (Constant s) [l, r] + val cabs = app "_cabs" + val capp = app @{const_syntax Rep_cfun} val capps = Library.foldl capp fun con1 authentic n (con,args) = - Library.foldl capp (c_ast authentic con, argvars n args); + Library.foldl capp (c_ast authentic con, argvars n args) fun case1 authentic (n, c) = - app "_case1" (con1 authentic n c, expvar n); - fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args); + app "_case1" (con1 authentic n c, expvar n) + fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args) fun when1 n (m, c) = - if n = m then arg1 (n, c) else (Constant @{const_syntax UU}); - val case_constant = Constant (syntax (case_const dummyT)); + if n = m then arg1 (n, c) else (Constant @{const_syntax UU}) + val case_constant = Constant (syntax (case_const dummyT)) fun case_trans authentic = ParsePrintRule (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (map_index (case1 authentic) spec)), - capp (capps (case_constant, map_index arg1 spec), Variable "x")); + capp (capps (case_constant, map_index arg1 spec), Variable "x")) fun one_abscon_trans authentic (n, c) = ParsePrintRule (cabs (con1 authentic n c, expvar n), - capps (case_constant, map_index (when1 n) spec)); + capps (case_constant, map_index (when1 n) spec)) fun abscon_trans authentic = - map_index (one_abscon_trans authentic) spec; + map_index (one_abscon_trans authentic) spec val trans_rules : ast Syntax.trrule list = case_trans false :: case_trans true :: - abscon_trans false @ abscon_trans true; + abscon_trans false @ abscon_trans true in - val thy = Sign.add_trrules_i trans_rules thy; - end; + val thy = Sign.add_trrules_i trans_rules thy + end (* prove beta reduction rule for case combinator *) - val case_beta = beta_of_def thy case_def; + val case_beta = beta_of_def thy case_def (* prove strictness of case combinator *) val case_strict = let - val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}]; - val goal = mk_trp (mk_strict case_app); - val rules = @{thms sscase1 ssplit1 strictify1 one_case1}; - val tacs = [resolve_tac rules 1]; - in prove thy defs goal (K tacs) end; + val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}] + val goal = mk_trp (mk_strict case_app) + val rules = @{thms sscase1 ssplit1 strictify1 one_case1} + val tacs = [resolve_tac rules 1] + in prove thy defs goal (K tacs) end (* prove rewrites for case combinator *) local fun one_case (con, args) f = let - val (vs, nonlazy) = get_vars args; - val assms = map (mk_trp o mk_defined) nonlazy; - val lhs = case_app ` list_ccomb (con, vs); - val rhs = list_ccomb (f, vs); - val concl = mk_trp (mk_eq (lhs, rhs)); - val goal = Logic.list_implies (assms, concl); - val defs = case_beta :: con_betas; - val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1}; - val rules2 = @{thms con_bottom_iff_rules}; - val rules3 = @{thms cfcomp2 one_case2}; - val rules = abs_inverse :: rules1 @ rules2 @ rules3; - val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]; - in prove thy defs goal (K tacs) end; + val (vs, nonlazy) = get_vars args + val assms = map (mk_trp o mk_defined) nonlazy + val lhs = case_app ` list_ccomb (con, vs) + val rhs = list_ccomb (f, vs) + val concl = mk_trp (mk_eq (lhs, rhs)) + val goal = Logic.list_implies (assms, concl) + val defs = case_beta :: con_betas + val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1} + val rules2 = @{thms con_bottom_iff_rules} + val rules3 = @{thms cfcomp2 one_case2} + val rules = abs_inverse :: rules1 @ rules2 @ rules3 + val tacs = [asm_simp_tac (beta_ss addsimps rules) 1] + in prove thy defs goal (K tacs) end in - val case_apps = map2 one_case spec fs; + val case_apps = map2 one_case spec fs end in @@ -537,26 +537,26 @@ (* define selector functions *) val ((sel_consts, sel_defs), thy) = let - fun rangeT s = snd (dest_cfunT (fastype_of s)); - fun mk_outl s = mk_cfcomp (from_sinl (dest_ssumT (rangeT s)), s); - fun mk_outr s = mk_cfcomp (from_sinr (dest_ssumT (rangeT s)), s); - fun mk_sfst s = mk_cfcomp (sfst_const (dest_sprodT (rangeT s)), s); - fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s); - fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s); + fun rangeT s = snd (dest_cfunT (fastype_of s)) + fun mk_outl s = mk_cfcomp (from_sinl (dest_ssumT (rangeT s)), s) + fun mk_outr s = mk_cfcomp (from_sinr (dest_ssumT (rangeT s)), s) + fun mk_sfst s = mk_cfcomp (sfst_const (dest_sprodT (rangeT s)), s) + fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s) + fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s) fun sels_of_arg s (lazy, NONE, T) = [] | sels_of_arg s (lazy, SOME b, T) = - [(b, if lazy then mk_down s else s, NoSyn)]; + [(b, if lazy then mk_down s else s, NoSyn)] fun sels_of_args s [] = [] | sels_of_args s (v :: []) = sels_of_arg s v | sels_of_args s (v :: vs) = - sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs; + sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs fun sels_of_cons s [] = [] | sels_of_cons s ((con, args) :: []) = sels_of_args s args | sels_of_cons s ((con, args) :: cs) = - sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs; + sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs val sel_eqns : (binding * term * mixfix) list = - sels_of_cons rep_const spec; + sels_of_cons rep_const spec in define_consts sel_eqns thy end @@ -566,21 +566,21 @@ let fun prep_arg (lazy, NONE, T) sels = ((lazy, NONE, T), sels) | prep_arg (lazy, SOME _, T) sels = - ((lazy, SOME (hd sels), T), tl sels); + ((lazy, SOME (hd sels), T), tl sels) fun prep_con (con, args) sels = - apfst (pair con) (fold_map prep_arg args sels); + apfst (pair con) (fold_map prep_arg args sels) in fst (fold_map prep_con spec sel_consts) - end; + end (* prove selector strictness rules *) val sel_stricts : thm list = let - val rules = rep_strict :: @{thms sel_strict_rules}; - val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; + val rules = rep_strict :: @{thms sel_strict_rules} + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1] fun sel_strict sel = let - val goal = mk_trp (mk_strict sel); + val goal = mk_trp (mk_strict sel) in prove thy sel_defs goal (K tacs) end @@ -591,37 +591,37 @@ (* prove selector application rules *) val sel_apps : thm list = let - val defs = con_betas @ sel_defs; - val rules = abs_inv :: @{thms sel_app_rules}; - val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; + val defs = con_betas @ sel_defs + val rules = abs_inv :: @{thms sel_app_rules} + val tacs = [asm_simp_tac (simple_ss addsimps rules) 1] fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) = let - val Ts : typ list = map #3 args; - val ns : string list = Datatype_Prop.make_tnames Ts; - val vs : term list = map Free (ns ~~ Ts); - val con_app : term = list_ccomb (con, vs); - val vs' : (bool * term) list = map #1 args ~~ vs; + val Ts : typ list = map #3 args + val ns : string list = Datatype_Prop.make_tnames Ts + val vs : term list = map Free (ns ~~ Ts) + val con_app : term = list_ccomb (con, vs) + val vs' : (bool * term) list = map #1 args ~~ vs fun one_same (n, sel, T) = let - val xs = map snd (filter_out fst (nth_drop n vs')); - val assms = map (mk_trp o mk_defined) xs; - val concl = mk_trp (mk_eq (sel ` con_app, nth vs n)); - val goal = Logic.list_implies (assms, concl); + val xs = map snd (filter_out fst (nth_drop n vs')) + val assms = map (mk_trp o mk_defined) xs + val concl = mk_trp (mk_eq (sel ` con_app, nth vs n)) + val goal = Logic.list_implies (assms, concl) in prove thy defs goal (K tacs) - end; + end fun one_diff (n, sel, T) = let - val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T)); + val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T)) in prove thy defs goal (K tacs) - end; + end fun one_con (j, (_, args')) : thm list = let fun prep (i, (lazy, NONE, T)) = NONE - | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T); + | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T) val sels : (int * term * typ) list = - map_filter prep (map_index I args'); + map_filter prep (map_index I args') in if i = j then map one_same sels @@ -637,25 +637,25 @@ (* prove selector definedness rules *) val sel_defins : thm list = let - val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules}; - val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; + val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules} + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1] fun sel_defin sel = let - val (T, U) = dest_cfunT (fastype_of sel); - val x = Free ("x", T); - val lhs = mk_eq (sel ` x, mk_bottom U); - val rhs = mk_eq (x, mk_bottom T); - val goal = mk_trp (mk_eq (lhs, rhs)); + val (T, U) = dest_cfunT (fastype_of sel) + val x = Free ("x", T) + val lhs = mk_eq (sel ` x, mk_bottom U) + val rhs = mk_eq (x, mk_bottom T) + val goal = mk_trp (mk_eq (lhs, rhs)) in prove thy sel_defs goal (K tacs) end fun one_arg (false, SOME sel, T) = SOME (sel_defin sel) - | one_arg _ = NONE; + | one_arg _ = NONE in case spec2 of [(con, args)] => map_filter one_arg args | _ => [] - end; + end in (sel_stricts @ sel_defins @ sel_apps, thy) @@ -677,81 +677,81 @@ fun vars_of args = let - val Ts = map snd args; - val ns = Datatype_Prop.make_tnames Ts; + val Ts = map snd args + val ns = Datatype_Prop.make_tnames Ts in map Free (ns ~~ Ts) - end; + end (* define discriminator functions *) local fun dis_fun i (j, (con, args)) = let - val (vs, nonlazy) = get_vars args; - val tr = if i = j then @{term TT} else @{term FF}; + val (vs, nonlazy) = get_vars args + val tr = if i = j then @{term TT} else @{term FF} in big_lambdas vs tr - end; + end fun dis_eqn (i, bind) : binding * term * mixfix = let - val dis_bind = Binding.prefix_name "is_" bind; - val rhs = list_ccomb (case_const trT, map_index (dis_fun i) spec); + val dis_bind = Binding.prefix_name "is_" bind + val rhs = list_ccomb (case_const trT, map_index (dis_fun i) spec) in (dis_bind, rhs, NoSyn) - end; + end in val ((dis_consts, dis_defs), thy) = define_consts (map_index dis_eqn bindings) thy - end; + end (* prove discriminator strictness rules *) local fun dis_strict dis = - let val goal = mk_trp (mk_strict dis); - in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end; + let val goal = mk_trp (mk_strict dis) + in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end in - val dis_stricts = map dis_strict dis_consts; - end; + val dis_stricts = map dis_strict dis_consts + end (* prove discriminator/constructor rules *) local fun dis_app (i, dis) (j, (con, args)) = let - val (vs, nonlazy) = get_vars args; - val lhs = dis ` list_ccomb (con, vs); - val rhs = if i = j then @{term TT} else @{term FF}; - val assms = map (mk_trp o mk_defined) nonlazy; - val concl = mk_trp (mk_eq (lhs, rhs)); - val goal = Logic.list_implies (assms, concl); - val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; - in prove thy dis_defs goal (K tacs) end; + val (vs, nonlazy) = get_vars args + val lhs = dis ` list_ccomb (con, vs) + val rhs = if i = j then @{term TT} else @{term FF} + val assms = map (mk_trp o mk_defined) nonlazy + val concl = mk_trp (mk_eq (lhs, rhs)) + val goal = Logic.list_implies (assms, concl) + val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1] + in prove thy dis_defs goal (K tacs) end fun one_dis (i, dis) = - map_index (dis_app (i, dis)) spec; + map_index (dis_app (i, dis)) spec in - val dis_apps = flat (map_index one_dis dis_consts); - end; + val dis_apps = flat (map_index one_dis dis_consts) + end (* prove discriminator definedness rules *) local fun dis_defin dis = let - val x = Free ("x", lhsT); - val simps = dis_apps @ @{thms dist_eq_tr}; + val x = Free ("x", lhsT) + val simps = dis_apps @ @{thms dist_eq_tr} val tacs = [rtac @{thm iffI} 1, asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2, rtac exhaust 1, atac 1, DETERM_UNTIL_SOLVED (CHANGED - (asm_full_simp_tac (simple_ss addsimps simps) 1))]; - val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)); - in prove thy [] goal (K tacs) end; + (asm_full_simp_tac (simple_ss addsimps simps) 1))] + val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)) + in prove thy [] goal (K tacs) end in - val dis_defins = map dis_defin dis_consts; - end; + val dis_defins = map dis_defin dis_consts + end in (dis_stricts @ dis_defins @ dis_apps, thy) - end; + end (******************************************************************************) (*************** definitions and theorems for match combinators ***************) @@ -770,80 +770,80 @@ (* get a fresh type variable for the result type *) val resultT : typ = let - val ts : string list = map fst (Term.add_tfreesT lhsT []); - val t : string = Name.variant ts "'t"; - in TFree (t, @{sort pcpo}) end; + val ts : string list = map fst (Term.add_tfreesT lhsT []) + val t : string = Name.variant ts "'t" + in TFree (t, @{sort pcpo}) end (* define match combinators *) local - val x = Free ("x", lhsT); - fun k args = Free ("k", map snd args -->> mk_matchT resultT); - val fail = mk_fail resultT; + val x = Free ("x", lhsT) + fun k args = Free ("k", map snd args -->> mk_matchT resultT) + val fail = mk_fail resultT fun mat_fun i (j, (con, args)) = let - val (vs, nonlazy) = get_vars_avoiding ["x","k"] args; + val (vs, nonlazy) = get_vars_avoiding ["x","k"] args in if i = j then k args else big_lambdas vs fail - end; + end fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix = let - val mat_bind = Binding.prefix_name "match_" bind; + val mat_bind = Binding.prefix_name "match_" bind val funs = map_index (mat_fun i) spec - val body = list_ccomb (case_const (mk_matchT resultT), funs); - val rhs = big_lambda x (big_lambda (k args) (body ` x)); + val body = list_ccomb (case_const (mk_matchT resultT), funs) + val rhs = big_lambda x (big_lambda (k args) (body ` x)) in (mat_bind, rhs, NoSyn) - end; + end in val ((match_consts, match_defs), thy) = define_consts (map_index mat_eqn (bindings ~~ spec)) thy - end; + end (* register match combinators with fixrec package *) local - val con_names = map (fst o dest_Const o fst) spec; - val mat_names = map (fst o dest_Const) match_consts; + val con_names = map (fst o dest_Const o fst) spec + val mat_names = map (fst o dest_Const) match_consts in - val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy; - end; + val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy + end (* prove strictness of match combinators *) local fun match_strict mat = let - val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)); - val k = Free ("k", U); - val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V)); - val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; - in prove thy match_defs goal (K tacs) end; + val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)) + val k = Free ("k", U) + val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V)) + val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1] + in prove thy match_defs goal (K tacs) end in - val match_stricts = map match_strict match_consts; - end; + val match_stricts = map match_strict match_consts + end (* prove match/constructor rules *) local - val fail = mk_fail resultT; + val fail = mk_fail resultT fun match_app (i, mat) (j, (con, args)) = let - val (vs, nonlazy) = get_vars_avoiding ["k"] args; - val (_, (kT, _)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)); - val k = Free ("k", kT); - val lhs = mat ` list_ccomb (con, vs) ` k; - val rhs = if i = j then list_ccomb (k, vs) else fail; - val assms = map (mk_trp o mk_defined) nonlazy; - val concl = mk_trp (mk_eq (lhs, rhs)); - val goal = Logic.list_implies (assms, concl); - val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; - in prove thy match_defs goal (K tacs) end; + val (vs, nonlazy) = get_vars_avoiding ["k"] args + val (_, (kT, _)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)) + val k = Free ("k", kT) + val lhs = mat ` list_ccomb (con, vs) ` k + val rhs = if i = j then list_ccomb (k, vs) else fail + val assms = map (mk_trp o mk_defined) nonlazy + val concl = mk_trp (mk_eq (lhs, rhs)) + val goal = Logic.list_implies (assms, concl) + val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1] + in prove thy match_defs goal (K tacs) end fun one_match (i, mat) = - map_index (match_app (i, mat)) spec; + map_index (match_app (i, mat)) spec in - val match_apps = flat (map_index one_match match_consts); - end; + val match_apps = flat (map_index one_match match_consts) + end in (match_stricts @ match_apps, thy) - end; + end (******************************************************************************) (******************************* main function ********************************) @@ -855,46 +855,46 @@ (iso_info : Domain_Take_Proofs.iso_info) (thy : theory) = let - val dname = Binding.name_of dbind; - val _ = writeln ("Proving isomorphism properties of domain "^dname^" ..."); + val dname = Binding.name_of dbind + val _ = writeln ("Proving isomorphism properties of domain "^dname^" ...") - val bindings = map #1 spec; + val bindings = map #1 spec (* retrieve facts about rep/abs *) - val lhsT = #absT iso_info; - val {rep_const, abs_const, ...} = iso_info; - val abs_iso_thm = #abs_inverse iso_info; - val rep_iso_thm = #rep_inverse iso_info; - val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm]; - val rep_strict = iso_locale RS @{thm iso.rep_strict}; - val abs_strict = iso_locale RS @{thm iso.abs_strict}; - val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff}; - val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff}; - val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict]; + val lhsT = #absT iso_info + val {rep_const, abs_const, ...} = iso_info + val abs_iso_thm = #abs_inverse iso_info + val rep_iso_thm = #rep_inverse iso_info + val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm] + val rep_strict = iso_locale RS @{thm iso.rep_strict} + val abs_strict = iso_locale RS @{thm iso.abs_strict} + val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff} + val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff} + val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict] (* qualify constants and theorems with domain name *) - val thy = Sign.add_path dname thy; + val thy = Sign.add_path dname thy (* define constructor functions *) val (con_result, thy) = let - fun prep_arg (lazy, sel, T) = (lazy, T); - fun prep_con (b, args, mx) = (b, map prep_arg args, mx); - val con_spec = map prep_con spec; + fun prep_arg (lazy, sel, T) = (lazy, T) + fun prep_con (b, args, mx) = (b, map prep_arg args, mx) + val con_spec = map prep_con spec in add_constructors con_spec abs_const iso_locale thy - end; + end val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews, - inverts, injects, dist_les, dist_eqs} = con_result; + inverts, injects, dist_les, dist_eqs} = con_result (* prepare constructor spec *) val con_specs : (term * (bool * typ) list) list = let - fun prep_arg (lazy, sel, T) = (lazy, T); - fun prep_con c (b, args, mx) = (c, map prep_arg args); + fun prep_arg (lazy, sel, T) = (lazy, T) + fun prep_con c (b, args, mx) = (c, map prep_arg args) in map2 prep_con con_consts spec - end; + end (* define case combinator *) val ((case_const : typ -> term, cases : thm list), thy) = @@ -905,34 +905,34 @@ val (sel_thms : thm list, thy : theory) = let val sel_spec : (term * (bool * binding option * typ) list) list = - map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec; + map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec in add_selectors sel_spec rep_const abs_iso_thm rep_strict rep_bottom_iff con_betas thy - end; + end (* define and prove theorems for discriminator functions *) val (dis_thms : thm list, thy : theory) = add_discriminators bindings con_specs lhsT - exhaust case_const cases thy; + exhaust case_const cases thy (* define and prove theorems for match combinators *) val (match_thms : thm list, thy : theory) = add_match_combinators bindings con_specs lhsT - exhaust case_const cases thy; + exhaust case_const cases thy (* restore original signature path *) - val thy = Sign.parent_path thy; + val thy = Sign.parent_path thy (* bind theorem names in global theory *) val (_, thy) = let - fun qualified name = Binding.qualified true name dbind; - val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec; - val dname = fst (dest_Type lhsT); - val simp = Simplifier.simp_add; - val case_names = Rule_Cases.case_names names; - val cases_type = Induct.cases_type dname; + fun qualified name = Binding.qualified true name dbind + val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec + val dname = fst (dest_Type lhsT) + val simp = Simplifier.simp_add + val case_names = Rule_Cases.case_names names + val cases_type = Induct.cases_type dname in Global_Theory.add_thmss [ ((qualified "iso_rews" , iso_rews ), [simp]), @@ -948,7 +948,7 @@ ((qualified "inverts" , inverts ), [simp]), ((qualified "injects" , injects ), [simp]), ((qualified "match_rews", match_thms ), [simp])] thy - end; + end val result = { @@ -967,9 +967,9 @@ sel_rews = sel_thms, dis_rews = dis_thms, match_rews = match_thms - }; + } in (result, thy) - end; + end -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Tue Nov 30 14:21:57 2010 -0800 @@ -13,20 +13,20 @@ Domain_Constructors.constr_info list -> theory -> thm list * theory - val quiet_mode: bool Unsynchronized.ref; - val trace_domain: bool Unsynchronized.ref; -end; + 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; +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 (); +fun message s = if !quiet_mode then () else writeln s +fun trace s = if !trace_domain then tracing s else () -open HOLCF_Library; +open HOLCF_Library (******************************************************************************) (***************************** proofs about take ******************************) @@ -38,60 +38,60 @@ (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 {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 = Free ("n", @{typ nat}) + val n' = @{const Suc} $ n local - val newTs = map (#absT o #iso_info) constr_infos; - val subs = newTs ~~ map (fn t => t $ n) take_consts; + 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; + | 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; + let val m = Domain_Take_Proofs.map_of_typ thy subs T + in if is_ID m then v else mk_capply (m, v) end end fun prove_take_apps ((dbind, take_const), constr_info) thy = let - val {iso_info, con_specs, con_betas, ...} = constr_info; - val {abs_inverse, ...} = iso_info; + val {iso_info, con_specs, con_betas, ...} = constr_info + val {abs_inverse, ...} = iso_info fun prove_take_app (con_const, args) = let - val Ts = map snd args; - val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts); - val vs = map Free (ns ~~ Ts); - val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)); - val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts); - val goal = mk_trp (mk_eq (lhs, rhs)); + val Ts = map snd args + val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts) + val vs = map Free (ns ~~ Ts) + val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)) + val rhs = list_ccomb (con_const, map2 (map_of_arg 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; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + @ take_Suc_thms @ deflation_thms @ deflation_take_thms + val tac = simp_tac (HOL_basic_ss addsimps rules) 1 in Goal.prove_global thy [] [] goal (K tac) - end; - val take_apps = map prove_take_app con_specs; + end + val take_apps = map prove_take_app con_specs in yield_singleton Global_Theory.add_thmss ((Binding.qualified true "take_rews" dbind, take_apps), [Simplifier.simp_add]) thy - end; + end in fold_map prove_take_apps (dbinds ~~ take_consts ~~ constr_infos) thy -end; +end (******************************************************************************) (****************************** induction rules *******************************) (******************************************************************************) val case_UU_allI = - @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}; + @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis} fun prove_induction (comp_dbind : binding) @@ -100,135 +100,135 @@ (take_rews : thm list) (thy : theory) = let - val comp_dname = Binding.name_of comp_dbind; + 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 iso_infos = map #iso_info constr_infos + val exhausts = map #exhaust constr_infos + val con_rews = maps #con_rews constr_infos + val {take_consts, take_induct_thms, ...} = take_info - val newTs = map #absT iso_infos; - val P_names = Datatype_Prop.indexify_names (map (K "P") newTs); - val x_names = Datatype_Prop.indexify_names (map (K "x") newTs); - val P_types = map (fn T => T --> HOLogic.boolT) newTs; - val Ps = map Free (P_names ~~ P_types); - val xs = map Free (x_names ~~ newTs); - val n = Free ("n", HOLogic.natT); + val newTs = map #absT iso_infos + val P_names = Datatype_Prop.indexify_names (map (K "P") newTs) + val x_names = Datatype_Prop.indexify_names (map (K "x") newTs) + val P_types = map (fn T => T --> HOLogic.boolT) newTs + val Ps = map Free (P_names ~~ P_types) + val xs = map Free (x_names ~~ newTs) + val n = Free ("n", HOLogic.natT) fun con_assm defined p (con, args) = let - val Ts = map snd args; - val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts); - val vs = map Free (ns ~~ Ts); - val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + val Ts = map snd args + val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts) + val vs = map Free (ns ~~ Ts) + val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)) fun ind_hyp (v, T) t = case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t - | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t); - val t1 = mk_trp (p $ list_ccomb (con, vs)); - val t2 = fold_rev ind_hyp (vs ~~ Ts) t1; - val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2); - in fold_rev Logic.all vs (if defined then t3 else t2) end; + | 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); + mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons + val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos) - val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews); + val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews) fun quant_tac ctxt i = EVERY - (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names); + (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names) (* FIXME: move this message to domain_take_proofs.ML *) - val is_finite = #is_finite take_info; + val is_finite = #is_finite take_info val _ = if is_finite then message ("Proving finiteness rule for domain "^comp_dname^" ...") - else (); + else () - val _ = trace " Proving finite_ind..."; + 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); + (Ps ~~ take_consts ~~ xs) + val goal = mk_trp (foldr1 mk_conj concls) fun tacf {prems, context} = let (* Prove stronger prems, without definedness side conditions *) fun con_thm p (con, args) = let - val subgoal = con_assm false p (con, args); - val rules = prems @ con_rews @ simp_thms; - val simplify = asm_simp_tac (HOL_basic_ss addsimps rules); + val subgoal = con_assm false p (con, args) + val rules = prems @ con_rews @ simp_thms + val simplify = asm_simp_tac (HOL_basic_ss addsimps rules) fun arg_tac (lazy, _) = - rtac (if lazy then allI else case_UU_allI) 1; + rtac (if lazy then allI else case_UU_allI) 1 val tacs = rewrite_goals_tac @{thms atomize_all atomize_imp} :: map arg_tac args @ - [REPEAT (rtac impI 1), ALLGOALS simplify]; + [REPEAT (rtac impI 1), ALLGOALS simplify] in Goal.prove context [] [] subgoal (K (EVERY tacs)) - end; - fun eq_thms (p, cons) = map (con_thm p) cons; - val conss = map #con_specs constr_infos; - val prems' = maps eq_thms (Ps ~~ conss); + end + fun eq_thms (p, cons) = map (con_thm p) cons + val conss = map #con_specs constr_infos + val prems' = maps eq_thms (Ps ~~ conss) val tacs1 = [ quant_tac context 1, simp_tac HOL_ss 1, InductTacs.induct_tac context [[SOME "n"]] 1, simp_tac (take_ss addsimps prems) 1, - TRY (safe_tac HOL_cs)]; + TRY (safe_tac HOL_cs)] fun con_tac _ = asm_simp_tac take_ss 1 THEN - (resolve_tac prems' THEN_ALL_NEW etac spec) 1; + (resolve_tac prems' THEN_ALL_NEW etac spec) 1 fun cases_tacs (cons, exhaust) = res_inst_tac context [(("y", 0), "x")] exhaust 1 :: asm_simp_tac (take_ss addsimps prems) 1 :: - map con_tac cons; + 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; + end + in Goal.prove_global thy [] assms goal tacf end - val _ = trace " Proving ind..."; + 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; + val concls = map (op $) (Ps ~~ xs) + val goal = mk_trp (foldr1 mk_conj concls) + val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps fun tacf {prems, context} = let fun finite_tac (take_induct, fin_ind) = rtac take_induct 1 THEN (if is_finite then all_tac else resolve_tac prems 1) THEN - (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1; - val fin_inds = Project_Rule.projections context finite_ind; + (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1 + val fin_inds = Project_Rule.projections context finite_ind in TRY (safe_tac HOL_cs) THEN EVERY (map finite_tac (take_induct_thms ~~ fin_inds)) - end; + 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 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; + 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; + map (fn s => "bottom_" ^ Long_Name.base_name s) dnames fun one_eq bot constr_info = - let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c)); - in bot :: map name_of (#con_specs constr_info) end; - in adms @ flat (map2 one_eq bottoms constr_infos) end; + let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c)) + in bot :: map name_of (#con_specs constr_info) end + in adms @ flat (map2 one_eq bottoms constr_infos) end - val inducts = Project_Rule.projections (ProofContext.init_global thy) ind; + val inducts = Project_Rule.projections (ProofContext.init_global thy) ind fun ind_rule (dname, rule) = ((Binding.empty, rule), - [Rule_Cases.case_names case_ns, Induct.induct_type dname]); + [Rule_Cases.case_names case_ns, Induct.induct_type dname]) in thy @@ -236,7 +236,7 @@ ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), ((Binding.qualified true "induct" comp_dbind, ind ), [])] |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) -end; (* prove_induction *) +end (* prove_induction *) (******************************************************************************) (************************ bisimulation and coinduction ************************) @@ -249,83 +249,83 @@ (take_rews : thm list list) (thy : theory) : theory = let - val iso_infos = map #iso_info constr_infos; - val newTs = map #absT iso_infos; + 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 {take_consts, take_0_thms, take_lemma_thms, ...} = take_info - val R_names = Datatype_Prop.indexify_names (map (K "R") newTs); - val R_types = map (fn T => T --> T --> boolT) newTs; - val Rs = map Free (R_names ~~ R_types); - val n = Free ("n", natT); - val reserved = "x" :: "y" :: R_names; + val R_names = Datatype_Prop.indexify_names (map (K "R") newTs) + val R_types = map (fn T => T --> T --> boolT) newTs + val Rs = map Free (R_names ~~ R_types) + val n = Free ("n", natT) + val reserved = "x" :: "y" :: R_names (* declare bisimulation predicate *) - val bisim_bind = Binding.suffix_name "_bisim" comp_dbind; - val bisim_type = R_types ---> boolT; + val bisim_bind = Binding.suffix_name "_bisim" comp_dbind + val bisim_type = R_types ---> boolT val (bisim_const, thy) = - Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; + Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy (* define bisimulation predicate *) local fun one_con T (con, args) = let - val Ts = map snd args; - val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts); - val ns2 = map (fn n => n^"'") ns1; - val vs1 = map Free (ns1 ~~ Ts); - val vs2 = map Free (ns2 ~~ Ts); - val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1)); - val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2)); + val Ts = map snd args + val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts) + val ns2 = map (fn n => n^"'") ns1 + val vs1 = map Free (ns1 ~~ Ts) + val vs2 = map Free (ns2 ~~ Ts) + val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1)) + val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2)) fun rel ((v1, v2), T) = case AList.lookup (op =) (newTs ~~ Rs) T of - NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2; - val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]); + 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; + 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; + 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); + end + val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos) + val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs) + val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs) in val (bisim_def_thm, thy) = thy |> yield_singleton (Global_Theory.add_defs false) - ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []); + ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []) end (* local *) (* prove coinduction lemma *) val coind_lemma = let - val assm = mk_trp (list_comb (bisim_const, Rs)); + 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); + 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; + end val goal = - mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts))); - val rules = @{thm Rep_cfun_strict1} :: take_0_thms; + mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts))) + val rules = @{thm Rep_cfun_strict1} :: take_0_thms fun tacf {prems, context} = let - val prem' = rewrite_rule [bisim_def_thm] (hd prems); - val prems' = Project_Rule.projections context prem'; - val dests = map (fn th => th RS spec RS spec RS mp) prems'; + val prem' = rewrite_rule [bisim_def_thm] (hd prems) + val prems' = Project_Rule.projections context prem' + val dests = map (fn th => th RS spec RS spec RS mp) prems' fun one_tac (dest, rews) = dtac dest 1 THEN safe_tac HOL_cs THEN - ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews)); + ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews)) in rtac @{thm nat.induct} 1 THEN simp_tac (HOL_ss addsimps rules) 1 THEN @@ -334,33 +334,33 @@ end in Goal.prove_global thy [] [assm] goal tacf - end; + 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)); + val x = Free ("x", T) + val y = Free ("y", T) + val assm1 = mk_trp (list_comb (bisim_const, Rs)) + val assm2 = mk_trp (R $ x $ y) + val goal = mk_trp (mk_eq (x, y)) fun tacf {prems, context} = let - val rule = hd prems RS coind_lemma; + val rule = hd prems RS coind_lemma in rtac take_lemma 1 THEN asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1 - end; + end in Goal.prove_global thy [] [assm1, assm2] goal tacf - end; - val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms); - val coind_binds = map (Binding.qualified true "coinduct") dbinds; + end + val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms) + val coind_binds = map (Binding.qualified true "coinduct") dbinds in thy |> snd o Global_Theory.add_thms (map Thm.no_attributes (coind_binds ~~ coinds)) -end; (* let *) +end (* let *) (******************************************************************************) (******************************* main function ********************************) @@ -373,67 +373,67 @@ (thy : theory) = let -val comp_dname = space_implode "_" (map Binding.name_of dbinds); -val comp_dbind = Binding.name comp_dname; +val comp_dname = space_implode "_" (map Binding.name_of dbinds) +val comp_dbind = Binding.name comp_dname (* Test for emptiness *) (* FIXME: reimplement emptiness test local - open Domain_Library; - val dnames = map (fst o fst) eqs; - val conss = map snd eqs; + open Domain_Library + val dnames = map (fst o fst) eqs + val conss = map snd eqs fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse rec_of arg <> n andalso rec_to (rec_of arg::ns) (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) - ) o snd) cons; + ) o snd) cons fun warn (n,cons) = if rec_to [] false (n,cons) - then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) - else false; + then (warning ("domain "^List.nth(dnames,n)^" is empty!") true) + else false in - val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; - val is_emptys = map warn n__eqs; -end; + 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; + 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; + | 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 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; + 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; + take_theorems dbinds take_info constr_infos thy -val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info; +val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info -val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss; +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; + 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; + prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy in (take_rews, thy) -end; (* let *) -end; (* struct *) +end (* let *) +end (* struct *) diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Nov 30 14:21:57 2010 -0800 @@ -29,20 +29,20 @@ -> theory -> theory val setup : theory -> theory -end; +end structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = struct val beta_rules = @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ - @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'}; + @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'} -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); +val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules) -val beta_tac = simp_tac beta_ss; +val beta_tac = simp_tac beta_ss -fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo}); +fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo}) (******************************************************************************) (******************************** theory data *********************************) @@ -58,7 +58,7 @@ ( val name = "domain_isodefl" val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" -); +) val setup = RepData.setup #> IsodeflData.setup @@ -67,51 +67,51 @@ (************************** building types and terms **************************) (******************************************************************************) -open HOLCF_Library; +open HOLCF_Library -infixr 6 ->>; -infixr -->>; +infixr 6 ->> +infixr -->> -val udomT = @{typ udom}; -val deflT = @{typ "defl"}; +val udomT = @{typ udom} +val deflT = @{typ "defl"} fun mk_DEFL T = - Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T; + Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T fun dest_DEFL (Const (@{const_name defl}, _) $ t) = Logic.dest_type t - | dest_DEFL t = raise TERM ("dest_DEFL", [t]); + | dest_DEFL t = raise TERM ("dest_DEFL", [t]) fun mk_LIFTDEFL T = - Const (@{const_name liftdefl}, Term.itselfT T --> deflT) $ Logic.mk_type T; + Const (@{const_name liftdefl}, Term.itselfT T --> deflT) $ Logic.mk_type T fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t - | dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [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 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 (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) in mk_capply (u_map_const, t) - end; + end -fun emb_const T = Const (@{const_name emb}, T ->> udomT); -fun prj_const T = Const (@{const_name prj}, udomT ->> T); -fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T); +fun emb_const T = Const (@{const_name emb}, T ->> udomT) +fun prj_const T = Const (@{const_name prj}, udomT ->> T) +fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T) fun isodefl_const T = - Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); + Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT) fun mk_deflation t = - Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; + Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t (* splits a cterm into the right and lefthand sides of equality *) -fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); +fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t) -fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); +fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) (******************************************************************************) (****************************** isomorphism info ******************************) @@ -119,9 +119,9 @@ 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]; + 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 @@ -132,19 +132,19 @@ fun mk_projs [] t = [] | mk_projs (x::[]) t = [(x, t)] - | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd 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) * 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); + 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; + val projs = mk_projs lhss fixpoint (* convert parameters to lambda abstractions *) fun mk_eqn (lhs, rhs) = @@ -154,48 +154,48 @@ | f $ Const (@{const_name TYPE}, T) => mk_eqn (f, Abs ("t", T, rhs)) | Const _ => Logic.mk_equals (lhs, rhs) - | _ => raise TERM ("lhs not of correct form", [lhs, rhs]); - val eqns = map mk_eqn projs; + | _ => 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 (Binding.suffix_name "_def") binds ~~ eqns) thy; + (map (Binding.suffix_name "_def") binds ~~ eqns) thy (* prove applied version of definitions *) fun prove_proj (lhs, rhs) = let - val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1; - val goal = Logic.mk_equals (lhs, rhs); - in Goal.prove_global thy [] [] goal (K tac) end; - val proj_thms = map prove_proj projs; + val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1 + val goal = Logic.mk_equals (lhs, rhs) + in Goal.prove_global thy [] [] goal (K tac) 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; + fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2] + val tuple_fixdef_thm = foldr1 pair_equalI proj_thms val cont_thm = Goal.prove_global thy [] [] (mk_trp (mk_cont functional)) - (K (beta_tac 1)); + (K (beta_tac 1)) val tuple_unfold_thm = (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) - |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv}; + |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv} fun mk_unfold_thms [] thm = [] | 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; + 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; + (mk_unfold_thms unfold_binds tuple_unfold_thm) thy in ((proj_thms, unfold_thms), thy) - end; + end (******************************************************************************) @@ -208,20 +208,20 @@ (tab2 : (typ * term) list) (T : typ) : term = let - val defl_simps = RepData.get (ProofContext.init_global thy); - val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps; - val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2; + val defl_simps = RepData.get (ProofContext.init_global thy) + val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) 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; + | _ => NONE) handle TERM _ => NONE fun proc2 t = (case dest_LIFTDEFL t of TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, deflT)) - | _ => NONE) handle TERM _ => NONE; + | _ => NONE) handle TERM _ => NONE in Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T) - end; + end (******************************************************************************) (********************* declaring definitions and theorems *********************) @@ -232,18 +232,18 @@ (thy : theory) : (term * thm) * theory = let - val typ = Term.fastype_of rhs; - val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy; - val eqn = Logic.mk_equals (const, rhs); - val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn); - val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy; + val typ = Term.fastype_of rhs + val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy + val eqn = Logic.mk_equals (const, rhs) + val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn) + val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy in ((const, def_thm), thy) - end; + end fun add_qualified_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms - ((Binding.qualified true name dbind, thm), []); + ((Binding.qualified true name dbind, thm), []) (******************************************************************************) (*************************** defining map functions ***************************) @@ -255,77 +255,77 @@ 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; + 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; + | mapT T = T ->> T (* declare map functions *) fun declare_map_const (tbind, (lhsT, rhsT)) thy = let - val map_type = mapT lhsT; - val map_bind = Binding.suffix_name "_map" tbind; + val map_type = mapT lhsT + val map_bind = Binding.suffix_name "_map" tbind in Sign.declare_const ((map_bind, map_type), NoSyn) thy - end; + end val (map_consts, thy) = thy |> - fold_map declare_map_const (dbinds ~~ dom_eqns); + 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 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; + (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), map_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; + 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; + 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_binds = map (Binding.suffix_name "_map") dbinds val ((map_apply_thms, map_unfold_thms), thy) = - add_fixdefs (map_binds ~~ map_specs) 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_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 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, rhsT)) = 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 (_, 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 start_thms = - @{thm split_def} :: map_apply_thms; + @{thm split_def} :: map_apply_thms val adm_rules = @{thms adm_conj adm_subst [OF _ adm_deflation] - cont2cont_fst cont2cont_snd cont_id}; + cont2cont_fst cont2cont_snd cont_id} val bottom_rules = - @{thms fst_strict snd_strict deflation_UU simp_thms}; + @{thms fst_strict snd_strict deflation_UU simp_thms} val deflation_rules = @{thms conjI deflation_ID} @ deflation_abs_rep_thms - @ Domain_Take_Proofs.get_deflation_thms thy; + @ Domain_Take_Proofs.get_deflation_thms thy in Goal.prove_global thy [] assms goal (fn {prems, ...} => EVERY @@ -337,34 +337,34 @@ simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, REPEAT (etac @{thm conjE} 1), REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)]) - end; + end fun conjuncts [] thm = [] | 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 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"); + 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); + (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; - val map_names = map (fst o dest_Const) map_consts; - fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []; - val argss = map args dom_eqns; + Domain_Take_Proofs.add_rec_type (dname, args) + val dnames = map (fst o dest_Type o fst) dom_eqns + val map_names = map (fst o dest_Const) map_consts + 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; + fold register_map (dnames ~~ argss) thy + end (* register deflation theorems *) - val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy; + val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy val result = { @@ -375,7 +375,7 @@ } in (result, thy) - end; + end (******************************************************************************) (******************************* main function ********************************) @@ -384,20 +384,20 @@ fun read_typ thy str sorts = let val ctxt = ProofContext.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; + |> 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; + 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; + in (T, sorts') end fun gen_domain_isomorphism (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list) @@ -406,49 +406,49 @@ : (Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info) * theory = let - val _ = Theory.requires thy "Domain" "domain isomorphisms"; + val _ = Theory.requires thy "Domain" "domain isomorphisms" (* this theory is used just for parsing *) val tmp_thy = thy |> Theory.copy |> Sign.add_types (map (fn (tvs, tbind, mx, _, morphs) => - (tbind, length tvs, mx)) doms_raw); + (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; + 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 []; + 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); + fun the_sort v = the (AList.lookup (op =) sorts v) (* declare arities in temporary theory *) val tmp_thy = let fun arity (vs, tbind, mx, _, _) = - (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"}); + (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"}) in fold AxClass.axiomatize_arity (map arity doms) tmp_thy - end; + end (* check bifiniteness of right-hand sides *) fun check_rhs (vs, tbind, mx, rhs, morphs) = 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; + quote (Syntax.string_of_typ_global tmp_thy rhs)) + val _ = map check_rhs doms (* domain equations *) fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) = - 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; + 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 (tyvars, _, _, _, _) = hd doms val new_doms = map (fn (tvs, tname, mx, _, _) => let val full_tname = Sign.full_name tmp_thy tname in @@ -458,133 +458,133 @@ else error ("Mutually recursive domains must have same type parameters") | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^ " : " ^ commas dups)) - end) doms; - val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms; - val morphs = map (fn (_, _, _, _, morphs) => morphs) doms; + 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; + 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)); + 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 []); + 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); + 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; + 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_bind = Binding.suffix_name "_defl" tbind val defl_type = - map Term.itselfT typeTs ---> map (K deflT) defl_args -->> deflT; + map Term.itselfT typeTs ---> map (K deflT) defl_args -->> deflT in Sign.declare_const ((defl_bind, defl_type), NoSyn) thy - end; + end val (defl_consts, thy) = - fold_map declare_defl_const (defl_flagss ~~ doms) 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; + 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; + 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; + 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_binds = map (Binding.suffix_name "_defl") dbinds val ((defl_apply_thms, defl_unfold_thms), thy) = - add_fixdefs (defl_binds ~~ defl_specs) 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 spec = (tbind, map (rpair dummyS) vs, mx) val ((_, _, _, {DEFL, liftemb_def, liftprj_def, ...}), thy) = - Domaindef.add_domaindef false NONE spec defl NONE thy; + Domaindef.add_domaindef false NONE spec defl NONE thy (* declare domain_defl_simps rules *) - val thy = Context.theory_map (RepData.add_thm DEFL) thy; + val thy = Context.theory_map (RepData.add_thm DEFL) thy in (DEFL, thy) - end; - val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) 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 = RepData.get (ProofContext.init_global thy); + val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT) + val DEFL_simps = RepData.get (ProofContext.init_global thy) val tac = rewrite_goals_tac (map mk_meta_eq DEFL_simps) - THEN TRY (resolve_tac defl_unfold_thms 1); + THEN TRY (resolve_tac defl_unfold_thms 1) in Goal.prove_global thy [] [] goal (K tac) - end; - val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns; + 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 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); + (DEFL_eq_binds ~~ DEFL_eq_thms) (* define rep/abs functions *) fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy = let - val rep_bind = Binding.suffix_name "_rep" tbind; - val abs_bind = Binding.suffix_name "_abs" tbind; + val rep_bind = Binding.suffix_name "_rep" tbind + val abs_bind = Binding.suffix_name "_abs" tbind val ((rep_const, rep_def), thy) = - define_const (rep_bind, coerce_const (lhsT, rhsT)) thy; + define_const (rep_bind, coerce_const (lhsT, rhsT)) thy val ((abs_const, abs_def), thy) = - define_const (abs_bind, coerce_const (rhsT, lhsT)) thy; + define_const (abs_bind, coerce_const (rhsT, lhsT)) thy in (((rep_const, abs_const), (rep_def, abs_def)), thy) - end; + end val ((rep_abs_consts, rep_abs_defs), thy) = thy |> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns) - |>> ListPair.unzip; + |>> 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}; + 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); + |> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm) in (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) - end; + end val ((iso_thms, isodefl_abs_rep_thms), thy) = thy |> fold_map mk_iso_thms (dbinds ~~ DEFL_eq_thms ~~ rep_abs_defs) - |>> ListPair.unzip; + |>> ListPair.unzip (* collect info about rep/abs *) val iso_infos : Domain_Take_Proofs.iso_info list = @@ -597,51 +597,51 @@ 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; + define_map_functions (dbinds ~~ iso_infos) thy val { map_consts, map_apply_thms, map_unfold_thms, - deflation_map_thms } = map_info; + deflation_map_thms } = 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)), deflT); - fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T); + 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)), deflT) + 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 (mk_upT T) $ mk_u_map (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; + in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end fun mk_goal (map_const, (T, rhsT)) = 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 (_, 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 start_thms = - @{thm split_def} :: defl_apply_thms @ map_apply_thms; + @{thm split_def} :: defl_apply_thms @ map_apply_thms val adm_rules = - @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}; + @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id} val bottom_rules = - @{thms fst_strict snd_strict isodefl_bottom simp_thms}; - 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; + @{thms fst_strict snd_strict isodefl_bottom simp_thms} + 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 - @ IsodeflData.get (ProofContext.init_global thy); + @ IsodeflData.get (ProofContext.init_global thy) in Goal.prove_global thy [] assms goal (fn {prems, ...} => EVERY @@ -656,69 +656,69 @@ simp_tac (HOL_basic_ss addsimps map_ID_simps) 1, REPEAT (etac @{thm conjE} 1), REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)]) - end; - val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds; + end + val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds fun conjuncts [] thm = [] | 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 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 IsodeflData.add_thm) isodefl_thms thy; + (conjuncts isodefl_binds isodefl_thm) + val thy = fold (Context.theory_map o IsodeflData.add_thm) 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); + 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) val tac = EVERY [rtac @{thm isodefl_DEFL_imp_ID} 1, stac DEFL_thm 1, rtac isodefl_thm 1, - REPEAT (resolve_tac @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)]; + REPEAT (resolve_tac @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)] in Goal.prove_global thy [] [] goal (K tac) - end; - val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds; + 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); + (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); + (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; + (dbinds ~~ iso_infos) thy val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} = - take_info; + 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}); + 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, rhsT)) = - 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; + 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 pair_collapse split_def} - @ map_apply_thms @ map_ID_thms; + @ map_apply_thms @ map_ID_thms val rules0 = - @{thms iterate_0 Pair_strict} @ take_0_thms; + @{thms iterate_0 Pair_strict} @ take_0_thms val rules1 = @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv} - @ take_Suc_thms; + @ take_Suc_thms val tac = EVERY [simp_tac (HOL_basic_ss addsimps start_rules) 1, @@ -726,39 +726,39 @@ rtac @{thm lub_eq} 1, rtac @{thm nat.induct} 1, simp_tac (HOL_basic_ss addsimps rules0) 1, - asm_full_simp_tac (beta_ss addsimps rules1) 1]; + asm_full_simp_tac (beta_ss addsimps rules1) 1] in Goal.prove_global thy [] [] goal (K tac) - end; + end (* prove lub of take equals ID *) fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy = let - val n = Free ("n", natT); - val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT); + val n = Free ("n", natT) + val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT) val tac = EVERY [rtac @{thm trans} 1, rtac map_ID_thm 2, cut_facts_tac [lub_take_lemma] 1, - REPEAT (etac @{thm Pair_inject} 1), atac 1]; - val lub_take_thm = Goal.prove_global thy [] [] goal (K tac); + REPEAT (etac @{thm Pair_inject} 1), atac 1] + val lub_take_thm = Goal.prove_global thy [] [] goal (K tac) in add_qualified_thm "lub_take" (dbind, lub_take_thm) thy - end; + end val (lub_take_thms, thy) = fold_map prove_lub_take - (dbinds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy; + (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; + (dbinds ~~ iso_infos) take_info lub_take_thms thy in ((iso_infos, take_info2), thy) - end; + end -val domain_isomorphism = gen_domain_isomorphism cert_typ; -val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ; +val domain_isomorphism = gen_domain_isomorphism cert_typ +val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ (******************************************************************************) (******************************** outer syntax ********************************) @@ -771,17 +771,17 @@ parser = (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))) - >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)); + >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)) -val parse_domain_isos = Parse.and_list1 parse_domain_iso; +val parse_domain_isos = Parse.and_list1 parse_domain_iso in val _ = Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" Keyword.thy_decl - (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd)); + (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd)) -end; +end -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Nov 30 14:21:57 2010 -0800 @@ -62,7 +62,7 @@ val map_ID_add : attribute val get_map_ID_thms : theory -> thm list val setup : theory -> theory -end; +end structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS = struct @@ -75,7 +75,7 @@ rep_const : term, abs_inverse : thm, rep_inverse : thm - }; + } type take_info = { take_consts : term list, @@ -87,7 +87,7 @@ take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list - }; + } type take_induct_info = { @@ -105,15 +105,15 @@ take_lemma_thms : thm list, is_finite : bool, take_induct_thms : thm list - }; + } val beta_rules = @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ - @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; + @{thms cont2cont_fst cont2cont_snd cont2cont_Pair} -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); +val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules) -val beta_tac = simp_tac beta_ss; +val beta_tac = simp_tac beta_ss (******************************************************************************) (******************************** theory data *********************************) @@ -122,56 +122,56 @@ 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; -); + type T = (bool list) Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) structure DeflMapData = Named_Thms ( val name = "domain_deflation" val description = "theorems like deflation a ==> deflation (foo_map$a)" -); +) structure Map_Id_Data = Named_Thms ( val name = "domain_map_ID" val description = "theorems like foo_map$ID = ID" -); +) fun add_rec_type (tname, bs) = - Rec_Data.map (Symtab.insert (K true) (tname, bs)); + Rec_Data.map (Symtab.insert (K true) (tname, bs)) fun add_deflation_thm thm = - Context.theory_map (DeflMapData.add_thm thm); + Context.theory_map (DeflMapData.add_thm thm) -val get_rec_tab = Rec_Data.get; -fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy); +val get_rec_tab = Rec_Data.get +fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy) -val map_ID_add = Map_Id_Data.add; -val get_map_ID_thms = Map_Id_Data.get o ProofContext.init_global; +val map_ID_add = Map_Id_Data.add +val get_map_ID_thms = Map_Id_Data.get o ProofContext.init_global -val setup = DeflMapData.setup #> Map_Id_Data.setup; +val setup = DeflMapData.setup #> Map_Id_Data.setup (******************************************************************************) (************************** building types and terms **************************) (******************************************************************************) -open HOLCF_Library; +open HOLCF_Library -infixr 6 ->>; -infix -->>; -infix 9 `; +infixr 6 ->> +infix -->> +infix 9 ` fun mapT (T as Type (_, Ts)) = (map (fn T => T ->> T) Ts) -->> (T ->> T) - | mapT T = T ->> T; + | mapT T = T ->> T fun mk_deflation t = - Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; + Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t -fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); +fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) (******************************************************************************) (****************************** isomorphism info ******************************) @@ -179,9 +179,9 @@ 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]; + 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 @@ -192,14 +192,14 @@ 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; + 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; + end (******************************************************************************) (********************* declaring definitions and theorems *********************) @@ -207,15 +207,15 @@ fun add_qualified_def name (dbind, eqn) = yield_singleton (Global_Theory.add_defs false) - ((Binding.qualified true name dbind, eqn), []); + ((Binding.qualified true name dbind, eqn), []) fun add_qualified_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms - ((Binding.qualified true name dbind, thm), []); + ((Binding.qualified true name dbind, thm), []) fun add_qualified_simp_thm name (dbind, thm) = yield_singleton Global_Theory.add_thms - ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]); + ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]) (******************************************************************************) (************************** defining take functions ***************************) @@ -227,119 +227,119 @@ 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; + 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 [] t = [] | mk_projs (x::[]) t = [(x, t)] - | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd 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)); + 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); + 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, (lhsT, rhsT)) = let - val body = map_of_typ thy (newTs ~~ copy_args) rhsT; + val body = map_of_typ thy (newTs ~~ copy_args) rhsT in mk_cfcomp2 (rep_abs, body) - end; + end val take_functional = big_lambda copy_arg - (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))); + (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))) val take_rhss = let - val n = Free ("n", HOLogic.natT); - val rhs = mk_iterate (n, take_functional); + val n = Free ("n", HOLogic.natT) + val rhs = mk_iterate (n, take_functional) in map (lambda n o snd) (mk_projs dbinds rhs) - end; + end (* define take constants *) fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy = let - val take_type = HOLogic.natT --> lhsT ->> lhsT; - val take_bind = Binding.suffix_name "_take" dbind; + val take_type = HOLogic.natT --> lhsT ->> lhsT + val take_bind = Binding.suffix_name "_take" dbind val (take_const, thy) = - Sign.declare_const ((take_bind, take_type), NoSyn) thy; - val take_eqn = Logic.mk_equals (take_const, take_rhs); + Sign.declare_const ((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; + 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; + |>> 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}; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; - val thm = Goal.prove_global thy [] [] goal (K tac); + val goal = mk_trp (mk_chain take_const) + val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd} + val tac = simp_tac (HOL_basic_ss addsimps rules) 1 + val thm = Goal.prove_global thy [] [] goal (K tac) in add_qualified_simp_thm "chain_take" (dbind, thm) thy - end; + end val (chain_take_thms, thy) = - fold_map prove_chain_take (take_consts ~~ dbinds) thy; + fold_map prove_chain_take (take_consts ~~ dbinds) thy (* prove take_0 lemmas *) fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) 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}; - val tac = simp_tac (HOL_basic_ss addsimps rules) 1; - val take_0_thm = Goal.prove_global thy [] [] goal (K tac); + 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} + val tac = simp_tac (HOL_basic_ss addsimps rules) 1 + val take_0_thm = Goal.prove_global thy [] [] goal (K tac) in add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy - end; + end val (take_0_thms, thy) = - fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy; + fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy (* prove take_Suc lemmas *) - val n = Free ("n", natT); - val take_is = map (fn t => t $ n) take_consts; + val n = Free ("n", natT) + val take_is = map (fn t => t $ n) take_consts fun prove_take_Suc (((take_const, rep_abs), dbind), (lhsT, 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 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; - val tac = simp_tac (beta_ss addsimps rules) 1; - val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac); + val rules = take_defs @ simps + val tac = simp_tac (beta_ss addsimps rules) 1 + val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac) in add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy - end; + end val (take_Suc_thms, thy) = fold_map prove_take_Suc - (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy; + (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_abs_rep_thms = map deflation_abs_rep iso_infos val deflation_take_thm = let - val n = Free ("n", natT); - fun mk_goal take_const = mk_deflation (take_const $ n); - val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)); + val n = Free ("n", natT) + fun mk_goal take_const = mk_deflation (take_const $ n) + val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)) val adm_rules = @{thms adm_conj adm_subst [OF _ adm_deflation] - cont2cont_fst cont2cont_snd cont_id}; + cont2cont_fst cont2cont_snd cont_id} val bottom_rules = - take_0_thms @ @{thms deflation_UU simp_thms}; + take_0_thms @ @{thms deflation_UU simp_thms} val deflation_rules = @{thms conjI deflation_ID} @ deflation_abs_rep_thms - @ get_deflation_thms thy; + @ get_deflation_thms thy in Goal.prove_global thy [] [] goal (fn _ => EVERY @@ -349,76 +349,76 @@ REPEAT (etac @{thm conjE} 1 ORELSE resolve_tac deflation_rules 1 ORELSE atac 1)]) - end; + end fun conjuncts [] thm = [] | 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 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; + (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]); + (@{thm deflation_strict} OF [deflation_take]) in add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy - end; + end val (take_strict_thms, thy) = fold_map prove_take_strict - (deflation_take_thms ~~ dbinds) thy; + (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]); + (@{thm deflation_chain_min} OF [chain_take, deflation_take]) in add_qualified_thm "take_take" (dbind, take_take_thm) thy - end; + end val (take_take_thms, thy) = fold_map prove_take_take - (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy; + (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]); + (@{thm deflation.below} OF [deflation_take]) in add_qualified_thm "take_below" (dbind, take_below_thm) thy - end; + end val (take_below_thms, thy) = fold_map prove_take_below - (deflation_take_thms ~~ dbinds) thy; + (deflation_take_thms ~~ dbinds) thy (* define finiteness predicates *) fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy = let - val finite_type = lhsT --> boolT; - val finite_bind = Binding.suffix_name "_finite" dbind; + val finite_type = lhsT --> boolT + val finite_bind = Binding.suffix_name "_finite" dbind val (finite_const, thy) = - Sign.declare_const ((finite_bind, finite_type), NoSyn) thy; - val x = Free ("x", lhsT); - val n = Free ("n", natT); + Sign.declare_const ((finite_bind, finite_type), NoSyn) thy + val x = Free ("x", lhsT) + val n = Free ("n", natT) val finite_rhs = lambda x (HOLogic.exists_const natT $ - (lambda n (mk_eq (mk_capply (take_const $ n, x), x)))); - val finite_eqn = Logic.mk_equals (finite_const, finite_rhs); + (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; + 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; + |>> ListPair.unzip val result = { @@ -431,11 +431,11 @@ take_strict_thms = take_strict_thms, finite_consts = finite_consts, finite_defs = finite_defs - }; + } in (result, thy) - end; + end fun prove_finite_take_induct (spec : (binding * iso_info) list) @@ -443,72 +443,72 @@ (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 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; + @{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}); + 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; - 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; + Const (@{const_name decisive}, fastype_of t --> boolT) $ t + 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}; + @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map} val tac = EVERY [ rtac @{thm nat.induct} 1, simp_tac (HOL_ss addsimps rules0) 1, - asm_simp_tac (HOL_ss addsimps rules1) 1]; - in Goal.prove_global thy [] [] goal (K tac) end; + asm_simp_tac (HOL_ss addsimps rules1) 1] + in Goal.prove_global thy [] [] goal (K tac) 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; + 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)); + val goal = mk_trp (finite_const $ Free ("x", absT)) val tac = EVERY [ rewrite_goals_tac finite_defs, rtac @{thm lub_ID_finite} 1, resolve_tac chain_take_thms 1, resolve_tac lub_take_thms 1, - resolve_tac decisive_thms 1]; + resolve_tac decisive_thms 1] in Goal.prove_global thy [] [] goal (K tac) - end; + end val finite_thms = - map prove_finite_thm (absTs ~~ finite_consts); + 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]); + (@{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); + (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); + (dbinds ~~ take_induct_thms) in ((finite_thms, take_induct_thms), thy) - end; + end fun add_lub_take_theorems (spec : (binding * iso_info) list) @@ -518,57 +518,57 @@ 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 {take_consts, take_0_thms, take_Suc_thms, ...} = take_info; - val {chain_take_thms, deflation_take_thms, ...} = take_info; + val dbinds = map fst spec + val iso_infos = map snd spec + val absTs = map #absT iso_infos + val repTs = map #repT iso_infos + val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info + val {chain_take_thms, deflation_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]); + (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]) in add_qualified_thm "take_lemma" (dbind, take_lemma) thy - end; + end val (take_lemma_thms, thy) = fold_map prove_take_lemma - (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy; + (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.zero_var_indexes - (@{thm lub_ID_reach} OF [chain_take, lub_take]); + (@{thm lub_ID_reach} OF [chain_take, lub_take]) in add_qualified_thm "reach" (dbind, thm) thy - end; + end val (reach_thms, thy) = fold_map prove_reach_lemma - (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy; + (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy (* test for finiteness of domain definitions *) local - val types = [@{type_name ssum}, @{type_name sprod}]; + 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; + let val d' = d andalso member (op =) types c in forall (finite d') Ts end - | finite' d _ = true; + | finite' d _ = true in - val is_finite = forall (finite true) repTs; - end; + val is_finite = forall (finite true) repTs + end val ((finite_thms, 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; + prove_finite_take_induct spec take_info lub_take_thms thy in ((SOME finites, take_inducts), thy) end @@ -576,14 +576,14 @@ let fun prove_take_induct (chain_take, lub_take) = Drule.zero_var_indexes - (@{thm lub_ID_take_induct} OF [chain_take, lub_take]); + (@{thm lub_ID_take_induct} OF [chain_take, lub_take]) val take_inducts = - map prove_take_induct (chain_take_thms ~~ lub_take_thms); + map prove_take_induct (chain_take_thms ~~ lub_take_thms) val thy = fold (snd oo add_qualified_thm "take_induct") - (dbinds ~~ take_inducts) thy; + (dbinds ~~ take_inducts) thy in ((NONE, take_inducts), thy) - end; + end val result = { @@ -601,9 +601,9 @@ take_lemma_thms = take_lemma_thms, is_finite = is_finite, take_induct_thms = take_induct_thms - }; + } in (result, thy) - end; + end -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Tue Nov 30 14:21:57 2010 -0800 @@ -9,7 +9,7 @@ sig val add_consts: (binding * typ * mixfix) list -> theory -> theory val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory -end; +end structure Cont_Consts: CONT_CONSTS = struct @@ -19,12 +19,12 @@ fun change_arrow 0 T = 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], []); + | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) fun trans_rules name2 name1 n mx = let - val vnames = Name.invents Name.context "a" n; - val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); + val vnames = Name.invents Name.context "a" n + val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1) in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), @@ -35,7 +35,7 @@ | Infixl _ => [extra_parse_rule] | Infixr _ => [extra_parse_rule] | _ => []) - end; + end (* transforming infix/mixfix declarations of constants with type ...->... @@ -46,26 +46,26 @@ *) fun transform thy (c, T, mx) = let - fun syntax b = Syntax.mark_const (Sign.full_bname thy b); - val c1 = Binding.name_of c; - val c2 = c1 ^ "_cont_syntax"; - val n = Syntax.mixfix_args mx; + fun syntax b = Syntax.mark_const (Sign.full_bname thy b) + val c1 = Binding.name_of c + val c2 = c1 ^ "_cont_syntax" + val n = Syntax.mixfix_args mx in ((c, T, NoSyn), (Binding.name c2, change_arrow n T, mx), trans_rules (syntax c2) (syntax c1) n mx) - end; + end fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0 - | cfun_arity _ = 0; + | cfun_arity _ = 0 fun is_contconst (_, _, NoSyn) = false | is_contconst (_, _, Binder _) = false (* FIXME ? *) | is_contconst (c, T, mx) = let val n = Syntax.mixfix_args mx handle ERROR msg => - cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c)); - in cfun_arity T >= n end; + cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c)) + in cfun_arity T >= n end (* add_consts *) @@ -74,20 +74,20 @@ 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; + 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_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) |> Sign.add_trrules_i (maps #3 transformed_decls) - end; + end in -val add_consts = gen_add_consts Sign.certify_typ; -val add_consts_cmd = gen_add_consts Syntax.read_typ_global; +val add_consts = gen_add_consts Sign.certify_typ +val add_consts_cmd = gen_add_consts Syntax.read_typ_global -end; +end -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/cont_proc.ML --- a/src/HOL/HOLCF/Tools/cont_proc.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML Tue Nov 30 14:21:57 2010 -0800 @@ -10,21 +10,21 @@ val cont_tac: int -> tactic val cont_proc: theory -> simproc val setup: theory -> theory -end; +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}; +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 contains no dangling bound variables *) -fun is_closed_term t = not (Term.loose_bvar (t, 0)); +fun is_closed_term t = not (Term.loose_bvar (t, 0)) (* checks whether a term is written entirely in the LCF sublanguage *) fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) = @@ -34,7 +34,7 @@ | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) = is_lcf_term (Term.incr_boundvars 1 t $ Bound 0) | is_lcf_term (Bound _) = true - | is_lcf_term t = is_closed_term t; + | is_lcf_term t = is_closed_term t (* efficiently generates a cont thm for every LAM abstraction in a term, @@ -42,13 +42,13 @@ *) local fun var 0 = [SOME cont_I] - | var n = NONE :: var (n-1); + | var n = NONE :: var (n-1) fun k NONE = cont_K - | k (SOME x) = x; + | k (SOME x) = x fun ap NONE NONE = NONE - | ap x y = SOME (k y RS (k x RS cont_A)); + | ap x y = SOME (k y RS (k x RS cont_A)) fun zip [] [] = [] | zip [] (y::ys) = (ap NONE y ) :: zip [] ys @@ -60,36 +60,36 @@ 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 (k x); - val Lx = x' RS cont_L; - in (map (fn y => SOME (k y RS Lx)) ys, x') end; + val x' = Thm.close_derivation (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) = let - val (cs1,ls1) = cont_thms1 b f; - val (cs2,ls2) = cont_thms1 b t; + 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)) = let - val (cs, ls) = cont_thms1 b t; - val (cs', l) = lam cs; + 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) = let - val t' = Term.incr_boundvars 1 t $ Bound 0; - val (cs, ls) = cont_thms1 b t'; - val (cs', l) = lam cs; + 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 _ _ = ([], []); + | 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; + 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 @@ -100,37 +100,37 @@ val cont_tac = let - val rules = [cont_K, cont_I, cont_R, cont_A, cont_L]; + 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::cs) => rtac c i; + | (c::cs) => rtac c i fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) = let - val f' = Const (@{const_name Abs_cfun}, dummyT) $ f; + val f' = Const (@{const_name Abs_cfun}, dummyT) $ f in if is_lcf_term f' then new_cont_tac f' else REPEAT_ALL_NEW (resolve_tac rules) end - | cont_tac_of_term _ = K no_tac; + | cont_tac_of_term _ = K no_tac in SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i) - end; + end local fun solve_cont thy _ t = let - val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI; + val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI in Option.map fst (Seq.pull (cont_tac 1 tr)) end in fun cont_proc thy = - Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont; -end; + Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont +end -fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy; +fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Tue Nov 30 14:21:57 2010 -0800 @@ -36,7 +36,7 @@ val pcpodef_proof_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> theory -> Proof.state -end; +end structure Cpodef :> CPODEF = struct @@ -53,22 +53,22 @@ (* building terms *) -fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT); -fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); +fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT) +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 (@{const_name below}, T --> T --> HOLogic.boolT) (* manipulating theorems *) fun fold_adm_mem thm NONE = thm | fold_adm_mem thm (SOME set_def) = let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp} - in rule OF [set_def, thm] end; + in rule OF [set_def, thm] end fun fold_UU_mem thm NONE = thm | fold_UU_mem thm (SOME set_def) = let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp} - in rule OF [set_def, thm] end; + in rule OF [set_def, thm] end (* proving class instances *) @@ -83,20 +83,20 @@ (thy: theory) = let - val admissible' = fold_adm_mem admissible set_def; - 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; - val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1; - val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy; + val admissible' = fold_adm_mem admissible set_def + 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 + val tac = Tactic.rtac (@{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 is_lub = make @{thm typedef_is_lub}; - val lub = make @{thm typedef_lub}; - val compact = make @{thm typedef_compact}; + 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 is_lub = make @{thm typedef_is_lub} + val lub = make @{thm typedef_lub} + val compact = make @{thm typedef_compact} val (_, thy) = thy |> Sign.add_path (Binding.name_of name) @@ -107,13 +107,13 @@ ((Binding.prefix_name "is_lub_" name, is_lub ), []), ((Binding.prefix_name "lub_" name, lub ), []), ((Binding.prefix_name "compact_" name, compact ), [])]) - ||> Sign.parent_path; + ||> Sign.parent_path val cpo_info : cpo_info = { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, - cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact }; + cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact } in (cpo_info, thy) - end; + end fun prove_pcpo (name: binding) @@ -126,20 +126,20 @@ (thy: theory) = let - val UU_mem' = fold_UU_mem UU_mem set_def; - val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem']; - val (full_tname, Ts) = dest_Type newT; - val lhs_sorts = map (snd o dest_TFree) Ts; - val tac = Tactic.rtac (@{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 Rep_defined = make @{thm typedef_Rep_defined}; - val Abs_defined = make @{thm typedef_Abs_defined}; + val UU_mem' = fold_UU_mem UU_mem set_def + val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'] + val (full_tname, Ts) = dest_Type newT + val lhs_sorts = map (snd o dest_TFree) Ts + val tac = Tactic.rtac (@{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 Rep_defined = make @{thm typedef_Rep_defined} + val Abs_defined = make @{thm typedef_Abs_defined} val (_, thy) = thy |> Sign.add_path (Binding.name_of name) @@ -150,70 +150,70 @@ ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []), ((Binding.suffix_name "_defined" Rep_name, Rep_defined), []), ((Binding.suffix_name "_defined" Abs_name, Abs_defined), [])]) - ||> Sign.parent_path; + ||> 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, - Rep_defined = Rep_defined, Abs_defined = Abs_defined }; + Rep_defined = Rep_defined, Abs_defined = Abs_defined } in (pcpo_info, thy) - end; + end (* prepare_cpodef *) fun declare_type_name a = - Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); + Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))) fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy = let - val _ = Theory.requires thy "Cpodef" "cpodefs"; + val _ = Theory.requires thy "Cpodef" "cpodefs" (*rhs*) val tmp_ctxt = ProofContext.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; + |> 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 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)); + error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT)) (*lhs*) - val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args; - val full_tname = Sign.full_name thy tname; - val newT = Type (full_tname, map TFree lhs_tfrees); + val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args + val full_tname = Sign.full_name thy tname + val newT = Type (full_tname, map TFree lhs_tfrees) val morphs = opt_morphs - |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); + |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) in (newT, oldT, set, morphs) end fun add_podef def opt_name typ set opt_morphs tac thy = let - val name = the_default (#1 typ) opt_name; + val name = the_default (#1 typ) opt_name val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy - |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac; - val oldT = #rep_type (#1 info); - val newT = #abs_type (#1 info); - val lhs_tfrees = map dest_TFree (snd (dest_Type newT)); + |> Typedef.add_typedef_global def opt_name typ set opt_morphs 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 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)))); + Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))) val lthy3 = thy2 - |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po}); + |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po}) val ((_, (_, below_ldef)), lthy4) = lthy3 |> Specification.definition (NONE, - ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn)); - val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4); - val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef; + ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn)) + val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4) + val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef val thy5 = lthy4 |> Class.prove_instantiation_instance (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) - |> Local_Theory.exit_global; - in ((info, below_def), thy5) end; + |> Local_Theory.exit_global + in ((info, below_def), thy5) end fun prepare_cpodef (prep_term: Proof.context -> 'a -> term) @@ -226,27 +226,27 @@ : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = let val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = - prepare prep_term name typ raw_set opt_morphs thy; + prepare prep_term name typ raw_set opt_morphs thy val goal_nonempty = - HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); + 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))); + 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, set_def, ...}), below_def), thy2) = thy - |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1); + |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1) val (cpo_info, thy3) = thy2 - |> prove_cpo name newT morphs type_definition set_def below_def admissible; + |> prove_cpo name newT morphs type_definition set_def below_def admissible in ((info, cpo_info), thy3) - end; + end in (goal_nonempty, goal_admissible, cpodef_result) end handle ERROR msg => - cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name)); + cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name)) fun prepare_pcpodef (prep_term: Proof.context -> 'a -> term) @@ -259,60 +259,60 @@ : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = let val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = - prepare prep_term name typ raw_set opt_morphs thy; + prepare prep_term name typ raw_set opt_morphs thy val goal_UU_mem = - HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)); + HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)) val goal_admissible = - HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); + HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) fun pcpodef_result UU_mem admissible thy = let - val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1; + val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1 val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy - |> add_podef def (SOME name) typ set opt_morphs tac; + |> add_podef def (SOME name) typ set opt_morphs tac val (cpo_info, thy3) = thy2 - |> prove_cpo name newT morphs type_definition set_def below_def admissible; + |> prove_cpo name newT morphs type_definition set_def below_def admissible val (pcpo_info, thy4) = thy3 - |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem; + |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem in ((info, cpo_info, pcpo_info), thy4) - end; + end in (goal_UU_mem, goal_admissible, pcpodef_result) end handle ERROR msg => - cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name)); + cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name)) (* tactic interface *) fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy = let - val name = the_default (#1 typ) opt_name; + val name = the_default (#1 typ) opt_name val (goal1, goal2, cpodef_result) = - prepare_cpodef Syntax.check_term def name typ set opt_morphs thy; + prepare_cpodef Syntax.check_term def name typ set opt_morphs thy val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) handle ERROR msg => cat_error msg - ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); + ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) 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; + ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) + in cpodef_result thm1 thm2 thy end fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy = let - val name = the_default (#1 typ) opt_name; + val name = the_default (#1 typ) opt_name val (goal1, goal2, pcpodef_result) = - prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy; + prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) handle ERROR msg => cat_error msg - ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); + ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) 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; + ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) + in pcpodef_result thm1 thm2 thy end (* proof interface *) @@ -322,34 +322,34 @@ fun gen_cpodef_proof prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) thy = let - val ctxt = ProofContext.init_global thy; - val args = map (apsnd (prep_constraint ctxt)) raw_args; + val ctxt = ProofContext.init_global thy + val args = map (apsnd (prep_constraint ctxt)) raw_args val (goal1, goal2, make_result) = - prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy; + prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) - | after_qed _ = raise Fail "cpodef_proof"; - in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end; + | after_qed _ = raise Fail "cpodef_proof" + in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end fun gen_pcpodef_proof prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) thy = let - val ctxt = ProofContext.init_global thy; - val args = map (apsnd (prep_constraint ctxt)) raw_args; + val ctxt = ProofContext.init_global thy + val args = map (apsnd (prep_constraint ctxt)) raw_args val (goal1, goal2, make_result) = - prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy; + prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) - | after_qed _ = raise Fail "pcpodef_proof"; - in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end; + | 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 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; +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; +end @@ -362,22 +362,22 @@ --| Parse.$$$ ")") (true, NONE) -- (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) -- - Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)); + Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)) fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) = (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) - ((def, the_default t opt_name), (t, args, mx), A, morphs); + ((def, the_default t opt_name), (t, args, mx), A, morphs) val _ = Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" Keyword.thy_goal (typedef_proof_decl >> - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))); + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))) val _ = Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" Keyword.thy_goal (typedef_proof_decl >> - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))); + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))) -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Tue Nov 30 14:21:57 2010 -0800 @@ -23,15 +23,15 @@ val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> theory -> theory -end; +end structure Domaindef :> DOMAINDEF = struct -open HOLCF_Library; +open HOLCF_Library -infixr 6 ->>; -infix -->>; +infixr 6 ->> +infix -->> (** type definitions **) @@ -44,39 +44,39 @@ liftprj_def : thm, liftdefl_def : thm, DEFL : thm - }; + } (* building types and terms *) -val udomT = @{typ udom}; -val deflT = @{typ 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 ->> udomT); -fun liftprj_const T = Const (@{const_name liftprj}, udomT ->> mk_upT T); -fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> deflT); +val udomT = @{typ udom} +val deflT = @{typ 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 ->> udomT) +fun liftprj_const T = Const (@{const_name liftprj}, udomT ->> mk_upT T) +fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> deflT) 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 (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) in mk_capply (u_map_const, t) - end; + end fun mk_cast (t, x) = capply_const (udomT, udomT) $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t) - $ x; + $ x (* manipulating theorems *) (* proving class instances *) fun declare_type_name a = - Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); + Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))) fun gen_add_domaindef (prep_term: Proof.context -> 'a -> term) @@ -88,130 +88,130 @@ (thy: theory) : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory = let - val _ = Theory.requires thy "Domain" "domaindefs"; + val _ = Theory.requires thy "Domain" "domaindefs" (*rhs*) val tmp_ctxt = ProofContext.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; + |> 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 deflT = Term.fastype_of defl val _ = if deflT = @{typ "defl"} then () - else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT)); + else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT)) (*lhs*) - val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args; - val lhs_sorts = map snd lhs_tfrees; - val full_tname = Sign.full_name thy tname; - val newT = Type (full_tname, map TFree lhs_tfrees); + val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args + val lhs_sorts = map snd lhs_tfrees + val full_tname = Sign.full_name thy tname + val newT = Type (full_tname, map TFree lhs_tfrees) (*morphisms*) val morphs = opt_morphs - |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); + |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) (*set*) - val set = @{const defl_set} $ defl; + val set = @{const defl_set} $ defl (*pcpodef*) - val tac1 = rtac @{thm defl_set_bottom} 1; - val tac2 = rtac @{thm adm_defl_set} 1; + val tac1 = rtac @{thm defl_set_bottom} 1 + val tac2 = rtac @{thm adm_defl_set} 1 val ((info, cpo_info, pcpo_info), thy) = thy - |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); + |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (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 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))); + 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)); + Abs ("x", Term.itselfT newT, defl)) val liftemb_eqn = Logic.mk_equals (liftemb_const newT, - mk_cfcomp (@{term "udom_emb u_approx"}, mk_u_map (emb_const newT))); + mk_cfcomp (@{term "udom_emb u_approx"}, mk_u_map (emb_const newT))) val liftprj_eqn = Logic.mk_equals (liftprj_const newT, - mk_cfcomp (mk_u_map (prj_const newT), @{term "udom_prj u_approx"})); + mk_cfcomp (mk_u_map (prj_const newT), @{term "udom_prj u_approx"})) val liftdefl_eqn = Logic.mk_equals (liftdefl_const newT, Abs ("t", Term.itselfT newT, - mk_capply (@{const u_defl}, defl_const newT $ Logic.mk_type newT))); + mk_capply (@{const u_defl}, defl_const newT $ Logic.mk_type newT))) - val name_def = Binding.suffix_name "_def" name; - 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, []); + val name_def = Binding.suffix_name "_def" name + 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 liftdomain}); + |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain}) val ((_, (_, emb_ldef)), lthy) = - Specification.definition (NONE, (emb_bind, emb_eqn)) lthy; + Specification.definition (NONE, (emb_bind, emb_eqn)) lthy val ((_, (_, prj_ldef)), lthy) = - Specification.definition (NONE, (prj_bind, prj_eqn)) lthy; + Specification.definition (NONE, (prj_bind, prj_eqn)) lthy val ((_, (_, defl_ldef)), lthy) = - Specification.definition (NONE, (defl_bind, defl_eqn)) lthy; + Specification.definition (NONE, (defl_bind, defl_eqn)) lthy val ((_, (_, liftemb_ldef)), lthy) = - Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy; + Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy val ((_, (_, liftprj_ldef)), lthy) = - Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy; + Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy val ((_, (_, liftdefl_ldef)), lthy) = - Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy; - val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); - val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef; - val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef; - val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef; - val liftemb_def = singleton (ProofContext.export lthy ctxt_thy) liftemb_ldef; - val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef; - val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef; + Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy + val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy) + val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef + val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef + val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef + val liftemb_def = singleton (ProofContext.export lthy ctxt_thy) liftemb_ldef + val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef + val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef val type_definition_thm = MetaSimplifier.rewrite_rule (the_list (#set_def (#2 info))) - (#type_definition (#2 info)); + (#type_definition (#2 info)) val typedef_thms = [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def, - liftemb_def, liftprj_def, liftdefl_def]; + liftemb_def, liftprj_def, liftdefl_def] val thy = lthy |> Class.prove_instantiation_instance (K (Tactic.rtac (@{thm typedef_liftdomain_class} OF typedef_thms) 1)) - |> Local_Theory.exit_global; + |> Local_Theory.exit_global (*other theorems*) - val defl_thm' = Thm.transfer thy defl_def; + val defl_thm' = Thm.transfer thy defl_def val (DEFL_thm, thy) = thy |> Sign.add_path (Binding.name_of name) |> Global_Theory.add_thm ((Binding.prefix_name "DEFL_" name, Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), []) - ||> Sign.restore_naming thy; + ||> 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 }; + 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 " ^ quote (Binding.str_of name)); + cat_error msg ("The error(s) above occurred in domaindef " ^ quote (Binding.str_of name)) fun add_domaindef def opt_name typ defl opt_morphs thy = let - val name = the_default (#1 typ) opt_name; + val name = the_default (#1 typ) opt_name in gen_add_domaindef Syntax.check_term def name typ defl opt_morphs thy - end; + end fun domaindef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy = let - val ctxt = ProofContext.init_global thy; - val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args; - in snd (gen_add_domaindef Syntax.read_term def name (b, args, mx) A morphs thy) end; + val ctxt = ProofContext.init_global thy + val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args + in snd (gen_add_domaindef Syntax.read_term def name (b, args, mx) A morphs thy) end (** outer syntax **) @@ -223,14 +223,14 @@ --| Parse.$$$ ")") (true, NONE) -- (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) -- - Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)); + Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)) fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) = - domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs); + domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) val _ = Outer_Syntax.command "domaindef" "HOLCF definition of domains from deflations" Keyword.thy_decl (domaindef_decl >> - (Toplevel.print oo (Toplevel.theory o mk_domaindef))); + (Toplevel.print oo (Toplevel.theory o mk_domaindef))) -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Tue Nov 30 14:21:57 2010 -0800 @@ -13,23 +13,23 @@ val add_matchers: (string * string) list -> theory -> theory val fixrec_simp_tac: Proof.context -> int -> tactic val setup: theory -> theory -end; +end structure Fixrec :> FIXREC = struct -open HOLCF_Library; +open HOLCF_Library -infixr 6 ->>; -infix -->>; -infix 9 `; +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}; +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); +fun fixrec_err s = error ("fixrec definition error:\n" ^ s) fun fixrec_eq_err thy s eq = - fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)); + fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)) (*************************************************************************) (***************************** building types ****************************) @@ -39,19 +39,19 @@ 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 - | binder_cfun _ = []; + | binder_cfun _ = [] fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U - | body_cfun T = T; + | body_cfun T = T fun strip_cfun T : typ list * typ = - (binder_cfun T, body_cfun T); + (binder_cfun T, body_cfun T) in fun matcherT (T, U) = - body_cfun T ->> (binder_cfun T -->> U) ->> U; + body_cfun T ->> (binder_cfun T -->> U) ->> U end @@ -59,21 +59,21 @@ (***************************** building terms ****************************) (*************************************************************************) -val mk_trp = HOLogic.mk_Trueprop; +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); +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$t) = chead_of f - | chead_of u = u; + | chead_of u = u -infix 0 ==; val (op ==) = Logic.mk_equals; -infix 1 ===; val (op ===) = HOLogic.mk_eq; +infix 0 == val (op ==) = Logic.mk_equals +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; + in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end fun mk_run t = let @@ -85,7 +85,7 @@ Const(@{const_name Rep_cfun}, _) $ Const(@{const_name Fixrec.succeed}, _) $ u => u | _ => run ` t - end; + end (*************************************************************************) @@ -94,26 +94,26 @@ 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; -); + 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, T)) = n | name_of (Free (n, T)) = n - | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t]); + | 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 prop_of; + name_of o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of in val add_unfold : attribute = Thm.declaration_attribute - (fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th))); + (fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th))) end @@ -122,73 +122,73 @@ (spec : (Attrib.binding * term) list) (lthy : local_theory) = let - val thy = ProofContext.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 thy = ProofContext.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); + val prop = mk_trp (mk_cont functional) fun err _ = error ( - "Continuity proof failed; please check that cont2cont rules\n" ^ + "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 = Cont2ContData.get lthy; - val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules)); - val slow_tac = SOLVED' (simp_tac (simpset_of lthy)); - val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err; + Syntax.string_of_term lthy prop) + val rules = Cont2ContData.get lthy + val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules)) + val slow_tac = SOLVED' (simp_tac (simpset_of lthy)) + val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err in Goal.prove lthy [] [] prop (K tac) - end; + end fun one_def (l as Free(n,_)) r = let val b = Long_Name.base_name n in ((Binding.name (b^"_def"), []), r) end - | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; + | 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; + | 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 predicate = lambda_tuple lhss (list_comb (P, lhss)); + |> 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 predicate = lambda_tuple lhss (list_comb (P, lhss)) val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm]) |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)] - |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}; + |> 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}; + |> Local_Defs.unfold lthy @{thms split_conv} fun unfolds [] thm = [] | 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 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"); + val thm_name = Binding.qualify true all_names (Binding.name "induct") in ((thm_name, []), [tuple_induct_thm]) - end; + 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); + val thm_name = Binding.qualify true name (Binding.name "unfold") + val src = Attrib.internal (K add_unfold) in ((thm_name, [src]), [thm]) - end; + end val (thmss, lthy) = lthy - |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms); + |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms) in (lthy, names, fixdef_thms, map snd unfold_thms) - end; + end (*************************************************************************) (*********** monadic notation and pattern matching compilation ***********) @@ -196,14 +196,14 @@ structure FixrecMatchData = Theory_Data ( - type T = string Symtab.table; - val empty = Symtab.empty; - val extend = I; - fun merge data = Symtab.merge (K true) 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 add_matchers ms = FixrecMatchData.map (fold Symtab.update ms) fun taken_names (t : term) : bstring list = let @@ -211,10 +211,10 @@ | 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; + | taken (_ , bs) = bs in taken (t, []) - end; + end (* builds a monadic term for matching a pattern *) (* returns (rhs, free variable, used varnames) *) @@ -244,87 +244,87 @@ | _ => raise TERM ("fixrec: invalid pattern ", [p]) in comp_pat pat rhs taken - end; + 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 => - let val (rhs', v, taken') = compile_pat match_name x rhs taken; + 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); + ^ ML_Syntax.print_term pat) fun strip_alls t = - if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t; + if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t fun compile_eq match_name eq = let - val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq)); + 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; + 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); + ListPair.unzip (map (compile_eq match_name) eqs) val const = case distinct (op =) consts of [n] => n - | _ => fixrec_err "all equations in block must define the same function"; + | _ => fixrec_err "all equations in block must define the same function" val vars = case distinct (op = o pairself length) (map fst matchers) of [vars] => vars - | _ => fixrec_err "all equations in block must have the same arity"; + | _ => 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))); + 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; + end (*************************************************************************) (********************** Proving associated theorems **********************) (*************************************************************************) -fun eta_tac i = CONVERSION Thm.eta_conversion i; +fun eta_tac i = CONVERSION Thm.eta_conversion i fun fixrec_simp_tac ctxt = let - val tab = FixrecUnfoldData.get (Context.Proof ctxt); - val ss = Simplifier.simpset_of ctxt; + val tab = FixrecUnfoldData.get (Context.Proof ctxt) + val ss = Simplifier.simpset_of ctxt fun concl t = if Logic.is_all t then concl (snd (Logic.dest_all t)) - else HOLogic.dest_Trueprop (Logic.strip_imp_concl t); + else HOLogic.dest_Trueprop (Logic.strip_imp_concl t) fun tac (t, i) = let val (c, T) = - (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}; + (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 (rtac rule i THEN eta_tac i THEN asm_simp_tac ss i) end in SUBGOAL (fn ti => the_default no_tac (try tac ti)) - end; + 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 ss = Simplifier.simpset_of ctxt; - val rule = unfold_thm RS @{thm ssubst_lhs}; - val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ss 1; - fun prove_term t = Goal.prove ctxt [] [] t (K tac); - fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t); + val ss = Simplifier.simpset_of ctxt + val rule = unfold_thm RS @{thm ssubst_lhs} + val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ss 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; + end (*************************************************************************) (************************* Main fixrec function **************************) @@ -339,54 +339,54 @@ (raw_spec' : (bool * (Attrib.binding * 'b)) list) (lthy : local_theory) = let - val (skips, raw_spec) = ListPair.unzip raw_spec'; + val (skips, raw_spec) = ListPair.unzip raw_spec' val (fixes : ((binding * typ) * mixfix) list, spec : (Attrib.binding * term) list) = - fst (prep_spec raw_fixes raw_spec lthy); + fst (prep_spec raw_fixes raw_spec lthy) val chead_of_spec = - chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd; + chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd fun name_of (Free (n, _)) = n - | name_of t = fixrec_err ("unknown term"); - val all_names = map (name_of o chead_of_spec) spec; - val names = distinct (op =) all_names; + | name_of t = fixrec_err ("unknown term") + val all_names = map (name_of o chead_of_spec) spec + val names = distinct (op =) all_names 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; + (all_names ~~ (spec ~~ skips)) + val blocks = map block_of_name names - val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy); + val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy) fun match_name c = case Symtab.lookup matcher_tab c of SOME m => m - | NONE => fixrec_err ("unknown pattern constructor: " ^ c); + | NONE => fixrec_err ("unknown pattern constructor: " ^ c) - val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks); - val spec' = map (pair Attrib.empty_binding) matches; + val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks) + val spec' = map (pair Attrib.empty_binding) matches val (lthy, cnames, fixdef_thms, unfold_thms) = - add_fixdefs fixes spec' lthy; + add_fixdefs fixes spec' lthy - val blocks' = map (map fst o filter_out snd) blocks; + val blocks' = map (map fst o filter_out snd) blocks val simps : (Attrib.binding * thm) list list = - map (make_simps lthy) (unfold_thms ~~ blocks'); + map (make_simps lthy) (unfold_thms ~~ blocks') fun mk_bind n : Attrib.binding = (Binding.qualify true n (Binding.name "simps"), - [Attrib.internal (K Simplifier.simp_add)]); + [Attrib.internal (K Simplifier.simp_add)]) val simps1 : (Attrib.binding * thm list) list = - map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps); + 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); + map (apsnd (fn thm => [thm])) (flat simps) val (_, lthy) = lthy - |> fold_map Local_Theory.note (simps1 @ simps2); + |> fold_map Local_Theory.note (simps1 @ simps2) in lthy - end; + end in -val add_fixrec = gen_fixrec Specification.check_spec; -val add_fixrec_cmd = gen_fixrec Specification.read_spec; +val add_fixrec = gen_fixrec Specification.check_spec +val add_fixrec_cmd = gen_fixrec Specification.read_spec -end; (* local *) +end (* local *) (*************************************************************************) @@ -395,23 +395,23 @@ val opt_thm_name' : (bool * Attrib.binding) parser = Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding) - || Parse_Spec.opt_thm_name ":" >> pair false; + || 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))); + opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c))) val alt_specs' : (bool * (Attrib.binding * string)) list parser = - let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "("); - in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end; + let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(") + in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end val _ = Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs') - >> (fn (fixes, specs) => add_fixrec_cmd fixes specs)); + >> (fn (fixes, specs) => add_fixrec_cmd fixes specs)) val setup = Method.setup @{binding fixrec_simp} (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac)) - "pattern prover for fixrec constants"; + "pattern prover for fixrec constants" -end; +end diff -r 10aeee1d5b71 -r 4352ca878c41 src/HOL/HOLCF/Tools/holcf_library.ML --- a/src/HOL/HOLCF/Tools/holcf_library.ML Tue Nov 30 14:01:49 2010 -0800 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML Tue Nov 30 14:21:57 2010 -0800 @@ -7,79 +7,79 @@ structure HOLCF_Library = struct -infixr 6 ->>; -infixr -->>; -infix 9 `; +infixr 6 ->> +infixr -->> +infix 9 ` (*** Operations from Isabelle/HOL ***) -val boolT = HOLogic.boolT; -val natT = HOLogic.natT; +val boolT = HOLogic.boolT +val natT = HOLogic.natT -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; +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; +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 UU}, T); +fun mk_bottom T = Const (@{const_name UU}, T) -fun below_const T = Const (@{const_name below}, [T, T] ---> boolT); -fun mk_below (t, u) = below_const (fastype_of t) $ t $ u; +fun below_const T = Const (@{const_name below}, [T, T] ---> boolT) +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_undef t = mk_eq (t, mk_bottom (fastype_of t)) -fun mk_defined t = mk_not (mk_undef t); +fun mk_defined t = mk_not (mk_undef t) fun mk_adm t = - Const (@{const_name adm}, fastype_of t --> boolT) $ t; + Const (@{const_name adm}, fastype_of t --> boolT) $ t fun mk_compact t = - Const (@{const_name compact}, fastype_of t --> boolT) $ t; + Const (@{const_name compact}, fastype_of t --> boolT) $ t fun mk_cont t = - Const (@{const_name cont}, fastype_of t --> boolT) $ t; + Const (@{const_name cont}, fastype_of t --> boolT) $ t fun mk_chain t = - Const (@{const_name chain}, Term.fastype_of t --> boolT) $ t; + Const (@{const_name chain}, Term.fastype_of t --> boolT) $ t fun mk_lub t = let - val T = Term.range_type (Term.fastype_of t); - val lub_const = Const (@{const_name lub}, (T --> boolT) --> T); - val UNIV_const = @{term "UNIV :: nat set"}; - val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT; - val image_const = Const (@{const_name image}, image_type); + val T = Term.range_type (Term.fastype_of t) + val lub_const = Const (@{const_name lub}, (T --> boolT) --> T) + val UNIV_const = @{term "UNIV :: nat set"} + val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT + val image_const = Const (@{const_name image}, image_type) in lub_const $ (image_const $ t $ UNIV_const) - end; + end (*** Continuous function space ***) -fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]); +fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]) -val (op ->>) = mk_cfunT; -val (op -->>) = Library.foldr mk_cfunT; +val (op ->>) = mk_cfunT +val (op -->>) = Library.foldr mk_cfunT fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U) - | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); + | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []) fun capply_const (S, T) = - Const(@{const_name Rep_cfun}, (S ->> T) --> (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)); + Const(@{const_name Abs_cfun}, (S --> T) --> (S ->> T)) fun mk_cabs t = let val T = fastype_of t @@ -87,48 +87,48 @@ (* builds the expression (% v1 v2 .. vn. rhs) *) fun lambdas [] rhs = rhs - | lambdas (v::vs) rhs = Term.lambda v (lambdas vs 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; + 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); + | 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) - | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); - in capply_const (S, T) $ t $ u end; + | _ => 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 (op `) = mk_capply -val list_ccomb : term * term list -> term = Library.foldl mk_capply; +val list_ccomb : term * term list -> term = Library.foldl mk_capply -fun mk_ID T = Const (@{const_name ID}, T ->> T); +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)); + Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V)) fun mk_cfcomp (f, g) = let - val (U, V) = dest_cfunT (fastype_of f); - val (T, U') = dest_cfunT (fastype_of g); + 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) else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) - end; + end -fun strictify_const T = Const (@{const_name strictify}, T ->> T); -fun mk_strictify t = strictify_const (fastype_of t) ` t; +fun strictify_const T = Const (@{const_name strictify}, T ->> T) +fun mk_strictify t = strictify_const (fastype_of t) ` t fun mk_strict t = - let val (T, U) = dest_cfunT (fastype_of t); - in mk_eq (t ` mk_bottom T, mk_bottom U) end; + let val (T, U) = dest_cfunT (fastype_of t) + in mk_eq (t ` mk_bottom T, mk_bottom U) end (*** Product type ***) @@ -137,153 +137,153 @@ fun mk_tupleT [] = HOLogic.unitT | mk_tupleT [T] = T - | mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts); + | 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); + | 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_split (Term.lambda v (lambda_tuple vs rhs)); + HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)) (*** Lifted cpo type ***) -fun mk_upT T = Type(@{type_name "u"}, [T]); +fun mk_upT T = Type(@{type_name "u"}, [T]) fun dest_upT (Type(@{type_name "u"}, [T])) = T - | dest_upT T = raise TYPE ("dest_upT", [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(@{const_name up}, T ->> mk_upT T) -fun mk_up t = up_const (fastype_of t) ` 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); + Const(@{const_name fup}, (T ->> U) ->> mk_upT T ->> U) -fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t; +fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t -fun from_up T = fup_const (T, T) ` mk_ID T; +fun from_up T = fup_const (T, T) ` mk_ID T (*** Lifted unit type ***) -val oneT = @{typ "one"}; +val oneT = @{typ "one"} -fun one_case_const T = Const (@{const_name one_case}, T ->> oneT ->> T); -fun mk_one_case t = one_case_const (fastype_of t) ` t; +fun one_case_const T = Const (@{const_name one_case}, T ->> oneT ->> 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(@{type_name sprod}, [T, U]) fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U) - | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []); + | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []) fun spair_const (T, U) = - Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U)); + Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U)) (* builds the expression (:t, u:) *) fun mk_spair (t, u) = - spair_const (fastype_of t, fastype_of u) ` 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); + | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts) fun sfst_const (T, U) = - Const(@{const_name sfst}, mk_sprodT (T, U) ->> T); + Const(@{const_name sfst}, mk_sprodT (T, U) ->> T) fun ssnd_const (T, U) = - Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U); + Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U) fun ssplit_const (T, U, V) = - Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V); + Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (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; + 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(@{type_name ssum}, [T, U]) fun dest_ssumT (Type(@{type_name ssum}, [T, U])) = (T, U) - | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []); + | 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(@{const_name sinl}, T ->> mk_ssumT (T, U)) +fun sinr_const (T, U) = Const(@{const_name sinr}, U ->> mk_ssumT (T, U)) (* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) fun mk_sinjects ts = let - val Ts = map fastype_of ts; + 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; + 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); + | inj ((t, T)::ts) = combine (t, T) (inj ts) in fst (inj (ts ~~ Ts)) - end; + end fun sscase_const (T, U, V) = Const(@{const_name sscase}, - (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V); + (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V) fun mk_sscase (t, u) = - let val (T, V) = dest_cfunT (fastype_of t); - val (U, V) = dest_cfunT (fastype_of u); - in sscase_const (T, U, V) ` t ` u end; + let val (T, V) = 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); + 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; + 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 (@{type_name "match"}, [T]) fun dest_matchT (Type(@{type_name "match"}, [T])) = T - | dest_matchT T = raise TYPE ("dest_matchT", [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 (@{const_name "Fixrec.fail"}, mk_matchT T) -fun succeed_const T = Const (@{const_name "Fixrec.succeed"}, T ->> mk_matchT T); -fun mk_succeed t = succeed_const (fastype_of t) ` t; +fun succeed_const T = Const (@{const_name "Fixrec.succeed"}, T ->> mk_matchT T) +fun mk_succeed t = succeed_const (fastype_of t) ` t (*** lifted boolean type ***) -val trT = @{typ "tr"}; +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(@{const_name fix}, (T ->> T) ->> T), t) end fun iterate_const T = - Const (@{const_name iterate}, natT --> (T ->> T) ->> (T ->> T)); + Const (@{const_name iterate}, natT --> (T ->> T) ->> (T ->> 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; + let val (T, _) = dest_cfunT (Term.fastype_of f) + in (iterate_const T $ n) ` f ` mk_bottom T end -end; +end