--- 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
--- 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 *)
--- 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
--- 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 *)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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