# HG changeset patch # User oheimb # Date 850918573 -3600 # Node ID 51993fea433fd6844c24405433338dc3983f56d0 # Parent 150644698367bb629b2fbddb838de7679d3b6a78 removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2 diff -r 150644698367 -r 51993fea433f src/HOLCF/Holcfb.ML --- a/src/HOLCF/Holcfb.ML Wed Dec 18 15:13:50 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: HOLCF/holcfb.ML - ID: $Id$ - Author: Franz Regensburger - Changed by: David von Oheimb - Copyright 1993 Technische Universitaet Muenchen -*) - - -open Holcfb; - -(* ------------------------------------------------------------------------ *) -(* Some lemmas in HOL.thy *) -(* ------------------------------------------------------------------------ *) - - - -val classical3 = (notE RS notI); (* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *) diff -r 150644698367 -r 51993fea433f src/HOLCF/Holcfb.thy --- a/src/HOLCF/Holcfb.thy Wed Dec 18 15:13:50 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ -(* Title: HOLCF/holcfb.thy - ID: $Id$ - Author: Franz Regensburger - Copyright 1993 Technische Universitaet Muenchen - -Basic definitions for the embedding of LCF into HOL. - -*) - -Holcfb = Nat diff -r 150644698367 -r 51993fea433f src/HOLCF/Makefile --- a/src/HOLCF/Makefile Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/Makefile Wed Dec 18 15:16:13 1996 +0100 @@ -21,14 +21,14 @@ BIN = $(ISABELLEBIN) COMP = $(ISABELLECOMP) -THYS = Holcfb.thy Void.thy Porder.thy Pcpo.thy \ +THYS = Void.thy Porder.thy Pcpo.thy \ Fun1.thy Fun2.thy Fun3.thy \ Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ Cprod1.thy Cprod2.thy Cprod3.thy \ Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \ - Tr1.thy Tr2.thy HOLCF.thy + Tr1.thy Tr2.thy Lift1.thy Lift2.thy Lift2.thy HOLCF.thy FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML) diff -r 150644698367 -r 51993fea433f src/HOLCF/One.ML --- a/src/HOLCF/One.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/One.ML Wed Dec 18 15:16:13 1996 +0100 @@ -45,7 +45,7 @@ prove_goalw One.thy [one_def] "~one << UU" (fn prems => [ - (rtac classical3 1), + (rtac classical2 1), (rtac less_up4b 1), (rtac (rep_one_iso RS subst) 1), (rtac (rep_one_iso RS subst) 1), @@ -96,4 +96,3 @@ val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"]; -Addsimps (one_when @ dist_less_one @ dist_eq_one); \ No newline at end of file diff -r 150644698367 -r 51993fea433f src/HOLCF/Pcpo.ML --- a/src/HOLCF/Pcpo.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/Pcpo.ML Wed Dec 18 15:16:13 1996 +0100 @@ -187,7 +187,7 @@ (fn prems => [ (cut_facts_tac prems 1), - (rtac classical3 1), + (rtac classical2 1), (atac 1), (hyp_subst_tac 1), (rtac refl_less 1) diff -r 150644698367 -r 51993fea433f src/HOLCF/Tr1.ML --- a/src/HOLCF/Tr1.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/Tr1.ML Wed Dec 18 15:16:13 1996 +0100 @@ -16,7 +16,7 @@ prove_goalw Tr1.thy [TT_def] "~TT << UU" (fn prems => [ - (rtac classical3 1), + (rtac classical2 1), (rtac defined_sinl 1), (rtac not_less2not_eq 1), (resolve_tac dist_less_one 1), @@ -29,7 +29,7 @@ prove_goalw Tr1.thy [FF_def] "~FF << UU" (fn prems => [ - (rtac classical3 1), + (rtac classical2 1), (rtac defined_sinr 1), (rtac not_less2not_eq 1), (resolve_tac dist_less_one 1), @@ -42,7 +42,7 @@ prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF" (fn prems => [ - (rtac classical3 1), + (rtac classical2 1), (rtac (less_ssum4c RS iffD1) 2), (rtac not_less2not_eq 1), (resolve_tac dist_less_one 1), @@ -53,7 +53,7 @@ prove_goalw Tr1.thy [FF_def,TT_def] "~FF << TT" (fn prems => [ - (rtac classical3 1), + (rtac classical2 1), (rtac (less_ssum4d RS iffD1) 2), (rtac not_less2not_eq 1), (resolve_tac dist_less_one 1), diff -r 150644698367 -r 51993fea433f src/HOLCF/Void.thy --- a/src/HOLCF/Void.thy Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/Void.thy Wed Dec 18 15:16:13 1996 +0100 @@ -9,7 +9,7 @@ Type void is defined as a set Void over type bool. *) -Void = Holcfb + +Void = Nat + types void 0 diff -r 150644698367 -r 51993fea433f src/HOLCF/domain/extender.ML --- a/src/HOLCF/domain/extender.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/domain/extender.ML Wed Dec 18 15:16:13 1996 +0100 @@ -1,14 +1,11 @@ -(* extender.ML - Author : David von Oheimb - Created: 17-May-95 - Updated: 31-May-95 extracted syntax.ML, theorems.ML - Updated: 07-Jul-95 streamlined format of cons list - Updated: 21-Jul-95 gen_by-section - Updated: 28-Aug-95 simultaneous domain equations - Copyright 1995 TU Muenchen +(* Title: HOLCF/domain/extender.ML + ID: $Id$ + Author : David von Oheimb + Copyright 1995, 1996 TU Muenchen + +theory extender for domain section *) - structure Domain_Extender = struct @@ -16,53 +13,77 @@ open Domain_Library; -(* ----- general testing and preprocessing of constructor list -------------------- *) +(* ----- general testing and preprocessing of constructor list -------------- *) - fun check_domain(eqs':((string * typ list) * - (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let - val dtnvs = map fst eqs'; - val cons' = flat (map snd eqs'); + fun check_and_sort_domain (eqs'':((string * typ list) * + (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = let + val dtnvs = map fst eqs''; + val cons' = flat (map snd eqs''); val test_dupl_typs = (case duplicates (map fst dtnvs) of [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); val test_dupl_cons = (case duplicates (map first cons') of [] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups)); val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of - [] => false | dups => error ("Duplicate selectors: "^commas_quote dups)); - val test_dupl_tvars = let fun vname (TFree(v,_)) = v - | vname _ = Imposs "extender:vname"; - in exists (fn tvars => case duplicates (map vname tvars) of - [] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups)) - (map snd dtnvs) end; - (*test for free type variables and invalid use of recursive type*) - val analyse_types = forall (fn ((_,typevars),cons') => - forall (fn con' => let + [] => false | dups => error("Duplicate selectors: "^commas_quote dups)); + val test_dupl_tvars = exists(fn s=>case duplicates(map(fst o rep_TFree)s)of + [] => false | dups => error("Duplicate type arguments: " + ^commas_quote dups)) + (map snd dtnvs); + val default = ["_default"]; + (*test for free type variables, Inconsistent sort constraints, + non-pcpo-types and invalid use of recursive type*) + in map (fn ((dname,typevars),cons') => let + val tvars = ref (map rep_TFree typevars) : (string * sort) list ref; + fun newsort (TFree(v,s)) = TFree(v,case assoc_string (!tvars,v) of + None => Imposs "extender:newsort" + | Some s => if s=default then Type.defaultS(tsig_of thy'') else s) + | newsort (Type(s,typl)) = Type(s,map newsort typl) + | newsort (TVar _) = Imposs "extender:newsort 2"; + val analyse_cons = forall (fn con' => let val types = map third (third con'); - fun analyse(t as TFree(v,_)) = t mem typevars orelse - error ("Free type variable " ^ v ^ " on rhs.") - | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl - | Some tvs => tvs = typl orelse - error ("Recursion of type " ^ s ^ " with different arguments")) - | analyse(TVar _) = Imposs "extender:analyse" - and analyses ts = forall analyse ts; - in analyses types end) cons' - ) eqs'; - in true end; (* let *) - + fun rm_sorts (TFree(s,_)) = TFree(s,[]) + | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) + | rm_sorts (TVar(s,_)) = TVar(s,[]) + and remove_sorts l = map rm_sorts l; + fun analyse(TFree(v,s)) = (case assoc_string(!tvars,v) of + None => error ("Free type variable " ^ v ^ " on rhs.") + | Some sort => s = default orelse + if sort = default + then (tvars:= (v,s):: !tvars;true) + else eq_set_string (s,sort) orelse + error ("Inconsistent sort constraints "^ + "for type variable "^quote v)) + | analyse(Type(s,typl)) = (case assoc_string (dtnvs,s) of + None => forall analyse typl + | Some tvs => remove_sorts tvs = remove_sorts typl orelse + error ("Recursion of type " ^ s ^ + " with different arguments")) + | analyse(TVar _) = Imposs "extender:analyse"; + in forall analyse types end) cons'; + fun check_pcpo t = (pcpo_type thy'' t orelse + error("Not a pcpo type: "^string_of_typ thy'' t); t); + fun check_type (t as Type(s,typl)) = (case assoc_string (dtnvs,s) of + None => check_pcpo t | Some _ => t) + | check_type t = check_pcpo t; + in ((dname,map newsort typevars), + map (upd_third (map (upd_third (check_type o newsort)))) cons') + end) eqs'' + end; (* let *) fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let val test_dupl_typs = (case duplicates typs' of [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); - val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false - | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss'; - val tsig = #tsig(Sign.rep_sg(sign_of thy')); - val tycons = map fst (#tycons(Type.rep_tsig tsig)); - val test_types = forall(fn t=>t mem tycons orelse error("Unknown type: "^t))typs'; + val test_dupl_cnstrs = map (fn cs => (case duplicates cs of [] => false + | ds => error ("Duplicate constructors: " ^ commas_quote ds))) cnstrss'; + val tycons = map fst (#tycons(Type.rep_tsig (tsig_of thy'))); + val test_types = forall (fn t => t mem tycons orelse + error("Unknown type: "^t)) typs'; val cnstrss = let fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t | None => error ("Unknown constructor: "^c); fun args_result_type (t as (Type(tn,[arg,rest]))) = - if tn = "->" orelse tn = "=>" - then let val (ts,r) = args_result_type rest in (arg::ts,r) end - else ([],t) + if tn = "->" orelse tn = "=>" + then let val (ts,r) = args_result_type rest in (arg::ts,r) end + else ([],t) | args_result_type t = ([],t); in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in (cn,mk_var_names args,(args,res)) end)) cnstrss' @@ -71,21 +92,22 @@ (typ list * (* argument types *) typ)) (* result type *) list list end; - fun test_equal_type tn (cn,_,(_,rt)) = fst (type_name_vars rt) = tn orelse - error("Inappropriate result type for constructor "^cn); + fun test_equal_type tn (cn,_,(_,rt)) = fst (rep_Type rt) = tn orelse + error("Inappropriate result type for constructor "^cn); val typs = map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs; - snd(third(hd(cnstrs))))) (typs'~~cnstrss); + snd(third(hd(cnstrs))))) (typs'~~cnstrss); val test_typs = map (fn (typ,cnstrs) => - if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"]))) - then error("Not a pcpo type: "^fst(type_name_vars typ)) - else map (fn (cn,_,(_,rt)) => rt=typ - orelse error("Non-identical result types for constructors "^ - first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss); + if not (pcpo_type thy' typ) + then error("Not a pcpo type: "^string_of_typ thy' typ) + else map (fn (cn,_,(_,rt)) => rt=typ orelse error( + "Non-identical result types for constructors "^ + first(hd cnstrs)^" and "^ cn )) cnstrs) + (typs~~cnstrss); val proper_args = let fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts | occurs _ _ = false; fun proper_arg cn atyp = forall (fn typ => let - val tn = fst(type_name_vars typ) + val tn = fst (rep_Type typ) in atyp=typ orelse not (occurs tn atyp) orelse error("Illegal use of type "^ tn ^ " as argument of constructor " ^cn)end )typs; @@ -97,8 +119,8 @@ in - fun add_domain (comp_dname,eqs') thy'' = let - val ok = check_domain eqs'; + fun add_domain (comp_dname,eqs'') thy'' = let + val eqs' = check_and_sort_domain eqs'' thy''; val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs'); val dts = map (Type o fst) eqs'; fun cons cons' = (map (fn (con,syn,args) => diff -r 150644698367 -r 51993fea433f src/HOLCF/domain/interface.ML --- a/src/HOLCF/domain/interface.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/domain/interface.ML Wed Dec 18 15:16:13 1996 +0100 @@ -1,13 +1,9 @@ -(* interface.ML - Author: David von Oheimb - Created: 17-May-95 - Updated: 24-May-95 - Updated: 03-Jun-95 incremental change of ThySyn - Updated: 11-Jul-95 use of ThyOps for cinfixes - Updated: 21-Jul-95 gen_by-section - Updated: 29-Aug-95 simultaneous domain equations - Updated: 25-Aug-95 better syntax for simultaneous domain equations - Copyright 1995 TU Muenchen +(* Title: HOLCF/domain/interface.ML + ID: $Id$ + Author : David von Oheimb + Copyright 1995, 1996 TU Muenchen + +parser for domain section *) structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData !!!!!! *) @@ -49,7 +45,7 @@ end; fun mk_domain (eqs'') = let - val dtnvs = map (type_name_vars o fst) eqs''; + val dtnvs = map (rep_Type o fst) eqs''; val dnames = map fst dtnvs; val num = length dnames; val comp_dname = implode (separate "_" dnames); @@ -67,9 +63,9 @@ (* ----- string for calling add_domain -------------------------------------- *) val thy_ext_string = let - fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v)) - and mk_typ (TFree(name,sort))= "TFree"^mk_pair(quote name, - mk_list(map quote sort)) + fun mk_tnv (n,v) = mk_pair (quote n, mk_list (map mk_typ v)) + and mk_typ (TFree(name,sort))= "TFree" ^ + mk_pair (quote name, mk_list (map quote sort)) | mk_typ (Type (name,args))= "Type" ^mk_tnv(name,args) | mk_typ _ = Imposs "interface:mk_typ"; fun mk_conslist cons' = @@ -132,33 +128,34 @@ (* ----- parser for domain declaration equation ----------------------------------- *) -(** - val sort = name >> (fn s => [strip_quotes s]) - || "{" $$-- !! (list (name >> strip_quotes) --$$ "}"); - val tvar = (type_var -- (optional ("::" $$-- !! sort) ["pcpo"])) >> TFree -**) - val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"])); - - val type_args = "(" $$-- !! (list1 tvar --$$ ")") - || tvar >> (fn x => [x]) - || empty >> K []; - val con_typ = type_args -- ident >> (fn (x,y) => Type(y,x)); - val typ = con_typ - || tvar; + val name' = name >> strip_quotes; + val type_var' = type_var >> strip_quotes; + val sort = name' >> (fn s => [s]) + || "{" $$-- !! (list name' --$$ "}"); + val tvar = (type_var' --(optional("::" $$-- !! sort)["_default"])) >>TFree; +(*val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"]));*) + fun type_args l = ("(" $$-- !! (list1 typ --$$ ")") + || tvar >> (fn x => [x]) + || empty >> K []) l + and con_typ l = (type_args -- name' >> (fn (x,y) => Type(y,x))) l + (* here ident may be used instead of name' + to avoid ambiguity with standard mixfix option *) + and typ l = (con_typ + || tvar) l; val domain_arg = "(" $$-- (optional ($$ "lazy" >> K true) false) - -- (optional ((ident >> Some) --$$ "::") None) + -- (optional ((name' >> Some) --$$ "::") None) -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp)) - || ident >> (fn x => (false,None,Type(x,[]))) + || name' >> (fn x => (false,None,Type(x,[]))) || tvar >> (fn x => (false,None,x)); - val domain_cons = (name >> strip_quotes) -- !! (repeat domain_arg) + val domain_cons = name' -- !! (repeat domain_arg) -- ThyOps.opt_cmixfix >> (fn ((con,args),syn) => (con,syn,args)); in val domain_decl = (enum1 "," (con_typ --$$ "=" -- !! (enum1 "|" domain_cons))) >> mk_domain; val gen_by_decl = (optional ($$ "finite" >> K true) false) -- - (enum1 "," (ident --$$ "by" -- !! - (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by; + (enum1 "," (name' --$$ "by" -- !! + (enum1 "|" name'))) >> mk_gen_by; end; (* local *) val user_keywords = "lazy"::"by"::"finite":: diff -r 150644698367 -r 51993fea433f src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/domain/library.ML Wed Dec 18 15:16:13 1996 +0100 @@ -1,7 +1,9 @@ (* Title: HOLCF/domain/library.ML - ID: $ $ + ID: $Id$ Author : David von Oheimb Copyright 1995, 1996 TU Muenchen + +library for domain section *) (* ----- general support ---------------------------------------------------- *) @@ -73,8 +75,11 @@ | index_vnames([],occupied) = []; in index_vnames(map (nonreserved o typid) types,[("O",0),("o",0)]) end; -fun type_name_vars (Type(name,typevars)) = (name,typevars) -| type_name_vars _ = Imposs "library:type_name_vars"; +fun rep_Type (Type x) = x | rep_Type _ = Imposs "library:rep_Type"; +fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree"; +val tsig_of = #tsig o Sign.rep_sg o sign_of; +fun pcpo_type thy t = Type.typ_instance(tsig_of thy,t,TVar(("'a",0),["pcpo"])); +fun string_of_typ thy = Sign.string_of_typ (sign_of thy); (* ----- constructor list handling ----- *) @@ -119,9 +124,14 @@ fun mk_lam (x,T) = Abs(x,dummyT,T); fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); local + fun sg [s] = %s + | sg (s::ss) = %%"_classes" $ %s $ sg ss + | sg _ = Imposs "library:sg"; + fun sf [] = %%"_emptysort" + | sf s = %%"_sort" $ sg s fun tf (Type (s,args)) = foldl (op $) (%s,map tf args) - | tf (TFree(s,_ )) = %s - | tf _ = Imposs "mk_constrainall"; + | tf (TFree(s,sort)) = %%"_ofsort" $ %s $ sf sort + | tf _ = Imposs "library:tf"; in fun mk_constrain (typ,T) = %%"_constrain" $ T $ tf typ; fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ); diff -r 150644698367 -r 51993fea433f src/HOLCF/domain/syntax.ML --- a/src/HOLCF/domain/syntax.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/domain/syntax.ML Wed Dec 18 15:16:13 1996 +0100 @@ -1,12 +1,11 @@ -(* syntax.ML - Author: David von Oheimb - Created: 31-May-95 - Updated: 16-Aug-95 case translation - Updated: 28-Aug-95 corrections for case translation, simultaneous domain equations - Copyright 1995 TU Muenchen +(* Title: HOLCF/domain/syntaxd.ML + ID: $Id$ + Author : David von Oheimb + Copyright 1995, 1996 TU Muenchen + +syntax generator for domain section *) - structure Domain_Syntax = struct local @@ -103,8 +102,8 @@ fun add_syntax (comp_dname,eqs': ((string * typ list) * (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = let - fun thy_type (dname,typevars) = (dname, length typevars, NoSyn); - fun thy_arity (dname,typevars) = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); + fun thy_type (dname,tvars) = (dname, length tvars, NoSyn); + fun thy_arity (dname,tvars) = (dname, map (snd o rep_TFree) tvars, ["pcpo"]); val thy_types = map (thy_type o fst) eqs'; val thy_arities = map (thy_arity o fst) eqs'; val dtypes = map (Type o fst) eqs'; diff -r 150644698367 -r 51993fea433f src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/domain/theorems.ML Wed Dec 18 15:16:13 1996 +0100 @@ -1,7 +1,9 @@ (* Title: HOLCF/domain/theorems.ML - ID: $ $ + ID: $Id$ Author : David von Oheimb Copyright 1995, 1996 TU Muenchen + +proof generator for domain section *) structure Domain_Theorems = struct @@ -42,30 +44,16 @@ (* ----- general proofs ----------------------------------------------------- *) -val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[ - fast_tac HOL_cs 1]))["(!x. P x & Q)=((!x. P x) & Q)", - "(!x. P & Q x) = (P & (!x. Q x))"]); - val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R" (fn prems =>[ resolve_tac prems 1, cut_facts_tac prems 1, fast_tac HOL_cs 1]); -val swap3 = prove_goal HOL.thy "[| Q ==> P; ~P |] ==> ~Q" (fn prems => [ - cut_facts_tac prems 1, - etac swap 1, - dtac notnotD 1, - etac (hd prems) 1]); - val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [ - rtac swap3 1, + rtac rev_contrapos 1, etac (antisym_less_inverse RS conjunct1) 1, resolve_tac prems 1]); -val cfst_strict = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [ - (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]); -val csnd_strict = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [ - (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]); in @@ -221,7 +209,7 @@ val con_defins = map (fn (con,args) => pg [] (lift_defined % (nonlazy args, mk_trp(defined(con_app con args)))) ([ - rtac swap3 1, + rtac rev_contrapos 1, eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1, asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons; val con_rews = con_stricts @ con_defins; @@ -257,7 +245,7 @@ fun dist (con1, args1) (con2, args2) = pg [] (lift_defined % ((nonlazy args1), (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([ - rtac swap3 1, + rtac rev_contrapos 1, eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1] @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2) @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]); @@ -371,7 +359,7 @@ val copy_con_rews = copy_rews @ con_rews; val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=> - (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([ + strict(dc_take dn $ %"n")) eqs)))([ nat_ind_tac "n" 1, simp_tac iterate_Cprod_ss 1, asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]); @@ -442,7 +430,7 @@ val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$ (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [ quant_tac 1, - simp_tac quant_ss 1, + simp_tac HOL_ss 1, nat_ind_tac "n" 1, simp_tac (take_ss addsimps prems) 1, TRY(safe_tac HOL_cs)] @@ -512,7 +500,7 @@ asm_simp_tac take_ss 1]) (nonlazy_rec args))) cons)) - 1 (conss~~casess))) handle ERROR => raise ERROR; + 1 (conss~~casess))); val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp( %%(dn^"_finite") $ %"x"))[ case_UU_tac take_rews 1 "x", diff -r 150644698367 -r 51993fea433f src/HOLCF/ex/Loop.ML --- a/src/HOLCF/ex/Loop.ML Wed Dec 18 15:13:50 1996 +0100 +++ b/src/HOLCF/ex/Loop.ML Wed Dec 18 15:16:13 1996 +0100 @@ -234,7 +234,7 @@ (rtac loop_lemma8 1), (resolve_tac prems 1), (resolve_tac prems 1), - (rtac classical3 1), + (rtac classical2 1), (resolve_tac prems 1), (etac box_equals 1), (rtac (loop_lemma4 RS spec RS mp RS sym) 1),