[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