# HG changeset patch # User wenzelm # Date 1180612918 -7200 # Node ID 9497234a27434f890d58ba952a2a8cef08402fa0 # Parent ed3f6685ff90493e4296ddf69694c4d3724502fd moved HOLCF tools to canonical place; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Thu May 31 13:24:13 2007 +0200 +++ b/src/HOLCF/Cfun.thy Thu May 31 14:01:58 2007 +0200 @@ -9,7 +9,7 @@ theory Cfun imports Pcpodef -uses ("cont_proc.ML") +uses ("Tools/cont_proc.ML") begin defaultsort cpo @@ -325,7 +325,7 @@ lemmas cont_lemmas1 = cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM -use "cont_proc.ML"; +use "Tools/cont_proc.ML"; setup ContProc.setup; (*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Thu May 31 13:24:13 2007 +0200 +++ b/src/HOLCF/Domain.thy Thu May 31 14:01:58 2007 +0200 @@ -7,15 +7,6 @@ theory Domain imports Ssum Sprod Up One Tr Fixrec -(* -files - ("domain/library.ML") - ("domain/syntax.ML") - ("domain/axioms.ML") - ("domain/theorems.ML") - ("domain/extender.ML") - ("domain/interface.ML") -*) begin defaultsort pcpo diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Thu May 31 13:24:13 2007 +0200 +++ b/src/HOLCF/Fixrec.thy Thu May 31 14:01:58 2007 +0200 @@ -7,7 +7,7 @@ theory Fixrec imports Sprod Ssum Up One Tr Fix -uses ("fixrec_package.ML") +uses ("Tools/fixrec_package.ML") begin subsection {* Maybe monad type *} @@ -542,7 +542,7 @@ subsection {* Initializing the fixrec package *} -use "fixrec_package.ML" +use "Tools/fixrec_package.ML" hide (open) const return bind fail run diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Thu May 31 13:24:13 2007 +0200 +++ b/src/HOLCF/HOLCF.thy Thu May 31 14:01:58 2007 +0200 @@ -9,13 +9,13 @@ imports Sprod Ssum Up Lift Discrete One Tr Domain Main uses "holcf_logic.ML" - "cont_consts.ML" - "domain/library.ML" - "domain/syntax.ML" - "domain/axioms.ML" - "domain/theorems.ML" - "domain/extender.ML" - "adm_tac.ML" + "Tools/cont_consts.ML" + "Tools/domain/domain_library.ML" + "Tools/domain/domain_syntax.ML" + "Tools/domain/domain_axioms.ML" + "Tools/domain/domain_theorems.ML" + "Tools/domain/domain_extender.ML" + "Tools/adm_tac.ML" begin diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Thu May 31 13:24:13 2007 +0200 +++ b/src/HOLCF/IsaMakefile Thu May 31 14:01:58 2007 +0200 @@ -27,15 +27,15 @@ HOL: @cd $(SRC)/HOL; $(ISATOOL) make HOL -$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.thy Cont.thy \ - Cprod.thy Discrete.thy Domain.thy Fix.thy Fixrec.thy \ - Ffun.thy HOLCF.thy Lift.thy One.thy \ - Pcpo.thy Porder.thy ROOT.ML Sprod.thy \ - Ssum.thy Tr.thy Pcpodef.thy pcpodef_package.ML \ - Up.thy adm_tac.ML cont_consts.ML cont_proc.ML fixrec_package.ML \ - domain/axioms.ML domain/extender.ML domain/library.ML \ - domain/syntax.ML domain/theorems.ML holcf_logic.ML ex/Stream.thy \ - document/root.tex +$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.thy Cont.thy Cprod.thy \ + Discrete.thy Domain.thy Ffun.thy Fix.thy Fixrec.thy HOLCF.thy Lift.thy \ + One.thy Pcpo.thy Pcpodef.thy Porder.thy ROOT.ML Sprod.thy Ssum.thy \ + Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML \ + Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \ + Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \ + Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \ + Tools/pcpodef_package.ML Tr.thy Up.thy document/root.tex ex/Stream.thy \ + holcf_logic.ML @$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Pcpodef.thy --- a/src/HOLCF/Pcpodef.thy Thu May 31 13:24:13 2007 +0200 +++ b/src/HOLCF/Pcpodef.thy Thu May 31 14:01:58 2007 +0200 @@ -7,7 +7,7 @@ theory Pcpodef imports Adm -uses ("pcpodef_package.ML") +uses ("Tools/pcpodef_package.ML") begin subsection {* Proving a subtype is a partial order *} @@ -266,6 +266,6 @@ subsection {* HOLCF type definition package *} -use "pcpodef_package.ML" +use "Tools/pcpodef_package.ML" end diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/adm_tac.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/adm_tac.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,180 @@ +(* ID: $Id$ + Author: Stefan Berghofer, TU Muenchen + +Admissibility tactic. + +Checks whether adm_subst theorem is applicable to the current proof +state: + + [| cont t; adm P |] ==> adm (%x. P (t x)) + +"t" is instantiated with a term of chain-finite type, so that +adm_chfin can be applied: + + adm (P::'a::{chfin,pcpo} => bool) + +*) + +signature ADM = +sig + val adm_tac: (int -> tactic) -> int -> tactic +end; + +structure Adm: ADM = +struct + + +(*** find_subterms t 0 [] + returns lists of terms with the following properties: + 1. all terms in the list are disjoint subterms of t + 2. all terms contain the variable which is bound at level 0 + 3. all occurences of the variable which is bound at level 0 + are "covered" by a term in the list + a list of integers is associated with every term which describes + the "path" leading to the subterm (required for instantiation of + the adm_subst theorem (see functions mk_term, inst_adm_subst_thm)) +***) + +fun find_subterms (Bound i) lev path = + if i = lev then [[(Bound 0, path)]] + else [] + | find_subterms (t as (Abs (_, _, t2))) lev path = + if List.filter (fn x => x<=lev) + (add_loose_bnos (t, 0, [])) = [lev] then + [(incr_bv (~lev, 0, t), path)]:: + (find_subterms t2 (lev+1) (0::path)) + else find_subterms t2 (lev+1) (0::path) + | find_subterms (t as (t1 $ t2)) lev path = + let val ts1 = find_subterms t1 lev (0::path); + val ts2 = find_subterms t2 lev (1::path); + fun combine [] y = [] + | combine (x::xs) ys = + (map (fn z => x @ z) ys) @ (combine xs ys) + in + (if List.filter (fn x => x<=lev) + (add_loose_bnos (t, 0, [])) = [lev] then + [[(incr_bv (~lev, 0, t), path)]] + else []) @ + (if ts1 = [] then ts2 + else if ts2 = [] then ts1 + else combine ts1 ts2) + end + | find_subterms _ _ _ = []; + + +(*** make term for instantiation of predicate "P" in adm_subst theorem ***) + +fun make_term t path paths lev = + if path mem paths then Bound lev + else case t of + (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1)) + | (t1 $ t2) => (make_term t1 (0::path) paths lev) $ + (make_term t2 (1::path) paths lev) + | t1 => t1; + + +(*** check whether all terms in list are equal ***) + +fun eq_terms [] = true + | eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts; + + +(*figure out internal names*) +val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"]; +val cont_name = Sign.intern_const (the_context ()) "cont"; +val adm_name = Sign.intern_const (the_context ()) "adm"; + + +(*** check whether type of terms in list is chain finite ***) + +fun is_chfin sign T params ((t, _)::_) = + let val parTs = map snd (rev params) + in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end; + + +(*** try to prove that terms in list are continuous + if successful, add continuity theorem to list l ***) + +fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) = + let val parTs = map snd (rev params); + val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT; + fun mk_all [] t = t + | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t)); + val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t))); + val t' = mk_all params (Logic.list_implies (prems, t)); + val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1)); + in (ts, thm)::l end + handle ERROR _ => l; + + +(*** instantiation of adm_subst theorem (a bit tricky) ***) + +fun inst_adm_subst_thm state i params s T subt t paths = + let val {thy = sign, maxidx, ...} = rep_thm state; + val j = maxidx+1; + val parTs = map snd (rev params); + val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst; + val types = valOf o (fst (types_sorts rule)); + val tT = types ("t", j); + val PT = types ("P", j); + fun mk_abs [] t = t + | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t); + val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt); + val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))]) + (make_term t [] paths 0)); + val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty; + val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye; + val ctye = map (fn (ixn, (S, T)) => + (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye'); + val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT)); + val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT)); + val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule + in rule' end; + + +(*** extract subgoal i from proof state ***) + +fun nth_subgoal i thm = List.nth (prems_of thm, i-1); + + +(*** the admissibility tactic ***) + +fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) = + if name = adm_name then SOME abs else NONE + | try_dest_adm _ = NONE; + +fun adm_tac tac i state = + state |> + let val goali = nth_subgoal i state in + (case try_dest_adm (Logic.strip_assums_concl goali) of + NONE => no_tac + | SOME (s, T, t) => + let + val sign = Thm.theory_of_thm state; + val prems = Logic.strip_assums_hyp goali; + val params = Logic.strip_params goali; + val ts = find_subterms t 0 []; + val ts' = List.filter eq_terms ts; + val ts'' = List.filter (is_chfin sign T params) ts'; + val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts''); + in + (case thms of + ((ts as ((t', _)::_), cont_thm)::_) => + let + val paths = map snd ts; + val rule = inst_adm_subst_thm state i params s T t' t paths; + in + compose_tac (false, rule, 2) i THEN + rtac cont_thm i THEN + REPEAT (assume_tac i) THEN + rtac adm_chfin i + end + | [] => no_tac) + end) + end; + + +end; + + +open Adm; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/cont_consts.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/cont_consts.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,110 @@ +(* Title: HOLCF/Tools/cont_consts.ML + ID: $Id$ + Author: Tobias Mayr, David von Oheimb, and Markus Wenzel + +HOLCF version of consts: handle continuous function types in mixfix +syntax. +*) + +signature CONT_CONSTS = +sig + val add_consts: (bstring * string * mixfix) list -> theory -> theory + val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory +end; + +structure ContConsts: CONT_CONSTS = +struct + + +(* misc utils *) + +open HOLCFLogic; + +fun first (x,_,_) = x; +fun second (_,x,_) = x; +fun third (_,_,x) = x; +fun upd_first f (x,y,z) = (f x, y, z); +fun upd_second f (x,y,z) = ( x, f y, z); +fun upd_third f (x,y,z) = ( x, y, f z); + +fun change_arrow 0 T = T +| change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T]) +| change_arrow _ _ = sys_error "cont_consts: change_arrow"; + +fun trans_rules name2 name1 n mx = let + fun argnames _ 0 = [] + | argnames c n = chr c::argnames (c+1) (n-1); + val vnames = argnames (ord "A") n; + val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); + in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), + Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") + [t,Variable arg])) + (Constant name1,vnames))] + @(case mx of InfixName _ => [extra_parse_rule] + | InfixlName _ => [extra_parse_rule] + | InfixrName _ => [extra_parse_rule] | _ => []) end; + + +(* transforming infix/mixfix declarations of constants with type ...->... + a declaration of such a constant is transformed to a normal declaration with + an internal name, the same type, and nofix. Additionally, a purely syntactic + declaration with the original name, type ...=>..., and the original mixfix + is generated and connected to the other declaration via some translation. +*) +fun fix_mixfix (syn , T, mx as Infix p ) = + (Syntax.const_name syn mx, T, InfixName (syn, p)) + | fix_mixfix (syn , T, mx as Infixl p ) = + (Syntax.const_name syn mx, T, InfixlName (syn, p)) + | fix_mixfix (syn , T, mx as Infixr p ) = + (Syntax.const_name syn mx, T, InfixrName (syn, p)) + | fix_mixfix decl = decl; +fun transform decl = let + val (c, T, mx) = fix_mixfix decl; + val c2 = "_cont_" ^ c; + val n = Syntax.mixfix_args mx + in ((c , T,NoSyn), + (c2,change_arrow n T,mx ), + trans_rules c2 c n mx) end; + +fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0 +| cfun_arity _ = 0; + +fun is_contconst (_,_,NoSyn ) = false +| is_contconst (_,_,Binder _) = false +| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx + handle ERROR msg => cat_error msg ("in mixfix annotation for " ^ + quote (Syntax.const_name c mx)); + + +(* add_consts(_i) *) + +fun gen_add_consts prep_typ raw_decls thy = + let + val decls = map (upd_second (prep_typ thy)) raw_decls; + val (contconst_decls, normal_decls) = List.partition is_contconst decls; + val transformed_decls = map transform contconst_decls; + in + thy + |> Sign.add_consts_i normal_decls + |> Sign.add_consts_i (map first transformed_decls) + |> Sign.add_syntax_i (map second transformed_decls) + |> Sign.add_trrules_i (List.concat (map third transformed_decls)) + end; + +val add_consts = gen_add_consts Sign.read_typ; +val add_consts_i = gen_add_consts Sign.certify_typ; + + +(* outer syntax *) + +local structure P = OuterParse and K = OuterKeyword in + +val constsP = + OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl + (Scan.repeat1 P.const >> (Toplevel.theory o add_consts)); + +val _ = OuterSyntax.add_parsers [constsP]; + +end; + +end; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/cont_proc.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/cont_proc.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,145 @@ +(* Title: HOLCF/Tools/cont_proc.ML + ID: $Id$ + Author: Brian Huffman +*) + +signature CONT_PROC = +sig + val is_lcf_term: term -> bool + val cont_thms: term -> thm list + val all_cont_thms: term -> thm list + val cont_tac: int -> tactic + val cont_proc: theory -> simproc + val setup: theory -> theory +end; + +structure ContProc: CONT_PROC = +struct + +(** theory context references **) + +val cont_K = thm "cont_const"; +val cont_I = thm "cont_id"; +val cont_A = thm "cont2cont_Rep_CFun"; +val cont_L = thm "cont2cont_LAM"; +val cont_R = thm "cont_Rep_CFun2"; + +(* checks whether a term contains no dangling bound variables *) +val is_closed_term = + let + fun bound_less i (t $ u) = + bound_less i t andalso bound_less i u + | bound_less i (Abs (_, _, t)) = bound_less (i+1) t + | bound_less i (Bound n) = n < i + | bound_less i _ = true; (* Const, Free, and Var are OK *) + in bound_less 0 end; + +(* checks whether a term is written entirely in the LCF sublanguage *) +fun is_lcf_term (Const ("Cfun.Rep_CFun", _) $ t $ u) = + is_lcf_term t andalso is_lcf_term u + | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t + | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false + | is_lcf_term (Bound _) = true + | is_lcf_term t = is_closed_term t; + +(* + efficiently generates a cont thm for every LAM abstraction in a term, + using forward proof and reusing common subgoals +*) +local + fun var 0 = [SOME cont_I] + | var n = NONE :: var (n-1); + + fun k NONE = cont_K + | k (SOME x) = x; + + fun ap NONE NONE = NONE + | ap x y = SOME (k y RS (k x RS cont_A)); + + fun zip [] [] = [] + | zip [] (y::ys) = (ap NONE y ) :: zip [] ys + | zip (x::xs) [] = (ap x NONE) :: zip xs [] + | zip (x::xs) (y::ys) = (ap x y ) :: zip xs ys + + fun lam [] = ([], cont_K) + | lam (x::ys) = + let + (* should use "standard" for thms that are used multiple times *) + (* it seems to allow for sharing in explicit proof objects *) + val x' = standard (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 ("Cfun.Rep_CFun", _) $ f $ t) = + let + val (cs1,ls1) = cont_thms1 b f; + val (cs2,ls2) = cont_thms1 b t; + in (zip cs1 cs2, if b then ls1 @ ls2 else []) end + | cont_thms1 b (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = + let + val (cs, ls) = cont_thms1 b t; + val (cs', l) = lam cs; + in (cs', l::ls) end + | cont_thms1 _ (Bound n) = (var n, []) + | cont_thms1 _ _ = ([], []); +in + (* precondition: is_lcf_term t = true *) + fun cont_thms t = snd (cont_thms1 false t); + fun all_cont_thms t = snd (cont_thms1 true t); +end; + +(* + Given the term "cont f", the procedure tries to construct the + theorem "cont f == True". If this theorem cannot be completely + solved by the introduction rules, then the procedure returns a + conditional rewrite rule with the unsolved subgoals as premises. +*) + +local + val rules = [cont_K, cont_I, cont_R, cont_A, cont_L]; + + val prev_cont_thms : thm list ref = ref []; + + fun old_cont_tac i thm = + case !prev_cont_thms of + [] => no_tac thm + | (c::cs) => (prev_cont_thms := cs; rtac c i thm); + + fun new_cont_tac f' i thm = + case all_cont_thms f' of + [] => no_tac thm + | (c::cs) => (prev_cont_thms := cs; rtac c i thm); + + fun cont_tac_of_term (Const ("Cont.cont", _) $ f) = + let + val f' = Const ("Cfun.Abs_CFun", dummyT) $ f; + in + if is_lcf_term f' + then old_cont_tac ORELSE' new_cont_tac f' + else REPEAT_ALL_NEW (resolve_tac rules) + end + | cont_tac_of_term _ = K no_tac; +in + val cont_tac = + SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i); +end; + +local + fun solve_cont thy _ t = + let + 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 thy "cont_proc" ["cont f"] solve_cont; +end; + +val setup = + (fn thy => + (Simplifier.change_simpset_of thy + (fn ss => ss addsimprocs [cont_proc thy]); thy)); + +end; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/domain/domain_axioms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,170 @@ +(* Title: HOLCF/Tools/domain/domain_axioms.ML + ID: $Id$ + Author: David von Oheimb + +Syntax generator for domain command. +*) + +structure Domain_Axioms = struct + +local + +open Domain_Library; +infixr 0 ===>;infixr 0 ==>;infix 0 == ; +infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; +infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; + +fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)= +let + +(* ----- axioms and definitions concerning the isomorphism ------------------ *) + + val dc_abs = %%:(dname^"_abs"); + val dc_rep = %%:(dname^"_rep"); + val x_name'= "x"; + val x_name = idx_name eqs x_name' (n+1); + val dnam = Sign.base_name dname; + + val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); + val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); + + val when_def = ("when_def",%%:(dname^"_when") == + foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => + Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); + + val copy_def = let + fun idxs z x arg = if is_rec arg + then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x) + else Bound(z-x); + fun one_con (con,args) = + foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args; + in ("copy_def", %%:(dname^"_copy") == + /\"f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end; + +(* -- definitions concerning the constructors, discriminators and selectors - *) + + fun con_def m n (_,args) = let + fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I) (Bound(z-x)); + fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); + fun inj y 1 _ = y + | inj y _ 0 = %%:sinlN`y + | inj y i j = %%:sinrN`(inj y (i-1) (j-1)); + in foldr /\# (dc_abs`(inj (parms args) m n)) args end; + + val con_defs = mapn (fn n => fn (con,args) => + (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; + + val dis_defs = let + fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => (foldr /\# + (if con'=con then %%:TT_N else %%:FF_N) args)) cons)) + in map ddef cons end; + + val mat_defs = let + fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => (foldr /\# + (if con'=con + then %%:returnN`(mk_ctuple (map (bound_arg args) args)) + else %%:failN) args)) cons)) + in map mdef cons end; + + val pat_defs = + let + fun pdef (con,args) = + let + val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; + val xs = map (bound_arg args) args; + val r = Bound (length args); + val rhs = case args of [] => %%:returnN ` HOLogic.unit + | _ => foldr1 cpair_pat ps ` mk_ctuple xs; + fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args'; + in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == + list_ccomb(%%:(dname^"_when"), map one_con cons)) + end + in map pdef cons end; + + val sel_defs = let + fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => if con'<>con then UU else + foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); + in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; + + +(* ----- axiom and definitions concerning induction ------------------------- *) + + val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n + `%x_name === %:x_name)); + val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj + (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n)); + val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name, + mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); + +in (dnam, + [abs_iso_ax, rep_iso_ax, reach_ax], + [when_def, copy_def] @ + con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ + [take_def, finite_def]) +end; (* let *) + +fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy)); + +fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x); +fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; + +fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x); +fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; + +in (* local *) + +fun add_axioms (comp_dnam, eqs : eq list) thy' = let + val comp_dname = Sign.full_name thy' comp_dnam; + val dnames = map (fst o fst) eqs; + val x_name = idx_name dnames "x"; + fun copy_app dname = %%:(dname^"_copy")`Bound 0; + val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == + /\"f"(foldr1 cpair (map copy_app dnames))); + val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R", + let + fun one_con (con,args) = let + val nonrec_args = filter_out is_rec args; + val rec_args = List.filter is_rec args; + val recs_cnt = length rec_args; + val allargs = nonrec_args @ rec_args + @ map (upd_vname (fn s=> s^"'")) rec_args; + val allvns = map vname allargs; + fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; + val vns1 = map (vname_arg "" ) args; + val vns2 = map (vname_arg "'") args; + val allargs_cnt = length nonrec_args + 2*recs_cnt; + val rec_idxs = (recs_cnt-1) downto 0; + val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) + (allargs~~((allargs_cnt-1) downto 0))); + fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ + Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); + val capps = foldr mk_conj (mk_conj( + Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), + Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) + (mapn rel_app 1 rec_args); + in foldr mk_ex (Library.foldr mk_conj + (map (defined o Bound) nonlazy_idxs,capps)) allvns end; + fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( + proj (Bound 2) eqs n $ Bound 1 $ Bound 0, + foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) + ::map one_con cons)))); + in foldr1 mk_conj (mapn one_comp 0 eqs)end )); + fun add_one (thy,(dnam,axs,dfs)) = thy + |> Theory.add_path dnam + |> add_defs_infer dfs + |> add_axioms_infer axs + |> Theory.parent_path; + val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); +in thy |> Theory.add_path comp_dnam + |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) + |> Theory.parent_path +end; + +end; (* local *) +end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/domain/domain_extender.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,183 @@ +(* Title: HOLCF/Tools/domain/domain_extender.ML + ID: $Id$ + Author: David von Oheimb + +Theory extender for domain command, including theory syntax. + +###TODO: + +this definition +domain empty = silly empty +yields +Exception- + TERM + ("typ_of_term: bad encoding of type", + [Abs ("uu", "_", Const ("NONE", "_"))]) raised +but this works fine: +domain Empty = silly Empty + +strange syntax errors are produced for: +domain xx = xx ("x yy") +domain 'a foo = foo (sel::"'a") +and bar = bar ("'a dummy") + +*) + +signature DOMAIN_EXTENDER = +sig + val add_domain: string * ((bstring * string list) * + (string * mixfix * (bool * string option * string) list) list) list + -> theory -> theory + val add_domain_i: string * ((bstring * string list) * + (string * mixfix * (bool * string option * typ) list) list) list + -> theory -> theory +end; + +structure Domain_Extender: DOMAIN_EXTENDER = +struct + +open Domain_Library; + +(* ----- general testing and preprocessing of constructor list -------------- *) +fun check_and_sort_domain (dtnvs: (string * typ list) list, + cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg = + let + val defaultS = Sign.defaultS sg; + val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of + [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); + val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of + [] => false | dups => error ("Duplicate constructors: " + ^ commas_quote dups)); + val test_dupl_sels = (case duplicates (op =) (List.mapPartial second + (List.concat (map third (List.concat cons'')))) of + [] => false | dups => error("Duplicate selectors: "^commas_quote dups)); + val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of + [] => false | dups => error("Duplicate type arguments: " + ^commas_quote dups)) (map snd dtnvs); + (* test for free type variables, illegal sort constraints on rhs, + non-pcpo-types and invalid use of recursive type; + replace sorts in type variables on rhs *) + fun analyse_equation ((dname,typevars),cons') = + let + val tvars = map dest_TFree typevars; + val distinct_typevars = map TFree tvars; + fun rm_sorts (TFree(s,_)) = TFree(s,[]) + | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) + | rm_sorts (TVar(s,_)) = TVar(s,[]) + and remove_sorts l = map rm_sorts l; + val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] + fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of + NONE => error ("Free type variable " ^ quote v ^ " on rhs.") + | SOME sort => if eq_set_string (s,defaultS) orelse + eq_set_string (s,sort ) + then TFree(v,sort) + else error ("Inconsistent sort constraint" ^ + " for type variable " ^ quote v)) + | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of + NONE => if s mem indirect_ok + then Type(s,map (analyse false) typl) + else Type(s,map (analyse true) typl) + | SOME typevars => if indirect + then error ("Indirect recursion of type " ^ + quote (string_of_typ sg t)) + else if dname <> s orelse (** BUG OR FEATURE?: + mutual recursion may use different arguments **) + remove_sorts typevars = remove_sorts typl + then Type(s,map (analyse true) typl) + else error ("Direct recursion of type " ^ + quote (string_of_typ sg t) ^ + " with different arguments")) + | analyse indirect (TVar _) = Imposs "extender:analyse"; + fun check_pcpo T = if pcpo_type sg T then T + else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T); + val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false))); + in ((dname,distinct_typevars), map analyse_con cons') end; + in ListPair.map analyse_equation (dtnvs,cons'') + end; (* let *) + +(* ----- calls for building new thy and thms -------------------------------- *) + +fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' = + let + val dtnvs = map ((fn (dname,vs) => + (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs)) + o fst) eqs'''; + val cons''' = map snd eqs'''; + fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn); + fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS); + val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs) + |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs; + val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons'''; + val eqs' = check_and_sort_domain (dtnvs,cons'') thy''; + val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs'); + val dts = map (Type o fst) eqs'; + val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; + fun strip ss = Library.drop (find_index_eq "'" ss +1, ss); + fun typid (Type (id,_)) = + let val c = hd (Symbol.explode (Sign.base_name id)) + in if Symbol.is_letter c then c else "t" end + | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) + | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); + fun one_con (con,mx,args) = + ((Syntax.const_name con mx), + ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy, + find_index_eq tp dts, + DatatypeAux.dtyp_of_typ new_dts tp), + sel,vn)) + (args,(mk_var_names(map (typid o third) args))) + ) : cons; + val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list; + val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs); + val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) => + Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs)) + |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs); + in + theorems_thy + |> Theory.add_path (Sign.base_name comp_dnam) + |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])])) + |> Theory.parent_path + end; + +val add_domain_i = gen_add_domain Sign.certify_typ; +val add_domain = gen_add_domain Sign.read_typ; + + +(** outer syntax **) + +local structure P = OuterParse and K = OuterKeyword in + +val dest_decl = + P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- + (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1 + || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")" + >> (fn t => (true,NONE,t)) + || P.typ >> (fn t => (false,NONE,t)); + +val cons_decl = + P.name -- Scan.repeat dest_decl -- P.opt_mixfix + >> (fn ((c, ds), mx) => (c, mx, ds)); + +val type_var' = (P.type_ident ^^ + Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) ""); +val type_args' = type_var' >> single || + P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || + Scan.succeed []; + +val domain_decl = (type_args' -- P.name >> Library.swap) -- + (P.$$$ "=" |-- P.enum1 "|" cons_decl); +val domains_decl = + Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl + >> (fn (opt_name, doms) => + (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms)); + +val domainP = + OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl + (domains_decl >> (Toplevel.theory o add_domain)); + + +val _ = OuterSyntax.add_keywords ["lazy"]; +val _ = OuterSyntax.add_parsers [domainP]; + +end; (* local structure *) + +end; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/domain/domain_library.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/domain/domain_library.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,230 @@ +(* Title: HOLCF/Tools/domain/domain_library.ML + ID: $Id$ + Author: David von Oheimb + +Library for domain command. +*) + + +(* ----- general support ---------------------------------------------------- *) + +fun mapn f n [] = [] +| mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; + +fun foldr'' f (l,f2) = let fun itr [] = raise Fail "foldr''" + | itr [a] = f2 a + | itr (a::l) = f(a, itr l) +in itr l end; +fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => + (y::ys,res2)) ([],start) xs; + + +fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; +fun upd_first f (x,y,z) = (f x, y, z); +fun upd_second f (x,y,z) = ( x, f y, z); +fun upd_third f (x,y,z) = ( x, y, f z); + +fun atomize thm = let val r_inst = read_instantiate; + fun at thm = case concl_of thm of + _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) + | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec)) + | _ => [thm]; +in map zero_var_indexes (at thm) end; + +(* ----- specific support for domain ---------------------------------------- *) + +structure Domain_Library = struct + +open HOLCFLogic; + +exception Impossible of string; +fun Imposs msg = raise Impossible ("Domain:"^msg); + +(* ----- name handling ----- *) + +val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs + | strip ["'"] = [] + | strip (c :: cs) = c :: strip cs + | strip [] = []; +in implode o strip o Symbol.explode end; + +fun extern_name con = case Symbol.explode con of + ("o"::"p"::" "::rest) => implode rest + | _ => con; +fun dis_name con = "is_"^ (extern_name con); +fun dis_name_ con = "is_"^ (strip_esc con); +fun mat_name con = "match_"^ (extern_name con); +fun mat_name_ con = "match_"^ (strip_esc con); +fun pat_name con = (extern_name con) ^ "_pat"; +fun pat_name_ con = (strip_esc con) ^ "_pat"; + +(* make distinct names out of the type list, + forbidding "o","n..","x..","f..","P.." as names *) +(* a number string is added if necessary *) +fun mk_var_names ids : string list = let + fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; + fun index_vnames(vn::vns,occupied) = + (case AList.lookup (op =) occupied vn of + NONE => if vn mem vns + then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) + else vn :: index_vnames(vns, occupied) + | SOME(i) => (vn^(string_of_int (i+1))) + :: index_vnames(vns,(vn,i+1)::occupied)) + | index_vnames([],occupied) = []; +in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; + +fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS); +fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg; + +(* ----- constructor list handling ----- *) + +type cons = (string * (* operator name of constr *) + ((bool*int*DatatypeAux.dtyp)* (* (lazy,recursive element or ~1) *) + string option* (* selector name *) + string) (* argument name *) + list); (* argument list *) +type eq = (string * (* name of abstracted type *) + typ list) * (* arguments of abstracted type *) + cons list; (* represented type, as a constructor list *) + +fun rec_of arg = second (first arg); +fun is_lazy arg = first (first arg); +val sel_of = second; +val vname = third; +val upd_vname = upd_third; +fun is_rec arg = rec_of arg >=0; +fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); +fun nonlazy args = map vname (filter_out is_lazy args); +fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); + +(* ----- qualified names of HOLCF constants ----- *) + +val lessN = "Porder.<<" +val UU_N = "Pcpo.UU"; +val admN = "Adm.adm"; +val compactN = "Adm.compact"; +val Rep_CFunN = "Cfun.Rep_CFun"; +val Abs_CFunN = "Cfun.Abs_CFun"; +val ID_N = "Cfun.ID"; +val cfcompN = "Cfun.cfcomp"; +val strictifyN = "Cfun.strictify"; +val cpairN = "Cprod.cpair"; +val cfstN = "Cprod.cfst"; +val csndN = "Cprod.csnd"; +val csplitN = "Cprod.csplit"; +val spairN = "Sprod.spair"; +val sfstN = "Sprod.sfst"; +val ssndN = "Sprod.ssnd"; +val ssplitN = "Sprod.ssplit"; +val sinlN = "Ssum.sinl"; +val sinrN = "Ssum.sinr"; +val sscaseN = "Ssum.sscase"; +val upN = "Up.up"; +val fupN = "Up.fup"; +val ONE_N = "One.ONE"; +val TT_N = "Tr.TT"; +val FF_N = "Tr.FF"; +val iterateN = "Fix.iterate"; +val fixN = "Fix.fix"; +val returnN = "Fixrec.return"; +val failN = "Fixrec.fail"; +val cpair_patN = "Fixrec.cpair_pat"; +val branchN = "Fixrec.branch"; + +val pcpoN = "Pcpo.pcpo" +val pcpoS = [pcpoN]; + + +(* ----- support for type and mixfix expressions ----- *) + +infixr 5 -->; + +(* ----- support for term expressions ----- *) + +fun %: s = Free(s,dummyT); +fun %# arg = %:(vname arg); +fun %%: s = Const(s,dummyT); + +local open HOLogic in +val mk_trp = mk_Trueprop; +fun mk_conj (S,T) = conj $ S $ T; +fun mk_disj (S,T) = disj $ S $ T; +fun mk_imp (S,T) = imp $ S $ T; +fun mk_lam (x,T) = Abs(x,dummyT,T); +fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); +fun mk_ex (x,P) = mk_exists (x,dummyT,P); +fun mk_constrain (typ,T) = TypeInfer.constrain T typ; +fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (mk_lam(x,P)) (typ --> boolT)); +end + +fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) + +infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T; +infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T; +infix 0 ==; fun S == T = %%:"==" $ S $ T; +infix 1 ===; fun S === T = %%:"op =" $ S $ T; +infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); +infix 1 <<; fun S << T = %%:lessN $ S $ T; +infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T); + +infix 9 ` ; fun f` x = %%:Rep_CFunN $ f $ x; +infix 9 `% ; fun f`% s = f` %: s; +infix 9 `%%; fun f`%%s = f` %%:s; +val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *) +fun con_app2 con f args = list_ccomb(%%:con,map f args); +fun con_app con = con_app2 con %#; +fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; +fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg); +fun prj _ _ x ( _::[]) _ = x +| prj f1 _ x (_::y::ys) 0 = f1 x y +| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); +fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; +fun cproj x = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x; +fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); + +fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T); +fun /\# (arg,T) = /\ (vname arg) T; +infixr 9 oo; fun S oo T = %%:cfcompN`S`T; +val UU = %%:UU_N; +fun strict f = f`UU === UU; +fun defined t = t ~= UU; +fun cpair (t,u) = %%:cpairN`t`u; +fun spair (t,u) = %%:spairN`t`u; +fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) +| mk_ctuple ts = foldr1 cpair ts; +fun mk_stuple [] = %%:ONE_N +| mk_stuple ts = foldr1 spair ts; +fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) +| mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; +fun mk_maybeT T = Type ("Fixrec.maybe",[T]); +fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2; +fun lift_defined f = lift (fn x => defined (f x)); +fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); + +fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = + (case cont_eta_contract body of + body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => + if not (0 mem loose_bnos f) then incr_boundvars ~1 f + else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') + | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) +| cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t +| cont_eta_contract t = t; + +fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); +fun when_funs cons = if length cons = 1 then ["f"] + else mapn (fn n => K("f"^(string_of_int n))) 1 cons; +fun when_body cons funarg = let + fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) + | one_fun n (_,args) = let + val l2 = length args; + fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x + else I) (Bound(l2-m)); + in cont_eta_contract (foldr'' + (fn (a,t) => %%:ssplitN`(/\# (a,t))) + (args, + fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args)))) + ) end; +in (if length cons = 1 andalso length(snd(hd cons)) <= 1 + then fn t => %%:strictifyN`t else I) + (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end; +end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/domain/domain_syntax.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,151 @@ +(* Title: HOLCF/Tools/domain/domain_syntax.ML + ID: $Id$ + Author: David von Oheimb + +Syntax generator for domain command. +*) + +structure Domain_Syntax = struct + +local + +open Domain_Library; +infixr 5 -->; infixr 6 ->>; +fun calc_syntax dtypeprod ((dname, typevars), + (cons': (string * mixfix * (bool * string option * typ) list) list)) = +let +(* ----- constants concerning the isomorphism ------------------------------- *) + +local + fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t + fun prod (_,_,args) = if args = [] then oneT + else foldr1 mk_sprodT (map opt_lazy args); + fun freetvar s = let val tvar = mk_TFree s in + if tvar mem typevars then freetvar ("t"^s) else tvar end; + fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args); +in + val dtype = Type(dname,typevars); + val dtype2 = foldr1 mk_ssumT (map prod cons'); + val dnam = Sign.base_name dname; + val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); + val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); + val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); + val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); +end; + +(* ----- constants concerning constructors, discriminators, and selectors --- *) + +local + val escape = let + fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs + else c::esc cs + | esc [] = [] + in implode o esc o Symbol.explode end; + fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s); + fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT, + Mixfix(escape ("is_" ^ con), [], Syntax.max_pri)); + (* strictly speaking, these constants have one argument, + but the mixfix (without arguments) is introduced only + to generate parse rules for non-alphanumeric names*) + fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)), + Mixfix(escape ("match_" ^ con), [], Syntax.max_pri)); + fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; + fun sel (_ ,_,args) = List.mapPartial sel1 args; + fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in + if tvar mem typevars then freetvar ("t"^s) n else tvar end; + fun mk_patT (a,b) = a ->> mk_maybeT b; + fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n); + fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) ---> + mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), + Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri)); + +in + val consts_con = map con cons'; + val consts_dis = map dis cons'; + val consts_mat = map mat cons'; + val consts_pat = map pat cons'; + val consts_sel = List.concat(map sel cons'); +end; + +(* ----- constants concerning induction ------------------------------------- *) + + val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn); + val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn); + +(* ----- case translation --------------------------------------------------- *) + +local open Syntax in + local + fun c_ast con mx = Constant (const_name con mx); + fun expvar n = Variable ("e"^(string_of_int n)); + fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^ + (string_of_int m)); + fun argvars n args = mapn (argvar n) 1 args; + fun app s (l,r) = mk_appl (Constant s) [l,r]; + val cabs = app "_cabs"; + val capp = app "Rep_CFun"; + fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args); + fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n); + fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args); + fun when1 n m = if n = m then arg1 n else K (Constant "UU"); + + fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"]; + fun app_pat x = mk_appl (Constant "_pat") [x]; + fun args_list [] = Constant "Unity" + | args_list xs = foldr1 (app "_args") xs; + in + val case_trans = ParsePrintRule + (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), + capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); + + val abscon_trans = mapn (fn n => fn (con,mx,args) => ParsePrintRule + (cabs (con1 n (con,mx,args), expvar n), + Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons'; + + val Case_trans = List.concat (map (fn (con,mx,args) => + let + val cname = c_ast con mx; + val pname = Constant (pat_name_ con); + val ns = 1 upto length args; + val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; + val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; + val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; + in + [ParseRule (app_pat (Library.foldl capp (cname, xs)), + mk_appl pname (map app_pat xs)), + ParseRule (app_var (Library.foldl capp (cname, xs)), + app_var (args_list xs)), + PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), + app "_match" (mk_appl pname ps, args_list vs))] + end) cons'); + end; +end; + +in ([const_rep, const_abs, const_when, const_copy] @ + consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ + [const_take, const_finite], + (case_trans::(abscon_trans @ Case_trans))) +end; (* let *) + +(* ----- putting all the syntax stuff together ------------------------------ *) + +in (* local *) + +fun add_syntax (comp_dnam,eqs': ((string * typ list) * + (string * mixfix * (bool * string option * typ) list) list) list) thy'' = +let + val dtypes = map (Type o fst) eqs'; + val boolT = HOLogic.boolT; + val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes); + val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); + val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn); + val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn); + val ctt = map (calc_syntax funprod) eqs'; +in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ + (if length eqs'>1 then [const_copy] else[])@ + [const_bisim]) + |> Sign.add_trrules_i (List.concat(map snd ctt)) +end; (* let *) + +end; (* local *) +end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/domain/domain_theorems.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,951 @@ +(* Title: HOLCF/Tools/domain/domain_theorems.ML + ID: $Id$ + Author: David von Oheimb + New proofs/tactics by Brian Huffman + +Proof generator for domain command. +*) + +val HOLCF_ss = simpset(); + +structure Domain_Theorems = struct + +local + +val adm_impl_admw = thm "adm_impl_admw"; +val antisym_less_inverse = thm "antisym_less_inverse"; +val beta_cfun = thm "beta_cfun"; +val cfun_arg_cong = thm "cfun_arg_cong"; +val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; +val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; +val chain_iterate = thm "chain_iterate"; +val compact_ONE = thm "compact_ONE"; +val compact_sinl = thm "compact_sinl"; +val compact_sinr = thm "compact_sinr"; +val compact_spair = thm "compact_spair"; +val compact_up = thm "compact_up"; +val contlub_cfun_arg = thm "contlub_cfun_arg"; +val contlub_cfun_fun = thm "contlub_cfun_fun"; +val fix_def2 = thm "fix_def2"; +val injection_eq = thm "injection_eq"; +val injection_less = thm "injection_less"; +val lub_equal = thm "lub_equal"; +val monofun_cfun_arg = thm "monofun_cfun_arg"; +val retraction_strict = thm "retraction_strict"; +val spair_eq = thm "spair_eq"; +val spair_less = thm "spair_less"; +val sscase1 = thm "sscase1"; +val ssplit1 = thm "ssplit1"; +val strictify1 = thm "strictify1"; +val wfix_ind = thm "wfix_ind"; + +open Domain_Library; +infixr 0 ===>; +infixr 0 ==>; +infix 0 == ; +infix 1 ===; +infix 1 ~= ; +infix 1 <<; +infix 1 ~<<; +infix 9 ` ; +infix 9 `% ; +infix 9 `%%; +infixr 9 oo; + +(* ----- general proof facilities ------------------------------------------- *) + +fun pg'' thy defs t tacs = + let + val t' = FixrecPackage.legacy_infer_term thy t; + val asms = Logic.strip_imp_prems t'; + val prop = Logic.strip_imp_concl t'; + fun tac prems = + rewrite_goals_tac defs THEN + EVERY (tacs (map (rewrite_rule defs) prems)); + in Goal.prove_global thy [] asms prop tac end; + +fun pg' thy defs t tacsf = + let + fun tacs [] = tacsf + | tacs prems = cut_facts_tac prems 1 :: tacsf; + in pg'' thy defs t tacs end; + +fun case_UU_tac rews i v = + case_tac (v^"=UU") i THEN + asm_simp_tac (HOLCF_ss addsimps rews) i; + +val chain_tac = + REPEAT_DETERM o resolve_tac + [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL]; + +(* ----- general proofs ----------------------------------------------------- *) + +val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R" + (fn prems =>[ + resolve_tac prems 1, + cut_facts_tac prems 1, + fast_tac HOL_cs 1]); + +val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" + (fn prems => + [blast_tac (claset () addDs [antisym_less_inverse]) 1]); + +in + +fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = +let + +val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ..."); +val pg = pg' thy; + +(* ----- getting the axioms and definitions --------------------------------- *) + +local + fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)); +in + val ax_abs_iso = ga "abs_iso" dname; + val ax_rep_iso = ga "rep_iso" dname; + val ax_when_def = ga "when_def" dname; + fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname; + val axs_con_def = map (get_def extern_name) cons; + val axs_dis_def = map (get_def dis_name) cons; + val axs_mat_def = map (get_def mat_name) cons; + val axs_pat_def = map (get_def pat_name) cons; + val axs_sel_def = + let + fun def_of_sel sel = ga (sel^"_def") dname; + fun def_of_arg arg = Option.map def_of_sel (sel_of arg); + fun defs_of_con (_, args) = List.mapPartial def_of_arg args; + in + List.concat (map defs_of_con cons) + end; + val ax_copy_def = ga "copy_def" dname; +end; (* local *) + +(* ----- theorems concerning the isomorphism -------------------------------- *) + +val dc_abs = %%:(dname^"_abs"); +val dc_rep = %%:(dname^"_rep"); +val dc_copy = %%:(dname^"_copy"); +val x_name = "x"; + +val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso]; +val abs_strict = ax_rep_iso RS (allI RS retraction_strict); +val rep_strict = ax_abs_iso RS (allI RS retraction_strict); +val abs_defin' = iso_locale RS iso_abs_defin'; +val rep_defin' = iso_locale RS iso_rep_defin'; +val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict]; + +(* ----- generating beta reduction rules from definitions-------------------- *) + +local + fun arglist (Const _ $ Abs (s, _, t)) = + let + val (vars,body) = arglist t; + in (s :: vars, body) end + | arglist t = ([], t); + fun bind_fun vars t = Library.foldr mk_All (vars, t); + fun bound_vars 0 = [] + | bound_vars i = Bound (i-1) :: bound_vars (i - 1); +in + fun appl_of_def def = + let + val (_ $ con $ lam) = concl_of def; + val (vars, rhs) = arglist lam; + val lhs = list_ccomb (con, bound_vars (length vars)); + val appl = bind_fun vars (lhs == rhs); + val cs = ContProc.cont_thms lam; + val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs; + in pg (def::betas) appl [rtac reflexive_thm 1] end; +end; + +val when_appl = appl_of_def ax_when_def; +val con_appls = map appl_of_def axs_con_def; + +local + fun arg2typ n arg = + let val t = TVar (("'a", n), pcpoS) + in (n + 1, if is_lazy arg then mk_uT t else t) end; + + fun args2typ n [] = (n, oneT) + | args2typ n [arg] = arg2typ n arg + | args2typ n (arg::args) = + let + val (n1, t1) = arg2typ n arg; + val (n2, t2) = args2typ n1 args + 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 (n2, t2) = cons2typ n1 cons + in (n2, mk_ssumT (t1, t2)) end; +in + fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons)); +end; + +local + val iso_swap = iso_locale RS iso_iso_swap; + fun one_con (con, args) = + let + val vns = map vname args; + val eqn = %:x_name === con_app2 con %: vns; + val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args)); + in Library.foldr mk_ex (vns, conj) end; + + val conj_assoc = thm "conj_assoc"; + val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons); + val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start; + val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1; + val thm3 = rewrite_rule [mk_meta_eq conj_assoc] thm2; + + (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) + val tacs = [ + rtac disjE 1, + etac (rep_defin' RS disjI1) 2, + etac disjI2 2, + rewrite_goals_tac [mk_meta_eq iso_swap], + rtac thm3 1]; +in + val exhaust = pg con_appls (mk_trp exh) tacs; + val casedist = + standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0)); +end; + +local + fun bind_fun t = Library.foldr mk_All (when_funs cons, t); + fun bound_fun i _ = Bound (length cons - i); + val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons); +in + val when_strict = + let + val axs = [when_appl, mk_meta_eq rep_strict]; + val goal = bind_fun (mk_trp (strict when_app)); + val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1]; + in pg axs goal tacs end; + + val when_apps = + let + fun one_when n (con,args) = + let + val axs = when_appl :: con_appls; + val goal = bind_fun (lift_defined %: (nonlazy args, + mk_trp (when_app`(con_app con args) === + list_ccomb (bound_fun n 0, map %# args)))); + val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1]; + in pg axs goal tacs end; + in mapn one_when 1 cons end; +end; +val when_rews = when_strict :: when_apps; + +(* ----- theorems concerning the constructors, discriminators and selectors - *) + +local + fun dis_strict (con, _) = + let + val goal = mk_trp (strict (%%:(dis_name con))); + in pg axs_dis_def goal [rtac when_strict 1] end; + + fun dis_app c (con, args) = + let + val lhs = %%:(dis_name c) ` con_app con args; + val rhs = %%:(if con = c then TT_N else FF_N); + val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); + val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs_dis_def goal tacs end; + + val dis_apps = List.concat (map (fn (c,_) => map (dis_app c) cons) cons); + + fun dis_defin (con, args) = + let + val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name); + val tacs = + [rtac casedist 1, + contr_tac 1, + DETERM_UNTIL_SOLVED (CHANGED + (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))]; + in pg [] goal tacs end; + + val dis_stricts = map dis_strict cons; + val dis_defins = map dis_defin cons; +in + val dis_rews = dis_stricts @ dis_defins @ dis_apps; +end; + +local + fun mat_strict (con, _) = + let + val goal = mk_trp (strict (%%:(mat_name con))); + val tacs = [rtac when_strict 1]; + in pg axs_mat_def goal tacs end; + + val mat_stricts = map mat_strict cons; + + fun one_mat c (con, args) = + let + val lhs = %%:(mat_name c) ` con_app con args; + val rhs = + if con = c + then %%:returnN ` mk_ctuple (map %# args) + else %%:failN; + val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); + val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs_mat_def goal tacs end; + + val mat_apps = + List.concat (map (fn (c,_) => map (one_mat c) cons) cons); +in + val mat_rews = mat_stricts @ mat_apps; +end; + +local + fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; + + fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args); + + fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit) + | pat_rhs (con,args) = + (%%:branchN $ foldr1 cpair_pat (ps args)) + `(%:"rhs")`(mk_ctuple (map %# args)); + + fun pat_strict c = + let + val axs = branch_def :: axs_pat_def; + val goal = mk_trp (strict (pat_lhs c ` (%:"rhs"))); + val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1]; + in pg axs goal tacs end; + + fun pat_app c (con, args) = + let + val axs = branch_def :: axs_pat_def; + val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args); + val rhs = if con = fst c then pat_rhs c else %%:failN; + val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); + val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs goal tacs end; + + val pat_stricts = map pat_strict cons; + val pat_apps = List.concat (map (fn c => map (pat_app c) cons) cons); +in + val pat_rews = pat_stricts @ pat_apps; +end; + +local + val rev_contrapos = thm "rev_contrapos"; + fun con_strict (con, args) = + let + fun one_strict vn = + let + fun f arg = if vname arg = vn then UU else %# arg; + val goal = mk_trp (con_app2 con f args === UU); + val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]; + in pg con_appls goal tacs end; + in map one_strict (nonlazy args) end; + + fun con_defin (con, args) = + let + val concl = mk_trp (defined (con_app con args)); + val goal = lift_defined %: (nonlazy args, concl); + val tacs = [ + rtac rev_contrapos 1, + eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1, + asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; + in pg [] goal tacs end; +in + val con_stricts = List.concat (map con_strict cons); + val con_defins = map con_defin cons; + val con_rews = con_stricts @ con_defins; +end; + +local + val rules = + [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE]; + fun con_compact (con, args) = + let + val concl = mk_trp (%%:compactN $ con_app con args); + val goal = lift (fn x => %%:compactN $ %#x) (args, concl); + val tacs = [ + rtac (iso_locale RS iso_compact_abs) 1, + REPEAT (resolve_tac rules 1 ORELSE atac 1)]; + in pg con_appls goal tacs end; +in + val con_compacts = map con_compact cons; +end; + +local + fun one_sel sel = + pg axs_sel_def (mk_trp (strict (%%:sel))) + [simp_tac (HOLCF_ss addsimps when_rews) 1]; + + fun sel_strict (_, args) = + List.mapPartial (Option.map one_sel o sel_of) args; +in + val sel_stricts = List.concat (map sel_strict cons); +end; + +local + fun sel_app_same c n sel (con, args) = + let + val nlas = nonlazy args; + val vns = map vname args; + val vnn = List.nth (vns, n); + val nlas' = List.filter (fn v => v <> vnn) nlas; + val lhs = (%%:sel)`(con_app con args); + val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn)); + val tacs1 = + if vnn mem nlas + then [case_UU_tac (when_rews @ con_stricts) 1 vnn] + else []; + val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs_sel_def goal (tacs1 @ tacs2) end; + + fun sel_app_diff c n sel (con, args) = + let + val nlas = nonlazy args; + val goal = mk_trp (%%:sel ` con_app con args === UU); + val tacs1 = map (case_UU_tac (when_rews @ con_stricts) 1) nlas; + val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs_sel_def goal (tacs1 @ tacs2) end; + + fun sel_app c n sel (con, args) = + if con = c + then sel_app_same c n sel (con, args) + else sel_app_diff c n sel (con, args); + + fun one_sel c n sel = map (sel_app c n sel) cons; + fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg); + fun one_con (c, args) = + List.concat (List.mapPartial I (mapn (one_sel' c) 0 args)); +in + val sel_apps = List.concat (map one_con cons); +end; + +local + fun sel_defin sel = + let + val goal = defined (%:x_name) ==> defined (%%:sel`%x_name); + val tacs = [ + rtac casedist 1, + contr_tac 1, + DETERM_UNTIL_SOLVED (CHANGED + (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))]; + in pg [] goal tacs end; +in + val sel_defins = + if length cons = 1 + then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg)) + (filter_out is_lazy (snd (hd cons))) + else []; +end; + +val sel_rews = sel_stricts @ sel_defins @ sel_apps; +val rev_contrapos = thm "rev_contrapos"; + +val distincts_le = + let + fun dist (con1, args1) (con2, args2) = + let + val goal = lift_defined %: (nonlazy args1, + mk_trp (con_app con1 args1 ~<< con_app con2 args2)); + val tacs = [ + rtac rev_contrapos 1, + eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1] + @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2) + @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; + in pg [] goal tacs end; + + fun distinct (con1, args1) (con2, args2) = + let + val arg1 = (con1, args1); + val arg2 = + (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) + (args2, Name.variant_list (map vname args1) (map vname args2))); + in [dist arg1 arg2, dist arg2 arg1] end; + fun distincts [] = [] + | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; + in distincts cons end; +val dist_les = List.concat (List.concat distincts_le); +val dist_eqs = + let + fun distinct (_,args1) ((_,args2), leqs) = + let + val (le1,le2) = (hd leqs, hd(tl leqs)); + val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) + in + if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else + if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else + [eq1, eq2] + end; + fun distincts [] = [] + | distincts ((c,leqs)::cs) = List.concat + (ListPair.map (distinct c) ((map #1 cs),leqs)) @ + distincts cs; + in map standard (distincts (cons ~~ distincts_le)) end; + +local + fun pgterm rel con args = + let + fun append s = upd_vname (fn v => v^s); + val (largs, rargs) = (args, map (append "'") args); + val concl = + foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)); + val prem = rel (con_app con largs, con_app con rargs); + val sargs = case largs of [_] => [] | _ => nonlazy args; + val prop = lift_defined %: (sargs, mk_trp (prem === concl)); + in pg con_appls prop end; + val cons' = List.filter (fn (_,args) => args<>[]) cons; +in + val inverts = + let + val abs_less = ax_abs_iso RS (allI RS injection_less); + val tacs = + [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1]; + in map (fn (con, args) => pgterm (op <<) con args tacs) cons' end; + + val injects = + let + val abs_eq = ax_abs_iso RS (allI RS injection_eq); + val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1]; + in map (fn (con, args) => pgterm (op ===) con args tacs) cons' end; +end; + +(* ----- theorems concerning one induction step ----------------------------- *) + +val copy_strict = + let + val goal = mk_trp (strict (dc_copy `% "f")); + val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1]; + in pg [ax_copy_def] goal tacs end; + +local + fun copy_app (con, args) = + let + val lhs = dc_copy`%"f"`(con_app con args); + val rhs = con_app2 con (app_rec_arg (cproj (%:"f") eqs)) args; + val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); + val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args; + val stricts = abs_strict::when_strict::con_stricts; + val tacs1 = map (case_UU_tac stricts 1 o vname) args'; + val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1]; + in pg [ax_copy_def] goal (tacs1 @ tacs2) end; +in + val copy_apps = map copy_app cons; +end; + +local + fun one_strict (con, args) = + let + val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); + val rews = copy_strict :: copy_apps @ con_rews; + val tacs = map (case_UU_tac rews 1) (nonlazy args) @ + [asm_simp_tac (HOLCF_ss addsimps rews) 1]; + in pg [] goal tacs end; + + fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args; +in + val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons); +end; + +val copy_rews = copy_strict :: copy_apps @ copy_stricts; + +in + thy + |> Theory.add_path (Sign.base_name dname) + |> (snd o (PureThy.add_thmss (map Thm.no_attributes [ + ("iso_rews" , iso_rews ), + ("exhaust" , [exhaust] ), + ("casedist" , [casedist]), + ("when_rews", when_rews ), + ("compacts", con_compacts), + ("con_rews", con_rews), + ("sel_rews", sel_rews), + ("dis_rews", dis_rews), + ("pat_rews", pat_rews), + ("dist_les", dist_les), + ("dist_eqs", dist_eqs), + ("inverts" , inverts ), + ("injects" , injects ), + ("copy_rews", copy_rews)]))) + |> (snd o PureThy.add_thmss + [(("match_rews", mat_rews), [Simplifier.simp_add])]) + |> Theory.parent_path + |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ + pat_rews @ dist_les @ dist_eqs @ copy_rews) +end; (* let *) + +fun comp_theorems (comp_dnam, eqs: eq list) thy = +let +val dnames = map (fst o fst) eqs; +val conss = map snd eqs; +val comp_dname = Sign.full_name thy comp_dnam; + +val d = writeln("Proving induction properties of domain "^comp_dname^" ..."); +val pg = pg' thy; + +(* ----- getting the composite axiom and definitions ------------------------ *) + +local + fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)); +in + val axs_reach = map (ga "reach" ) dnames; + val axs_take_def = map (ga "take_def" ) dnames; + val axs_finite_def = map (ga "finite_def") dnames; + val ax_copy2_def = ga "copy_def" comp_dnam; + val ax_bisim_def = ga "bisim_def" comp_dnam; +end; + +local + fun gt s dn = get_thm thy (Name (dn ^ "." ^ s)); + fun gts s dn = get_thms thy (Name (dn ^ "." ^ s)); +in + val cases = map (gt "casedist" ) dnames; + val con_rews = List.concat (map (gts "con_rews" ) dnames); + val copy_rews = List.concat (map (gts "copy_rews") dnames); +end; + +fun dc_take dn = %%:(dn^"_take"); +val x_name = idx_name dnames "x"; +val P_name = idx_name dnames "P"; +val n_eqs = length eqs; + +(* ----- theorems concerning finite approximation and finite induction ------ *) + +local + val iterate_Cprod_ss = simpset_of (theory "Fix"); + val copy_con_rews = copy_rews @ con_rews; + val copy_take_defs = + (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; + val take_stricts = + let + fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n"); + val goal = mk_trp (foldr1 mk_conj (map one_eq eqs)); + val tacs = [ + induct_tac "n" 1, + simp_tac iterate_Cprod_ss 1, + asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1]; + in pg copy_take_defs goal tacs end; + + val take_stricts' = rewrite_rule copy_take_defs take_stricts; + fun take_0 n dn = + let + val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU); + in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end; + val take_0s = mapn take_0 1 dnames; + val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1; + val take_apps = + let + fun mk_eqn dn (con, args) = + let + fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; + val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); + val rhs = con_app2 con (app_rec_arg mk_take) args; + in Library.foldr mk_all (map vname args, lhs === rhs) end; + fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; + val goal = mk_trp (foldr1 mk_conj (List.concat (map mk_eqns eqs))); + val simps = List.filter (has_fewer_prems 1) copy_rews; + fun con_tac (con, args) = + if nonlazy_rec args = [] + then all_tac + else EVERY (map c_UU_tac (nonlazy_rec args)) THEN + asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; + fun eq_tacs ((dn, _), cons) = map con_tac cons; + val tacs = + simp_tac iterate_Cprod_ss 1 :: + induct_tac "n" 1 :: + simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 :: + asm_full_simp_tac (HOLCF_ss addsimps simps) 1 :: + TRY (safe_tac HOL_cs) :: + List.concat (map eq_tacs eqs); + in pg copy_take_defs goal tacs end; +in + val take_rews = map standard + (atomize take_stricts @ take_0s @ atomize take_apps); +end; (* local *) + +local + fun one_con p (con,args) = + let + fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; + val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); + val t2 = lift ind_hyp (List.filter is_rec args, t1); + val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2); + in Library.foldr mk_All (map vname args, t3) end; + + fun one_eq ((p, cons), concl) = + mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); + + fun ind_term concf = Library.foldr one_eq + (mapn (fn n => fn x => (P_name n, x)) 1 conss, + mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); + val take_ss = HOL_ss addsimps take_rews; + fun quant_tac i = EVERY + (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames); + + fun ind_prems_tac prems = EVERY + (List.concat (map (fn cons => + (resolve_tac prems 1 :: + List.concat (map (fn (_,args) => + resolve_tac prems 1 :: + map (K(atac 1)) (nonlazy args) @ + map (K(atac 1)) (List.filter is_rec args)) + cons))) + conss)); + local + (* check whether every/exists constructor of the n-th part of the equation: + it has a possibly indirectly recursive argument that isn't/is possibly + indirectly lazy *) + fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => + is_rec arg andalso not(rec_of arg mem ns) andalso + ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse + rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) + (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) + ) o snd) cons; + fun all_rec_to ns = rec_to forall not all_rec_to ns; + fun warn (n,cons) = + if all_rec_to [] false (n,cons) + then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) + else false; + fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns; + + in + val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; + val is_emptys = map warn n__eqs; + val is_finite = forall (not o lazy_rec_to [] false) n__eqs; + end; +in (* local *) + val finite_ind = + let + fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n)); + val goal = ind_term concf; + + fun tacf prems = + let + val tacs1 = [ + quant_tac 1, + simp_tac HOL_ss 1, + induct_tac "n" 1, + simp_tac (take_ss addsimps prems) 1, + TRY (safe_tac HOL_cs)]; + fun arg_tac arg = + case_UU_tac (prems @ con_rews) 1 + (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); + fun con_tacs (con, args) = + asm_simp_tac take_ss 1 :: + map arg_tac (List.filter is_nonlazy_rec args) @ + [resolve_tac prems 1] @ + map (K (atac 1)) (nonlazy args) @ + map (K (etac spec 1)) (List.filter is_rec args); + fun cases_tacs (cons, cases) = + res_inst_tac [("x","x")] cases 1 :: + asm_simp_tac (take_ss addsimps prems) 1 :: + List.concat (map con_tacs cons); + in + tacs1 @ List.concat (map cases_tacs (conss ~~ cases)) + end; + in pg'' thy [] goal tacf end; + + val take_lemmas = + let + fun take_lemma n (dn, ax_reach) = + let + val lhs = dc_take dn $ Bound 0 `%(x_name n); + val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); + val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); + val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; + fun tacf prems = [ + res_inst_tac [("t", x_name n )] (ax_reach RS subst) 1, + res_inst_tac [("t", x_name n^"'")] (ax_reach RS subst) 1, + stac fix_def2 1, + REPEAT (CHANGED + (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)), + stac contlub_cfun_fun 1, + stac contlub_cfun_fun 2, + rtac lub_equal 3, + chain_tac 1, + rtac allI 1, + resolve_tac prems 1]; + in pg'' thy axs_take_def goal tacf end; + in mapn take_lemma 1 (dnames ~~ axs_reach) end; + +(* ----- theorems concerning finiteness and induction ----------------------- *) + + val (finites, ind) = + if is_finite + then (* finite case *) + let + fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x"); + fun dname_lemma dn = + let + val prem1 = mk_trp (defined (%:"x")); + val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU); + val prem2 = mk_trp (mk_disj (disj1, take_enough dn)); + val concl = mk_trp (take_enough dn); + val goal = prem1 ===> prem2 ===> concl; + val tacs = [ + etac disjE 1, + etac notE 1, + resolve_tac take_lemmas 1, + asm_simp_tac take_ss 1, + atac 1]; + in pg [] goal tacs end; + val finite_lemmas1a = map dname_lemma dnames; + + val finite_lemma1b = + let + fun mk_eqn n ((dn, args), _) = + let + val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU; + val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0; + in + mk_constrainall + (x_name n, Type (dn,args), mk_disj (disj1, disj2)) + end; + val goal = + mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs))); + fun arg_tacs vn = [ + eres_inst_tac [("x", vn)] all_dupE 1, + etac disjE 1, + asm_simp_tac (HOL_ss addsimps con_rews) 1, + asm_simp_tac take_ss 1]; + fun con_tacs (con, args) = + asm_simp_tac take_ss 1 :: + List.concat (map arg_tacs (nonlazy_rec args)); + fun foo_tacs n (cons, cases) = + simp_tac take_ss 1 :: + rtac allI 1 :: + res_inst_tac [("x",x_name n)] cases 1 :: + asm_simp_tac take_ss 1 :: + List.concat (map con_tacs cons); + val tacs = + rtac allI 1 :: + induct_tac "n" 1 :: + simp_tac take_ss 1 :: + TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) :: + List.concat (mapn foo_tacs 1 (conss ~~ cases)); + in pg [] goal tacs end; + + fun one_finite (dn, l1b) = + let + val goal = mk_trp (%%:(dn^"_finite") $ %:"x"); + val tacs = [ + case_UU_tac take_rews 1 "x", + eresolve_tac finite_lemmas1a 1, + step_tac HOL_cs 1, + step_tac HOL_cs 1, + cut_facts_tac [l1b] 1, + fast_tac HOL_cs 1]; + in pg axs_finite_def goal tacs end; + + val finites = map one_finite (dnames ~~ atomize finite_lemma1b); + val ind = + let + fun concf n dn = %:(P_name n) $ %:(x_name n); + fun tacf prems = + let + fun finite_tacs (finite, fin_ind) = [ + rtac(rewrite_rule axs_finite_def finite RS exE)1, + etac subst 1, + rtac fin_ind 1, + ind_prems_tac prems]; + in + TRY (safe_tac HOL_cs) :: + List.concat (map finite_tacs (finites ~~ atomize finite_ind)) + end; + in pg'' thy [] (ind_term concf) tacf end; + in (finites, ind) end (* let *) + + else (* infinite case *) + let + fun one_finite n dn = + read_instantiate_sg thy + [("P",dn^"_finite "^x_name n)] excluded_middle; + val finites = mapn one_finite 1 dnames; + + val goal = + let + fun one_adm n _ = mk_trp (%%:admN $ %:(P_name n)); + fun concf n dn = %:(P_name n) $ %:(x_name n); + in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; + fun tacf prems = + map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ + quant_tac 1, + rtac (adm_impl_admw RS wfix_ind) 1, + REPEAT_DETERM (rtac adm_all2 1), + REPEAT_DETERM ( + TRY (rtac adm_conj 1) THEN + rtac adm_subst 1 THEN + cont_tacR 1 THEN resolve_tac prems 1), + strip_tac 1, + rtac (rewrite_rule axs_take_def finite_ind) 1, + ind_prems_tac prems]; + val ind = (pg'' thy [] goal tacf + handle ERROR _ => + (warning "Cannot prove infinite induction rule"; refl)); + in (finites, ind) end; +end; (* local *) + +(* ----- theorem concerning coinduction ------------------------------------- *) + +local + val xs = mapn (fn n => K (x_name n)) 1 dnames; + fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); + val take_ss = HOL_ss addsimps take_rews; + val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); + val coind_lemma = + let + fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; + fun mk_eqn n dn = + (dc_take dn $ %:"n" ` bnd_arg n 0) === + (dc_take dn $ %:"n" ` bnd_arg n 1); + fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); + val goal = + mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", + Library.foldr mk_all2 (xs, + Library.foldr mk_imp (mapn mk_prj 0 dnames, + foldr1 mk_conj (mapn mk_eqn 0 dnames))))); + fun x_tacs n x = [ + rotate_tac (n+1) 1, + etac all2E 1, + eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, + TRY (safe_tac HOL_cs), + REPEAT (CHANGED (asm_simp_tac take_ss 1))]; + val tacs = [ + rtac impI 1, + induct_tac "n" 1, + simp_tac take_ss 1, + safe_tac HOL_cs] @ + List.concat (mapn x_tacs 0 xs); + in pg [ax_bisim_def] goal tacs end; +in + val coind = + let + fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); + fun mk_eqn x = %:x === %:(x^"'"); + val goal = + mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> + Logic.list_implies (mapn mk_prj 0 xs, + mk_trp (foldr1 mk_conj (map mk_eqn xs))); + val tacs = + TRY (safe_tac HOL_cs) :: + List.concat (map (fn take_lemma => [ + rtac take_lemma 1, + cut_facts_tac [coind_lemma] 1, + fast_tac HOL_cs 1]) + take_lemmas); + in pg [] goal tacs end; +end; (* local *) + +in thy |> Theory.add_path comp_dnam + |> (snd o (PureThy.add_thmss (map Thm.no_attributes [ + ("take_rews" , take_rews ), + ("take_lemmas", take_lemmas), + ("finites" , finites ), + ("finite_ind", [finite_ind]), + ("ind" , [ind ]), + ("coind" , [coind ])]))) + |> Theory.parent_path |> rpair take_rews +end; (* let *) +end; (* local *) +end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/fixrec_package.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/fixrec_package.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,317 @@ +(* Title: HOLCF/Tools/fixrec_package.ML + ID: $Id$ + Author: Amber Telfer and Brian Huffman + +Recursive function definition package for HOLCF. +*) + +signature FIXREC_PACKAGE = +sig + val legacy_infer_term: theory -> term -> term + val legacy_infer_prop: theory -> term -> term + val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory + val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory + val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory + val add_fixpat_i: (string * attribute list) * term list -> theory -> theory +end; + +structure FixrecPackage: FIXREC_PACKAGE = +struct + +(* legacy type inference *) + +fun legacy_infer_term thy t = + singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t); + +fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT); + + +val fix_eq2 = thm "fix_eq2"; +val def_fix_ind = thm "def_fix_ind"; + + +fun fixrec_err s = error ("fixrec definition error:\n" ^ s); +fun fixrec_eq_err thy s eq = + fixrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq)); + +(* ->> is taken from holcf_logic.ML *) +(* TODO: fix dependencies so we can import HOLCFLogic here *) +infixr 6 ->>; +fun S ->> T = Type ("Cfun.->",[S,T]); + +(* extern_name is taken from domain/library.ML *) +fun extern_name con = case Symbol.explode con of + ("o"::"p"::" "::rest) => implode rest + | _ => con; + +val mk_trp = HOLogic.mk_Trueprop; + +(* splits a cterm into the right and lefthand sides of equality *) +fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); + +(* similar to Thm.head_of, but for continuous application *) +fun chead_of (Const("Cfun.Rep_CFun",_)$f$t) = chead_of f + | chead_of u = u; + +(* these are helpful functions copied from HOLCF/domain/library.ML *) +fun %: s = Free(s,dummyT); +fun %%: s = Const(s,dummyT); +infix 0 ==; fun S == T = %%:"==" $ S $ T; +infix 1 ===; fun S === T = %%:"op =" $ S $ T; +infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x; + +(* builds the expression (LAM v. rhs) *) +fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(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); + +(* builds the expression (LAM . rhs) *) +fun lambda_ctuple [] rhs = big_lambda (%:"unit") rhs + | lambda_ctuple (v::[]) rhs = big_lambda v rhs + | lambda_ctuple (v::vs) rhs = + %%:"Cprod.csplit"`(big_lambda v (lambda_ctuple vs rhs)); + +(* builds the expression *) +fun mk_ctuple [] = %%:"UU" +| mk_ctuple (t::[]) = t +| mk_ctuple (t::ts) = %%:"Cprod.cpair"`t`(mk_ctuple ts); + +(*************************************************************************) +(************* fixed-point definitions and unfolding theorems ************) +(*************************************************************************) + +fun add_fixdefs eqs thy = + let + val (lhss,rhss) = ListPair.unzip (map dest_eqs eqs); + val fixpoint = %%:"Fix.fix"`lambda_ctuple lhss (mk_ctuple rhss); + + fun one_def (l as Const(n,T)) r = + let val b = Sign.base_name n in (b, (b^"_def", l == r)) end + | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; + fun defs [] _ = [] + | defs (l::[]) r = [one_def l r] + | defs (l::ls) r = one_def l (%%:"Cprod.cfst"`r) :: defs ls (%%:"Cprod.csnd"`r); + val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint); + + val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs; + val (fixdef_thms, thy') = + PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy; + val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms; + + val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); + val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold + (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, + simp_tac (simpset_of thy') 1]); + val ctuple_induct_thm = + (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind); + + fun unfolds [] thm = [] + | unfolds (n::[]) thm = [(n^"_unfold", thm)] + | unfolds (n::ns) thm = let + val thmL = thm RS cpair_eqD1; + val thmR = thm RS cpair_eqD2; + in (n^"_unfold", thmL) :: unfolds ns thmR end; + val unfold_thms = unfolds names ctuple_unfold_thm; + val thms = ctuple_induct_thm :: unfold_thms; + val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy'; + in + (thy'', names, fixdef_thms, map snd unfold_thms) + end; + +(*************************************************************************) +(*********** monadic notation and pattern matching compilation ***********) +(*************************************************************************) + +fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs + | add_names (Free(a,_) , bs) = insert (op =) a bs + | add_names (f $ u , bs) = add_names (f, add_names(u, bs)) + | add_names (Abs(a,_,t), bs) = add_names (t, insert (op =) a bs) + | add_names (_ , bs) = bs; + +fun add_terms ts xs = foldr add_names xs ts; + +(* builds a monadic term for matching a constructor pattern *) +fun pre_build pat rhs vs taken = + case pat of + Const("Cfun.Rep_CFun",_)$f$(v as Free(n,T)) => + pre_build f rhs (v::vs) taken + | Const("Cfun.Rep_CFun",_)$f$x => + let val (rhs', v, taken') = pre_build x rhs [] taken; + in pre_build f rhs' (v::vs) taken' end + | Const(c,T) => + let + val n = Name.variant taken "v"; + fun result_type (Type("Cfun.->",[_,T])) (x::xs) = result_type T xs + | result_type T _ = T; + val v = Free(n, result_type T vs); + val m = "match_"^(extern_name(Sign.base_name c)); + val k = lambda_ctuple vs rhs; + in + (%%:"Fixrec.bind"`(%%:m`v)`k, v, n::taken) + end + | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n) + | _ => fixrec_err "pre_build: invalid pattern"; + +(* builds a monadic term for matching a function definition pattern *) +(* returns (name, arity, matcher) *) +fun building pat rhs vs taken = + case pat of + Const("Cfun.Rep_CFun", _)$f$(v as Free(n,T)) => + building f rhs (v::vs) taken + | Const("Cfun.Rep_CFun", _)$f$x => + let val (rhs', v, taken') = pre_build x rhs [] taken; + in building f rhs' (v::vs) taken' end + | Const(name,_) => (name, length vs, big_lambdas vs rhs) + | _ => fixrec_err "function is not declared as constant in theory"; + +fun match_eq eq = + let val (lhs,rhs) = dest_eqs eq; + in building lhs (%%:"Fixrec.return"`rhs) [] (add_terms [eq] []) end; + +(* returns the sum (using +++) of the terms in ms *) +(* also applies "run" to the result! *) +fun fatbar arity ms = + let + fun unLAM 0 t = t + | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t + | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; + fun reLAM 0 t = t + | reLAM n t = reLAM (n-1) (%%:"Cfun.Abs_CFun" $ Abs("",dummyT,t)); + fun mplus (x,y) = %%:"Fixrec.mplus"`x`y; + val msum = foldr1 mplus (map (unLAM arity) ms); + in + reLAM arity (%%:"Fixrec.run"`msum) + end; + +fun unzip3 [] = ([],[],[]) + | unzip3 ((x,y,z)::ts) = + let val (xs,ys,zs) = unzip3 ts + in (x::xs, y::ys, z::zs) end; + +(* this is the pattern-matching compiler function *) +fun compile_pats eqs = + let + val ((n::names),(a::arities),mats) = unzip3 (map match_eq eqs); + val cname = if forall (fn x => n=x) names then n + else fixrec_err "all equations in block must define the same function"; + val arity = if forall (fn x => a=x) arities then a + else fixrec_err "all equations in block must have the same arity"; + val rhs = fatbar arity mats; + in + mk_trp (%%:cname === rhs) + end; + +(*************************************************************************) +(********************** Proving associated theorems **********************) +(*************************************************************************) + +(* proves a block of pattern matching equations as theorems, using unfold *) +fun make_simps thy (unfold_thm, eqns) = + let + val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1]; + fun prove_term t = Goal.prove_global thy [] [] t (K (EVERY tacs)); + fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts); + in + map prove_eqn eqns + end; + +(*************************************************************************) +(************************* Main fixrec function **************************) +(*************************************************************************) + +fun gen_add_fixrec prep_prop prep_attrib strict blocks thy = + let + val eqns = List.concat blocks; + val lengths = map length blocks; + + val ((names, srcss), strings) = apfst split_list (split_list eqns); + val atts = map (map (prep_attrib thy)) srcss; + val eqn_ts = map (prep_prop thy) strings; + val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq))) + handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts; + val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts; + + fun unconcat [] _ = [] + | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n)); + val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts'); + val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks; + val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy; + in + if strict then let (* only prove simp rules if strict = true *) + val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts); + val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks)); + val (simp_thms, thy'') = PureThy.add_thms simps thy'; + + val simp_names = map (fn name => name^"_simps") cnames; + val simp_attribute = rpair [Simplifier.simp_add]; + val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms); + in + (snd o PureThy.add_thmss simps') thy'' + end + else thy' + end; + +val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute; +val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I); + + +(*************************************************************************) +(******************************** Fixpat *********************************) +(*************************************************************************) + +fun fix_pat thy t = + let + val T = fastype_of t; + val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); + val cname = case chead_of t of Const(c,_) => c | _ => + fixrec_err "function is not declared as constant in theory"; + val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold")); + val simp = Goal.prove_global thy [] [] eq + (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); + in simp end; + +fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = + let + val atts = map (prep_attrib thy) srcs; + val ts = map (prep_term thy) strings; + val simps = map (fix_pat thy) ts; + in + (snd o PureThy.add_thmss [((name, simps), atts)]) thy + end; + +val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute; +val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I); + + +(*************************************************************************) +(******************************** Parsers ********************************) +(*************************************************************************) + +local structure P = OuterParse and K = OuterKeyword in + +val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop; + +val fixrec_strict = P.opt_keyword "permissive" >> not; + +val fixrec_decl = fixrec_strict -- P.and_list1 (Scan.repeat1 fixrec_eqn); + +(* this builds a parser for a new keyword, fixrec, whose functionality +is defined by add_fixrec *) +val fixrecP = + OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl + (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec)); + +(* fixpat parser *) +val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop; + +val fixpatP = + OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl + (fixpat_decl >> (Toplevel.theory o add_fixpat)); + +val _ = OuterSyntax.add_parsers [fixrecP, fixpatP]; + +end; (* local structure *) + +end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/Tools/pcpodef_package.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/pcpodef_package.ML Thu May 31 14:01:58 2007 +0200 @@ -0,0 +1,213 @@ +(* Title: HOLCF/Tools/pcpodef_package.ML + ID: $Id$ + Author: Brian Huffman + +Primitive domain definitions for HOLCF, similar to Gordon/HOL-style +typedef. +*) + +signature PCPODEF_PACKAGE = +sig + val quiet_mode: bool ref + val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string + * (string * string) option -> theory -> Proof.state + val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term + * (string * string) option -> theory -> Proof.state + val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string + * (string * string) option -> theory -> Proof.state + val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term + * (string * string) option -> theory -> Proof.state +end; + +structure PcpodefPackage: PCPODEF_PACKAGE = +struct + +(** theory context references **) + +val typedef_po = thm "typedef_po"; +val typedef_cpo = thm "typedef_cpo"; +val typedef_pcpo = thm "typedef_pcpo"; +val typedef_lub = thm "typedef_lub"; +val typedef_thelub = thm "typedef_thelub"; +val typedef_compact = thm "typedef_compact"; +val cont_Rep = thm "typedef_cont_Rep"; +val cont_Abs = thm "typedef_cont_Abs"; +val Rep_strict = thm "typedef_Rep_strict"; +val Abs_strict = thm "typedef_Abs_strict"; +val Rep_defined = thm "typedef_Rep_defined"; +val Abs_defined = thm "typedef_Abs_defined"; + + +(** type definitions **) + +(* messages *) + +val quiet_mode = ref false; +fun message s = if ! quiet_mode then () else writeln s; + + +(* prepare_cpodef *) + +fun err_in_cpodef msg name = + cat_error msg ("The error(s) above occurred in cpodef " ^ quote name); + +fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); + +fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT); +fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); + +fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = + let + val ctxt = ProofContext.init thy; + val full = Sign.full_name thy; + + (*rhs*) + val full_name = full name; + val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; + val setT = Term.fastype_of set; + val rhs_tfrees = term_tfrees set; + val oldT = HOLogic.dest_setT setT handle TYPE _ => + error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT)); + fun mk_nonempty A = + HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)); + fun mk_admissible A = + mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)); + fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A); + val goal = if pcpo + then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set)) + else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set)); + + (*lhs*) + val defS = Sign.defaultS thy; + val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; + val lhs_sorts = map snd lhs_tfrees; + val tname = Syntax.type_name t mx; + val full_tname = full tname; + val newT = Type (full_tname, map TFree lhs_tfrees); + + val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs; + val RepC = Const (full Rep_name, newT --> oldT); + fun lessC T = Const ("Porder.<<", T --> T --> HOLogic.boolT); + val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT, + Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))); + + fun make_po tac theory = theory + |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac + ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"]) + (ClassPackage.intro_classes_tac []) + ||>> PureThy.add_defs_i true [Thm.no_attributes less_def] + |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) => + AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"]) + (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1) + #> pair (type_definition, less_definition, set_def)); + + fun make_cpo admissible (type_def, less_def, set_def) theory = + let + val admissible' = fold_rule (the_list set_def) admissible; + val cpo_thms = [type_def, less_def, admissible']; + in + theory + |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"]) + (Tactic.rtac (typedef_cpo OF cpo_thms) 1) + |> Theory.add_path name + |> PureThy.add_thms + ([(("adm_" ^ name, admissible'), []), + (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []), + (("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []), + (("lub_" ^ name, typedef_lub OF cpo_thms), []), + (("thelub_" ^ name, typedef_thelub OF cpo_thms), []), + (("compact_" ^ name, typedef_compact OF cpo_thms), [])]) + |> snd + |> Theory.parent_path + end; + + fun make_pcpo UUmem (type_def, less_def, set_def) theory = + let + val UUmem' = fold_rule (the_list set_def) UUmem; + val pcpo_thms = [type_def, less_def, UUmem']; + in + theory + |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"]) + (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1) + |> Theory.add_path name + |> PureThy.add_thms + ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []), + ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []), + ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []), + ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), []) + ]) + |> snd + |> Theory.parent_path + end; + + fun pcpodef_result UUmem_admissible theory = + let + val UUmem = UUmem_admissible RS conjunct1; + val admissible = UUmem_admissible RS conjunct2; + in + theory + |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1) + |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs) + end; + + fun cpodef_result nonempty_admissible theory = + let + val nonempty = nonempty_admissible RS conjunct1; + val admissible = nonempty_admissible RS conjunct2; + in + theory + |> make_po (Tactic.rtac nonempty 1) + |-> make_cpo admissible + end; + + in (goal, if pcpo then pcpodef_result else cpodef_result) end + handle ERROR msg => err_in_cpodef msg name; + + +(* cpodef_proof interface *) + +fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = + let + val (goal, pcpodef_result) = + prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; + fun after_qed [[th]] = ProofContext.theory (pcpodef_result th); + in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end; + +fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x; +fun pcpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term true x; + +fun cpodef_proof x = gen_pcpodef_proof ProofContext.read_term false x; +fun cpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term false x; + + +(** outer syntax **) + +local structure P = OuterParse and K = OuterKeyword in + +(* copied from HOL/Tools/typedef_package.ML *) +val typedef_proof_decl = + Scan.optional (P.$$$ "(" |-- + ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s))) + --| P.$$$ ")") (true, NONE) -- + (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)); + +fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = + (if pcpo then pcpodef_proof else cpodef_proof) + ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs); + +val pcpodefP = + OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal + (typedef_proof_decl >> + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))); + +val cpodefP = + OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal + (typedef_proof_decl >> + (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))); + +val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP]; + +end; + +end; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/adm_tac.ML --- a/src/HOLCF/adm_tac.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,180 +0,0 @@ -(* ID: $Id$ - Author: Stefan Berghofer, TU Muenchen - -Admissibility tactic. - -Checks whether adm_subst theorem is applicable to the current proof -state: - - [| cont t; adm P |] ==> adm (%x. P (t x)) - -"t" is instantiated with a term of chain-finite type, so that -adm_chfin can be applied: - - adm (P::'a::{chfin,pcpo} => bool) - -*) - -signature ADM = -sig - val adm_tac: (int -> tactic) -> int -> tactic -end; - -structure Adm: ADM = -struct - - -(*** find_subterms t 0 [] - returns lists of terms with the following properties: - 1. all terms in the list are disjoint subterms of t - 2. all terms contain the variable which is bound at level 0 - 3. all occurences of the variable which is bound at level 0 - are "covered" by a term in the list - a list of integers is associated with every term which describes - the "path" leading to the subterm (required for instantiation of - the adm_subst theorem (see functions mk_term, inst_adm_subst_thm)) -***) - -fun find_subterms (Bound i) lev path = - if i = lev then [[(Bound 0, path)]] - else [] - | find_subterms (t as (Abs (_, _, t2))) lev path = - if List.filter (fn x => x<=lev) - (add_loose_bnos (t, 0, [])) = [lev] then - [(incr_bv (~lev, 0, t), path)]:: - (find_subterms t2 (lev+1) (0::path)) - else find_subterms t2 (lev+1) (0::path) - | find_subterms (t as (t1 $ t2)) lev path = - let val ts1 = find_subterms t1 lev (0::path); - val ts2 = find_subterms t2 lev (1::path); - fun combine [] y = [] - | combine (x::xs) ys = - (map (fn z => x @ z) ys) @ (combine xs ys) - in - (if List.filter (fn x => x<=lev) - (add_loose_bnos (t, 0, [])) = [lev] then - [[(incr_bv (~lev, 0, t), path)]] - else []) @ - (if ts1 = [] then ts2 - else if ts2 = [] then ts1 - else combine ts1 ts2) - end - | find_subterms _ _ _ = []; - - -(*** make term for instantiation of predicate "P" in adm_subst theorem ***) - -fun make_term t path paths lev = - if path mem paths then Bound lev - else case t of - (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1)) - | (t1 $ t2) => (make_term t1 (0::path) paths lev) $ - (make_term t2 (1::path) paths lev) - | t1 => t1; - - -(*** check whether all terms in list are equal ***) - -fun eq_terms [] = true - | eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts; - - -(*figure out internal names*) -val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"]; -val cont_name = Sign.intern_const (the_context ()) "cont"; -val adm_name = Sign.intern_const (the_context ()) "adm"; - - -(*** check whether type of terms in list is chain finite ***) - -fun is_chfin sign T params ((t, _)::_) = - let val parTs = map snd (rev params) - in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end; - - -(*** try to prove that terms in list are continuous - if successful, add continuity theorem to list l ***) - -fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) = - let val parTs = map snd (rev params); - val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT; - fun mk_all [] t = t - | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t)); - val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t))); - val t' = mk_all params (Logic.list_implies (prems, t)); - val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1)); - in (ts, thm)::l end - handle ERROR _ => l; - - -(*** instantiation of adm_subst theorem (a bit tricky) ***) - -fun inst_adm_subst_thm state i params s T subt t paths = - let val {thy = sign, maxidx, ...} = rep_thm state; - val j = maxidx+1; - val parTs = map snd (rev params); - val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst; - val types = valOf o (fst (types_sorts rule)); - val tT = types ("t", j); - val PT = types ("P", j); - fun mk_abs [] t = t - | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t); - val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt); - val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))]) - (make_term t [] paths 0)); - val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty; - val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye; - val ctye = map (fn (ixn, (S, T)) => - (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye'); - val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT)); - val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT)); - val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule - in rule' end; - - -(*** extract subgoal i from proof state ***) - -fun nth_subgoal i thm = List.nth (prems_of thm, i-1); - - -(*** the admissibility tactic ***) - -fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) = - if name = adm_name then SOME abs else NONE - | try_dest_adm _ = NONE; - -fun adm_tac tac i state = - state |> - let val goali = nth_subgoal i state in - (case try_dest_adm (Logic.strip_assums_concl goali) of - NONE => no_tac - | SOME (s, T, t) => - let - val sign = Thm.theory_of_thm state; - val prems = Logic.strip_assums_hyp goali; - val params = Logic.strip_params goali; - val ts = find_subterms t 0 []; - val ts' = List.filter eq_terms ts; - val ts'' = List.filter (is_chfin sign T params) ts'; - val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts''); - in - (case thms of - ((ts as ((t', _)::_), cont_thm)::_) => - let - val paths = map snd ts; - val rule = inst_adm_subst_thm state i params s T t' t paths; - in - compose_tac (false, rule, 2) i THEN - rtac cont_thm i THEN - REPEAT (assume_tac i) THEN - rtac adm_chfin i - end - | [] => no_tac) - end) - end; - - -end; - - -open Adm; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/cont_consts.ML --- a/src/HOLCF/cont_consts.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,110 +0,0 @@ -(* Title: HOLCF/cont_consts.ML - ID: $Id$ - Author: Tobias Mayr, David von Oheimb, and Markus Wenzel - -HOLCF version of consts: handle continuous function types in mixfix -syntax. -*) - -signature CONT_CONSTS = -sig - val add_consts: (bstring * string * mixfix) list -> theory -> theory - val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory -end; - -structure ContConsts: CONT_CONSTS = -struct - - -(* misc utils *) - -open HOLCFLogic; - -fun first (x,_,_) = x; -fun second (_,x,_) = x; -fun third (_,_,x) = x; -fun upd_first f (x,y,z) = (f x, y, z); -fun upd_second f (x,y,z) = ( x, f y, z); -fun upd_third f (x,y,z) = ( x, y, f z); - -fun change_arrow 0 T = T -| change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T]) -| change_arrow _ _ = sys_error "cont_consts: change_arrow"; - -fun trans_rules name2 name1 n mx = let - fun argnames _ 0 = [] - | argnames c n = chr c::argnames (c+1) (n-1); - val vnames = argnames (ord "A") n; - val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); - in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), - Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") - [t,Variable arg])) - (Constant name1,vnames))] - @(case mx of InfixName _ => [extra_parse_rule] - | InfixlName _ => [extra_parse_rule] - | InfixrName _ => [extra_parse_rule] | _ => []) end; - - -(* transforming infix/mixfix declarations of constants with type ...->... - a declaration of such a constant is transformed to a normal declaration with - an internal name, the same type, and nofix. Additionally, a purely syntactic - declaration with the original name, type ...=>..., and the original mixfix - is generated and connected to the other declaration via some translation. -*) -fun fix_mixfix (syn , T, mx as Infix p ) = - (Syntax.const_name syn mx, T, InfixName (syn, p)) - | fix_mixfix (syn , T, mx as Infixl p ) = - (Syntax.const_name syn mx, T, InfixlName (syn, p)) - | fix_mixfix (syn , T, mx as Infixr p ) = - (Syntax.const_name syn mx, T, InfixrName (syn, p)) - | fix_mixfix decl = decl; -fun transform decl = let - val (c, T, mx) = fix_mixfix decl; - val c2 = "_cont_" ^ c; - val n = Syntax.mixfix_args mx - in ((c , T,NoSyn), - (c2,change_arrow n T,mx ), - trans_rules c2 c n mx) end; - -fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0 -| cfun_arity _ = 0; - -fun is_contconst (_,_,NoSyn ) = false -| is_contconst (_,_,Binder _) = false -| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx - handle ERROR msg => cat_error msg ("in mixfix annotation for " ^ - quote (Syntax.const_name c mx)); - - -(* add_consts(_i) *) - -fun gen_add_consts prep_typ raw_decls thy = - let - val decls = map (upd_second (prep_typ thy)) raw_decls; - val (contconst_decls, normal_decls) = List.partition is_contconst decls; - val transformed_decls = map transform contconst_decls; - in - thy - |> Sign.add_consts_i normal_decls - |> Sign.add_consts_i (map first transformed_decls) - |> Sign.add_syntax_i (map second transformed_decls) - |> Sign.add_trrules_i (List.concat (map third transformed_decls)) - end; - -val add_consts = gen_add_consts Sign.read_typ; -val add_consts_i = gen_add_consts Sign.certify_typ; - - -(* outer syntax *) - -local structure P = OuterParse and K = OuterKeyword in - -val constsP = - OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl - (Scan.repeat1 P.const >> (Toplevel.theory o add_consts)); - -val _ = OuterSyntax.add_parsers [constsP]; - -end; - -end; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/cont_proc.ML --- a/src/HOLCF/cont_proc.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,145 +0,0 @@ -(* Title: HOLCF/cont_proc.ML - ID: $Id$ - Author: Brian Huffman -*) - -signature CONT_PROC = -sig - val is_lcf_term: term -> bool - val cont_thms: term -> thm list - val all_cont_thms: term -> thm list - val cont_tac: int -> tactic - val cont_proc: theory -> simproc - val setup: theory -> theory -end; - -structure ContProc: CONT_PROC = -struct - -(** theory context references **) - -val cont_K = thm "cont_const"; -val cont_I = thm "cont_id"; -val cont_A = thm "cont2cont_Rep_CFun"; -val cont_L = thm "cont2cont_LAM"; -val cont_R = thm "cont_Rep_CFun2"; - -(* checks whether a term contains no dangling bound variables *) -val is_closed_term = - let - fun bound_less i (t $ u) = - bound_less i t andalso bound_less i u - | bound_less i (Abs (_, _, t)) = bound_less (i+1) t - | bound_less i (Bound n) = n < i - | bound_less i _ = true; (* Const, Free, and Var are OK *) - in bound_less 0 end; - -(* checks whether a term is written entirely in the LCF sublanguage *) -fun is_lcf_term (Const ("Cfun.Rep_CFun", _) $ t $ u) = - is_lcf_term t andalso is_lcf_term u - | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t - | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false - | is_lcf_term (Bound _) = true - | is_lcf_term t = is_closed_term t; - -(* - efficiently generates a cont thm for every LAM abstraction in a term, - using forward proof and reusing common subgoals -*) -local - fun var 0 = [SOME cont_I] - | var n = NONE :: var (n-1); - - fun k NONE = cont_K - | k (SOME x) = x; - - fun ap NONE NONE = NONE - | ap x y = SOME (k y RS (k x RS cont_A)); - - fun zip [] [] = [] - | zip [] (y::ys) = (ap NONE y ) :: zip [] ys - | zip (x::xs) [] = (ap x NONE) :: zip xs [] - | zip (x::xs) (y::ys) = (ap x y ) :: zip xs ys - - fun lam [] = ([], cont_K) - | lam (x::ys) = - let - (* should use "standard" for thms that are used multiple times *) - (* it seems to allow for sharing in explicit proof objects *) - val x' = standard (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 ("Cfun.Rep_CFun", _) $ f $ t) = - let - val (cs1,ls1) = cont_thms1 b f; - val (cs2,ls2) = cont_thms1 b t; - in (zip cs1 cs2, if b then ls1 @ ls2 else []) end - | cont_thms1 b (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = - let - val (cs, ls) = cont_thms1 b t; - val (cs', l) = lam cs; - in (cs', l::ls) end - | cont_thms1 _ (Bound n) = (var n, []) - | cont_thms1 _ _ = ([], []); -in - (* precondition: is_lcf_term t = true *) - fun cont_thms t = snd (cont_thms1 false t); - fun all_cont_thms t = snd (cont_thms1 true t); -end; - -(* - Given the term "cont f", the procedure tries to construct the - theorem "cont f == True". If this theorem cannot be completely - solved by the introduction rules, then the procedure returns a - conditional rewrite rule with the unsolved subgoals as premises. -*) - -local - val rules = [cont_K, cont_I, cont_R, cont_A, cont_L]; - - val prev_cont_thms : thm list ref = ref []; - - fun old_cont_tac i thm = - case !prev_cont_thms of - [] => no_tac thm - | (c::cs) => (prev_cont_thms := cs; rtac c i thm); - - fun new_cont_tac f' i thm = - case all_cont_thms f' of - [] => no_tac thm - | (c::cs) => (prev_cont_thms := cs; rtac c i thm); - - fun cont_tac_of_term (Const ("Cont.cont", _) $ f) = - let - val f' = Const ("Cfun.Abs_CFun", dummyT) $ f; - in - if is_lcf_term f' - then old_cont_tac ORELSE' new_cont_tac f' - else REPEAT_ALL_NEW (resolve_tac rules) - end - | cont_tac_of_term _ = K no_tac; -in - val cont_tac = - SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i); -end; - -local - fun solve_cont thy _ t = - let - 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 thy "cont_proc" ["cont f"] solve_cont; -end; - -val setup = - (fn thy => - (Simplifier.change_simpset_of thy - (fn ss => ss addsimprocs [cont_proc thy]); thy)); - -end; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,170 +0,0 @@ -(* Title: HOLCF/domain/axioms.ML - ID: $Id$ - Author: David von Oheimb - -Syntax generator for domain section. -*) - -structure Domain_Axioms = struct - -local - -open Domain_Library; -infixr 0 ===>;infixr 0 ==>;infix 0 == ; -infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; -infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; - -fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)= -let - -(* ----- axioms and definitions concerning the isomorphism ------------------ *) - - val dc_abs = %%:(dname^"_abs"); - val dc_rep = %%:(dname^"_rep"); - val x_name'= "x"; - val x_name = idx_name eqs x_name' (n+1); - val dnam = Sign.base_name dname; - - val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); - val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); - - val when_def = ("when_def",%%:(dname^"_when") == - foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => - Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); - - val copy_def = let - fun idxs z x arg = if is_rec arg - then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x) - else Bound(z-x); - fun one_con (con,args) = - foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args; - in ("copy_def", %%:(dname^"_copy") == - /\"f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end; - -(* -- definitions concerning the constructors, discriminators and selectors - *) - - fun con_def m n (_,args) = let - fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I) (Bound(z-x)); - fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); - fun inj y 1 _ = y - | inj y _ 0 = %%:sinlN`y - | inj y i j = %%:sinrN`(inj y (i-1) (j-1)); - in foldr /\# (dc_abs`(inj (parms args) m n)) args end; - - val con_defs = mapn (fn n => fn (con,args) => - (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; - - val dis_defs = let - fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (foldr /\# - (if con'=con then %%:TT_N else %%:FF_N) args)) cons)) - in map ddef cons end; - - val mat_defs = let - fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (foldr /\# - (if con'=con - then %%:returnN`(mk_ctuple (map (bound_arg args) args)) - else %%:failN) args)) cons)) - in map mdef cons end; - - val pat_defs = - let - fun pdef (con,args) = - let - val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - val xs = map (bound_arg args) args; - val r = Bound (length args); - val rhs = case args of [] => %%:returnN ` HOLogic.unit - | _ => foldr1 cpair_pat ps ` mk_ctuple xs; - fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args'; - in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == - list_ccomb(%%:(dname^"_when"), map one_con cons)) - end - in map pdef cons end; - - val sel_defs = let - fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => if con'<>con then UU else - foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); - in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; - - -(* ----- axiom and definitions concerning induction ------------------------- *) - - val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n - `%x_name === %:x_name)); - val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj - (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n)); - val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name, - mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); - -in (dnam, - [abs_iso_ax, rep_iso_ax, reach_ax], - [when_def, copy_def] @ - con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ - [take_def, finite_def]) -end; (* let *) - -fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy)); - -fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x); -fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; - -fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x); -fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; - -in (* local *) - -fun add_axioms (comp_dnam, eqs : eq list) thy' = let - val comp_dname = Sign.full_name thy' comp_dnam; - val dnames = map (fst o fst) eqs; - val x_name = idx_name dnames "x"; - fun copy_app dname = %%:(dname^"_copy")`Bound 0; - val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == - /\"f"(foldr1 cpair (map copy_app dnames))); - val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R", - let - fun one_con (con,args) = let - val nonrec_args = filter_out is_rec args; - val rec_args = List.filter is_rec args; - val recs_cnt = length rec_args; - val allargs = nonrec_args @ rec_args - @ map (upd_vname (fn s=> s^"'")) rec_args; - val allvns = map vname allargs; - fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; - val vns1 = map (vname_arg "" ) args; - val vns2 = map (vname_arg "'") args; - val allargs_cnt = length nonrec_args + 2*recs_cnt; - val rec_idxs = (recs_cnt-1) downto 0; - val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) - (allargs~~((allargs_cnt-1) downto 0))); - fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ - Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); - val capps = foldr mk_conj (mk_conj( - Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) - (mapn rel_app 1 rec_args); - in foldr mk_ex (Library.foldr mk_conj - (map (defined o Bound) nonlazy_idxs,capps)) allvns end; - fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( - proj (Bound 2) eqs n $ Bound 1 $ Bound 0, - foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) - ::map one_con cons)))); - in foldr1 mk_conj (mapn one_comp 0 eqs)end )); - fun add_one (thy,(dnam,axs,dfs)) = thy - |> Theory.add_path dnam - |> add_defs_infer dfs - |> add_axioms_infer axs - |> Theory.parent_path; - val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); -in thy |> Theory.add_path comp_dnam - |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) - |> Theory.parent_path -end; - -end; (* local *) -end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/domain/extender.ML --- a/src/HOLCF/domain/extender.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,183 +0,0 @@ -(* Title: HOLCF/domain/extender.ML - ID: $Id$ - Author: David von Oheimb - -Theory extender for domain section, including new-style theory syntax. - -###TODO: - -this definition -domain empty = silly empty -yields -Exception- - TERM - ("typ_of_term: bad encoding of type", - [Abs ("uu", "_", Const ("NONE", "_"))]) raised -but this works fine: -domain Empty = silly Empty - -strange syntax errors are produced for: -domain xx = xx ("x yy") -domain 'a foo = foo (sel::"'a") -and bar = bar ("'a dummy") - -*) - -signature DOMAIN_EXTENDER = -sig - val add_domain: string * ((bstring * string list) * - (string * mixfix * (bool * string option * string) list) list) list - -> theory -> theory - val add_domain_i: string * ((bstring * string list) * - (string * mixfix * (bool * string option * typ) list) list) list - -> theory -> theory -end; - -structure Domain_Extender: DOMAIN_EXTENDER = -struct - -open Domain_Library; - -(* ----- general testing and preprocessing of constructor list -------------- *) -fun check_and_sort_domain (dtnvs: (string * typ list) list, - cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg = - let - val defaultS = Sign.defaultS sg; - val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of - [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); - val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of - [] => false | dups => error ("Duplicate constructors: " - ^ commas_quote dups)); - val test_dupl_sels = (case duplicates (op =) (List.mapPartial second - (List.concat (map third (List.concat cons'')))) of - [] => false | dups => error("Duplicate selectors: "^commas_quote dups)); - val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of - [] => false | dups => error("Duplicate type arguments: " - ^commas_quote dups)) (map snd dtnvs); - (* test for free type variables, illegal sort constraints on rhs, - non-pcpo-types and invalid use of recursive type; - replace sorts in type variables on rhs *) - fun analyse_equation ((dname,typevars),cons') = - let - val tvars = map dest_TFree typevars; - val distinct_typevars = map TFree tvars; - fun rm_sorts (TFree(s,_)) = TFree(s,[]) - | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) - | rm_sorts (TVar(s,_)) = TVar(s,[]) - and remove_sorts l = map rm_sorts l; - val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] - fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of - NONE => error ("Free type variable " ^ quote v ^ " on rhs.") - | SOME sort => if eq_set_string (s,defaultS) orelse - eq_set_string (s,sort ) - then TFree(v,sort) - else error ("Inconsistent sort constraint" ^ - " for type variable " ^ quote v)) - | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of - NONE => if s mem indirect_ok - then Type(s,map (analyse false) typl) - else Type(s,map (analyse true) typl) - | SOME typevars => if indirect - then error ("Indirect recursion of type " ^ - quote (string_of_typ sg t)) - else if dname <> s orelse (** BUG OR FEATURE?: - mutual recursion may use different arguments **) - remove_sorts typevars = remove_sorts typl - then Type(s,map (analyse true) typl) - else error ("Direct recursion of type " ^ - quote (string_of_typ sg t) ^ - " with different arguments")) - | analyse indirect (TVar _) = Imposs "extender:analyse"; - fun check_pcpo T = if pcpo_type sg T then T - else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T); - val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false))); - in ((dname,distinct_typevars), map analyse_con cons') end; - in ListPair.map analyse_equation (dtnvs,cons'') - end; (* let *) - -(* ----- calls for building new thy and thms -------------------------------- *) - -fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' = - let - val dtnvs = map ((fn (dname,vs) => - (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs)) - o fst) eqs'''; - val cons''' = map snd eqs'''; - fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn); - fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS); - val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs) - |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs; - val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons'''; - val eqs' = check_and_sort_domain (dtnvs,cons'') thy''; - val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs'); - val dts = map (Type o fst) eqs'; - val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; - fun strip ss = Library.drop (find_index_eq "'" ss +1, ss); - fun typid (Type (id,_)) = - let val c = hd (Symbol.explode (Sign.base_name id)) - in if Symbol.is_letter c then c else "t" end - | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) - | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); - fun one_con (con,mx,args) = - ((Syntax.const_name con mx), - ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy, - find_index_eq tp dts, - DatatypeAux.dtyp_of_typ new_dts tp), - sel,vn)) - (args,(mk_var_names(map (typid o third) args))) - ) : cons; - val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list; - val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs); - val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) => - Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs)) - |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs); - in - theorems_thy - |> Theory.add_path (Sign.base_name comp_dnam) - |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])])) - |> Theory.parent_path - end; - -val add_domain_i = gen_add_domain Sign.certify_typ; -val add_domain = gen_add_domain Sign.read_typ; - - -(** outer syntax **) - -local structure P = OuterParse and K = OuterKeyword in - -val dest_decl = - P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- - (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1 - || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")" - >> (fn t => (true,NONE,t)) - || P.typ >> (fn t => (false,NONE,t)); - -val cons_decl = - P.name -- Scan.repeat dest_decl -- P.opt_mixfix - >> (fn ((c, ds), mx) => (c, mx, ds)); - -val type_var' = (P.type_ident ^^ - Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) ""); -val type_args' = type_var' >> single || - P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || - Scan.succeed []; - -val domain_decl = (type_args' -- P.name >> Library.swap) -- - (P.$$$ "=" |-- P.enum1 "|" cons_decl); -val domains_decl = - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl - >> (fn (opt_name, doms) => - (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms)); - -val domainP = - OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl - (domains_decl >> (Toplevel.theory o add_domain)); - - -val _ = OuterSyntax.add_keywords ["lazy"]; -val _ = OuterSyntax.add_parsers [domainP]; - -end; (* local structure *) - -end; diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,230 +0,0 @@ -(* Title: HOLCF/domain/library.ML - ID: $Id$ - Author: David von Oheimb - -Library for domain section. -*) - - -(* ----- general support ---------------------------------------------------- *) - -fun mapn f n [] = [] -| mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; - -fun foldr'' f (l,f2) = let fun itr [] = raise Fail "foldr''" - | itr [a] = f2 a - | itr (a::l) = f(a, itr l) -in itr l end; -fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => - (y::ys,res2)) ([],start) xs; - - -fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; -fun upd_first f (x,y,z) = (f x, y, z); -fun upd_second f (x,y,z) = ( x, f y, z); -fun upd_third f (x,y,z) = ( x, y, f z); - -fun atomize thm = let val r_inst = read_instantiate; - fun at thm = case concl_of thm of - _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) - | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec)) - | _ => [thm]; -in map zero_var_indexes (at thm) end; - -(* ----- specific support for domain ---------------------------------------- *) - -structure Domain_Library = struct - -open HOLCFLogic; - -exception Impossible of string; -fun Imposs msg = raise Impossible ("Domain:"^msg); - -(* ----- name handling ----- *) - -val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs - | strip ["'"] = [] - | strip (c :: cs) = c :: strip cs - | strip [] = []; -in implode o strip o Symbol.explode end; - -fun extern_name con = case Symbol.explode con of - ("o"::"p"::" "::rest) => implode rest - | _ => con; -fun dis_name con = "is_"^ (extern_name con); -fun dis_name_ con = "is_"^ (strip_esc con); -fun mat_name con = "match_"^ (extern_name con); -fun mat_name_ con = "match_"^ (strip_esc con); -fun pat_name con = (extern_name con) ^ "_pat"; -fun pat_name_ con = (strip_esc con) ^ "_pat"; - -(* make distinct names out of the type list, - forbidding "o","n..","x..","f..","P.." as names *) -(* a number string is added if necessary *) -fun mk_var_names ids : string list = let - fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; - fun index_vnames(vn::vns,occupied) = - (case AList.lookup (op =) occupied vn of - NONE => if vn mem vns - then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) - else vn :: index_vnames(vns, occupied) - | SOME(i) => (vn^(string_of_int (i+1))) - :: index_vnames(vns,(vn,i+1)::occupied)) - | index_vnames([],occupied) = []; -in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; - -fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS); -fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg; - -(* ----- constructor list handling ----- *) - -type cons = (string * (* operator name of constr *) - ((bool*int*DatatypeAux.dtyp)* (* (lazy,recursive element or ~1) *) - string option* (* selector name *) - string) (* argument name *) - list); (* argument list *) -type eq = (string * (* name of abstracted type *) - typ list) * (* arguments of abstracted type *) - cons list; (* represented type, as a constructor list *) - -fun rec_of arg = second (first arg); -fun is_lazy arg = first (first arg); -val sel_of = second; -val vname = third; -val upd_vname = upd_third; -fun is_rec arg = rec_of arg >=0; -fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); -fun nonlazy args = map vname (filter_out is_lazy args); -fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); - -(* ----- qualified names of HOLCF constants ----- *) - -val lessN = "Porder.<<" -val UU_N = "Pcpo.UU"; -val admN = "Adm.adm"; -val compactN = "Adm.compact"; -val Rep_CFunN = "Cfun.Rep_CFun"; -val Abs_CFunN = "Cfun.Abs_CFun"; -val ID_N = "Cfun.ID"; -val cfcompN = "Cfun.cfcomp"; -val strictifyN = "Cfun.strictify"; -val cpairN = "Cprod.cpair"; -val cfstN = "Cprod.cfst"; -val csndN = "Cprod.csnd"; -val csplitN = "Cprod.csplit"; -val spairN = "Sprod.spair"; -val sfstN = "Sprod.sfst"; -val ssndN = "Sprod.ssnd"; -val ssplitN = "Sprod.ssplit"; -val sinlN = "Ssum.sinl"; -val sinrN = "Ssum.sinr"; -val sscaseN = "Ssum.sscase"; -val upN = "Up.up"; -val fupN = "Up.fup"; -val ONE_N = "One.ONE"; -val TT_N = "Tr.TT"; -val FF_N = "Tr.FF"; -val iterateN = "Fix.iterate"; -val fixN = "Fix.fix"; -val returnN = "Fixrec.return"; -val failN = "Fixrec.fail"; -val cpair_patN = "Fixrec.cpair_pat"; -val branchN = "Fixrec.branch"; - -val pcpoN = "Pcpo.pcpo" -val pcpoS = [pcpoN]; - - -(* ----- support for type and mixfix expressions ----- *) - -infixr 5 -->; - -(* ----- support for term expressions ----- *) - -fun %: s = Free(s,dummyT); -fun %# arg = %:(vname arg); -fun %%: s = Const(s,dummyT); - -local open HOLogic in -val mk_trp = mk_Trueprop; -fun mk_conj (S,T) = conj $ S $ T; -fun mk_disj (S,T) = disj $ S $ T; -fun mk_imp (S,T) = imp $ S $ T; -fun mk_lam (x,T) = Abs(x,dummyT,T); -fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); -fun mk_ex (x,P) = mk_exists (x,dummyT,P); -fun mk_constrain (typ,T) = TypeInfer.constrain T typ; -fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (mk_lam(x,P)) (typ --> boolT)); -end - -fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) - -infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T; -infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T; -infix 0 ==; fun S == T = %%:"==" $ S $ T; -infix 1 ===; fun S === T = %%:"op =" $ S $ T; -infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); -infix 1 <<; fun S << T = %%:lessN $ S $ T; -infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T); - -infix 9 ` ; fun f` x = %%:Rep_CFunN $ f $ x; -infix 9 `% ; fun f`% s = f` %: s; -infix 9 `%%; fun f`%%s = f` %%:s; -val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *) -fun con_app2 con f args = list_ccomb(%%:con,map f args); -fun con_app con = con_app2 con %#; -fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; -fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg); -fun prj _ _ x ( _::[]) _ = x -| prj f1 _ x (_::y::ys) 0 = f1 x y -| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); -fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; -fun cproj x = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x; -fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); - -fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T); -fun /\# (arg,T) = /\ (vname arg) T; -infixr 9 oo; fun S oo T = %%:cfcompN`S`T; -val UU = %%:UU_N; -fun strict f = f`UU === UU; -fun defined t = t ~= UU; -fun cpair (t,u) = %%:cpairN`t`u; -fun spair (t,u) = %%:spairN`t`u; -fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) -| mk_ctuple ts = foldr1 cpair ts; -fun mk_stuple [] = %%:ONE_N -| mk_stuple ts = foldr1 spair ts; -fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) -| mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; -fun mk_maybeT T = Type ("Fixrec.maybe",[T]); -fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2; -fun lift_defined f = lift (fn x => defined (f x)); -fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); - -fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = - (case cont_eta_contract body of - body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => - if not (0 mem loose_bnos f) then incr_boundvars ~1 f - else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') - | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) -| cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t -| cont_eta_contract t = t; - -fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); -fun when_funs cons = if length cons = 1 then ["f"] - else mapn (fn n => K("f"^(string_of_int n))) 1 cons; -fun when_body cons funarg = let - fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) - | one_fun n (_,args) = let - val l2 = length args; - fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x - else I) (Bound(l2-m)); - in cont_eta_contract (foldr'' - (fn (a,t) => %%:ssplitN`(/\# (a,t))) - (args, - fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args)))) - ) end; -in (if length cons = 1 andalso length(snd(hd cons)) <= 1 - then fn t => %%:strictifyN`t else I) - (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end; -end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/domain/syntax.ML --- a/src/HOLCF/domain/syntax.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,151 +0,0 @@ -(* Title: HOLCF/domain/syntax.ML - ID: $Id$ - Author: David von Oheimb - -Syntax generator for domain section. -*) - -structure Domain_Syntax = struct - -local - -open Domain_Library; -infixr 5 -->; infixr 6 ->>; -fun calc_syntax dtypeprod ((dname, typevars), - (cons': (string * mixfix * (bool * string option * typ) list) list)) = -let -(* ----- constants concerning the isomorphism ------------------------------- *) - -local - fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t - fun prod (_,_,args) = if args = [] then oneT - else foldr1 mk_sprodT (map opt_lazy args); - fun freetvar s = let val tvar = mk_TFree s in - if tvar mem typevars then freetvar ("t"^s) else tvar end; - fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args); -in - val dtype = Type(dname,typevars); - val dtype2 = foldr1 mk_ssumT (map prod cons'); - val dnam = Sign.base_name dname; - val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); - val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); - val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); - val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); -end; - -(* ----- constants concerning constructors, discriminators, and selectors --- *) - -local - val escape = let - fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs - else c::esc cs - | esc [] = [] - in implode o esc o Symbol.explode end; - fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s); - fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT, - Mixfix(escape ("is_" ^ con), [], Syntax.max_pri)); - (* strictly speaking, these constants have one argument, - but the mixfix (without arguments) is introduced only - to generate parse rules for non-alphanumeric names*) - fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)), - Mixfix(escape ("match_" ^ con), [], Syntax.max_pri)); - fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; - fun sel (_ ,_,args) = List.mapPartial sel1 args; - fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in - if tvar mem typevars then freetvar ("t"^s) n else tvar end; - fun mk_patT (a,b) = a ->> mk_maybeT b; - fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n); - fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) ---> - mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), - Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri)); - -in - val consts_con = map con cons'; - val consts_dis = map dis cons'; - val consts_mat = map mat cons'; - val consts_pat = map pat cons'; - val consts_sel = List.concat(map sel cons'); -end; - -(* ----- constants concerning induction ------------------------------------- *) - - val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn); - val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn); - -(* ----- case translation --------------------------------------------------- *) - -local open Syntax in - local - fun c_ast con mx = Constant (const_name con mx); - fun expvar n = Variable ("e"^(string_of_int n)); - fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^ - (string_of_int m)); - fun argvars n args = mapn (argvar n) 1 args; - fun app s (l,r) = mk_appl (Constant s) [l,r]; - val cabs = app "_cabs"; - val capp = app "Rep_CFun"; - fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args); - fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n); - fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args); - fun when1 n m = if n = m then arg1 n else K (Constant "UU"); - - fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"]; - fun app_pat x = mk_appl (Constant "_pat") [x]; - fun args_list [] = Constant "Unity" - | args_list xs = foldr1 (app "_args") xs; - in - val case_trans = ParsePrintRule - (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), - capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); - - val abscon_trans = mapn (fn n => fn (con,mx,args) => ParsePrintRule - (cabs (con1 n (con,mx,args), expvar n), - Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons'; - - val Case_trans = List.concat (map (fn (con,mx,args) => - let - val cname = c_ast con mx; - val pname = Constant (pat_name_ con); - val ns = 1 upto length args; - val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; - val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; - val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; - in - [ParseRule (app_pat (Library.foldl capp (cname, xs)), - mk_appl pname (map app_pat xs)), - ParseRule (app_var (Library.foldl capp (cname, xs)), - app_var (args_list xs)), - PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), - app "_match" (mk_appl pname ps, args_list vs))] - end) cons'); - end; -end; - -in ([const_rep, const_abs, const_when, const_copy] @ - consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ - [const_take, const_finite], - (case_trans::(abscon_trans @ Case_trans))) -end; (* let *) - -(* ----- putting all the syntax stuff together ------------------------------ *) - -in (* local *) - -fun add_syntax (comp_dnam,eqs': ((string * typ list) * - (string * mixfix * (bool * string option * typ) list) list) list) thy'' = -let - val dtypes = map (Type o fst) eqs'; - val boolT = HOLogic.boolT; - val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes); - val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); - val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn); - val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn); - val ctt = map (calc_syntax funprod) eqs'; -in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ - (if length eqs'>1 then [const_copy] else[])@ - [const_bisim]) - |> Sign.add_trrules_i (List.concat(map snd ctt)) -end; (* let *) - -end; (* local *) -end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,951 +0,0 @@ -(* Title: HOLCF/domain/theorems.ML - ID: $Id$ - Author: David von Oheimb - New proofs/tactics by Brian Huffman - -Proof generator for domain section. -*) - -val HOLCF_ss = simpset(); - -structure Domain_Theorems = struct - -local - -val adm_impl_admw = thm "adm_impl_admw"; -val antisym_less_inverse = thm "antisym_less_inverse"; -val beta_cfun = thm "beta_cfun"; -val cfun_arg_cong = thm "cfun_arg_cong"; -val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; -val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; -val chain_iterate = thm "chain_iterate"; -val compact_ONE = thm "compact_ONE"; -val compact_sinl = thm "compact_sinl"; -val compact_sinr = thm "compact_sinr"; -val compact_spair = thm "compact_spair"; -val compact_up = thm "compact_up"; -val contlub_cfun_arg = thm "contlub_cfun_arg"; -val contlub_cfun_fun = thm "contlub_cfun_fun"; -val fix_def2 = thm "fix_def2"; -val injection_eq = thm "injection_eq"; -val injection_less = thm "injection_less"; -val lub_equal = thm "lub_equal"; -val monofun_cfun_arg = thm "monofun_cfun_arg"; -val retraction_strict = thm "retraction_strict"; -val spair_eq = thm "spair_eq"; -val spair_less = thm "spair_less"; -val sscase1 = thm "sscase1"; -val ssplit1 = thm "ssplit1"; -val strictify1 = thm "strictify1"; -val wfix_ind = thm "wfix_ind"; - -open Domain_Library; -infixr 0 ===>; -infixr 0 ==>; -infix 0 == ; -infix 1 ===; -infix 1 ~= ; -infix 1 <<; -infix 1 ~<<; -infix 9 ` ; -infix 9 `% ; -infix 9 `%%; -infixr 9 oo; - -(* ----- general proof facilities ------------------------------------------- *) - -fun pg'' thy defs t tacs = - let - val t' = FixrecPackage.legacy_infer_term thy t; - val asms = Logic.strip_imp_prems t'; - val prop = Logic.strip_imp_concl t'; - fun tac prems = - rewrite_goals_tac defs THEN - EVERY (tacs (map (rewrite_rule defs) prems)); - in Goal.prove_global thy [] asms prop tac end; - -fun pg' thy defs t tacsf = - let - fun tacs [] = tacsf - | tacs prems = cut_facts_tac prems 1 :: tacsf; - in pg'' thy defs t tacs end; - -fun case_UU_tac rews i v = - case_tac (v^"=UU") i THEN - asm_simp_tac (HOLCF_ss addsimps rews) i; - -val chain_tac = - REPEAT_DETERM o resolve_tac - [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL]; - -(* ----- general proofs ----------------------------------------------------- *) - -val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R" - (fn prems =>[ - resolve_tac prems 1, - cut_facts_tac prems 1, - fast_tac HOL_cs 1]); - -val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" - (fn prems => - [blast_tac (claset () addDs [antisym_less_inverse]) 1]); - -in - -fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = -let - -val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ..."); -val pg = pg' thy; - -(* ----- getting the axioms and definitions --------------------------------- *) - -local - fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)); -in - val ax_abs_iso = ga "abs_iso" dname; - val ax_rep_iso = ga "rep_iso" dname; - val ax_when_def = ga "when_def" dname; - fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname; - val axs_con_def = map (get_def extern_name) cons; - val axs_dis_def = map (get_def dis_name) cons; - val axs_mat_def = map (get_def mat_name) cons; - val axs_pat_def = map (get_def pat_name) cons; - val axs_sel_def = - let - fun def_of_sel sel = ga (sel^"_def") dname; - fun def_of_arg arg = Option.map def_of_sel (sel_of arg); - fun defs_of_con (_, args) = List.mapPartial def_of_arg args; - in - List.concat (map defs_of_con cons) - end; - val ax_copy_def = ga "copy_def" dname; -end; (* local *) - -(* ----- theorems concerning the isomorphism -------------------------------- *) - -val dc_abs = %%:(dname^"_abs"); -val dc_rep = %%:(dname^"_rep"); -val dc_copy = %%:(dname^"_copy"); -val x_name = "x"; - -val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso]; -val abs_strict = ax_rep_iso RS (allI RS retraction_strict); -val rep_strict = ax_abs_iso RS (allI RS retraction_strict); -val abs_defin' = iso_locale RS iso_abs_defin'; -val rep_defin' = iso_locale RS iso_rep_defin'; -val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict]; - -(* ----- generating beta reduction rules from definitions-------------------- *) - -local - fun arglist (Const _ $ Abs (s, _, t)) = - let - val (vars,body) = arglist t; - in (s :: vars, body) end - | arglist t = ([], t); - fun bind_fun vars t = Library.foldr mk_All (vars, t); - fun bound_vars 0 = [] - | bound_vars i = Bound (i-1) :: bound_vars (i - 1); -in - fun appl_of_def def = - let - val (_ $ con $ lam) = concl_of def; - val (vars, rhs) = arglist lam; - val lhs = list_ccomb (con, bound_vars (length vars)); - val appl = bind_fun vars (lhs == rhs); - val cs = ContProc.cont_thms lam; - val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs; - in pg (def::betas) appl [rtac reflexive_thm 1] end; -end; - -val when_appl = appl_of_def ax_when_def; -val con_appls = map appl_of_def axs_con_def; - -local - fun arg2typ n arg = - let val t = TVar (("'a", n), pcpoS) - in (n + 1, if is_lazy arg then mk_uT t else t) end; - - fun args2typ n [] = (n, oneT) - | args2typ n [arg] = arg2typ n arg - | args2typ n (arg::args) = - let - val (n1, t1) = arg2typ n arg; - val (n2, t2) = args2typ n1 args - 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 (n2, t2) = cons2typ n1 cons - in (n2, mk_ssumT (t1, t2)) end; -in - fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons)); -end; - -local - val iso_swap = iso_locale RS iso_iso_swap; - fun one_con (con, args) = - let - val vns = map vname args; - val eqn = %:x_name === con_app2 con %: vns; - val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args)); - in Library.foldr mk_ex (vns, conj) end; - - val conj_assoc = thm "conj_assoc"; - val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons); - val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start; - val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1; - val thm3 = rewrite_rule [mk_meta_eq conj_assoc] thm2; - - (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) - val tacs = [ - rtac disjE 1, - etac (rep_defin' RS disjI1) 2, - etac disjI2 2, - rewrite_goals_tac [mk_meta_eq iso_swap], - rtac thm3 1]; -in - val exhaust = pg con_appls (mk_trp exh) tacs; - val casedist = - standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0)); -end; - -local - fun bind_fun t = Library.foldr mk_All (when_funs cons, t); - fun bound_fun i _ = Bound (length cons - i); - val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons); -in - val when_strict = - let - val axs = [when_appl, mk_meta_eq rep_strict]; - val goal = bind_fun (mk_trp (strict when_app)); - val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1]; - in pg axs goal tacs end; - - val when_apps = - let - fun one_when n (con,args) = - let - val axs = when_appl :: con_appls; - val goal = bind_fun (lift_defined %: (nonlazy args, - mk_trp (when_app`(con_app con args) === - list_ccomb (bound_fun n 0, map %# args)))); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1]; - in pg axs goal tacs end; - in mapn one_when 1 cons end; -end; -val when_rews = when_strict :: when_apps; - -(* ----- theorems concerning the constructors, discriminators and selectors - *) - -local - fun dis_strict (con, _) = - let - val goal = mk_trp (strict (%%:(dis_name con))); - in pg axs_dis_def goal [rtac when_strict 1] end; - - fun dis_app c (con, args) = - let - val lhs = %%:(dis_name c) ` con_app con args; - val rhs = %%:(if con = c then TT_N else FF_N); - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_dis_def goal tacs end; - - val dis_apps = List.concat (map (fn (c,_) => map (dis_app c) cons) cons); - - fun dis_defin (con, args) = - let - val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name); - val tacs = - [rtac casedist 1, - contr_tac 1, - DETERM_UNTIL_SOLVED (CHANGED - (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))]; - in pg [] goal tacs end; - - val dis_stricts = map dis_strict cons; - val dis_defins = map dis_defin cons; -in - val dis_rews = dis_stricts @ dis_defins @ dis_apps; -end; - -local - fun mat_strict (con, _) = - let - val goal = mk_trp (strict (%%:(mat_name con))); - val tacs = [rtac when_strict 1]; - in pg axs_mat_def goal tacs end; - - val mat_stricts = map mat_strict cons; - - fun one_mat c (con, args) = - let - val lhs = %%:(mat_name c) ` con_app con args; - val rhs = - if con = c - then %%:returnN ` mk_ctuple (map %# args) - else %%:failN; - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_mat_def goal tacs end; - - val mat_apps = - List.concat (map (fn (c,_) => map (one_mat c) cons) cons); -in - val mat_rews = mat_stricts @ mat_apps; -end; - -local - fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - - fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args); - - fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit) - | pat_rhs (con,args) = - (%%:branchN $ foldr1 cpair_pat (ps args)) - `(%:"rhs")`(mk_ctuple (map %# args)); - - fun pat_strict c = - let - val axs = branch_def :: axs_pat_def; - val goal = mk_trp (strict (pat_lhs c ` (%:"rhs"))); - val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1]; - in pg axs goal tacs end; - - fun pat_app c (con, args) = - let - val axs = branch_def :: axs_pat_def; - val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args); - val rhs = if con = fst c then pat_rhs c else %%:failN; - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs goal tacs end; - - val pat_stricts = map pat_strict cons; - val pat_apps = List.concat (map (fn c => map (pat_app c) cons) cons); -in - val pat_rews = pat_stricts @ pat_apps; -end; - -local - val rev_contrapos = thm "rev_contrapos"; - fun con_strict (con, args) = - let - fun one_strict vn = - let - fun f arg = if vname arg = vn then UU else %# arg; - val goal = mk_trp (con_app2 con f args === UU); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]; - in pg con_appls goal tacs end; - in map one_strict (nonlazy args) end; - - fun con_defin (con, args) = - let - val concl = mk_trp (defined (con_app con args)); - val goal = lift_defined %: (nonlazy args, concl); - val tacs = [ - rtac rev_contrapos 1, - eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1, - asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; - in pg [] goal tacs end; -in - val con_stricts = List.concat (map con_strict cons); - val con_defins = map con_defin cons; - val con_rews = con_stricts @ con_defins; -end; - -local - val rules = - [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE]; - fun con_compact (con, args) = - let - val concl = mk_trp (%%:compactN $ con_app con args); - val goal = lift (fn x => %%:compactN $ %#x) (args, concl); - val tacs = [ - rtac (iso_locale RS iso_compact_abs) 1, - REPEAT (resolve_tac rules 1 ORELSE atac 1)]; - in pg con_appls goal tacs end; -in - val con_compacts = map con_compact cons; -end; - -local - fun one_sel sel = - pg axs_sel_def (mk_trp (strict (%%:sel))) - [simp_tac (HOLCF_ss addsimps when_rews) 1]; - - fun sel_strict (_, args) = - List.mapPartial (Option.map one_sel o sel_of) args; -in - val sel_stricts = List.concat (map sel_strict cons); -end; - -local - fun sel_app_same c n sel (con, args) = - let - val nlas = nonlazy args; - val vns = map vname args; - val vnn = List.nth (vns, n); - val nlas' = List.filter (fn v => v <> vnn) nlas; - val lhs = (%%:sel)`(con_app con args); - val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn)); - val tacs1 = - if vnn mem nlas - then [case_UU_tac (when_rews @ con_stricts) 1 vnn] - else []; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_sel_def goal (tacs1 @ tacs2) end; - - fun sel_app_diff c n sel (con, args) = - let - val nlas = nonlazy args; - val goal = mk_trp (%%:sel ` con_app con args === UU); - val tacs1 = map (case_UU_tac (when_rews @ con_stricts) 1) nlas; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_sel_def goal (tacs1 @ tacs2) end; - - fun sel_app c n sel (con, args) = - if con = c - then sel_app_same c n sel (con, args) - else sel_app_diff c n sel (con, args); - - fun one_sel c n sel = map (sel_app c n sel) cons; - fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg); - fun one_con (c, args) = - List.concat (List.mapPartial I (mapn (one_sel' c) 0 args)); -in - val sel_apps = List.concat (map one_con cons); -end; - -local - fun sel_defin sel = - let - val goal = defined (%:x_name) ==> defined (%%:sel`%x_name); - val tacs = [ - rtac casedist 1, - contr_tac 1, - DETERM_UNTIL_SOLVED (CHANGED - (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))]; - in pg [] goal tacs end; -in - val sel_defins = - if length cons = 1 - then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg)) - (filter_out is_lazy (snd (hd cons))) - else []; -end; - -val sel_rews = sel_stricts @ sel_defins @ sel_apps; -val rev_contrapos = thm "rev_contrapos"; - -val distincts_le = - let - fun dist (con1, args1) (con2, args2) = - let - val goal = lift_defined %: (nonlazy args1, - mk_trp (con_app con1 args1 ~<< con_app con2 args2)); - val tacs = [ - rtac rev_contrapos 1, - eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1] - @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2) - @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; - in pg [] goal tacs end; - - fun distinct (con1, args1) (con2, args2) = - let - val arg1 = (con1, args1); - val arg2 = - (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) - (args2, Name.variant_list (map vname args1) (map vname args2))); - in [dist arg1 arg2, dist arg2 arg1] end; - fun distincts [] = [] - | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; - in distincts cons end; -val dist_les = List.concat (List.concat distincts_le); -val dist_eqs = - let - fun distinct (_,args1) ((_,args2), leqs) = - let - val (le1,le2) = (hd leqs, hd(tl leqs)); - val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) - in - if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else - if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else - [eq1, eq2] - end; - fun distincts [] = [] - | distincts ((c,leqs)::cs) = List.concat - (ListPair.map (distinct c) ((map #1 cs),leqs)) @ - distincts cs; - in map standard (distincts (cons ~~ distincts_le)) end; - -local - fun pgterm rel con args = - let - fun append s = upd_vname (fn v => v^s); - val (largs, rargs) = (args, map (append "'") args); - val concl = - foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)); - val prem = rel (con_app con largs, con_app con rargs); - val sargs = case largs of [_] => [] | _ => nonlazy args; - val prop = lift_defined %: (sargs, mk_trp (prem === concl)); - in pg con_appls prop end; - val cons' = List.filter (fn (_,args) => args<>[]) cons; -in - val inverts = - let - val abs_less = ax_abs_iso RS (allI RS injection_less); - val tacs = - [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1]; - in map (fn (con, args) => pgterm (op <<) con args tacs) cons' end; - - val injects = - let - val abs_eq = ax_abs_iso RS (allI RS injection_eq); - val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1]; - in map (fn (con, args) => pgterm (op ===) con args tacs) cons' end; -end; - -(* ----- theorems concerning one induction step ----------------------------- *) - -val copy_strict = - let - val goal = mk_trp (strict (dc_copy `% "f")); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1]; - in pg [ax_copy_def] goal tacs end; - -local - fun copy_app (con, args) = - let - val lhs = dc_copy`%"f"`(con_app con args); - val rhs = con_app2 con (app_rec_arg (cproj (%:"f") eqs)) args; - val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); - val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args; - val stricts = abs_strict::when_strict::con_stricts; - val tacs1 = map (case_UU_tac stricts 1 o vname) args'; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1]; - in pg [ax_copy_def] goal (tacs1 @ tacs2) end; -in - val copy_apps = map copy_app cons; -end; - -local - fun one_strict (con, args) = - let - val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); - val rews = copy_strict :: copy_apps @ con_rews; - val tacs = map (case_UU_tac rews 1) (nonlazy args) @ - [asm_simp_tac (HOLCF_ss addsimps rews) 1]; - in pg [] goal tacs end; - - fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args; -in - val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons); -end; - -val copy_rews = copy_strict :: copy_apps @ copy_stricts; - -in - thy - |> Theory.add_path (Sign.base_name dname) - |> (snd o (PureThy.add_thmss (map Thm.no_attributes [ - ("iso_rews" , iso_rews ), - ("exhaust" , [exhaust] ), - ("casedist" , [casedist]), - ("when_rews", when_rews ), - ("compacts", con_compacts), - ("con_rews", con_rews), - ("sel_rews", sel_rews), - ("dis_rews", dis_rews), - ("pat_rews", pat_rews), - ("dist_les", dist_les), - ("dist_eqs", dist_eqs), - ("inverts" , inverts ), - ("injects" , injects ), - ("copy_rews", copy_rews)]))) - |> (snd o PureThy.add_thmss - [(("match_rews", mat_rews), [Simplifier.simp_add])]) - |> Theory.parent_path - |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ - pat_rews @ dist_les @ dist_eqs @ copy_rews) -end; (* let *) - -fun comp_theorems (comp_dnam, eqs: eq list) thy = -let -val dnames = map (fst o fst) eqs; -val conss = map snd eqs; -val comp_dname = Sign.full_name thy comp_dnam; - -val d = writeln("Proving induction properties of domain "^comp_dname^" ..."); -val pg = pg' thy; - -(* ----- getting the composite axiom and definitions ------------------------ *) - -local - fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)); -in - val axs_reach = map (ga "reach" ) dnames; - val axs_take_def = map (ga "take_def" ) dnames; - val axs_finite_def = map (ga "finite_def") dnames; - val ax_copy2_def = ga "copy_def" comp_dnam; - val ax_bisim_def = ga "bisim_def" comp_dnam; -end; - -local - fun gt s dn = get_thm thy (Name (dn ^ "." ^ s)); - fun gts s dn = get_thms thy (Name (dn ^ "." ^ s)); -in - val cases = map (gt "casedist" ) dnames; - val con_rews = List.concat (map (gts "con_rews" ) dnames); - val copy_rews = List.concat (map (gts "copy_rews") dnames); -end; - -fun dc_take dn = %%:(dn^"_take"); -val x_name = idx_name dnames "x"; -val P_name = idx_name dnames "P"; -val n_eqs = length eqs; - -(* ----- theorems concerning finite approximation and finite induction ------ *) - -local - val iterate_Cprod_ss = simpset_of (theory "Fix"); - val copy_con_rews = copy_rews @ con_rews; - val copy_take_defs = - (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; - val take_stricts = - let - fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n"); - val goal = mk_trp (foldr1 mk_conj (map one_eq eqs)); - val tacs = [ - induct_tac "n" 1, - simp_tac iterate_Cprod_ss 1, - asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1]; - in pg copy_take_defs goal tacs end; - - val take_stricts' = rewrite_rule copy_take_defs take_stricts; - fun take_0 n dn = - let - val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU); - in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end; - val take_0s = mapn take_0 1 dnames; - val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1; - val take_apps = - let - fun mk_eqn dn (con, args) = - let - fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; - val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); - val rhs = con_app2 con (app_rec_arg mk_take) args; - in Library.foldr mk_all (map vname args, lhs === rhs) end; - fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; - val goal = mk_trp (foldr1 mk_conj (List.concat (map mk_eqns eqs))); - val simps = List.filter (has_fewer_prems 1) copy_rews; - fun con_tac (con, args) = - if nonlazy_rec args = [] - then all_tac - else EVERY (map c_UU_tac (nonlazy_rec args)) THEN - asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; - fun eq_tacs ((dn, _), cons) = map con_tac cons; - val tacs = - simp_tac iterate_Cprod_ss 1 :: - induct_tac "n" 1 :: - simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 :: - asm_full_simp_tac (HOLCF_ss addsimps simps) 1 :: - TRY (safe_tac HOL_cs) :: - List.concat (map eq_tacs eqs); - in pg copy_take_defs goal tacs end; -in - val take_rews = map standard - (atomize take_stricts @ take_0s @ atomize take_apps); -end; (* local *) - -local - fun one_con p (con,args) = - let - fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; - val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); - val t2 = lift ind_hyp (List.filter is_rec args, t1); - val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2); - in Library.foldr mk_All (map vname args, t3) end; - - fun one_eq ((p, cons), concl) = - mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); - - fun ind_term concf = Library.foldr one_eq - (mapn (fn n => fn x => (P_name n, x)) 1 conss, - mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); - val take_ss = HOL_ss addsimps take_rews; - fun quant_tac i = EVERY - (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames); - - fun ind_prems_tac prems = EVERY - (List.concat (map (fn cons => - (resolve_tac prems 1 :: - List.concat (map (fn (_,args) => - resolve_tac prems 1 :: - map (K(atac 1)) (nonlazy args) @ - map (K(atac 1)) (List.filter is_rec args)) - cons))) - conss)); - local - (* check whether every/exists constructor of the n-th part of the equation: - it has a possibly indirectly recursive argument that isn't/is possibly - indirectly lazy *) - fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => - is_rec arg andalso not(rec_of arg mem ns) andalso - ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse - rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) - (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) - ) o snd) cons; - fun all_rec_to ns = rec_to forall not all_rec_to ns; - fun warn (n,cons) = - if all_rec_to [] false (n,cons) - then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) - else false; - fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns; - - in - val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; - val is_emptys = map warn n__eqs; - val is_finite = forall (not o lazy_rec_to [] false) n__eqs; - end; -in (* local *) - val finite_ind = - let - fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n)); - val goal = ind_term concf; - - fun tacf prems = - let - val tacs1 = [ - quant_tac 1, - simp_tac HOL_ss 1, - induct_tac "n" 1, - simp_tac (take_ss addsimps prems) 1, - TRY (safe_tac HOL_cs)]; - fun arg_tac arg = - case_UU_tac (prems @ con_rews) 1 - (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); - fun con_tacs (con, args) = - asm_simp_tac take_ss 1 :: - map arg_tac (List.filter is_nonlazy_rec args) @ - [resolve_tac prems 1] @ - map (K (atac 1)) (nonlazy args) @ - map (K (etac spec 1)) (List.filter is_rec args); - fun cases_tacs (cons, cases) = - res_inst_tac [("x","x")] cases 1 :: - asm_simp_tac (take_ss addsimps prems) 1 :: - List.concat (map con_tacs cons); - in - tacs1 @ List.concat (map cases_tacs (conss ~~ cases)) - end; - in pg'' thy [] goal tacf end; - - val take_lemmas = - let - fun take_lemma n (dn, ax_reach) = - let - val lhs = dc_take dn $ Bound 0 `%(x_name n); - val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); - val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); - val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; - fun tacf prems = [ - res_inst_tac [("t", x_name n )] (ax_reach RS subst) 1, - res_inst_tac [("t", x_name n^"'")] (ax_reach RS subst) 1, - stac fix_def2 1, - REPEAT (CHANGED - (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)), - stac contlub_cfun_fun 1, - stac contlub_cfun_fun 2, - rtac lub_equal 3, - chain_tac 1, - rtac allI 1, - resolve_tac prems 1]; - in pg'' thy axs_take_def goal tacf end; - in mapn take_lemma 1 (dnames ~~ axs_reach) end; - -(* ----- theorems concerning finiteness and induction ----------------------- *) - - val (finites, ind) = - if is_finite - then (* finite case *) - let - fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x"); - fun dname_lemma dn = - let - val prem1 = mk_trp (defined (%:"x")); - val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU); - val prem2 = mk_trp (mk_disj (disj1, take_enough dn)); - val concl = mk_trp (take_enough dn); - val goal = prem1 ===> prem2 ===> concl; - val tacs = [ - etac disjE 1, - etac notE 1, - resolve_tac take_lemmas 1, - asm_simp_tac take_ss 1, - atac 1]; - in pg [] goal tacs end; - val finite_lemmas1a = map dname_lemma dnames; - - val finite_lemma1b = - let - fun mk_eqn n ((dn, args), _) = - let - val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU; - val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0; - in - mk_constrainall - (x_name n, Type (dn,args), mk_disj (disj1, disj2)) - end; - val goal = - mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs))); - fun arg_tacs vn = [ - eres_inst_tac [("x", vn)] all_dupE 1, - etac disjE 1, - asm_simp_tac (HOL_ss addsimps con_rews) 1, - asm_simp_tac take_ss 1]; - fun con_tacs (con, args) = - asm_simp_tac take_ss 1 :: - List.concat (map arg_tacs (nonlazy_rec args)); - fun foo_tacs n (cons, cases) = - simp_tac take_ss 1 :: - rtac allI 1 :: - res_inst_tac [("x",x_name n)] cases 1 :: - asm_simp_tac take_ss 1 :: - List.concat (map con_tacs cons); - val tacs = - rtac allI 1 :: - induct_tac "n" 1 :: - simp_tac take_ss 1 :: - TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) :: - List.concat (mapn foo_tacs 1 (conss ~~ cases)); - in pg [] goal tacs end; - - fun one_finite (dn, l1b) = - let - val goal = mk_trp (%%:(dn^"_finite") $ %:"x"); - val tacs = [ - case_UU_tac take_rews 1 "x", - eresolve_tac finite_lemmas1a 1, - step_tac HOL_cs 1, - step_tac HOL_cs 1, - cut_facts_tac [l1b] 1, - fast_tac HOL_cs 1]; - in pg axs_finite_def goal tacs end; - - val finites = map one_finite (dnames ~~ atomize finite_lemma1b); - val ind = - let - fun concf n dn = %:(P_name n) $ %:(x_name n); - fun tacf prems = - let - fun finite_tacs (finite, fin_ind) = [ - rtac(rewrite_rule axs_finite_def finite RS exE)1, - etac subst 1, - rtac fin_ind 1, - ind_prems_tac prems]; - in - TRY (safe_tac HOL_cs) :: - List.concat (map finite_tacs (finites ~~ atomize finite_ind)) - end; - in pg'' thy [] (ind_term concf) tacf end; - in (finites, ind) end (* let *) - - else (* infinite case *) - let - fun one_finite n dn = - read_instantiate_sg thy - [("P",dn^"_finite "^x_name n)] excluded_middle; - val finites = mapn one_finite 1 dnames; - - val goal = - let - fun one_adm n _ = mk_trp (%%:admN $ %:(P_name n)); - fun concf n dn = %:(P_name n) $ %:(x_name n); - in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; - fun tacf prems = - map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ - quant_tac 1, - rtac (adm_impl_admw RS wfix_ind) 1, - REPEAT_DETERM (rtac adm_all2 1), - REPEAT_DETERM ( - TRY (rtac adm_conj 1) THEN - rtac adm_subst 1 THEN - cont_tacR 1 THEN resolve_tac prems 1), - strip_tac 1, - rtac (rewrite_rule axs_take_def finite_ind) 1, - ind_prems_tac prems]; - val ind = (pg'' thy [] goal tacf - handle ERROR _ => - (warning "Cannot prove infinite induction rule"; refl)); - in (finites, ind) end; -end; (* local *) - -(* ----- theorem concerning coinduction ------------------------------------- *) - -local - val xs = mapn (fn n => K (x_name n)) 1 dnames; - fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); - val take_ss = HOL_ss addsimps take_rews; - val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); - val coind_lemma = - let - fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; - fun mk_eqn n dn = - (dc_take dn $ %:"n" ` bnd_arg n 0) === - (dc_take dn $ %:"n" ` bnd_arg n 1); - fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); - val goal = - mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", - Library.foldr mk_all2 (xs, - Library.foldr mk_imp (mapn mk_prj 0 dnames, - foldr1 mk_conj (mapn mk_eqn 0 dnames))))); - fun x_tacs n x = [ - rotate_tac (n+1) 1, - etac all2E 1, - eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, - TRY (safe_tac HOL_cs), - REPEAT (CHANGED (asm_simp_tac take_ss 1))]; - val tacs = [ - rtac impI 1, - induct_tac "n" 1, - simp_tac take_ss 1, - safe_tac HOL_cs] @ - List.concat (mapn x_tacs 0 xs); - in pg [ax_bisim_def] goal tacs end; -in - val coind = - let - fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); - fun mk_eqn x = %:x === %:(x^"'"); - val goal = - mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> - Logic.list_implies (mapn mk_prj 0 xs, - mk_trp (foldr1 mk_conj (map mk_eqn xs))); - val tacs = - TRY (safe_tac HOL_cs) :: - List.concat (map (fn take_lemma => [ - rtac take_lemma 1, - cut_facts_tac [coind_lemma] 1, - fast_tac HOL_cs 1]) - take_lemmas); - in pg [] goal tacs end; -end; (* local *) - -in thy |> Theory.add_path comp_dnam - |> (snd o (PureThy.add_thmss (map Thm.no_attributes [ - ("take_rews" , take_rews ), - ("take_lemmas", take_lemmas), - ("finites" , finites ), - ("finite_ind", [finite_ind]), - ("ind" , [ind ]), - ("coind" , [coind ])]))) - |> Theory.parent_path |> rpair take_rews -end; (* let *) -end; (* local *) -end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,317 +0,0 @@ -(* Title: HOLCF/fixrec_package.ML - ID: $Id$ - Author: Amber Telfer and Brian Huffman - -Recursive function definition package for HOLCF. -*) - -signature FIXREC_PACKAGE = -sig - val legacy_infer_term: theory -> term -> term - val legacy_infer_prop: theory -> term -> term - val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory - val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory - val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory - val add_fixpat_i: (string * attribute list) * term list -> theory -> theory -end; - -structure FixrecPackage: FIXREC_PACKAGE = -struct - -(* legacy type inference *) - -fun legacy_infer_term thy t = - singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t); - -fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT); - - -val fix_eq2 = thm "fix_eq2"; -val def_fix_ind = thm "def_fix_ind"; - - -fun fixrec_err s = error ("fixrec definition error:\n" ^ s); -fun fixrec_eq_err thy s eq = - fixrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq)); - -(* ->> is taken from holcf_logic.ML *) -(* TODO: fix dependencies so we can import HOLCFLogic here *) -infixr 6 ->>; -fun S ->> T = Type ("Cfun.->",[S,T]); - -(* extern_name is taken from domain/library.ML *) -fun extern_name con = case Symbol.explode con of - ("o"::"p"::" "::rest) => implode rest - | _ => con; - -val mk_trp = HOLogic.mk_Trueprop; - -(* splits a cterm into the right and lefthand sides of equality *) -fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); - -(* similar to Thm.head_of, but for continuous application *) -fun chead_of (Const("Cfun.Rep_CFun",_)$f$t) = chead_of f - | chead_of u = u; - -(* these are helpful functions copied from HOLCF/domain/library.ML *) -fun %: s = Free(s,dummyT); -fun %%: s = Const(s,dummyT); -infix 0 ==; fun S == T = %%:"==" $ S $ T; -infix 1 ===; fun S === T = %%:"op =" $ S $ T; -infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x; - -(* builds the expression (LAM v. rhs) *) -fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(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); - -(* builds the expression (LAM . rhs) *) -fun lambda_ctuple [] rhs = big_lambda (%:"unit") rhs - | lambda_ctuple (v::[]) rhs = big_lambda v rhs - | lambda_ctuple (v::vs) rhs = - %%:"Cprod.csplit"`(big_lambda v (lambda_ctuple vs rhs)); - -(* builds the expression *) -fun mk_ctuple [] = %%:"UU" -| mk_ctuple (t::[]) = t -| mk_ctuple (t::ts) = %%:"Cprod.cpair"`t`(mk_ctuple ts); - -(*************************************************************************) -(************* fixed-point definitions and unfolding theorems ************) -(*************************************************************************) - -fun add_fixdefs eqs thy = - let - val (lhss,rhss) = ListPair.unzip (map dest_eqs eqs); - val fixpoint = %%:"Fix.fix"`lambda_ctuple lhss (mk_ctuple rhss); - - fun one_def (l as Const(n,T)) r = - let val b = Sign.base_name n in (b, (b^"_def", l == r)) end - | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; - fun defs [] _ = [] - | defs (l::[]) r = [one_def l r] - | defs (l::ls) r = one_def l (%%:"Cprod.cfst"`r) :: defs ls (%%:"Cprod.csnd"`r); - val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint); - - val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs; - val (fixdef_thms, thy') = - PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy; - val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms; - - val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); - val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold - (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, - simp_tac (simpset_of thy') 1]); - val ctuple_induct_thm = - (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind); - - fun unfolds [] thm = [] - | unfolds (n::[]) thm = [(n^"_unfold", thm)] - | unfolds (n::ns) thm = let - val thmL = thm RS cpair_eqD1; - val thmR = thm RS cpair_eqD2; - in (n^"_unfold", thmL) :: unfolds ns thmR end; - val unfold_thms = unfolds names ctuple_unfold_thm; - val thms = ctuple_induct_thm :: unfold_thms; - val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy'; - in - (thy'', names, fixdef_thms, map snd unfold_thms) - end; - -(*************************************************************************) -(*********** monadic notation and pattern matching compilation ***********) -(*************************************************************************) - -fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs - | add_names (Free(a,_) , bs) = insert (op =) a bs - | add_names (f $ u , bs) = add_names (f, add_names(u, bs)) - | add_names (Abs(a,_,t), bs) = add_names (t, insert (op =) a bs) - | add_names (_ , bs) = bs; - -fun add_terms ts xs = foldr add_names xs ts; - -(* builds a monadic term for matching a constructor pattern *) -fun pre_build pat rhs vs taken = - case pat of - Const("Cfun.Rep_CFun",_)$f$(v as Free(n,T)) => - pre_build f rhs (v::vs) taken - | Const("Cfun.Rep_CFun",_)$f$x => - let val (rhs', v, taken') = pre_build x rhs [] taken; - in pre_build f rhs' (v::vs) taken' end - | Const(c,T) => - let - val n = Name.variant taken "v"; - fun result_type (Type("Cfun.->",[_,T])) (x::xs) = result_type T xs - | result_type T _ = T; - val v = Free(n, result_type T vs); - val m = "match_"^(extern_name(Sign.base_name c)); - val k = lambda_ctuple vs rhs; - in - (%%:"Fixrec.bind"`(%%:m`v)`k, v, n::taken) - end - | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n) - | _ => fixrec_err "pre_build: invalid pattern"; - -(* builds a monadic term for matching a function definition pattern *) -(* returns (name, arity, matcher) *) -fun building pat rhs vs taken = - case pat of - Const("Cfun.Rep_CFun", _)$f$(v as Free(n,T)) => - building f rhs (v::vs) taken - | Const("Cfun.Rep_CFun", _)$f$x => - let val (rhs', v, taken') = pre_build x rhs [] taken; - in building f rhs' (v::vs) taken' end - | Const(name,_) => (name, length vs, big_lambdas vs rhs) - | _ => fixrec_err "function is not declared as constant in theory"; - -fun match_eq eq = - let val (lhs,rhs) = dest_eqs eq; - in building lhs (%%:"Fixrec.return"`rhs) [] (add_terms [eq] []) end; - -(* returns the sum (using +++) of the terms in ms *) -(* also applies "run" to the result! *) -fun fatbar arity ms = - let - fun unLAM 0 t = t - | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t - | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; - fun reLAM 0 t = t - | reLAM n t = reLAM (n-1) (%%:"Cfun.Abs_CFun" $ Abs("",dummyT,t)); - fun mplus (x,y) = %%:"Fixrec.mplus"`x`y; - val msum = foldr1 mplus (map (unLAM arity) ms); - in - reLAM arity (%%:"Fixrec.run"`msum) - end; - -fun unzip3 [] = ([],[],[]) - | unzip3 ((x,y,z)::ts) = - let val (xs,ys,zs) = unzip3 ts - in (x::xs, y::ys, z::zs) end; - -(* this is the pattern-matching compiler function *) -fun compile_pats eqs = - let - val ((n::names),(a::arities),mats) = unzip3 (map match_eq eqs); - val cname = if forall (fn x => n=x) names then n - else fixrec_err "all equations in block must define the same function"; - val arity = if forall (fn x => a=x) arities then a - else fixrec_err "all equations in block must have the same arity"; - val rhs = fatbar arity mats; - in - mk_trp (%%:cname === rhs) - end; - -(*************************************************************************) -(********************** Proving associated theorems **********************) -(*************************************************************************) - -(* proves a block of pattern matching equations as theorems, using unfold *) -fun make_simps thy (unfold_thm, eqns) = - let - val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1]; - fun prove_term t = Goal.prove_global thy [] [] t (K (EVERY tacs)); - fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts); - in - map prove_eqn eqns - end; - -(*************************************************************************) -(************************* Main fixrec function **************************) -(*************************************************************************) - -fun gen_add_fixrec prep_prop prep_attrib strict blocks thy = - let - val eqns = List.concat blocks; - val lengths = map length blocks; - - val ((names, srcss), strings) = apfst split_list (split_list eqns); - val atts = map (map (prep_attrib thy)) srcss; - val eqn_ts = map (prep_prop thy) strings; - val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq))) - handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts; - val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts; - - fun unconcat [] _ = [] - | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n)); - val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts'); - val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks; - val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy; - in - if strict then let (* only prove simp rules if strict = true *) - val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts); - val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks)); - val (simp_thms, thy'') = PureThy.add_thms simps thy'; - - val simp_names = map (fn name => name^"_simps") cnames; - val simp_attribute = rpair [Simplifier.simp_add]; - val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms); - in - (snd o PureThy.add_thmss simps') thy'' - end - else thy' - end; - -val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute; -val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I); - - -(*************************************************************************) -(******************************** Fixpat *********************************) -(*************************************************************************) - -fun fix_pat thy t = - let - val T = fastype_of t; - val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); - val cname = case chead_of t of Const(c,_) => c | _ => - fixrec_err "function is not declared as constant in theory"; - val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold")); - val simp = Goal.prove_global thy [] [] eq - (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); - in simp end; - -fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = - let - val atts = map (prep_attrib thy) srcs; - val ts = map (prep_term thy) strings; - val simps = map (fix_pat thy) ts; - in - (snd o PureThy.add_thmss [((name, simps), atts)]) thy - end; - -val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute; -val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I); - - -(*************************************************************************) -(******************************** Parsers ********************************) -(*************************************************************************) - -local structure P = OuterParse and K = OuterKeyword in - -val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop; - -val fixrec_strict = P.opt_keyword "permissive" >> not; - -val fixrec_decl = fixrec_strict -- P.and_list1 (Scan.repeat1 fixrec_eqn); - -(* this builds a parser for a new keyword, fixrec, whose functionality -is defined by add_fixrec *) -val fixrecP = - OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl - (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec)); - -(* fixpat parser *) -val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop; - -val fixpatP = - OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl - (fixpat_decl >> (Toplevel.theory o add_fixpat)); - -val _ = OuterSyntax.add_parsers [fixrecP, fixpatP]; - -end; (* local structure *) - -end; (* struct *) diff -r ed3f6685ff90 -r 9497234a2743 src/HOLCF/pcpodef_package.ML --- a/src/HOLCF/pcpodef_package.ML Thu May 31 13:24:13 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,213 +0,0 @@ -(* Title: HOLCF/pcpodef_package.ML - ID: $Id$ - Author: Brian Huffman - -Primitive domain definitions for HOLCF, similar to Gordon/HOL-style -typedef. -*) - -signature PCPODEF_PACKAGE = -sig - val quiet_mode: bool ref - val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string - * (string * string) option -> theory -> Proof.state - val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term - * (string * string) option -> theory -> Proof.state - val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string - * (string * string) option -> theory -> Proof.state - val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term - * (string * string) option -> theory -> Proof.state -end; - -structure PcpodefPackage: PCPODEF_PACKAGE = -struct - -(** theory context references **) - -val typedef_po = thm "typedef_po"; -val typedef_cpo = thm "typedef_cpo"; -val typedef_pcpo = thm "typedef_pcpo"; -val typedef_lub = thm "typedef_lub"; -val typedef_thelub = thm "typedef_thelub"; -val typedef_compact = thm "typedef_compact"; -val cont_Rep = thm "typedef_cont_Rep"; -val cont_Abs = thm "typedef_cont_Abs"; -val Rep_strict = thm "typedef_Rep_strict"; -val Abs_strict = thm "typedef_Abs_strict"; -val Rep_defined = thm "typedef_Rep_defined"; -val Abs_defined = thm "typedef_Abs_defined"; - - -(** type definitions **) - -(* messages *) - -val quiet_mode = ref false; -fun message s = if ! quiet_mode then () else writeln s; - - -(* prepare_cpodef *) - -fun err_in_cpodef msg name = - cat_error msg ("The error(s) above occurred in cpodef " ^ quote name); - -fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); - -fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT); -fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); - -fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = - let - val ctxt = ProofContext.init thy; - val full = Sign.full_name thy; - - (*rhs*) - val full_name = full name; - val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; - val setT = Term.fastype_of set; - val rhs_tfrees = term_tfrees set; - val oldT = HOLogic.dest_setT setT handle TYPE _ => - error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT)); - fun mk_nonempty A = - HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)); - fun mk_admissible A = - mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)); - fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A); - val goal = if pcpo - then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set)) - else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set)); - - (*lhs*) - val defS = Sign.defaultS thy; - val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; - val lhs_sorts = map snd lhs_tfrees; - val tname = Syntax.type_name t mx; - val full_tname = full tname; - val newT = Type (full_tname, map TFree lhs_tfrees); - - val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs; - val RepC = Const (full Rep_name, newT --> oldT); - fun lessC T = Const ("Porder.<<", T --> T --> HOLogic.boolT); - val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT, - Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))); - - fun make_po tac theory = theory - |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac - ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"]) - (ClassPackage.intro_classes_tac []) - ||>> PureThy.add_defs_i true [Thm.no_attributes less_def] - |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) => - AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"]) - (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1) - #> pair (type_definition, less_definition, set_def)); - - fun make_cpo admissible (type_def, less_def, set_def) theory = - let - val admissible' = fold_rule (the_list set_def) admissible; - val cpo_thms = [type_def, less_def, admissible']; - in - theory - |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"]) - (Tactic.rtac (typedef_cpo OF cpo_thms) 1) - |> Theory.add_path name - |> PureThy.add_thms - ([(("adm_" ^ name, admissible'), []), - (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []), - (("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []), - (("lub_" ^ name, typedef_lub OF cpo_thms), []), - (("thelub_" ^ name, typedef_thelub OF cpo_thms), []), - (("compact_" ^ name, typedef_compact OF cpo_thms), [])]) - |> snd - |> Theory.parent_path - end; - - fun make_pcpo UUmem (type_def, less_def, set_def) theory = - let - val UUmem' = fold_rule (the_list set_def) UUmem; - val pcpo_thms = [type_def, less_def, UUmem']; - in - theory - |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"]) - (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1) - |> Theory.add_path name - |> PureThy.add_thms - ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []), - ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []), - ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []), - ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), []) - ]) - |> snd - |> Theory.parent_path - end; - - fun pcpodef_result UUmem_admissible theory = - let - val UUmem = UUmem_admissible RS conjunct1; - val admissible = UUmem_admissible RS conjunct2; - in - theory - |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1) - |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs) - end; - - fun cpodef_result nonempty_admissible theory = - let - val nonempty = nonempty_admissible RS conjunct1; - val admissible = nonempty_admissible RS conjunct2; - in - theory - |> make_po (Tactic.rtac nonempty 1) - |-> make_cpo admissible - end; - - in (goal, if pcpo then pcpodef_result else cpodef_result) end - handle ERROR msg => err_in_cpodef msg name; - - -(* cpodef_proof interface *) - -fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = - let - val (goal, pcpodef_result) = - prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; - fun after_qed [[th]] = ProofContext.theory (pcpodef_result th); - in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end; - -fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x; -fun pcpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term true x; - -fun cpodef_proof x = gen_pcpodef_proof ProofContext.read_term false x; -fun cpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term false x; - - -(** outer syntax **) - -local structure P = OuterParse and K = OuterKeyword in - -(* copied from HOL/Tools/typedef_package.ML *) -val typedef_proof_decl = - Scan.optional (P.$$$ "(" |-- - ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s))) - --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- - Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)); - -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = - (if pcpo then pcpodef_proof else cpodef_proof) - ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs); - -val pcpodefP = - OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal - (typedef_proof_decl >> - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))); - -val cpodefP = - OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal - (typedef_proof_decl >> - (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))); - -val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP]; - -end; - -end;