--- 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 *)
--- 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
--- 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)
--- 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
--- 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)
--- 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),
--- 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
--- 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) =>
--- 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"::
--- 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);
--- 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';
--- 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",
--- 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),