(* *********************************************************************** *)
(* *)
(* Project: HOLZ: Structure Preserving Encoding of Z in Isabelle *)
(* Author: B.Wolff, Albert-Ludwigs-Universität Freiburg *)
(* $Date: 2003/09/05 14:26:32 $ *)
(* Purpose of this file: encoding pre-parsed Z into HOL-Z representation *)
(* Main Task: making Z binding structure explicit *)
(* in HOL. *)
(* *)
(* *********************************************************************** *)
signature ZENCODER =
sig
type bindings = (string*typ) list
val init : unit -> unit
(* internal debugging states *)
val init_axprep : (string * thm -> bool) -> unit
(* set post-processor for axiomatic definitions *)
val schema_read : ZTheory.ztheory -> string -> term
val string_of_zthm : ZTheory.ztheory -> thm -> string
val add_abs_type : string -> ZTheory.ztheory -> ZTheory.ztheory
(* NOT YET PORTED *)
val add_free_type : (* dt_type *) string list * string *
(string * (* dt_type *) string list * mixfix) list
-> ZTheory.ztheory
-> ZTheory.ztheory
(* will become: (string list * bstring * mixfix
* (bstring * string list * mixfix) list) list ... *)
val add_schemes : string -> string list ->
ZTheory.ztheory ->
ZTheory.ztheory
val add_schemes_i : string -> (term list * bindings option) list ->
ZTheory.ztheory ->
ZTheory.ztheory
val add_conjecture : string -> string ->
ZTheory.ztheory ->
ZTheory.ztheory
val add_conjecture_i:string -> term ->
ZTheory.ztheory ->
ZTheory.ztheory
val get_schemes : ZTheory.ztheory -> (string * thm) list
val get_axdefs : ZTheory.ztheory -> (string * thm) list
val get_conjectures: ZTheory.ztheory -> (string * thm) list
end;
structure ZEncoder (* : ZENCODER *) = (* for debugging *)
struct
type bindings = (string*typ) list
open ZPrelude ZEnv ZTheory Sign Term HOLogic;
(*drop the first n elements from a list*)
fun drop (n, []) = []
| drop (n, x :: xs) =
if n > 0 then drop (n - 1, xs) else x :: xs;
(* parametric case ?! *)
(*
-- rough approximation of the type of a term;
uses the fact that HOL-Z operators are constants
and hence have known types, and schema names are variables
and have hence known types. Sufficient to recognize correct
schema expressions without schema variables.
*)
(* *********************************************************************** *)
(* *)
(* type handling *)
(* *)
(* *********************************************************************** *)
(* constructs type approximations for constant-head lifter, i.e
expressions of the form %x1 ... xn. C E1 ... Em. The underlying
assumption of the encoder is that this is sufficient for
deciding whether schemas (must have been defined in the
Z-section before, are thus constants) are imported
"asSet", "asPredicate" or "asBool". *)
val ZschemaT = boolT
fun type_of_appl l ty = if ty = dummyT then ty
else let val (argty,rty)= strip_type ty
in if l < length(argty)
then drop(l, argty) ---> rty
else rty
end
fun type_of_doms tS ty = if ty = dummyT then (map (K dummyT) tS,tS)
else let val (argty,rty)= strip_type ty
fun fill([],[]) = ([],[])
|fill([],a::R) = let val (c,t)=fill([],R)
in (dummyT::c,a::t)end
|fill(a::R,[]) = ([],[])
|fill(b::S,a::R) = let val (c,t)=fill(S,R)
in (b::c, a::t)end
in fill(argty,tS) end;
(* a raw type approximation taking Z constructs into account *)
fun type_of sg (Free (n,ty)) = if n="pre" then ZschemaT --> ZschemaT else
if not(ty = dummyT) then ty
else (case const_type sg
(intern_const sg
(destroke n)) of
SOME t => t
| NONE => dummyT)
|type_of sg (Const("DELTA",_)) = ZschemaT --> ZschemaT
|type_of sg (Const("XI",_)) = ZschemaT --> ZschemaT
|type_of sg (Const("PRE",_)) = ZschemaT --> ZschemaT
|type_of sg (Const("%E",_)) = [ZschemaT,ZschemaT] ---> ZschemaT
|type_of sg (Const("%E1",_)) = [ZschemaT,ZschemaT] ---> ZschemaT
|type_of sg (Const("%A",_)) = [ZschemaT,ZschemaT] ---> ZschemaT
|type_of sg (Const("_schset",_)) = [dummyT,dummyT] ---> (HOLogic.mk_setT dummyT)
|type_of sg (Const("_hiding",_)) = error "no hiding yet"
|type_of sg (Const("_rename",_)) = error "no renaming yet"
|type_of sg (Const("op |\\",_)) = error "no projection yet"
|type_of sg (Const("op %%;",_)) = error "no composition yet"
|type_of sg (Const("op >>",_)) = error "no piping yet"
|type_of sg (Const(n,ty)) = if not(ty = dummyT) then ty
else (case const_type sg
(intern_const sg
(destroke n)) of
SOME t => t
| NONE => dummyT)
|type_of sg (t as _ $ _) = let val (hd,args) = strip_comb t
val l = length args
val ty = type_of sg hd
in type_of_appl l ty end
|type_of sg (Bound _) = dummyT
|type_of sg (Var(_,t)) = t
|type_of sg (Abs(_,T,body))= T --> (type_of sg body);
fun type_of_appl l ty = if ty = dummyT then ty
else let val (argty,rty)= strip_type ty
in if l < length(argty)
then drop(l, argty) ---> rty
else rty
end
fun type_of_doms tS ty = if ty = dummyT then (map (K dummyT) tS,tS)
else let val (argty,rty)= strip_type ty
fun fill([],[]) = ([],[])
|fill([],a::R) = let val (c,t)=fill([],R)
in (dummyT::c,a::t)end
|fill(a::R,[]) = ([],[])
|fill(b::S,a::R)= let val (c,t)=fill(S,R)
in (b::c, a::t) end
in fill(argty,tS) end;
(* alias "boolfun" *)
fun is_pred (ty as Type("fun", _)) = (snd(strip_type ty) = boolT)
|is_pred _ = false;
fun is_set (Type ("set", [T])) = true
|is_set _ = false;
fun is_setfun (ty as Type("fun", _)) = (is_set (snd(strip_type ty)))
|is_setfun _ = false;
datatype tyclass = Bool | Other | Pred | Prop | Set | Setfun
fun tycl ty = if ty = boolT then Bool
else if ty = propT then Prop
else if is_pred ty then Pred
else if is_set ty then Set
else if is_setfun ty then Setfun
else Other
fun tycl2string Bool = "Bool"
|tycl2string Other = "Other"
|tycl2string Pred = "Pred"
|tycl2string Prop = "Prop"
|tycl2string Set = "Set"
|tycl2string Setfun= "Setfun"
fun zSchemaSign e (Const ("DECL",_) $ decl $ pred) =
zSchemaSign e decl (* append_zsig zSchemaSign e pred *)
|zSchemaSign e (Const ("ZPure.DECL",_) $ decl $ pred) =
zSchemaSign e decl (* append_zsig zSchemaSign e pred *)
|zSchemaSign e (Const("True",_)) = mt_zsig
|zSchemaSign e (Const("False",_)) = mt_zsig
|zSchemaSign e (Const("op :",_)$Free(s,t)$e2) = insert_zsig (s,t) mt_zsig
|zSchemaSign e (Const ("op &",T2) $ S $ T) = (zSchemaSign e S) union_zsig
(zSchemaSign e T)
|zSchemaSign e (Const ("op |",T2) $ S $ T) = (zSchemaSign e S) union_zsig
(zSchemaSign e T)
|zSchemaSign e (Const ("op -->",T2) $ S $ T) = (zSchemaSign e S) union_zsig
(zSchemaSign e T)
|zSchemaSign e (Const ("op =",_) $
(Const ("theta",_) $ _ $ S) $
(Const ("theta",_) $ _ $ T)) =
let fun H (Free s,e) = insert_zsig s e
val S' = foldl H mt_zsig (strip_tuple S)
val T' = foldl H mt_zsig (strip_tuple T)
in S' union_zsig T' end
|zSchemaSign e (Const("SNAME",_) $ _ $ T) =
let fun H (Free s,e) = insert_zsig s e
in foldl H (mt_zsig) (strip_tuple T) end
|zSchemaSign e (Const("DELTA",_) $ S $ T) = (zSchemaSign e S) union_zsig
(zSchemaSign e T)
|zSchemaSign e (Const("XI",_) $ S $ T $ U) = (zSchemaSign e S)
|zSchemaSign e (Const("PRE",_) $ T) =
filter_zsig (fn (x,_) => not(is_stroke_name x orelse is_out_name x))
(zSchemaSign e T)
|zSchemaSign e (Free("pre",_) $ T) =
filter_zsig (fn (x,_) => not(is_stroke_name x orelse is_out_name x))
(zSchemaSign e T)
|zSchemaSign e (Const("Bex",_)$ S $ (Abs(s,ty,T))) =
(zSchemaSign e S) union_zsig (delete_zsig (s,ty) (zSchemaSign e T))
|zSchemaSign e (Const("Ball",_)$ S $ (Abs(s,ty,T))) =
(zSchemaSign e S) union_zsig (delete_zsig (s,ty) (zSchemaSign e T))
|zSchemaSign e (Const("All",_)$ (Abs(s,ty,T))) =
(delete_zsig (s,ty) (zSchemaSign e T))
|zSchemaSign e (Const("Ex",_)$ (Abs(s,ty,T))) =
(delete_zsig (s,ty) (zSchemaSign e T))
|zSchemaSign e (Const("%E",_) $ S $ T) =
(zSchemaSign e T) diff_zsig (zSchemaSign e S)
|zSchemaSign e (Const("%E1",_) $ S $ T) =
(zSchemaSign e T) diff_zsig (zSchemaSign e S)
|zSchemaSign e (Const("%A",_) $ S $ T) =
(zSchemaSign e T) diff_zsig (zSchemaSign e S)
|zSchemaSign e (Const("_schset",_) $ S $ T) =
(zSchemaSign e T) diff_zsig (zSchemaSign e S)
|zSchemaSign e (Const("_hiding",_) $ S $ T) = error "no hiding yet"
|zSchemaSign e (Const("_rename",_) $ S $ T) = error "no renaming yet"
|zSchemaSign e (Const("op |\\",_) $ S $ T) = error "no projection yet"
|zSchemaSign e (Const("op %%;",_) $ S $ T) = error "no composition yet"
|zSchemaSign e (Const("op >>",_) $ S $ T) = error "no piping yet"
|zSchemaSign e (t as _ $ _) =
let val (hd,args) = strip_comb t
fun H(ty,t) = if ty = boolT
then zSchemaSign e t
else mt_zsig
val ty = type_of e t
in if type_of_appl (length args) ty = boolT
then foldl (fn (s1,s2) => s2 union_zsig s1)
mt_zsig (map2 H (type_of_doms args ty))
else mt_zsig
end
|zSchemaSign e _ = mt_zsig (* veeery liberal, but we admit e.g.
meta-variables, what makes the machinery
quite heuristic. But this is handy
in most cases like "schema = ?X" *)
(* *********************************************************************** *)
(* *)
(* lifting: marking schema names, converting theta *)
(* *)
(* *********************************************************************** *)
fun mk_tuple tS = let val a::R = rev tS
in foldl mk_prod a R end
(* lifting expands elementary schema references and handles
theta-expressions over (expanded) schema references *)
(* Riddle: where the heck were the free's stroked?
Well, in the lookup. bu *)
fun lift zsig (Free (s,t)) =
(case lookup (zsig,s) of
NONE => Free(s,t)
| SOME n => if null(schemasig_of n)
then (Const("SNAME0",dummyT)$ Const(destroke s,t))
else Const("SNAME",dummyT) $ Const(destroke s,t) $
(mk_tuple(map Free (schemasig_of n))))
|lift zsig (Const("%theta",_) $ (Free(s,t))) =
(case lookup (zsig,s) of
NONE => error ("illegal schema reference: %theta "^s)
|SOME n => Const ("theta",dummyT) $(mk_string s) $
(mk_tuple (map Free (schemasig_of n))))
|lift zsig (Abs(s,ty,t)) = Abs(s,ty, lift zsig t)
|lift zsig (s $ t) = (lift zsig s) $ (lift zsig t)
|lift zsig s = s
(* *********************************************************************** *)
(* *)
(* making Z-Binding Structure explicit *)
(* *)
(* *********************************************************************** *)
(* Schemas can be used "asBoolean" (which is the default in our encoding),
"asSet" or "asPredicate". The function mk_context_adaptor generates
conversions between these three, according to their need in the context
of a term t. This need is expressed by the "expected type" of a term
which is compared to its "result type". The types were represented by
type classes as defined above.
*)
fun add_store_defs S thy =
let val (thy',thms) = PureThy.add_defs true S thy
val H = map (fn((s,_),_) => s) S
val _ = map2 bind_thm (H,thms)
in thy' end;
fun add_store_defs_i S thy =
let val (thy',thms) = PureThy.add_defs_i true S thy
val H = map (fn((s,_),_) => s) S
val _ = map2 bind_thm (H,thms)
in thy' end;
fun add_store_axioms_i S thy =
let val (thy',thms) = PureThy.add_axioms_i S thy
val H = map (fn((s,_),_) => s) S
val _ = map2 bind_thm (H,thms)
in thy' end;
fun top_sg() = #sign(rep_thm(topthm()));
fun pp t = Sign.string_of_term (top_sg()) t;
fun mk_context_adapter sg t0 (expected_type,result_type) t =
let fun sgn t0 = schemasig_of(zSchemaSign sg t0) in
(* delayed for efficency reasons *)
(case (expected_type, result_type) of
(* |- A with A a schema name *)
(Prop,Pred) => Const("ZPure.turnstyle",dummyT)$t
|(Prop,Bool) =>(let val bds = sgn t0
in case bds of
[] => t
| _ => Const("ZPure.turnstyle",dummyT) $
(gen_binder bds t)
end)
|(Prop,x) => error ("internal error: context_adapter 1 "^
(tycl2string x)^" "^(pp t))
(* standard case: convert a rhs to a predicate over signature *)
|(Pred,Bool) => (gen_binder (sgn t0) t)
|(Pred,Other)=> (gen_binder (sgn t0) t)
|(Pred,_) => t
(* |(Pred,x) => error ("internal error: context_adapter 2"^
(tycl2string x)^(pp t))
adapter generator must be admissive - whenever you detect
a context gap, generate a bridge; but since you do not know
the types exactly, do nothing whenever something weird occurs ... *)
(* predicate application: P(x1,...,xn) |-> (x1,...,xn) : P *)
|(Bool,Bool) => t
|(Bool,_) => (case t of
e1 $ e2 => if is_setfun(type_of sg e1)
then Const("asPred",dummyT) $ e1 $ e2
else t
| _ => t)
(* HO predicate applications not supported*)
(* seq (A /\ B) etc. *)
|(Set,Bool) => Const("asSet",dummyT) $
(gen_binder (sgn t0) t )
(* seq A *)
|(Set,Pred) => Const("asSet",dummyT) $ t
|(Set,Set) => t
|(Set,_) => (case t of
Const("SNAME",_)$f$args => Const("asSet",dummyT)$f
| Const("SNAME0",_)$f => Const("asSet",dummyT)$f
(* produces rubbish, but is rubbish anyway *)
| _ => t)
|(Setfun,x) => let fun skip_abs f (Abs(a,ty,t)) = Abs(a,ty, skip_abs f t)
|skip_abs f x = f x
in skip_abs (mk_context_adapter sg t0 (Set,x)) t end
(* |(Set,x) => error ("internal error: context_adapter 3"^
(tycl2string x)^(pp t)) *)
| _ => t)
end
fun exp_binding sg zenv (exp_ty,t) =
let val rty = type_of sg t
in mk_context_adapter sg t (exp_ty,tycl rty)
(case t of
Free("pre",_) $ S =>
let val sgm = filter_zsig (fn (x,_)=> is_stroke_name x
orelse
is_out_name x)
(zSchemaSign sg S)
in Const("PRE",dummyT) $
(gen_binder (schemasig_of sgm)
(exp_binding sg zenv (Bool,S)))
end
|Const("Ball",_)$S$(Abs(s,ty,T)) =>
Const("Ball",dummyT)$
(exp_binding sg zenv (Set, S))$
(Abs(s,ty,abstract_over1(Free(s,ty),
exp_binding sg zenv (Bool,(T)))))
|Const("Bex",_)$S$(Abs(s,ty,T)) =>
Const("Bex",dummyT)$
(exp_binding sg zenv (Set, S))$
(Abs(s,ty,abstract_over1(Free(s,ty),
exp_binding sg zenv (Bool,(T)))))
|Const("All",_)$(Abs(s,ty,T)) =>
Const("All",dummyT)$
(Abs(s,ty,abstract_over1(Free(s,ty),
exp_binding sg zenv (Bool,(T)))))
|Const("Ex",_)$(Abs(s,ty,T)) =>
Const("Ex",dummyT)$
(Abs(s,ty,abstract_over1(Free(s,ty),
exp_binding sg zenv (Bool,(T)))))
|Const("%A",_)$S$T =>
let val sgm = (zSchemaSign sg S)
val S' = exp_binding sg zenv (Set, S)
val T' = exp_binding sg zenv (Bool, T)
(* should be Pred since type signature
of SBall requires `a => bool for this
argument. However, since the context
adaption is done here and not outermost
as in the default, the expected type is set
to bool in order to avoid an own adaption ...*)
in Const("SBall",dummyT) $ S' $
(gen_binder (schemasig_of sgm) T')
end
|Const("%E",_)$S$T =>
let val sgm = (zSchemaSign sg S)
val S' = exp_binding sg zenv (Set, S)
val T' = exp_binding sg zenv (Bool, T)
(* see %A above ... *)
in Const("SBex",dummyT) $ S' $
(gen_binder (schemasig_of sgm) T')
end
|Const("%E1",_)$S$T =>
let val sgm = (zSchemaSign sg S)
val S' = exp_binding sg zenv (Set, S)
val T' = exp_binding sg zenv (Bool, T)
(* see %A above ... *)
in Const("SBex1",dummyT) $ S' $
(gen_binder (schemasig_of sgm) T')
end
|Const("_schset",_) $ S $ T =>
let val sgm = (zSchemaSign sg S)
val S' = exp_binding sg zenv (Set, S)
val T' = exp_binding sg zenv (Bool, T)
in Const("SSet",dummyT) $ S' $
(gen_binder (schemasig_of sgm) T')
end
|e $ e' => let val (hd,args) = strip_comb t
val ty = type_of sg hd
val hd' = exp_binding sg zenv (tycl ty,hd)
val (A,B) = (type_of_doms args ty)
val args' = map2 (exp_binding sg zenv)
(map tycl A,B)
in list_comb(hd',args') end
|Abs(x,t,e) =>
let val ty = if t = dummyT then type_of_appl 1 rty
else type_of_appl 1 t
in Abs(x,t, exp_binding sg zenv (tycl ty,e)) end
|t => t)
end;
fun exp_binding_in_item sg zenv (t as (Const("==",_) $ lhs $ rhs)) =
(* == generated by translations _SCHEME *)
Const("==",dummyT)
$ lhs
$ (exp_binding sg zenv (Pred,rhs))
| exp_binding_in_item sg zenv (Const("op =",_) $ lhs $ rhs) =
(* A <=> B *)
Const("op =",dummyT) $
(exp_binding sg zenv (Pred,lhs)) $
(exp_binding sg zenv (Pred,rhs))
| exp_binding_in_item sg zenv tt =
(* case in goals *)
exp_binding sg zenv (Prop, tt)
(* *********************************************************************** *)
(* *)
(* projection expansion ... *)
(* *)
(* *********************************************************************** *)
fun flat (ls: 'c list list) : 'c list = foldr (op @) [] ls;
fun expand_select zenv ns (Const("_select",_) $ e1 $ (Const(x,_))) =
let val selS = lookup_selectors zenv x
in map (gen_proj x e1)(selS) end
| expand_select zenv ns (Const("_select",_) $ e1 $ (Free(x,_))) =
let val selS = lookup_selectors zenv x
in map (gen_proj x e1)(selS) end
| expand_select zenv ns (Const("_select",_) $ e1 $ (Bound x)) =
let val x = List.nth(ns,x)
val selS = lookup_selectors zenv x
in map (gen_proj x e1)(selS) end
| expand_select zenv ns (A $ B) =
let val A' = expand_select zenv ns A
val B' = expand_select zenv ns B
in flat(map (fn a => map (fn b => a $ b) B') A') end
| expand_select zenv ns (Abs(x,t,e)) = map (fn y => Abs(x,t,y))
(expand_select zenv (x::ns) e)
| expand_select zenv ns X = [X];
(* the overall structure of the conversion:
- lifting
- binding expansion
- selection expansion *)
fun schema_conv sg zenv t =
let fun dest_Trueprop' (Const ("Trueprop", _) $ P) = P
| dest_Trueprop' t = t;
val t = dest_Trueprop' t
fun mk_Trueprop'(P as (Const ("==", _) $ _ $ _)) = P
| mk_Trueprop' P = mk_Trueprop P
in expand_select zenv []
(mk_Trueprop'
(exp_binding_in_item sg zenv
(lift (schemas_of zenv)
(dest_Trueprop' t))))
end
(* *********************************************************************** *)
(* *)
(* parsing ... *)
(* *)
(* *********************************************************************** *)
val ZENV = ref mt_zenv;
val ZENV_test = ref mt_zenv;
fun protect_zenv f x = let val h = !ZENV
val g = f x
in (ZENV := h; g) end;
(* parsing and printing of schemes depends on the internal variable
ZENV. Since this is necessarily updated during interactive
proving, both routines protect the content of this global variable *)
fun schema_parser thy zenv scheme =
let val h = !ZENV;
val t = (ZENV:=zenv;
Syntax.read thy (Sign.is_logtype thy) (syn_of thy) propT (scheme)
(* generates list of raw-term-parses. *)
);
in (ZENV:=h; t) end;
fun string_of_zthm thy zenv thm =
let val h = !ZENV;
val t = (ZENV:=zenv;string_of_thm thm);
in (ZENV:=h; t) end;
(* *********************************************************************** *)
(* *)
(* add operations (main interface) ... *)
(* *)
(* *********************************************************************** *)
fun strip_Zsig (Const("ZPure.SBinder",_) $ _ $ Abs (n,t,T))
= insert_zsig (n,t) (strip_Zsig T)
|strip_Zsig (Const("ZPure.SBinder0",_) $ _ $ Abs (n,t,T))
= insert_zsig (n,t) mt_zsig
|strip_Zsig _ = mt_zsig;
fun strip_Binder (Const("ZPure.SBinder",_) $ _ $ Abs (n,t,T))
= strip_Binder T
|strip_Binder (Const("ZPure.SBinder0",_) $ _ $ Abs (n,t,T))
= T
|strip_Binder T = T
val SCHEMANAMES = ref([]:string list)
val AXDEFS = ref([]:string list)
val CONJECTURES = ref([]:string list)
val FREEDEFS = ref([]:string list)
val PARSES = ref([]:term list);
val PARSES1 = ref([]:term list);
val PARSES2 = ref([]:term list);
fun init () = (SCHEMANAMES := []; AXDEFS :=[];
CONJECTURES:=[]; FREEDEFS:=[];
PARSES := []; PARSES1 := []; PARSES2:= [])
val AXPREP = ref(NONE:((string * thm)->unit) option);
fun init_axprep p = (AXPREP:=SOME p);
fun do_axprep thy (n,thm) = case !AXPREP of
SOME p => (context thy;p(n,thm))
| NONE => ();
fun gen_abs_type_thm str thy =
let val nthm = prove_goalw thy [get_thm thy (Name (str^"_def"))]
("x : "^str)
(K [asm_simp_tac (simpset_of thy) 1])
in fst(PureThy.add_thms [((str^"_simp",nthm),[Simplifier.simp_add_global])] thy)
end
fun add_abs_type ztype thy=
(thy
|> Theory.add_types [(ztype, 0, NoSyn)]
|> Theory.add_arities [(ztype, [], "type")]
|> Theory.add_consts [(ztype, ztype^" set", NoSyn)]
|> add_store_defs [((ztype^"_def",ztype^" == UNIV"),[])] )
|> gen_abs_type_thm ztype;
(* functions for processing free datatype declarations, e.g.:
Report ::= ok| allready_known
KNOWN LIMITATION: 1) DOES ONLY WORK FOR ENUMERATIONS
2) DOES NOT GENERATE "x : tname".
*)
fun add_free_type (dt_types, tname, cons) thy =
let val (thy,{case_thms,distinct,exhaustion,induction,
rec_thms,inject, simps,size, split_thms})
= DatatypePackage.add_datatype
false [tname]
[(dt_types,tname,NoSyn,cons)]
thy
(* TODO: Korrektes Verbuchen all dieser Fakten. *)
(* OLD:
val thy = (tname_add_primrec size_tname_eqns thy)
val _ = deny (quote tname mem (Sign.stamp_names_of (sign_of thy)))
("Datatype \\"^tname^
"\\ would clash with the theory of the same name!\n") *)
in thy
|> Theory.add_consts [(tname, tname^" set", NoSyn)]
|> add_store_defs [((tname^"_def",tname^" == UNIV"),[])]
|> gen_abs_type_thm tname
end
(* FOR DEBUGGING : Global Vars containing the input,
the input after binding expansion, the input after typewchecking *)
fun add_scheme_i thy_name (schemaS,bindsOpt) thy =
let val _ = (PARSES := schemaS @ (!PARSES) );
val zenv = ZTheory.get_zenv thy
(* AND NOW: structural conversion ! ! ! *)
val schemaS = flat(map (schema_conv (sign_of thy) zenv) schemaS)
val _ = (PARSES1 := schemaS);
(* AND NOW: typechecking ! ! ! *)
val (schema,_) = Sign.infer_types (Sign.pp thy) thy
(K NONE) (K NONE) [] true (schemaS,propT)
val _ = (PARSES2:=[schema]);
(* AND NOW: conversion into Isabelle-Definitions ! ! ! *)
in case schema of
(* schema definition >>> *)
(Const ("==", T) $ Free (name,typ) $ D) =>
(let val () = writeln("Converting schema definition "^name^".")
val(typ,D)= case bindsOpt of
SOME _ => if is_set(typ) (* a set expression
denotes a schema *)
then let val tt = (dest_setT typ)-->boolT
in (tt,
Const("ZPure.asPred",typ-->tt)$D)
end (* convert it into predicate
(the default represenation)*)
else (typ,D)
|_ => (typ,D)
val thy1 = Theory.add_consts_i [(name, typ, NoSyn)](thy);
(* This worked in Isabelle98:
val term = Const("==", typ --> typ --> propT)
$ Const (thy_name^"."^name,typ) $ D; *)
(* Now this seems to be more appropriate: *)
val thy_name'= NameSpace.path_of(Sign.naming_of thy1)
val term = Const("==", typ --> typ --> propT)
$ Const (thy_name'^"."^name,typ) $ D;
val thy2 = add_store_defs_i [((name^"_def", term),[])] thy1;
val mm = case bindsOpt of (* if ZETA-type available *)
SOME x => update_zsig(K x)(mt_zsig) (*take it *)
|NONE => strip_Zsig D (* help yourself *)
val zsig1 = if not(null(schemasig_of mm))
(* is it really a schema ? *)
then ZEnv.insert ((name,mm), schemas_of zenv)
else (schemas_of zenv)
val _ = (ZENV_test := update_Zenv_by_Zsig zenv zsig1)
val _ = (SCHEMANAMES:= (name^"_def")::(!SCHEMANAMES))
in ZTheory.put_zenv (update_Zenv_by_Zsig zenv zsig1) (thy2)
end)
|(Const ("==", T) $ Const (name,typ) $ D) =>
error("add_scheme_i: "^ name ^
" was already defined!")
| (* axiomatic definition >>> *)
(Const ("Trueprop",ty) $
(Const ("ZPure.turnstyle", _) $ S)) =>
(let val Zsig{schemasig,...} = strip_Zsig S
val name= (fst(hd schemasig) ^ "_axdef")
val () = (writeln ("Parsing axiomatic definition "^name^"."))
fun cast E = (map (fn (x,y) => (x,y,NoSyn)) E)
val thy = Theory.add_consts_i (cast schemasig) (thy);
val () = (AXDEFS:=(name)::(!AXDEFS))
fun cast2 E = map (fn (x,y) => Const(thy_name^"."^x,y)) E
val S' = subst_bounds(List.rev(cast2 schemasig),
strip_Binder S);
val S'' = Const ("Trueprop",ty) $ S';
val thy = add_store_axioms_i [((name,S''),[])] thy
val _ = do_axprep thy (name,get_axiom thy name)
in thy end)
end;
fun add_scheme thy_name schema thy =
let val zenv = ZTheory.get_zenv thy
in add_scheme_i thy_name ((schema_parser thy zenv schema),NONE) thy end
(* val add_schemes : string list -> ztheory -> ztheory *)
fun add_schemes thy_name S zthy =
foldl (fn(m,zthy) => add_scheme thy_name m zthy) zthy S ;
fun add_schemes_i thy_name S zthy =
foldl (fn(m,zthy) => add_scheme_i thy_name m zthy) zthy S ;
fun add_conjecture_i thy_name conj thy =
let val _ = (PARSES := (!PARSES) @ [conj]);
val zenv = ZTheory.get_zenv thy
(* AND NOW: structural conversion ! ! ! *)
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
| dest_Trueprop t = t;
val conjS = map dest_Trueprop
(schema_conv (sign_of thy) zenv conj)
val _ = (PARSES1 := conjS);
(* AND NOW: typechecking ! ! ! *)
val name = "conjecture_"^(Int.toString(length(!CONJECTURES)))
val thy_name' = NameSpace.path_of(Sign.naming_of thy)
val () = writeln("Converting conjecture "^name^".")
val thy1 = Theory.add_consts_i [(name, boolT, NoSyn)](thy);
val conjS = map (fn conj => (Const ("==", boolT --> boolT --> propT) $
Const (thy_name'^"."^name,boolT) $ conj)) conjS
val (conj',_) = Sign.infer_types (Sign.pp thy) thy1
(K NONE) (K NONE) [] true (conjS,propT)
val _ = (PARSES2:=[conj']);
(* AND NOW: conversion into Isabelle-Definitions ! ! ! *)
val thy2 = add_store_defs_i [((name^"_def", conj'),[])] thy1;
val _ = (CONJECTURES:= (name^"_def")::(!CONJECTURES))
in thy2 end
fun add_conjecture thy_name S thy =
let val zenv = ZTheory.get_zenv thy
in add_conjecture_i thy_name (hd(schema_parser thy zenv S)) thy end
(* *********************************************************************** *)
(* *)
(* OLD STYLE DECLARATIONS ... *)
(* *)
(* *********************************************************************** *)
fun get_schemes thy = map (fn x => (x, get_axiom thy x))(!SCHEMANAMES);
fun get_axdefs thy = map (fn x => (x, get_axiom thy x))(!AXDEFS);
fun get_conjectures thy = map (fn x => (x, get_axiom thy x))(!CONJECTURES);
val string_of_zthm = fn zthy => let val zenv = ZTheory.get_zenv thy
in string_of_zthm thy zenv end
fun schema_read thy zenv schema =
let val ts = schema_parser thy zenv schema;
val _ = (PARSES := ts @ (!PARSES) );
val ts = flat(map (schema_conv (sign_of thy) zenv) ts);
val _ = (PARSES1 := ts @ (!PARSES1) );
val (anno_semterm,_) = Sign.infer_types (Sign.pp thy) thy
(K NONE) (K NONE) [] true (ts,propT)
val _ = (PARSES2 := [anno_semterm] @ (!PARSES2) );
in anno_semterm end;
val schema_read= fn thy => let val zenv = ZTheory.get_zenv thy
in schema_read thy zenv end
end;