# HG changeset patch # User oheimb # Date 854725918 -3600 # Node ID 3a8604f408c97cee4fd8a36dae40af184035bf62 # Parent f86367e104f5a16b32219c4cad7c1a30a436c1b6 moved Coind.*, Dagstuhl.*, Focus_ex.* to HOLCF/ex, marked the remaining files as obsolete (new versions in HOLCF/ex) diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Coind.ML --- a/src/HOLCF/explicit_domains/Coind.ML Fri Jan 31 16:39:27 1997 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,138 +0,0 @@ -(* Title: HOLCF/Coind.ML - ID: $Id$ - Author: Franz Regensburger - Copyright 1993 Technische Universitaet Muenchen -*) - -open Coind; - -(* ------------------------------------------------------------------------- *) -(* expand fixed point properties *) -(* ------------------------------------------------------------------------- *) - - -val nats_def2 = fix_prover2 Coind.thy nats_def - "nats = scons`dzero`(smap`dsucc`nats)"; - -val from_def2 = fix_prover2 Coind.thy from_def - "from = (LAM n.scons`n`(from`(dsucc`n)))"; - - - -(* ------------------------------------------------------------------------- *) -(* recursive properties *) -(* ------------------------------------------------------------------------- *) - - -val from = prove_goal Coind.thy "from`n = scons`n`(from`(dsucc`n))" - (fn prems => - [ - (rtac trans 1), - (stac from_def2 1), - (Simp_tac 1), - (rtac refl 1) - ]); - - -val from1 = prove_goal Coind.thy "from`UU = UU" - (fn prems => - [ - (rtac trans 1), - (stac from 1), - (resolve_tac stream_constrdef 1), - (rtac refl 1) - ]); - -val coind_rews = - [iterator1, iterator2, iterator3, smap1, smap2,from1]; - - -(* ------------------------------------------------------------------------- *) -(* the example *) -(* prove: nats = from`dzero *) -(* ------------------------------------------------------------------------- *) - - -val coind_lemma1 = prove_goal Coind.thy "iterator`n`(smap`dsucc)`nats =\ -\ scons`n`(iterator`(dsucc`n)`(smap`dsucc)`nats)" - (fn prems => - [ - (res_inst_tac [("s","n")] dnat_ind 1), - (simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1), - (simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1), - (rtac trans 1), - (rtac nats_def2 1), - (simp_tac (!simpset addsimps (coind_rews @ dnat_rews)) 1), - (rtac trans 1), - (etac iterator3 1), - (rtac trans 1), - (Asm_simp_tac 1), - (rtac trans 1), - (etac smap2 1), - (rtac cfun_arg_cong 1), - (asm_simp_tac (!simpset addsimps ([iterator3 RS sym] @ dnat_rews)) 1) - ]); - - -val nats_eq_from = prove_goal Coind.thy "nats = from`dzero" - (fn prems => - [ - (res_inst_tac [("R", -"% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1), - (res_inst_tac [("x","dzero")] exI 2), - (asm_simp_tac (!simpset addsimps coind_rews) 2), - (rewtac stream_bisim_def), - (strip_tac 1), - (etac exE 1), - (case_tac "n=UU" 1), - (rtac disjI1 1), - (asm_simp_tac (!simpset addsimps coind_rews) 1), - (rtac disjI2 1), - (etac conjE 1), - (hyp_subst_tac 1), - (res_inst_tac [("x","n")] exI 1), - (res_inst_tac [("x","iterator`(dsucc`n)`(smap`dsucc)`nats")] exI 1), - (res_inst_tac [("x","from`(dsucc`n)")] exI 1), - (etac conjI 1), - (rtac conjI 1), - (rtac coind_lemma1 1), - (rtac conjI 1), - (rtac from 1), - (res_inst_tac [("x","dsucc`n")] exI 1), - (fast_tac HOL_cs 1) - ]); - -(* another proof using stream_coind_lemma2 *) - -val nats_eq_from = prove_goal Coind.thy "nats = from`dzero" - (fn prems => - [ - (res_inst_tac [("R","% p q.? n. p = \ -\ iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1), - (rtac stream_coind_lemma2 1), - (strip_tac 1), - (etac exE 1), - (case_tac "n=UU" 1), - (asm_simp_tac (!simpset addsimps coind_rews) 1), - (res_inst_tac [("x","UU::dnat")] exI 1), - (simp_tac (!simpset addsimps coind_rews addsimps stream_rews) 1), - (etac conjE 1), - (hyp_subst_tac 1), - (rtac conjI 1), - (stac coind_lemma1 1), - (stac from 1), - (asm_simp_tac (!simpset addsimps stream_rews) 1), - (res_inst_tac [("x","dsucc`n")] exI 1), - (rtac conjI 1), - (rtac trans 1), - (stac coind_lemma1 1), - (asm_simp_tac (!simpset addsimps stream_rews) 1), - (rtac refl 1), - (rtac trans 1), - (stac from 1), - (asm_simp_tac (!simpset addsimps stream_rews) 1), - (rtac refl 1), - (res_inst_tac [("x","dzero")] exI 1), - (asm_simp_tac (!simpset addsimps coind_rews) 1) - ]); - diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Coind.thy --- a/src/HOLCF/explicit_domains/Coind.thy Fri Jan 31 16:39:27 1997 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -(* Title: HOLCF/Coind.thy - ID: $Id$ - Author: Franz Regensburger - Copyright 1993 Technische Universitaet Muenchen - -Example for co-induction on streams -*) - -Coind = Stream2 + - - -consts - - nats :: "dnat stream" - from :: "dnat -> dnat stream" - -defs - nats_def "nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))" - - from_def "from == fix`(LAM h n.scons`n`(h`(dsucc`n)))" - -end - -(* - smap`f`UU = UU - x~=UU --> smap`f`(scons`x`xs) = scons`(f`x)`(smap`f`xs) - - nats = scons`dzero`(smap`dsucc`nats) - - from`n = scons`n`(from`(dsucc`n)) -*) - - diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Dagstuhl.ML --- a/src/HOLCF/explicit_domains/Dagstuhl.ML Fri Jan 31 16:39:27 1997 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,75 +0,0 @@ -(* $Id$ *) - -open Dagstuhl; - -val YS_def2 = fix_prover2 Dagstuhl.thy YS_def "YS = scons`y`YS"; -val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = scons`y`(scons`y`YYS)"; - - -val prems = goal Dagstuhl.thy "YYS << scons`y`YYS"; -by (rewtac YYS_def); -by (rtac fix_ind 1); -by (resolve_tac adm_thms 1); -by (cont_tacR 1); -by (rtac minimal 1); -by (stac beta_cfun 1); -by (cont_tacR 1); -by (rtac monofun_cfun_arg 1); -by (rtac monofun_cfun_arg 1); -by (atac 1); -val lemma3 = result(); - -val prems = goal Dagstuhl.thy "scons`y`YYS << YYS"; -by (stac YYS_def2 1); -back(); -by (rtac monofun_cfun_arg 1); -by (rtac lemma3 1); -val lemma4=result(); - -(* val lemma5 = lemma3 RS (lemma4 RS antisym_less) *) - -val prems = goal Dagstuhl.thy "scons`y`YYS = YYS"; -by (rtac antisym_less 1); -by (rtac lemma4 1); -by (rtac lemma3 1); -val lemma5=result(); - -val prems = goal Dagstuhl.thy "YS = YYS"; -by (rtac stream_take_lemma 1); -by (nat_ind_tac "n" 1); -by (simp_tac (!simpset addsimps stream_rews) 1); -by (stac YS_def2 1); -by (stac YYS_def2 1); -by (asm_simp_tac (!simpset addsimps stream_rews) 1); -by (rtac (lemma5 RS sym RS subst) 1); -by (rtac refl 1); -val wir_moel=result(); - -(* ------------------------------------------------------------------------ *) -(* Zweite L"osung: Bernhard M"oller *) -(* statt Beweis von wir_moel "uber take_lemma beidseitige Inclusion *) -(* verwendet lemma5 *) -(* ------------------------------------------------------------------------ *) - -val prems = goal Dagstuhl.thy "YYS << YS"; -by (rewtac YYS_def); -by (rtac fix_least 1); -by (stac beta_cfun 1); -by (cont_tacR 1); -by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1); -val lemma6=result(); - -val prems = goal Dagstuhl.thy "YS << YYS"; -by (rewtac YS_def); -by (rtac fix_ind 1); -by (resolve_tac adm_thms 1); -by (cont_tacR 1); -by (rtac minimal 1); -by (stac beta_cfun 1); -by (cont_tacR 1); -by (stac (lemma5 RS sym) 1); -by (etac monofun_cfun_arg 1); -val lemma7 = result(); - -val wir_moel = lemma6 RS (lemma7 RS antisym_less); - diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Dagstuhl.thy --- a/src/HOLCF/explicit_domains/Dagstuhl.thy Fri Jan 31 16:39:27 1997 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* $Id$ *) - - -Dagstuhl = Stream2 + - -consts - y :: "'a" - YS :: "'a stream" - YYS :: "'a stream" - -defs - -YS_def "YS == fix`(LAM x. scons`y`x)" -YYS_def "YYS == fix`(LAM z. scons`y`(scons`y`z))" - -end - diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Dlist.thy --- a/src/HOLCF/explicit_domains/Dlist.thy Fri Jan 31 16:39:27 1997 +0100 +++ b/src/HOLCF/explicit_domains/Dlist.thy Fri Jan 31 16:51:58 1997 +0100 @@ -4,6 +4,8 @@ ID: $ $ Copyright 1994 Technische Universitaet Muenchen +NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dlist.thy INSTEAD. + Theory for finite lists 'a dlist = one ++ ('a ** 'a dlist) The type is axiomatized as the least solution of the domain equation above. diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Dnat.thy --- a/src/HOLCF/explicit_domains/Dnat.thy Fri Jan 31 16:39:27 1997 +0100 +++ b/src/HOLCF/explicit_domains/Dnat.thy Fri Jan 31 16:51:58 1997 +0100 @@ -3,6 +3,8 @@ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen +NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD. + Theory for the domain of natural numbers dnat = one ++ dnat The type is axiomatized as the least solution of the domain equation above. diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Dnat2.thy --- a/src/HOLCF/explicit_domains/Dnat2.thy Fri Jan 31 16:39:27 1997 +0100 +++ b/src/HOLCF/explicit_domains/Dnat2.thy Fri Jan 31 16:51:58 1997 +0100 @@ -3,6 +3,8 @@ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen +NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD. + Additional constants for dnat *) diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Focus_ex.ML --- a/src/HOLCF/explicit_domains/Focus_ex.ML Fri Jan 31 16:39:27 1997 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,153 +0,0 @@ -(* - ID: $Id$ - Author: Franz Regensburger - Copyright 1995 Technische Universitaet Muenchen - -*) - -open Focus_ex; - - Delsimps (ex_simps @ all_simps); - -(* first some logical trading *) - -val prems = goal Focus_ex.thy -"is_g(g) = \ -\ (? f. is_f(f) & (!x.(? z. = f` & \ -\ (! w y. = f` --> z << w))))"; -by (simp_tac (!simpset addsimps [is_g,is_net_g]) 1); -by (fast_tac HOL_cs 1); -val lemma1 = result(); - -val prems = goal Focus_ex.thy -"(? f. is_f(f) & (!x. (? z. = f` & \ -\ (! w y. = f` --> z << w)))) \ -\ = \ -\ (? f. is_f(f) & (!x. ? z.\ -\ g`x = cfst`(f`) & \ -\ z = csnd`(f`) & \ -\ (! w y. = f` --> z << w)))"; -by (rtac iffI 1); -by (etac exE 1); -by (res_inst_tac [("x","f")] exI 1); -by (REPEAT (etac conjE 1)); -by (etac conjI 1); -by (strip_tac 1); -by (etac allE 1); -by (etac exE 1); -by (res_inst_tac [("x","z")] exI 1); -by (REPEAT (etac conjE 1)); -by (rtac conjI 1); -by (rtac conjI 2); -by (atac 3); -by (dtac sym 1); -by (Asm_simp_tac 1); -by (dtac sym 1); -by (Asm_simp_tac 1); -by (etac exE 1); -by (res_inst_tac [("x","f")] exI 1); -by (REPEAT (etac conjE 1)); -by (etac conjI 1); -by (strip_tac 1); -by (etac allE 1); -by (etac exE 1); -by (res_inst_tac [("x","z")] exI 1); -by (REPEAT (etac conjE 1)); -by (rtac conjI 1); -by (atac 2); -by (rtac trans 1); -by (rtac (surjective_pairing_Cprod2) 2); -by (etac subst 1); -by (etac subst 1); -by (rtac refl 1); -val lemma2 = result(); - -(* direction def_g(g) --> is_g(g) *) - -val prems = goal Focus_ex.thy "def_g(g) --> is_g(g)"; -by (simp_tac (!simpset addsimps [def_g,lemma1, lemma2]) 1); -by (rtac impI 1); -by (etac exE 1); -by (res_inst_tac [("x","f")] exI 1); -by (REPEAT (etac conjE 1)); -by (etac conjI 1); -by (strip_tac 1); -by (res_inst_tac [("x","fix`(LAM k.csnd`(f`))")] exI 1); -by (rtac conjI 1); -by (Asm_simp_tac 1); -by (rtac conjI 1); -by (rtac trans 1); -by (rtac fix_eq 1); -by (Simp_tac 1); -by (strip_tac 1); -by (rtac fix_least 1); -by (dtac sym 1); -back(); -by (Asm_simp_tac 1); -val lemma3 = result(); - -(* direction is_g(g) --> def_g(g) *) -val prems = goal Focus_ex.thy "is_g(g) --> def_g(g)"; -by (simp_tac (!simpset addsimps [lemma1,lemma2,def_g]) 1); -by (rtac impI 1); -by (etac exE 1); -by (res_inst_tac [("x","f")] exI 1); -by (REPEAT (etac conjE 1)); -by (etac conjI 1); -by (rtac ext_cfun 1); -by (etac allE 1); -by (etac exE 1); -by (REPEAT (etac conjE 1)); -by (subgoal_tac "fix`(LAM k. csnd`(f`)) = z" 1); -by (Asm_simp_tac 1); -by (subgoal_tac "! w y. f` = --> z << w" 1); -by (rtac sym 1); -by (rtac fix_eqI 1); -by (Asm_simp_tac 1); -by (etac sym 1); -by (rtac allI 1); -by (Simp_tac 1); -by (strip_tac 1); -by (subgoal_tac "f` = ),za>" 1); -by (fast_tac HOL_cs 1); -by (rtac trans 1); -by (rtac (surjective_pairing_Cprod2 RS sym) 1); -by (etac cfun_arg_cong 1); -by (strip_tac 1); -by (REPEAT (etac allE 1)); -by (etac mp 1); -by (etac sym 1); -val lemma4 = result(); - -(* now we assemble the result *) - -val prems = goal Focus_ex.thy "def_g = is_g"; -by (rtac ext 1); -by (rtac iffI 1); -by (etac (lemma3 RS mp) 1); -by (etac (lemma4 RS mp) 1); -val loopback_eq = result(); - -val prems = goal Focus_ex.thy -"(? f.\ -\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\ -\ -->\ -\ (? g. def_g(g::'b stream -> 'c stream ))"; -by (simp_tac (!simpset addsimps [def_g]) 1); -by (strip_tac 1); -by (etac exE 1); -by (rtac exI 1); -by (rtac exI 1); -by (etac conjI 1); -by (rtac refl 1); -val L2 = result(); - -val prems = goal Focus_ex.thy -"(? f.\ -\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\ -\ -->\ -\ (? g. is_g(g::'b stream -> 'c stream ))"; -by (rtac (loopback_eq RS subst) 1); -by (rtac L2 1); -val conservative_loopback = result(); - diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Focus_ex.thy --- a/src/HOLCF/explicit_domains/Focus_ex.thy Fri Jan 31 16:39:27 1997 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,143 +0,0 @@ -(* - ID: $Id$ - Author: Franz Regensburger - Copyright 1995 Technische Universitaet Muenchen - -*) - -(* Specification of the following loop back device - - - g - -------------------- - | ------- | - x | | | | y - ------|---->| |------| -----> - | z | f | z | - | -->| |--- | - | | | | | | - | | ------- | | - | | | | - | <-------------- | - | | - -------------------- - - -First step: Notation in Agent Network Description Language (ANDL) ------------------------------------------------------------------ - -agent f - input channel i1:'b i2: ('b,'c) tc - output channel o1:'c o2: ('b,'c) tc -is - Rf(i1,i2,o1,o2) (left open in the example) -end f - -agent g - input channel x:'b - output channel y:'c -is network - = f` -end network -end g - - -Remark: the type of the feedback depends at most on the types of the input and - output of g. (No type miracles inside g) - -Second step: Translation of ANDL specification to HOLCF Specification ---------------------------------------------------------------------- - -Specification of agent f ist translated to predicate is_f - -is_f :: ('b stream * ('b,'c) tc stream -> - 'c stream * ('b,'c) tc stream) => bool - -is_f f = ! i1 i2 o1 o2. - f` = --> Rf(i1,i2,o1,o2) - -Specification of agent g is translated to predicate is_g which uses -predicate is_net_g - -is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => - 'b stream => 'c stream => bool - -is_net_g f x y = - ? z. = f` & - ! oy hz. = f` --> z << hz - - -is_g :: ('b stream -> 'c stream) => bool - -is_g g = ? f. is_f f & (! x y. g`x = y --> is_net_g f x y - -Third step: (show conservativity) ------------ - -Suppose we have a model for the theory TH1 which contains the axiom - - ? f. is_f f - -In this case there is also a model for the theory TH2 that enriches TH1 by -axiom - - ? g. is_g g - -The result is proved by showing that there is a definitional extension -that extends TH1 by a definition of g. - - -We define: - -def_g g = - (? f. is_f f & - g = (LAM x. cfst`(f`))>)) ) - -Now we prove: - - (?f. is_f f ) --> (? g. is_g g) - -using the theorems - -loopback_eq) def_g = is_g (real work) - -L1) (? f. is_f f ) --> (? g. def_g g) (trivial) - -*) - -Focus_ex = Stream + - -types tc 2 - -arities tc:: (pcpo,pcpo)pcpo - -consts - -is_f :: - "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" -is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => - 'b stream => 'c stream => bool" -is_g :: "('b stream -> 'c stream) => bool" -def_g :: "('b stream -> 'c stream) => bool" -Rf :: -"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool" - -defs - -is_f "is_f f == (! i1 i2 o1 o2. - f` = --> Rf(i1,i2,o1,o2))" - -is_net_g "is_net_g f x y == (? z. - = f` & - (! oy hz. = f` --> z << hz))" - -is_g "is_g g == (? f. - is_f f & - (!x y. g`x = y --> is_net_g f x y))" - - -def_g "def_g g == (? f. - is_f f & - g = (LAM x. cfst`(f`))>)))" - -end diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/ROOT.ML --- a/src/HOLCF/explicit_domains/ROOT.ML Fri Jan 31 16:39:27 1997 +0100 +++ b/src/HOLCF/explicit_domains/ROOT.ML Fri Jan 31 16:51:58 1997 +0100 @@ -16,9 +16,5 @@ time_use_thy "Stream2"; time_use_thy "Dlist"; -time_use_thy "Coind"; -time_use_thy "Dagstuhl"; -time_use_thy "Focus_ex"; - OS.FileSys.chDir ".."; maketest "END: Root file for HOLCF examples: explicit domain axiomatization"; diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Stream.thy --- a/src/HOLCF/explicit_domains/Stream.thy Fri Jan 31 16:39:27 1997 +0100 +++ b/src/HOLCF/explicit_domains/Stream.thy Fri Jan 31 16:51:58 1997 +0100 @@ -3,6 +3,8 @@ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen +NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD. + Theory for streams without defined empty stream 'a stream = 'a ** ('a stream)u diff -r f86367e104f5 -r 3a8604f408c9 src/HOLCF/explicit_domains/Stream2.thy --- a/src/HOLCF/explicit_domains/Stream2.thy Fri Jan 31 16:39:27 1997 +0100 +++ b/src/HOLCF/explicit_domains/Stream2.thy Fri Jan 31 16:51:58 1997 +0100 @@ -3,6 +3,8 @@ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen +NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD. + Additional constants for stream *)