Added package for definition by specification.
authorskalberg
Thu Jul 17 15:23:20 2003 +0200 (2003-07-17)
changeset 1411565ec3f73d00b
parent 14114 e97ca1034caa
child 14116 63337d8e6e0f
Added package for definition by specification.
etc/isar-keywords.el
src/HOL/Hilbert_Choice.thy
src/HOL/IsaMakefile
src/HOL/Tools/specification_package.ML
     1.1 --- a/etc/isar-keywords.el	Wed Jul 16 12:09:41 2003 +0200
     1.2 +++ b/etc/isar-keywords.el	Thu Jul 17 15:23:20 2003 +0200
     1.3 @@ -136,6 +136,7 @@
     1.4      "setup"
     1.5      "show"
     1.6      "sorry"
     1.7 +    "specification"
     1.8      "subsect"
     1.9      "subsection"
    1.10      "subsubsect"
    1.11 @@ -373,6 +374,7 @@
    1.12      "instance"
    1.13      "lemma"
    1.14      "recdef_tc"
    1.15 +    "specification"
    1.16      "theorem"
    1.17      "typedef"))
    1.18  
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jul 16 12:09:41 2003 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Jul 17 15:23:20 2003 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
     2.5  
     2.6  theory Hilbert_Choice = NatArith
     2.7 -files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
     2.8 +files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML") ("Tools/specification_package.ML"):
     2.9  
    2.10  
    2.11  subsection {* Hilbert's epsilon *}
    2.12 @@ -268,4 +268,6 @@
    2.13  use "Tools/meson.ML"
    2.14  setup meson_setup
    2.15  
    2.16 +use "Tools/specification_package.ML"
    2.17 +
    2.18  end
     3.1 --- a/src/HOL/IsaMakefile	Wed Jul 16 12:09:41 2003 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Thu Jul 17 15:23:20 2003 +0200
     3.3 @@ -104,6 +104,7 @@
     3.4    Tools/meson.ML Tools/numeral_syntax.ML \
     3.5    Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \
     3.6    Tools/record_package.ML Tools/rewrite_hol_proof.ML \
     3.7 +  Tools/specification_package.ML \
     3.8    Tools/split_rule.ML Tools/typedef_package.ML \
     3.9    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    3.10    Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/specification_package.ML	Thu Jul 17 15:23:20 2003 +0200
     4.3 @@ -0,0 +1,162 @@
     4.4 +(*  Title:      HOL/Tools/specification_package.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Sebastian Skalberg, TU Muenchen
     4.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.8 +
     4.9 +Package for defining constants by specification.
    4.10 +*)
    4.11 +
    4.12 +signature SPECIFICATION_PACKAGE =
    4.13 +sig
    4.14 +    val quiet_mode: bool ref
    4.15 +    val add_specification: (bstring * bool) list -> bstring * Args.src list
    4.16 +			   -> theory * thm -> theory * thm
    4.17 +    val add_specification_i: (bstring * bool) list -> bstring * theory attribute list
    4.18 +			     -> theory * thm -> theory * thm
    4.19 +end
    4.20 +
    4.21 +structure SpecificationPackage : SPECIFICATION_PACKAGE =
    4.22 +struct
    4.23 +
    4.24 +(* messages *)
    4.25 +
    4.26 +val quiet_mode = ref false
    4.27 +fun message s = if ! quiet_mode then () else writeln s
    4.28 +
    4.29 +local
    4.30 +    val _ = Goal "[| Ex P ; c == Eps P |] ==> P c"
    4.31 +    val _ = by (Asm_simp_tac 1)
    4.32 +    val _ = by (rtac (thm "someI_ex") 1)
    4.33 +    val _ = ba 1
    4.34 +in
    4.35 +val helper = Goals.result()
    4.36 +end
    4.37 +
    4.38 +(* Akin to HOLogic.exists_const *)
    4.39 +fun choice_const T = Const("Hilbert_Choice.Eps",(T-->HOLogic.boolT)-->T)
    4.40 +
    4.41 +(* Actual code *)
    4.42 +
    4.43 +fun proc_exprop [] arg = arg
    4.44 +  | proc_exprop ((cname,covld)::cos) (thy,thm) =
    4.45 +    case concl_of thm of
    4.46 +	Const("Trueprop",_) $ (Const("Ex",_) $ P) =>
    4.47 +	let
    4.48 +	    val ctype = domain_type (type_of P)
    4.49 +	    val cdefname = Thm.def_name (Sign.base_name cname)
    4.50 +	    val def_eq = Logic.mk_equals (Const(cname,ctype),choice_const ctype $  P)
    4.51 +	    val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
    4.52 +	    val thm' = [thm,hd thms] MRS helper
    4.53 +	in
    4.54 +	    proc_exprop cos (thy',thm')
    4.55 +	end
    4.56 +      | _ => raise THM ("Internal error: Bad specification theorem",0,[thm])
    4.57 +
    4.58 +fun add_specification_i cos (name,atts) arg =
    4.59 +    let
    4.60 +	fun apply_attributes arg = Thm.apply_attributes(arg,atts)
    4.61 +	fun add_final (arg as (thy,thm)) =
    4.62 +	    if name = ""
    4.63 +	    then arg
    4.64 +	    else (writeln ("specification " ^ name ^ ": " ^ (string_of_thm thm));
    4.65 +		  PureThy.store_thm((name,thm),[]) thy)
    4.66 +    in
    4.67 +	arg |> apsnd freezeT
    4.68 +	    |> proc_exprop cos
    4.69 +	    |> apsnd standard
    4.70 +	    |> apply_attributes
    4.71 +	    |> add_final
    4.72 +    end
    4.73 +
    4.74 +fun add_specification cos (name,atts) arg =
    4.75 +    add_specification_i cos (name,map (Attrib.global_attribute thy) atts) arg
    4.76 +
    4.77 +(* Collect all intances of constants in term *)
    4.78 +
    4.79 +fun collect_consts (        t $ u,tms) = collect_consts (u,collect_consts (t,tms))
    4.80 +  | collect_consts (   Abs(_,_,t),tms) = collect_consts (t,tms)
    4.81 +  | collect_consts (tm as Const _,tms) = gen_ins (op aconv) (tm,tms)
    4.82 +  | collect_consts (            _,tms) = tms
    4.83 +
    4.84 +(* Complementing Type.varify... *)
    4.85 +
    4.86 +fun unvarify t fmap =
    4.87 +    let
    4.88 +	val fmap' = map Library.swap fmap
    4.89 +	fun unthaw (f as (a,S)) =
    4.90 +	    (case assoc (fmap',a) of
    4.91 +		 None => TVar f
    4.92 +	       | Some b => TFree (b,S))
    4.93 +    in
    4.94 +	map_term_types (map_type_tvar unthaw) t
    4.95 +    end
    4.96 +
    4.97 +(* The syntactic meddling needed to setup add_specification for work *)
    4.98 +
    4.99 +fun process_spec cos alt_name sprop int thy =
   4.100 +    let
   4.101 +	val sg = sign_of thy
   4.102 +	fun typ_equiv t u =
   4.103 +	    let
   4.104 +		val tsig = Sign.tsig_of sg
   4.105 +	    in
   4.106 +		Type.typ_instance(tsig,t,u) andalso
   4.107 +		Type.typ_instance(tsig,u,t)
   4.108 +	    end
   4.109 +	val prop = term_of (Thm.read_cterm sg (sprop,HOLogic.boolT))
   4.110 +	val (prop_thawed,vmap) = Type.varify (prop,[])
   4.111 +	val thawed_prop_consts = collect_consts (prop_thawed,[])
   4.112 +	val (sconsts,overloaded) = Library.split_list cos
   4.113 +	val consts = map (term_of o Thm.read_cterm sg o rpair TypeInfer.logicT) sconsts
   4.114 +	val _ = assert (not (Library.exists (not o Term.is_Const) consts))
   4.115 +		       "Non-constant found as parameter"
   4.116 +	fun proc_const c =
   4.117 +	    let
   4.118 +		val c' = fst (Type.varify (c,[]))
   4.119 +		val (cname,ctyp) = dest_Const c'
   4.120 +	    in
   4.121 +		case filter (fn t => let val (name,typ) = dest_Const t
   4.122 +				     in name = cname andalso typ_equiv typ ctyp
   4.123 +				     end) thawed_prop_consts of
   4.124 +		    [] => error ("Constant \"" ^ (Sign.string_of_term sg c) ^ "\" not found in specification")
   4.125 +		  | [cf] => unvarify cf vmap
   4.126 +		  | _ => error ("Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found in specification")
   4.127 +	    end
   4.128 +	val proc_consts = map proc_const consts
   4.129 +	fun mk_exist (c,prop) =
   4.130 +	    let
   4.131 +		val T = type_of c
   4.132 +	    in
   4.133 +		HOLogic.exists_const T $ Abs("x",T,Term.abstract_over (c,prop))
   4.134 +	    end
   4.135 +	val ex_prop = foldr mk_exist (proc_consts,prop)
   4.136 +	val cnames = map (fst o dest_Const) proc_consts
   4.137 +    in
   4.138 +	IsarThy.theorem_i Drule.internalK
   4.139 +	    (("",[add_specification (cnames ~~ overloaded) alt_name]),
   4.140 +	     (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy
   4.141 +    end
   4.142 +
   4.143 +(* outer syntax *)
   4.144 +
   4.145 +local structure P = OuterParse and K = OuterSyntax.Keyword in
   4.146 +
   4.147 +(* taken from ~~/Pure/Isar/isar_syn.ML *)
   4.148 +val opt_overloaded =
   4.149 +  Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false
   4.150 +
   4.151 +val specification_decl =
   4.152 +    P.$$$ "(" |-- Scan.repeat1 (P.term -- opt_overloaded) --| P.$$$ ")" --
   4.153 +	  P.opt_thm_name ":" -- P.prop
   4.154 +
   4.155 +val specificationP =
   4.156 +  OuterSyntax.command "specification" "define constants by specification" K.thy_goal
   4.157 +    (specification_decl >> (fn ((cos,alt_name), prop) =>
   4.158 +			       Toplevel.print o (Toplevel.theory_to_proof (process_spec cos alt_name prop))))
   4.159 +
   4.160 +val _ = OuterSyntax.add_parsers [specificationP]
   4.161 +
   4.162 +end
   4.163 +
   4.164 +
   4.165 +end