[opentheory-users] Fwd: [Hol-checkins] SF.net SVN: hol:[8845] HOL/src/opentheory

Joe Hurd joe at gilith.com
Mon Jan 10 18:58:02 UTC 2011


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
>



More information about the opentheory-users mailing list