[opentheory-users] Fwd: [Hol-checkins] SF.net SVN: hol:[8845] HOL/src/opentheory
Ramana Kumar
ramana.kumar at gmail.com
Mon Jan 10 19:19:49 UTC 2011
Cool - just always go for the latest HOL version (I just checked in
some changes and an additional example).
On Mon, Jan 10, 2011 at 6:58 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> This looks excellent - I will give it a go as soon as I get some time.
>
> Cheers,
>
> Joe
>
> On Mon, Jan 10, 2011 at 9:35 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> My new implementation of the article reader for HOL4 (svn r8845) now
>> successfully reads bool-1.0 (although I didn't check all the theorems
>> were there - it looks reasonable, though).
>>
>> In the HOL repo, src/opentheory/selftest.sml is an example of how to
>> use the reader, and src/opentheory/Opentheory.sig has some descriptive
>> comments.
>>
>>
>> ---------- Forwarded message ----------
>> From: <xrchz at users.sourceforge.net>
>> Date: Mon, Jan 10, 2011 at 5:32 PM
>> Subject: [Hol-checkins] SF.net SVN: hol:[8845] HOL/src/opentheory
>> To: hol-checkins at lists.sf.net
>>
>>
>> Revision: 8845
>> http://hol.svn.sourceforge.net/hol/?rev=8845&view=rev
>> Author: xrchz
>> Date: 2011-01-10 17:32:29 +0000 (Mon, 10 Jan 2011)
>>
>> Log Message:
>> -----------
>> Complete rewrite of Opentheory reader
>>
>> It now successfully reads the package bool-1.0 in the gilith repository,
>> and that is the selftest (only runs if you have opentheory installed).
>>
>> The selftest file is also an example of the work you might need to do to
>> read an opentheory article that defines constants that are already
>> defined in HOL.
>>
>> When the article is only going to define new things, the work would
>> likely be less, although some helper functions (TODO) in the Opentheory
>> module would make it easier.
>>
>> Modified Paths:
>> --------------
>> HOL/src/opentheory/Opentheory.sig
>> HOL/src/opentheory/Opentheory.sml
>> HOL/src/opentheory/selftest.sml
>>
>> Modified: HOL/src/opentheory/Opentheory.sig
>> ===================================================================
>> --- HOL/src/opentheory/Opentheory.sig 2011-01-10 06:01:44 UTC (rev 8844)
>> +++ HOL/src/opentheory/Opentheory.sig 2011-01-10 17:32:29 UTC (rev 8845)
>> @@ -1,12 +1,51 @@
>> signature Opentheory = sig
>> - type thms = Thm.thm Net.net
>> - type types = (string, Type.hol_type list -> Type.hol_type) Redblackmap.dict
>> - type consts = (string, Type.hol_type -> Term.term) Redblackmap.dict
>> - val empty_thms : thms
>> - val empty_types : types
>> - val empty_consts : consts
>> - val thmsFromList : Thm.thm list -> thms
>> - val typesFromList : (string * (Type.hol_type list ->
>> Type.hol_type)) list -> types
>> - val constsFromList : (string * (Type.hol_type -> Term.term)) list -> consts
>> - val read_article : TextIO.instream ->
>> {thms:thms,types:types,consts:consts} -> Thm.thm list
>> +type term = Term.term type hol_type = Type.hol_type type thm = Thm.thm
>> +type ('a,'b) dict = ('a,'b) Redblackmap.dict
>> +
>> +(* maps between OpenTheory names and HOL4 names: *)
>> +type thy_tyop = {Thy:string,Tyop:string}
>> +type thy_const = {Thy:string,Name:string}
>> +type 'a to_ot = ('a,string) dict
>> +type 'a from_ot= (string,'a) dict
>> +val tyop_to_ot : unit -> thy_tyop to_ot
>> +val tyop_from_ot : unit -> thy_tyop from_ot
>> +val const_to_ot : unit -> thy_const to_ot
>> +val const_from_ot: unit -> thy_const from_ot
>> +
>> +(* record of data an article reader must provide: *)
>> +type reader = {
>> + tyops : (string, {axiom:thm, args:hol_type list, rep:string, abs:string} ->
>> + {rep_abs:thm, abs_rep:thm, rep:term, abs:term,
>> tyop:thy_tyop})
>> + dict,
>> + consts : (string, term -> {const:thy_const, def:thm}) dict,
>> + axioms : thm Net.net -> (term list * term) -> thm}
>> +
>> +(*
>> +tyops are type operators the article will define, indexed by their OpenTheory
>> +names. Each name is mapped to a function that does something equivalent to
>> +defining the new type. Each function is provided the type axiom, a list of
>> +arguments (type variables) for the type operator in the desired order, and the
>> +OpenTheory names of the rep and abs constants. It must return the new type
>> +operator, the rep and abs constants, and the type bijection theorems.
>> +If axiom = |- P t then these are:
>> + abs_rep = |- (!a. abs (rep a) = a)
>> + rep_abs = |- (!r. P r = (rep(abs r) = r))
>> +
>> +consts are constants the article will define, indexed by their OpenTheory
>> +names. Each name is mapped to a function that does something equivalent to
>> +defining the new constant. Each function is provided the right hand side rhs of
>> +the definition and must return the name of the constant and an equational
>> +theorem |- const = rhs.
>> +
>> +axioms are theorems that the article depends on about possibly both input
>> +and output tyops and constants. They are represented by a function that takes
>> +the collection of theorems the article has already proved, represented by a
>> +conclusion-indexed net, and a pair (h,c) representing the desired axiom, and
>> +must return a theorem h |- c.
>> +*)
>> +
>> +val raw_read_article : {tyop_from_ot:thy_tyop from_ot,
>> + const_from_ot:thy_const from_ot}
>> + -> TextIO.instream -> reader -> thm list
>> +val read_article : string -> reader -> thm list
>> end
>>
>> Modified: HOL/src/opentheory/Opentheory.sml
>> ===================================================================
>> --- HOL/src/opentheory/Opentheory.sml 2011-01-10 06:01:44 UTC (rev 8844)
>> +++ HOL/src/opentheory/Opentheory.sml 2011-01-10 17:32:29 UTC (rev 8845)
>> @@ -1,221 +1,162 @@
>> structure Opentheory :> Opentheory = struct
>>
>> -val ERR = Feedback.mk_HOL_ERR "Opentheory"
>> +open boolSyntax HolKernel Parse
>>
>> +local open Drule Conv in
>> + fun DEDUCT_ANTISYM th1 th2 =
>> + IMP_ANTISYM_RULE
>> + (DISCH (concl th2) th1)
>> + (DISCH (concl th1) th2)
>> + fun absThm (v,tu) = let
>> + val (t,u) = dest_eq(concl tu)
>> + val vt = mk_abs(v,t)
>> + val vu = mk_abs(v,u)
>> + val vtvu = mk_eq(vt,vu)
>> + val x = FUN_EQ_CONV vtvu
>> + val x = CONV_RULE (RAND_CONV (QUANT_CONV (LAND_CONV BETA_CONV))) x
>> + val x = CONV_RULE (RAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) x
>> + in EQ_MP (SYM x) (GEN v tu) end
>> +end
>> +
>> +val ERR = mk_HOL_ERR "Opentheory"
>> +
>> structure Map = Redblackmap
>> -type thms = Thm.thm Net.net
>> -type types = (string, Type.hol_type list -> Type.hol_type) Map.dict
>> -type consts = (string, Type.hol_type -> Term.term) Map.dict
>> +type ('a,'b) dict = ('a,'b) Map.dict
>>
>> -val empty_thms = Net.empty
>> -val empty_types = Map.mkDict String.compare
>> -val empty_consts = Map.mkDict String.compare
>> -val thmsFromList = List.foldl (fn (th,n) => Net.insert(Thm.concl
>> th,th) n) empty_thms
>> -val typesFromList = Map.fromList String.compare
>> -val constsFromList = Map.fromList String.compare
>> +type thy_tyop = {Thy:string,Tyop:string}
>> +type thy_const = {Thy:string,Name:string}
>> +type 'a to_ot = ('a,string) dict
>> +type 'a from_ot= (string,'a) dict
>> +fun lex_cmp c (f1,f2) (x1,x2) =
>> + case c(f1 x1,f1 x2) of EQUAL => c(f2 x1,f2 x2) | z => z
>> +val thy_tyop_cmp = lex_cmp String.compare (#Tyop,#Thy)
>> +val thy_const_cmp = lex_cmp String.compare (#Name,#Thy)
>> +val the_tyop_to_ot = ref (Map.mkDict thy_tyop_cmp)
>> +val the_tyop_from_ot = ref (Map.mkDict String.compare)
>> +val the_const_to_ot = ref (Map.mkDict thy_const_cmp)
>> +val the_const_from_ot= ref (Map.mkDict String.compare)
>> +fun tyop_to_ot() = !the_tyop_to_ot
>> +fun tyop_from_ot() = !the_tyop_from_ot
>> +fun const_to_ot() = !the_const_to_ot
>> +fun const_from_ot()= !the_const_from_ot
>>
>> datatype object
>> = ONum of int
>> | OName of string
>> | OList of object list
>> -| OTypeOp of string
>> -| OType of Type.hol_type
>> -| OConst of string
>> -| OVar of Term.term
>> -| OTerm of Term.term
>> -| OThm of Thm.thm
>> +| OTypeOp of thy_tyop
>> +| OType of hol_type
>> +| OConst of thy_const
>> +| OVar of term
>> +| OTerm of term
>> +| OThm of thm
>>
>> -datatype command
>> -= Num of int
>> -| Name of string
>> -| AbsTerm
>> -| AbsThm
>> -| AppTerm
>> -| AppThm
>> -| Assume
>> -| Axiom
>> -| BetaConv
>> -| Cons
>> -| Const
>> -| ConstTerm
>> -| DeductAntisym
>> -| Def
>> -| DefineConst
>> -| DefineTypeOp
>> -| EqMp
>> -| Nil
>> -| OpType
>> -| Pop
>> -| Ref
>> -| Refl
>> -| Remove
>> -| Subst
>> -| Thm
>> -| TypeOp
>> -| Var
>> -| VarTerm
>> -| VarType
>> +type reader =
>> + {tyops : (string, {axiom:thm, args:hol_type list, rep:string,
>> abs:string} ->
>> + {rep_abs:thm, abs_rep:thm, rep:term, abs:term,
>> tyop:thy_tyop})
>> + dict,
>> + consts : (string, term -> {const:thy_const, def:thm}) dict,
>> + axioms : thm Net.net -> (term list * term) -> thm}
>>
>> -fun st_ (st,{stack,dict,thms}) = {stack=st,dict=dict,thms=thms}
>> -fun push (ob,state) = st_ (ob::(#stack state),state)
>> -
>> -fun find_thm thms (h,c) = let
>> - val candidates = Net.index c thms
>> - fun equal thm = let
>> - val c' = Thm.concl thm
>> - val thm' = Drule.PART_MATCH Lib.I thm (#2(boolSyntax.strip_forall c))
>> - in Lib.set_eq h (Thm.hyp thm') end handle Feedback.HOL_ERR _ => false
>> - val SOME th = List.find equal candidates
>> -in th end
>> -
>> -fun find_const consts (n,t) = Map.find(consts,n) t
>> -handle Map.NotFound => Term.mk_const(n,t)
>> -handle Feedback.HOL_ERR _ => raise ERR "find_const" ("need "^n^" of
>> type "^(Parse.type_to_string t))
>> -
>> -local open Thm Drule in
>> -fun DEDUCT_ANTISYM th1 th2 =
>> - IMP_ANTISYM_RULE
>> - (DISCH (concl th1) th2)
>> - (DISCH (concl th2) th1)
>> +fun st_(st,{stack,dict,thms}) = {stack=st,dict=dict,thms=thms}
>> +fun push (ob,st) = st_(ob::(#stack st),st)
>> +local open Substring in
>> + val trimlr = fn s => string(trimr 1 (triml 1 (full s)))
>> + val trimr = fn s => string(trimr 1 (full s))
>> end
>>
>> -val unOTermls = List.map (fn OTerm t => t)
>> -val unOTypels = List.map (fn OType t => t)
>> -val unONamels = List.map (fn OName n => n)
>> -
>> -fun find_type types (t,ls) = let
>> - val ls = unOTypels ls
>> -in
>> - (Map.find(types,t)) ls
>> - handle Map.NotFound => let
>> - val s = Parse.type_to_string(Type.mk_type(t,ls))
>> - handle Feedback.HOL_ERR _ =>
>> - (* PolyML.makestring (t, (Map.listItems types)) *)
>> - ("TyOp = "^t^", Args = "^(String.concatWith ", " (List.map
>> Parse.type_to_string ls)))
>> - in raise ERR "find_type" ("need "^s) end
>> -end
>> -
>> -exception Comment
>> -
>> -fun
>> - parse_line "absTerm" = AbsTerm
>> -| parse_line "absThm" = AbsThm
>> -| parse_line "appTerm" = AppTerm
>> -| parse_line "appThm" = AppThm
>> -| parse_line "assume" = Assume
>> -| parse_line "axiom" = Axiom
>> -| parse_line "betaConv" = BetaConv
>> -| parse_line "cons" = Cons
>> -| parse_line "const" = Const
>> -| parse_line "constTerm" = ConstTerm
>> -| parse_line "deductAntisym" = DeductAntisym
>> -| parse_line "def" = Def
>> -| parse_line "defineConst" = DefineConst
>> -| parse_line "defineTypeOp" = DefineTypeOp
>> -| parse_line "eqMp" = EqMp
>> -| parse_line "nil" = Nil
>> -| parse_line "opType" = OpType
>> -| parse_line "pop" = Pop
>> -| parse_line "ref" = Ref
>> -| parse_line "refl" = Refl
>> -| parse_line "remove" = Remove
>> -| parse_line "subst" = Subst
>> -| parse_line "thm" = Thm
>> -| parse_line "typeOp" = TypeOp
>> -| parse_line "var" = Var
>> -| parse_line "varTerm" = VarTerm
>> -| parse_line "varType" = VarType
>> -| parse_line s = let
>> - val c = String.sub(s,0)
>> - in if c = #"\"" then Name (String.substring(s,1,String.size s -2)) else
>> - if Char.isDigit c then Num (Option.valOf (Int.fromString s))
>> - else raise Comment
>> - end
>> -
>> -fun read_article file {types,consts,thms} = let
>> - val find_asm = find_thm thms
>> - val find_const = find_const consts
>> - val find_type = find_type types
>> - fun f (Num i) st = push(ONum i,st)
>> - | f (Name s) st = push(OName s,st)
>> - | f AbsTerm (st as {stack=OTerm b::OVar v::os,...}) =
>> st_(OTerm(Term.mk_abs(v,b))::os,st)
>> - | f AppTerm (st as {stack=OTerm x::OTerm f::os,...}) =
>> st_(OTerm(Term.mk_comb(f,x))::os,st)
>> - | f AppThm (st as {stack=OThm xy::OThm fg::os,...}) = let
>> - val (f,g) = boolSyntax.dest_eq(Thm.concl fg)
>> - val (x,y) = boolSyntax.dest_eq(Thm.concl xy)
>> - val fxgx = Thm.AP_THM fg x
>> - val gxgy = Thm.AP_TERM g xy
>> - in st_(OThm(Thm.TRANS fxgx gxgy)::os,st) end
>> - | f Assume (st as {stack=OTerm t::os,...}) =
>> st_(OThm(Thm.ASSUME t)::os,st)
>> - | f Axiom (st as {stack=OTerm t::OList ts::os,...}) =
>> st_(OThm(find_asm(unOTermls ts,t))::os,st)
>> - | f BetaConv (st as {stack=OTerm t::os,...}) =
>> st_(OThm(Thm.BETA_CONV t)::os,st)
>> - | f Cons (st as {stack=OList t::h::os,...}) =
>> st_(OList(h::t)::os,st)
>> - | f Const (st as {stack=OName n::os,...}) =
>> st_(OConst n::os,st)
>> - | f ConstTerm (st as {stack=OType t::OConst c::os,...}) =
>> st_(OTerm(find_const (c,t))::os,st)
>> - | f DeductAntisym (st as {stack=OThm t1::OThm t2::os,...}) =
>> st_(OThm(DEDUCT_ANTISYM t1 t2)::os,st)
>> - | f Def {stack=ONum k::x::os,dict,thms} =
>> {stack=x::os,dict=Map.insert(dict,k,x),thms=thms}
>> - | f DefineConst (st as {stack=OTerm t::OName n::os,...}) = let
>> - val t = boolSyntax.mk_eq(Term.mk_var(n,Term.type_of t),t)
>> - val def = Definition.new_definition(n,t)
>> - handle Feedback.HOL_ERR _ => raise ERR "read_article"
>> ("DefineConst "^n^" by "^Parse.term_to_string t^" failed")
>> - in st_(OThm def::OConst n::os,st) end
>> - | f DefineTypeOp (st as {stack=OThm th::OList ls::OName
>> rep::OName abs::OName n::os,...}) = let
>> - val ls = unONamels ls
>> - val sorted = Lib.sort (Lib.curry (Lib.equal LESS o String.compare)) ls
>> - val s = let fun f (a,a',s) = if a = a' then s else let
>> - val a = Type.mk_vartype a
>> - val a' = Type.mk_vartype a'
>> - val op |-> = Lib.|-> infix |->
>> - in (a |-> a')::(a' |-> a)::s end
>> - in ListPair.foldlEq f [] (ls,sorted) end
>> - val th = Thm.INST_TYPE s th
>> - val Pt = Thm.concl th
>> - val (P,t) = Term.dest_comb(Pt)
>> - val th = Thm.EXISTS(boolSyntax.mk_exists(t,Pt),t) th
>> - val tyax = Definition.new_type_definition(n,th)
>> - val th = Drule.define_new_type_bijections
>> {name=n^"_repfns",ABS=abs,REP=rep,tyax=tyax}
>> - val th1 = Drule.SPEC_ALL (Thm.CONJUNCT1 th)
>> - val th2 = Drule.SPEC_ALL (Thm.CONJUNCT2 th)
>> - in st_(OThm th2::OThm th1::OConst rep::OConst abs::OTypeOp n::os,st) end
>> - | f EqMp (st as {stack=OThm fg::OThm f::os,...}) =
>> st_(OThm(Thm.EQ_MP fg f)::os,st)
>> - | f Nil st = push(OList [],st)
>> - | f OpType (st as {stack=OList ls::OTypeOp t::os,...}) =
>> st_(OType(find_type(t,ls))::os,st)
>> - | f Pop (st as {stack=x::os,...}) = st_(os,st)
>> - | f Ref (st as {stack=ONum k::os,dict,...}) =
>> st_(Map.find(dict,k)::os,st)
>> - | f Refl (st as {stack=OTerm t::os,...}) =
>> st_(OThm(Thm.REFL t)::os,st)
>> - | f Remove {stack=ONum k::os,dict,thms} = let
>> +fun raw_read_article {tyop_from_ot,const_from_ot} input
>> {tyops,consts,axioms} = let
>> + val ERR = ERR "read_article"
>> + fun unOTermls c = List.map (fn OTerm t => t | _ => raise ERR (c^"
>> failed to pop a list of terms"))
>> + fun unOTypels c = List.map (fn OType t => t | _ => raise ERR (c^"
>> failed to pop a list of types"))
>> + fun ot_to_const c s = Map.find(const_from_ot,s)
>> + handle Map.NotFound => raise ERR (c^": no map from "^s^" to a constant")
>> + fun ot_to_tyop c s = Map.find(tyop_from_ot ,s)
>> + handle Map.NotFound => raise ERR (c^": no map from "^s^" to a type operator")
>> + fun f "absTerm"(st as {stack=OTerm b::OVar v::os,...}) =
>> st_(OTerm(mk_abs(v,b))::os,st)
>> + | f "absThm" (st as {stack=OThm th::OVar v::os,...}) =
>> (st_(OThm(absThm(v,th))::os,st)
>> + handle HOL_ERR e => raise ERR ("absThm: failed with "^format_ERR e))
>> + | f "appTerm"(st as {stack=OTerm x::OTerm f::os,...})=
>> st_(OTerm(mk_comb(f,x))::os,st)
>> + | f "appThm" (st as {stack=OThm xy::OThm fg::os,...})= let
>> + val (f,g) = dest_eq(concl fg)
>> + val (x,y) = dest_eq(concl xy)
>> + val fxgx = AP_THM fg x
>> + val gxgy = AP_TERM g xy
>> + in st_(OThm(TRANS fxgx gxgy)::os,st) end
>> + | f "assume" (st as {stack=OTerm t::os,...}) =
>> st_(OThm(ASSUME t)::os,st)
>> + | f "axiom" (st as {stack=OTerm t::OList ts::os,thms,...})
>> = st_(OThm(axioms thms (unOTermls "axiom" ts,t))::os,st)
>> + | f "betaConv" (st as {stack=OTerm t::os,...}) =
>> st_(OThm(BETA_CONV t)::os,st)
>> + | f "cons" (st as {stack=OList t::h::os,...}) =
>> st_(OList(h::t)::os,st)
>> + | f "const" (st as {stack=OName n::os,...}) =
>> st_(OConst (ot_to_const "const" n)::os,st)
>> + | f "constTerm" (st as {stack=OType Ty::OConst {Thy,Name}::os,...})
>> + = st_(OTerm(mk_thy_const
>> {Ty=Ty,Thy=Thy,Name=Name})::os,st)
>> + | f "deductAntisym"(st as {stack=OThm t1::OThm t2::os,...}) =
>> st_(OThm(DEDUCT_ANTISYM t1 t2)::os,st)
>> + | f "def" {stack=ONum k::x::os,dict,thms} =
>> {stack=x::os,dict=Map.insert(dict,k,x),thms=thms}
>> + | f "defineConst" (st as {stack=OTerm t::OName n::os,...}) = let
>> + val {const,def} = Map.find(consts,n) t
>> + handle Map.NotFound => raise ERR ("defineConst: no map from
>> "^n^" to a definition function")
>> + in st_(OThm def::OConst const::os,st) end
>> + | f "defineTypeOp" (st as {stack=OThm th::OList ls::OName
>> rep::OName abs::OName n::os,...}) = let
>> + val ls = List.map (fn OName s => mk_vartype s | _ => raise
>> ERR "defineTypeOp failed to pop a list of names") ls
>> + val {abs,rep,abs_rep,rep_abs,tyop} = Map.find(tyops,n)
>> {axiom=th,args=ls,rep=rep,abs=abs}
>> + val {Thy,Name,...} = dest_thy_const rep val rep = {Thy=Thy,Name=Name}
>> + val {Thy,Name,...} = dest_thy_const abs val abs = {Thy=Thy,Name=Name}
>> + in st_(OThm rep_abs::OThm abs_rep::OConst rep::OConst
>> abs::OTypeOp tyop::os,st) end
>> + | f "eqMp" (st as {stack=OThm f::OThm fg::os,...}) =
>> (st_(OThm(EQ_MP fg f)::os,st)
>> + handle HOL_ERR _ => raise ERR ("EqMp failed on "^thm_to_string
>> fg^" and "^thm_to_string f))
>> + | f "nil" st =
>> push(OList [],st)
>> + | f "opType" (st as {stack=OList ls::OTypeOp {Thy,Tyop}::os,...})
>> + =
>> st_(OType(mk_thy_type{Thy=Thy,Tyop=Tyop,Args=unOTypels "opType"
>> ls})::os,st)
>> + | f "pop" (st as {stack=x::os,...}) = st_(os,st)
>> + | f "ref" (st as {stack=ONum k::os,dict,...}) =
>> st_(Map.find(dict,k)::os,st)
>> + | f "refl" (st as {stack=OTerm t::os,...}) =
>> st_(OThm(REFL t)::os,st)
>> + | f "remove" {stack=ONum k::os,dict,thms} = let
>> val (dict,x) = Map.remove(dict,k)
>> in {stack=x::os,dict=dict,thms=thms} end
>> - | f Subst (st as {stack=OThm th::OList[OList tys,OList
>> tms]::os,...}) = let
>> - val tys = List.map (fn OList [OName a, OType t] =>
>> {redex=Type.mk_vartype a, residue=t}) tys
>> - val tms = List.map (fn OList [OVar v, OTerm t] => {redex=v,
>> residue=t}) tms
>> - val th = Thm.INST_TYPE tys th
>> - val th = Thm.INST tms th
>> + | f "subst" (st as {stack=OThm th::OList[OList tys,OList
>> tms]::os,...}) = let
>> + val tys = List.map (fn OList [OName a, OType t] =>
>> {redex=mk_vartype a, residue=t}
>> + | _ => raise ERR "subst failed to pop a
>> list of [name,type] pairs") tys
>> + val tms = List.map (fn OList [OVar v, OTerm t] => {redex=v, residue=t}
>> + | _ => raise ERR "subst failed to pop a
>> list of [var,term] pairs") tms
>> + val th = INST_TYPE tys th
>> + val th = INST tms th
>> in st_(OThm th::os,st) end
>> - | f Thm {stack=OTerm c::OList ls::OThm th::os,dict,thms} = let
>> - val th = Thm.EQ_MP (Thm.ALPHA (Thm.concl th) c) th
>> + | f "thm" {stack=OTerm c::OList ls::OThm th::os,dict,thms} = let
>> + val th = EQ_MP (ALPHA (concl th) c) th
>> + handle HOL_ERR _ => raise ERR "thm: desired conclusion not
>> alpha-equivalent to theorem's conclusion"
>> fun ft (OTerm h, th) = let
>> - val c = Thm.concl th
>> - val th = Thm.DISCH h th
>> - val c' = Thm.concl th
>> + val c = concl th
>> + val th = DISCH h th
>> + val c' = concl th
>> in
>> - if Term.aconv c c' then
>> + if aconv c c' then
>> Drule.ADD_ASSUM h th
>> else let
>> val (h',_) = boolSyntax.dest_imp c'
>> - val h'h = Thm.ALPHA h' h
>> + val h'h = ALPHA h' h
>> val th = Drule.SUBS_OCCS [([1],h'h)] th
>> in Drule.UNDISCH th end
>> - end
>> + end | ft _ = raise ERR "thm failed to pop a list of terms"
>> val th = List.foldl ft th ls
>> - in {stack=os,dict=dict,thms=th::thms} end
>> - | f TypeOp (st as {stack=OName n::os,...}) =
>> st_(OTypeOp n::os,st)
>> - | f Var (st as {stack=OType t::OName n::os,...}) =
>> st_(OVar(Term.mk_var(n,t))::os,st)
>> - | f VarTerm (st as {stack=OVar t::os,...}) = st_(OTerm t::os,st)
>> - | f VarType (st as {stack=OName n::os,...}) =
>> st_(OType(Type.mk_vartype n)::os,st)
>> - fun stripnl s = let open Substring in string(trimr 1 (full s)) end
>> - fun loop x = case TextIO.inputLine file of
>> - NONE => x before TextIO.closeIn(file)
>> - | SOME line => loop (f (parse_line (stripnl line)) x handle Comment => x)
>> -in #thms (loop {stack=[],dict=Map.mkDict(Int.compare),thms=[]}) end
>> + in {stack=os,dict=dict,thms=Net.insert(concl th,th)thms} end
>> + | f "typeOp" (st as {stack=OName n::os,...}) =
>> st_(OTypeOp (ot_to_tyop "typeOp" n)::os,st)
>> + | f "var" (st as {stack=OType t::OName n::os,...}) =
>> st_(OVar(mk_var(n,t))::os,st)
>> + | f "varTerm" (st as {stack=OVar t::os,...}) =
>> st_(OTerm t::os,st)
>> + | f "varType" (st as {stack=OName n::os,...}) =
>> st_(OType(mk_vartype n)::os,st)
>> + | f s st = let val c = String.sub(s,0) open Char Option Int
>> + in if c = #"\"" then push(OName(valOf(String.fromString (trimlr
>> s))),st) else
>> + if isDigit c then push(ONum(valOf(fromString s)),st) else
>> + if c = #"#" then st else
>> + raise ERR ("Unknown command: "^s)
>> + end
>> + fun loop x = case TextIO.inputLine input of
>> + NONE => x before TextIO.closeIn(input)
>> + | SOME line => loop (f (trimr line) x)
>> +in Net.listItems (#thms (loop
>> {stack=[],dict=Map.mkDict(Int.compare),thms=Net.empty})) end
>> +
>> +fun read_article s r =
>> + raw_read_article
>> + {tyop_from_ot=tyop_from_ot(),
>> + const_from_ot=const_from_ot()}
>> + (TextIO.openIn s) r
>> end
>>
>> Modified: HOL/src/opentheory/selftest.sml
>> ===================================================================
>> --- HOL/src/opentheory/selftest.sml 2011-01-10 06:01:44 UTC (rev 8844)
>> +++ HOL/src/opentheory/selftest.sml 2011-01-10 17:32:29 UTC (rev 8845)
>> @@ -1,17 +1,63 @@
>> -open Opentheory
>> +open Opentheory boolTheory boolLib bossLib HolKernel
>> fun cmd pkg out = ("opentheory info --article -o "^out^" "^pkg)
>> -val pkg = "bool-def-1.0"
>> -val tmp = OS.FileSys.tmpName()
>> -val _ = if OS.Process.isSuccess(Systeml.system_ps (cmd pkg tmp)) then let
>> -val thms = read_article (TextIO.openIn tmp) {
>> - thms=empty_thms,
>> +val pkg = "bool-1.0"
>> +(*
>> +show: "Data.Bool"
>> +input type operators: -> bool
>> +input constants: = select
>> +assumptions:
>> +defined constants: ! /\ ==> ? ?! \/ ~ cond let F T
>> +axioms:
>> + |- !t. (\x. t x) = t
>> + |- !P x. P x ==> P ((select) P)
>> +
>> types=typesFromList
>> [("bool",fn [] => Type.bool),
>> ("->",fn ls => Type.mk_type("fun",ls))],
>> consts=constsFromList
>> [("=",fn ty => Term.mk_const("=",ty)),
>> - ("Data.Bool.select",fn ty => Term.mk_const("@",ty))]}
>> -val thms = thmsFromList thms
>> + ("Data.Bool.select",fn ty => Term.mk_const("@",ty))]
>> +*)
>> +val tmp = OS.FileSys.tmpName()
>> +val _ = if OS.Process.isSuccess(Systeml.system_ps (cmd pkg tmp)) then let
>> +val input = TextIO.openIn tmp
>> +val tyop_from_ot = Redblackmap.fromList String.compare [
>> + ("bool",{Thy="min",Tyop="bool"}),
>> + ("->",{Thy="min",Tyop="fun"})]
>> +val const_from_ot = Redblackmap.fromList String.compare [
>> + ("=",{Thy="min",Name="="}),
>> + ("Data.Bool.select",{Thy="min",Name="@"})]
>> +val A = INST_TYPE[alpha|->mk_vartype"A",beta|->mk_vartype"B"]
>> +val reader = {
>> + tyops=Redblackmap.mkDict String.compare,
>> + consts=
>> + Redblackmap.fromList String.compare [
>> + ("Data.Bool.!", fn _ => {const={Thy="bool",Name="!"},def=A FORALL_DEF}),
>> + ("Data.Bool./\\", let
>> + val th = prove(``$/\ = \p q. (\f. f p q) =
>> \f:bool->bool->bool. f T T``,
>> + SRW_TAC [][AND_DEF,FUN_EQ_THM] THEN EQ_TAC
>> THEN SRW_TAC [][])
>> + in fn _ => {const={Thy="bool",Name="/\\"},def=th} end),
>> + ("Data.Bool.==>",let
>> + val th = METIS_PROVE [] ``$==> = \p q. p /\ q <=> p``
>> + in fn _ => {const={Thy="min",Name="==>"},def=th} end),
>> + ("Data.Bool.?", let
>> + val th = prove(``$? = \P. !q. (!x. P x ==> q) ==> q``,
>> + SRW_TAC [][EXISTS_DEF,FUN_EQ_THM,EQ_IMP_THM] THEN
>> + FIRST_X_ASSUM MATCH_MP_TAC THEN METIS_TAC [SELECT_AX])
>> + in fn _ => {const={Thy="bool",Name="?"},def=A th} end),
>> + ("Data.Bool.?!", fn _ => {const={Thy="bool",Name="?!"},def=A
>> EXISTS_UNIQUE_DEF}),
>> + ("Data.Bool.\\/", fn _ => {const={Thy="bool",Name="\\/"},def=OR_DEF}),
>> + ("Data.Bool.~", fn _ => {const={Thy="bool",Name="~"},def=NOT_DEF}),
>> + ("Data.Bool.cond", fn _ =>
>> {const={Thy="bool",Name="COND"},def=A COND_DEF}),
>> + ("Data.Bool.let", fn _ => {const={Thy="bool",Name="LET"},def=A LET_DEF}),
>> + ("Data.Bool.F", fn _ => {const={Thy="bool",Name="F"},def=F_DEF}),
>> + ("Data.Bool.T", fn _ => {const={Thy="bool",Name="T"},def=T_DEF})],
>> + axioms=let open List Net Thm
>> + fun ins th = insert(concl th,th)
>> + val n = ins (A ETA_AX) (ins (A SELECT_AX) empty)
>> + fun f _ (_,c) = hd (index c n)
>> + in f end }
>> +val thms = raw_read_article {tyop_from_ot=tyop_from_ot,
>> const_from_ot=const_from_ot} input reader
>> (* TODO: check that thms is the same set that opentheory
>> says the package should have produced *)
>> in () end else ()
>>
>>
>> This was sent by the SourceForge.net collaborative development
>> platform, the world's largest Open Source development site.
>>
>> ------------------------------------------------------------------------------
>> Gaining the trust of online customers is vital for the success of any company
>> that requires sensitive data to be transmitted over the Web. Learn how to
>> best implement a security strategy that keeps consumers' information secure
>> and instills the confidence they need to proceed with transactions.
>> http://p.sf.net/sfu/oracle-sfdevnl
>> _______________________________________________
>> Hol-checkins mailing list
>> Hol-checkins at lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-checkins
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
More information about the opentheory-users
mailing list