# HG changeset patch # User wenzelm # Date 1163459742 -3600 # Node ID 073c79be780c170cc79bf1ea7880611166c8449a # Parent 1fb804b96d7cdbf33471680142a93c1ff90476fe removed legacy read/cert/string_of; removed obsolete IsarThy.theorem_i; tuned comments; diff -r 1fb804b96d7c -r 073c79be780c src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Nov 14 00:15:39 2006 +0100 +++ b/src/HOL/Tools/typedef_package.ML Tue Nov 14 00:15:42 2006 +0100 @@ -2,7 +2,8 @@ ID: $Id$ Author: Markus Wenzel and Stefan Berghofer, TU Muenchen -Gordon/HOL-style type definitions. +Gordon/HOL-style type definitions: create a new syntactic type +represented by a non-empty subset. *) signature TYPEDEF_PACKAGE = @@ -29,7 +30,6 @@ structure TypedefPackage: TYPEDEF_PACKAGE = struct - (** theory context references **) val type_definitionN = "Typedef.type_definition"; @@ -93,27 +93,25 @@ (* prepare_typedef *) -fun read_term thy used s = - #1 (Thm.read_def_cterm (thy, K NONE, K NONE) used true (s, HOLogic.typeT)); - -fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg; - fun err_in_typedef msg name = cat_error msg ("The error(s) above occurred in typedef " ^ quote name); +fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); + fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy = let val _ = Theory.requires thy "Typedef" "typedefs"; + val ctxt = ProofContext.init thy; val full = Sign.full_name thy; (*rhs*) val full_name = full name; - val cset = prep_term thy vs raw_set; - val {T = setT, t = set, ...} = Thm.rep_cterm cset; + val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; + val setT = Term.fastype_of set; val rhs_tfrees = Term.add_tfrees set []; val rhs_tfreesT = Term.add_tfreesT setT []; val oldT = HOLogic.dest_setT setT handle TYPE _ => - error ("Not a set type: " ^ quote (Sign.string_of_typ thy setT)); + error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT)); fun mk_nonempty A = HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A))); val goal = mk_nonempty set; @@ -154,19 +152,18 @@ |-> (fn [th] => pair (SOME th)) else (NONE, thy); - fun typedef_result nonempty context = - Context.the_theory context - |> add_typedecls [(t, vs, mx)] - |> Theory.add_consts_i + fun typedef_result nonempty = + add_typedecls [(t, vs, mx)] + #> Theory.add_consts_i ((if def then [(name, setT', NoSyn)] else []) @ [(Rep_name, newT --> oldT, NoSyn), (Abs_name, oldT --> newT, NoSyn)]) - |> add_def (Logic.mk_defpair (setC, set)) - ||>> PureThy.add_axioms_i [((typedef_name, typedef_prop), + #> add_def (Logic.mk_defpair (setC, set)) + ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop), [apsnd (fn cond_axm => nonempty RS cond_axm)])] - ||> Theory.add_deps "" (dest_Const RepC) typedef_deps - ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps - |-> (fn (set_def, [type_definition]) => fn thy1 => + ##> Theory.add_deps "" (dest_Const RepC) typedef_deps + ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps + #-> (fn (set_def, [type_definition]) => fn thy1 => let fun make th = Drule.standard (th OF [type_definition]); val abs_inject = make Abs_inject; @@ -197,7 +194,7 @@ Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; val thy3 = thy2 |> put_info full_tname info; - in ((full_tname, info), Context.Theory thy3) end); + in ((full_tname, info), thy3) end); (* errors *) @@ -225,11 +222,10 @@ (*test theory errors now!*) val test_thy = Theory.copy thy; - val _ = - Context.Theory test_thy + val _ = test_thy |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal); - in (cset, goal, goal_pat, typedef_result) end + in (set, goal, goal_pat, typedef_result) end handle ERROR msg => err_in_typedef msg name; @@ -239,22 +235,19 @@ fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy = let + val string_of_term = ProofContext.string_of_term (ProofContext.init thy); val name = the_default (#1 typ) opt_name; - val (cset, goal, _, typedef_result) = + val (set, goal, _, typedef_result) = prepare_typedef prep_term def name typ set opt_morphs thy; - val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); + val _ = message ("Proving non-emptiness of set " ^ quote (string_of_term set) ^ " ..."); val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg => - cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset)); - in - Context.Theory thy - |> typedef_result non_empty - ||> Context.the_theory - end; + cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_term set)); + in typedef_result non_empty thy end; in -val add_typedef = gen_typedef read_term; -val add_typedef_i = gen_typedef cert_term; +val add_typedef = gen_typedef ProofContext.read_term; +val add_typedef_i = gen_typedef ProofContext.cert_term; end; @@ -267,18 +260,17 @@ let val (_, goal, goal_pat, typedef_result) = prepare_typedef prep_term def name typ set opt_morphs thy; - fun att (thy, th) = - let val ((name, {type_definition, ...}), thy') = typedef_result th thy - in (thy', type_definition) end; + fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th); in - thy - |> IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, [goal_pat]) + ProofContext.init thy + |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", []) + [(("", []), [(goal, [goal_pat])])] end; in -val typedef = gen_typedef read_term; -val typedef_i = gen_typedef cert_term; +val typedef = gen_typedef ProofContext.read_term; +val typedef_i = gen_typedef ProofContext.cert_term; end; diff -r 1fb804b96d7c -r 073c79be780c src/HOLCF/pcpodef_package.ML --- a/src/HOLCF/pcpodef_package.ML Tue Nov 14 00:15:39 2006 +0100 +++ b/src/HOLCF/pcpodef_package.ML Tue Nov 14 00:15:42 2006 +0100 @@ -2,7 +2,8 @@ ID: $Id$ Author: Brian Huffman -Gordon/HOL-style type definitions for HOLCF. +Primitive domain definitions for HOLCF, similar to Gordon/HOL-style +typedef. *) signature PCPODEF_PACKAGE = @@ -21,7 +22,6 @@ structure PcpodefPackage: PCPODEF_PACKAGE = struct - (** theory context references **) val typedef_po = thm "typedef_po"; @@ -48,28 +48,26 @@ (* prepare_cpodef *) -fun read_term thy used s = - #1 (Thm.read_def_cterm (thy, K NONE, K NONE) used true (s, HOLogic.typeT)); - -fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg; - 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 gen_prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = +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 cset = prep_term thy vs raw_set; - val {T = setT, t = set, ...} = Thm.rep_cterm cset; + 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 (Sign.string_of_typ thy setT)); + 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 = @@ -78,25 +76,22 @@ 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 lhs_tfrees = map (fn v => (v, AList.lookup (op =) rhs_tfrees v |> the_default HOLogic.typeS)) vs; + 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) = getOpt (opt_morphs, ("Rep_" ^ name, "Abs_" ^ name)); + 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 option_fold_rule NONE = I - | option_fold_rule (SOME def) = fold_rule [def]; - - fun make_po tac thy = - thy + 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 []) @@ -104,86 +99,88 @@ |-> (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) - #> rpair (type_definition, less_definition, set_def)); - - fun make_cpo admissible (theory, defs as (type_def, less_def, set_def)) = + #> pair (type_definition, less_definition, set_def)); + + fun make_cpo admissible (type_def, less_def, set_def) theory = let - val admissible' = option_fold_rule set_def admissible; + val admissible' = fold_rule (the_list set_def) admissible; val cpo_thms = [type_def, less_def, admissible']; - val (_, theory') = - 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 + 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), [])]) - ||> Theory.parent_path; - in (theory', defs) end; + |> snd + |> Theory.parent_path + end; - fun make_pcpo UUmem (theory, defs as (type_def, less_def, set_def)) = + fun make_pcpo UUmem (type_def, less_def, set_def) theory = let - val UUmem' = option_fold_rule set_def UUmem; + val UUmem' = fold_rule (the_list set_def) UUmem; val pcpo_thms = [type_def, less_def, UUmem']; - val (_, theory') = - 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 + 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), []) ]) - ||> Theory.parent_path; - in (theory', defs) end; - - fun pcpodef_result (context, UUmem_admissible) = + |> snd + |> Theory.parent_path + end; + + fun pcpodef_result UUmem_admissible theory = let - val theory = Context.the_theory context; 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) - |> make_cpo admissible - |> make_pcpo UUmem - |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def)) + |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs) end; - - fun cpodef_result (context, nonempty_admissible) = + + fun cpodef_result nonempty_admissible theory = let - val theory = Context.the_theory context; val nonempty = nonempty_admissible RS conjunct1; val admissible = nonempty_admissible RS conjunct2; in theory |> make_po (Tactic.rtac nonempty 1) - |> make_cpo admissible - |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def)) + |-> 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, att) = - gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; - in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, []) thy end; + 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 + ProofContext.init thy + |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", []) [(("", []), [(goal, [])])] + end; -fun pcpodef_proof x = gen_pcpodef_proof read_term true x; -fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x; +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 read_term false x; -fun cpodef_proof_i x = gen_pcpodef_proof cert_term false 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 **) @@ -200,7 +197,7 @@ fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = (if pcpo then pcpodef_proof else cpodef_proof) - ((def, getOpt (opt_name, Syntax.type_name t mx)), (t, vs, mx), A, morphs); + ((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