src/HOLCF/Stream.ML
author nipkow
Sat, 11 Mar 1995 17:46:14 +0100
changeset 948 3647161d15d3
parent 892 d0dc8d057929
child 1168 74be52691d62
permissions -rw-r--r--
Added type constraints to enforce correct choice of variable names.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     1
(*  Title: 	HOLCF/stream.ML
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
    Author: 	Franz Regensburger
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
    Copyright   1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
Lemmas for stream.thy
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
open Stream;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    11
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    12
(* The isomorphisms stream_rep_iso and stream_abs_iso are strict           *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    14
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    15
val stream_iso_strict= stream_rep_iso RS (stream_abs_iso RS 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
	(allI  RSN (2,allI RS iso_strict)));
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    17
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
val stream_rews = [stream_iso_strict RS conjunct1,
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
		stream_iso_strict RS conjunct2];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    20
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    21
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    22
(* Properties of stream_copy                                               *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    23
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    24
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    25
fun prover defs thm =  prove_goalw Stream.thy defs thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    27
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    28
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    29
	(asm_simp_tac (HOLCF_ss addsimps 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    30
		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    31
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    32
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    33
val stream_copy = 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    34
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    35
	prover [stream_copy_def] "stream_copy[f][UU]=UU",
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    36
	prover [stream_copy_def,scons_def] 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    37
	"x~=UU ==> stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    38
	];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    39
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    40
val stream_rews =  stream_copy @ stream_rews; 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    41
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    42
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    43
(* Exhaustion and elimination for streams                                  *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    44
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    45
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
    46
qed_goalw "Exh_stream" Stream.thy [scons_def]
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    47
	"s = UU | (? x xs. x~=UU & s = scons[x][xs])"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    48
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    49
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    50
	(simp_tac HOLCF_ss  1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    51
	(rtac (stream_rep_iso RS subst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    52
	(res_inst_tac [("p","stream_rep[s]")] sprodE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    53
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    54
	(asm_simp_tac HOLCF_ss  1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    55
	(res_inst_tac [("p","y")] liftE1 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    56
	(contr_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    57
	(rtac disjI2 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    58
	(rtac exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    59
	(rtac exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    60
	(etac conjI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    61
	(asm_simp_tac HOLCF_ss  1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    62
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    63
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
    64
qed_goal "streamE" Stream.thy 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    65
	"[| s=UU ==> Q; !!x xs.[|s=scons[x][xs];x~=UU|]==>Q|]==>Q"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    66
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    67
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    68
	(rtac (Exh_stream RS disjE) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    69
	(eresolve_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    70
	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    71
	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    72
	(resolve_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    73
	(fast_tac HOL_cs 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    74
	(fast_tac HOL_cs 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    75
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    76
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    77
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    78
(* Properties of stream_when                                               *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    79
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    80
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    81
fun prover defs thm =  prove_goalw Stream.thy defs thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    82
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    83
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    84
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    85
	(asm_simp_tac (HOLCF_ss addsimps 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    86
		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    87
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    88
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    89
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    90
val stream_when = [
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    91
	prover [stream_when_def] "stream_when[f][UU]=UU",
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    92
	prover [stream_when_def,scons_def] 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    93
		"x~=UU ==> stream_when[f][scons[x][xs]]= f[x][xs]"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    94
	];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    95
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    96
val stream_rews = stream_when @ stream_rews;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    97
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    98
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    99
(* Rewrites for  discriminators and  selectors                             *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   100
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   101
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   102
fun prover defs thm = prove_goalw Stream.thy defs thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   103
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   104
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   105
	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   106
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   107
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   108
val stream_discsel = [
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   109
	prover [is_scons_def] "is_scons[UU]=UU",
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   110
	prover [shd_def] "shd[UU]=UU",
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   111
	prover [stl_def] "stl[UU]=UU"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   112
	];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   113
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   114
fun prover defs thm = prove_goalw Stream.thy defs thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   115
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   116
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   117
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   118
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   119
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   120
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   121
val stream_discsel = [
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   122
prover [is_scons_def,shd_def,stl_def] "x~=UU ==> is_scons[scons[x][xs]]=TT",
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   123
prover [is_scons_def,shd_def,stl_def] "x~=UU ==> shd[scons[x][xs]]=x",
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   124
prover [is_scons_def,shd_def,stl_def] "x~=UU ==> stl[scons[x][xs]]=xs"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   125
	] @ stream_discsel;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   126
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   127
val stream_rews = stream_discsel @ stream_rews;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   128
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   129
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   130
(* Definedness and strictness                                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   131
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   132
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   133
fun prover contr thm = prove_goal Stream.thy thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   134
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   135
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   136
	(res_inst_tac [("P1",contr)] classical3 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   137
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   138
	(dtac sym 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   139
	(asm_simp_tac HOLCF_ss  1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   140
	(simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   141
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   142
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   143
val stream_constrdef = [
948
3647161d15d3 Added type constraints to enforce correct choice of variable names.
nipkow
parents: 892
diff changeset
   144
	prover "is_scons[UU::'a stream] ~= UU" "x~=UU ==> scons[x::'a][xs]~=UU"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   145
	]; 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   146
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   147
fun prover defs thm = prove_goalw Stream.thy defs thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   148
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   149
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   150
	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   151
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   152
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   153
val stream_constrdef = [
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   154
	prover [scons_def] "scons[UU][xs]=UU"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   155
	] @ stream_constrdef;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   156
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   157
val stream_rews = stream_constrdef @ stream_rews;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   158
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   159
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   160
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   161
(* Distinctness wrt. << and =                                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   162
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   163
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   164
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   165
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   166
(* Invertibility                                                           *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   167
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   168
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   169
val stream_invert =
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   170
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   171
prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   172
\ scons[x1][x2] << scons[y1][y2]|] ==> x1<< y1 & x2 << y2"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   173
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   174
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   175
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   176
	(rtac conjI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   177
	(dres_inst_tac [("fo5","stream_when[LAM x l.x]")] monofun_cfun_arg 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   178
	(etac box_less 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   179
	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   180
	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   181
	(dres_inst_tac [("fo5","stream_when[LAM x l.l]")] monofun_cfun_arg 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   182
	(etac box_less 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   183
	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   184
	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   185
	])
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   186
	];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   187
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   188
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   189
(* Injectivity                                                             *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   190
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   191
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   192
val stream_inject = 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   193
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   194
prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   195
\ scons[x1][x2] = scons[y1][y2]|] ==> x1= y1 & x2 = y2"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   196
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   197
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   198
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   199
	(rtac conjI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   200
	(dres_inst_tac [("f","stream_when[LAM x l.x]")] cfun_arg_cong 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   201
	(etac box_equals 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   202
	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   203
	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   204
	(dres_inst_tac [("f","stream_when[LAM x l.l]")] cfun_arg_cong 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   205
	(etac box_equals 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   206
	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   207
	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   208
	])
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   209
	];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   210
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   211
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   212
(* definedness for  discriminators and  selectors                          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   213
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   214
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   215
fun prover thm = prove_goal Stream.thy thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   216
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   217
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   218
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   219
	(rtac streamE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   220
	(contr_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   221
	(REPEAT (asm_simp_tac (HOLCF_ss addsimps stream_discsel) 1))
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   222
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   223
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   224
val stream_discsel_def = 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   225
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   226
	prover "s~=UU ==> is_scons[s]~=UU", 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   227
	prover "s~=UU ==> shd[s]~=UU" 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   228
	];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   229
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   230
val stream_rews = stream_discsel_def @ stream_rews;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   231
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   232
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   233
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   234
(* Properties stream_take                                                  *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   235
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   236
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   237
val stream_take =
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   238
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   239
prove_goalw Stream.thy [stream_take_def] "stream_take(n)[UU]=UU"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   240
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   241
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   242
	(res_inst_tac [("n","n")] natE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   243
	(asm_simp_tac iterate_ss 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   244
	(asm_simp_tac iterate_ss 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   245
	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   246
	]),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   247
prove_goalw Stream.thy [stream_take_def] "stream_take(0)[xs]=UU"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   248
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   249
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   250
	(asm_simp_tac iterate_ss 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   251
	])];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   252
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   253
fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   254
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   255
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   256
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   257
	(simp_tac iterate_ss 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   258
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   259
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   260
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   261
val stream_take = [
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   262
prover 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   263
  "x~=UU ==> stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   264
	] @ stream_take;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   265
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   266
val stream_rews = stream_take @ stream_rews;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   267
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   268
(* ------------------------------------------------------------------------*)
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   269
(* enhance the simplifier                                                  *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   270
(* ------------------------------------------------------------------------*)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   271
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   272
qed_goal "stream_copy2" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   273
     "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   274
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   275
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   276
	(res_inst_tac [("Q","x=UU")] classical2 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   277
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   278
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   279
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   280
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   281
qed_goal "shd2" Stream.thy "shd[scons[x][xs]]=x"
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   282
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   283
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   284
	(res_inst_tac [("Q","x=UU")] classical2 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   285
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   286
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   287
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   288
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   289
qed_goal "stream_take2" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   290
 "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   291
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   292
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   293
	(res_inst_tac [("Q","x=UU")] classical2 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   294
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   295
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   296
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   298
val stream_rews = [stream_iso_strict RS conjunct1,
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   299
		   stream_iso_strict RS conjunct2,
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   300
                   hd stream_copy, stream_copy2]
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   301
                  @ stream_when
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   302
                  @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))  
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   303
                  @ stream_constrdef
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   304
                  @ stream_discsel_def
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   305
                  @ [ stream_take2] @ (tl stream_take);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   306
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   307
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   308
(* ------------------------------------------------------------------------*)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   309
(* take lemma for streams                                                  *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   310
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   311
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   312
fun prover reach defs thm  = prove_goalw Stream.thy defs thm
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   313
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   314
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   315
	(res_inst_tac [("t","s1")] (reach RS subst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   316
	(res_inst_tac [("t","s2")] (reach RS subst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   317
	(rtac (fix_def2 RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   318
	(rtac (contlub_cfun_fun RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   319
	(rtac is_chain_iterate 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   320
	(rtac (contlub_cfun_fun RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   321
	(rtac is_chain_iterate 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   322
	(rtac lub_equal 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   323
	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   324
	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   325
	(rtac allI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   326
	(resolve_tac prems 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   327
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   328
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   329
val stream_take_lemma = prover stream_reach  [stream_take_def]
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   330
	"(!!n.stream_take(n)[s1]=stream_take(n)[s2]) ==> s1=s2";
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   331
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   332
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   333
qed_goal "stream_reach2" Stream.thy  "lub(range(%i.stream_take(i)[s]))=s"
430
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   334
 (fn prems =>
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   335
	[
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   336
	(res_inst_tac [("t","s")] (stream_reach RS subst) 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   337
	(rtac (fix_def2 RS ssubst) 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   338
	(rewrite_goals_tac [stream_take_def]),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   339
	(rtac (contlub_cfun_fun RS ssubst) 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   340
	(rtac is_chain_iterate 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   341
	(rtac refl 1)
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   342
	]);
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   343
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   344
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   345
(* Co -induction for streams                                               *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   346
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   347
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   348
qed_goalw "stream_coind_lemma" Stream.thy [stream_bisim_def] 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   349
"stream_bisim(R) ==> ! p q.R(p,q) --> stream_take(n)[p]=stream_take(n)[q]"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   350
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   351
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   352
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   353
	(nat_ind_tac "n" 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   354
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   355
	(strip_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   356
	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   357
	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   358
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   359
	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   360
	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   361
	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   362
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   363
	(REPEAT (etac conjE 1)),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   364
	(rtac cfun_arg_cong 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   365
	(fast_tac HOL_cs 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   366
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   367
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   368
qed_goal "stream_coind" Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   369
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   370
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   371
	(rtac stream_take_lemma 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   372
	(rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   373
	(resolve_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   374
	(resolve_tac prems 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   375
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   376
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   377
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   378
(* structural induction for admissible predicates                          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   379
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   380
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   381
qed_goal "stream_finite_ind" Stream.thy
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   382
"[|P(UU);\
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   383
\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   384
\  |] ==> !s.P(stream_take(n)[s])"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   385
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   386
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   387
	(nat_ind_tac "n" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   388
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   389
	(resolve_tac prems 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   390
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   391
	(res_inst_tac [("s","s")] streamE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   392
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   393
	(resolve_tac prems 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   394
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   395
	(resolve_tac prems 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   396
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   397
	(etac spec 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   398
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   399
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   400
qed_goalw "stream_finite_ind2" Stream.thy  [stream_finite_def]
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   401
"(!!n.P(stream_take(n)[s])) ==>  stream_finite(s) -->P(s)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   402
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   403
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   404
	(strip_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   405
	(etac exE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   406
	(etac subst 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   407
	(resolve_tac prems 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   408
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   409
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   410
qed_goal "stream_finite_ind3" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   411
"[|P(UU);\
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   412
\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   413
\  |] ==> stream_finite(s) --> P(s)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   414
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   415
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   416
	(rtac stream_finite_ind2 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   417
	(rtac (stream_finite_ind RS spec) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   418
	(REPEAT (resolve_tac prems 1)),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   419
	(REPEAT (atac 1))
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   420
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   421
625
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   422
(* prove induction using definition of admissibility 
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   423
   stream_reach rsp. stream_reach2 
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   424
   and finite induction stream_finite_ind *)
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   425
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   426
qed_goal "stream_ind" Stream.thy
625
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   427
"[|adm(P);\
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   428
\  P(UU);\
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   429
\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   430
\  |] ==> P(s)"
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   431
 (fn prems =>
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   432
	[
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   433
	(rtac (stream_reach2 RS subst) 1),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   434
	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   435
	(resolve_tac prems 1),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   436
	(SELECT_GOAL (rewrite_goals_tac [stream_take_def]) 1),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   437
	(rtac ch2ch_fappL 1),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   438
	(rtac is_chain_iterate 1),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   439
	(rtac allI 1),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   440
	(rtac (stream_finite_ind RS spec) 1),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   441
	(REPEAT (resolve_tac prems 1)),
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   442
	(REPEAT (atac 1))
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   443
	]);
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   444
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   445
(* prove induction with usual LCF-Method using fixed point induction *)
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   446
qed_goal "stream_ind" Stream.thy
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   447
"[|adm(P);\
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   448
\  P(UU);\
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   449
\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   450
\  |] ==> P(s)"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   451
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   452
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   453
	(rtac (stream_reach RS subst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   454
	(res_inst_tac [("x","s")] spec 1),
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   455
	(rtac wfix_ind 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   456
	(rtac adm_impl_admw 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   457
	(REPEAT (resolve_tac adm_thms 1)),
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   458
	(rtac adm_subst 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   459
	(contX_tacR 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   460
	(resolve_tac prems 1),
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   461
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   462
	(rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   463
	(REPEAT (resolve_tac prems 1)),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   464
	(REPEAT (atac 1))
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   465
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   466
625
119391dd1d59 New version
nipkow
parents: 430
diff changeset
   467
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   468
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   469
(* simplify use of Co-induction                                            *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   470
(* ------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   471
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   472
qed_goal "surjectiv_scons" Stream.thy "scons[shd[s]][stl[s]]=s"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   473
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   474
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   475
	(res_inst_tac [("s","s")] streamE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   476
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   477
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   478
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   479
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   480
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   481
qed_goalw "stream_coind_lemma2" Stream.thy [stream_bisim_def]
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   482
"!s1 s2. R(s1, s2)-->shd[s1]=shd[s2] & R(stl[s1],stl[s2]) ==>stream_bisim(R)"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   483
 (fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   484
	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   485
	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   486
	(strip_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   487
	(etac allE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   488
	(etac allE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   489
	(dtac mp 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   490
	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   491
	(etac conjE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   492
	(res_inst_tac [("Q","s1 = UU & s2 = UU")] classical2 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   493
	(rtac disjI1 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   494
	(fast_tac HOL_cs 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   495
	(rtac disjI2 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   496
	(rtac disjE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   497
	(etac (de_morgan2 RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   498
	(res_inst_tac [("x","shd[s1]")] exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   499
	(res_inst_tac [("x","stl[s1]")] exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   500
	(res_inst_tac [("x","stl[s2]")] exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   501
	(rtac conjI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   502
	(eresolve_tac stream_discsel_def 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   503
	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   504
	(eres_inst_tac [("s","shd[s1]"),("t","shd[s2]")] subst 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   505
	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   506
	(res_inst_tac [("x","shd[s2]")] exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   507
	(res_inst_tac [("x","stl[s1]")] exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   508
	(res_inst_tac [("x","stl[s2]")] exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   509
	(rtac conjI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   510
	(eresolve_tac stream_discsel_def 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   511
	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   512
	(res_inst_tac [("s","shd[s1]"),("t","shd[s2]")] ssubst 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   513
	(etac sym 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   514
	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   515
	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   516
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   517
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   518
(* ------------------------------------------------------------------------*)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   519
(* theorems about finite and infinite streams                              *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   520
(* ------------------------------------------------------------------------*)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   521
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   522
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   523
(* 2 lemmas about stream_finite                                            *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   524
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   525
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   526
qed_goalw "stream_finite_UU" Stream.thy [stream_finite_def]
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   527
	 "stream_finite(UU)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   528
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   529
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   530
	(rtac exI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   531
	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   532
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   533
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   534
qed_goal "inf_stream_not_UU" Stream.thy  "~stream_finite(s)  ==> s ~= UU"
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   535
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   536
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   537
	(cut_facts_tac prems 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   538
	(etac swap 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   539
	(dtac notnotD 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   540
	(hyp_subst_tac  1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   541
	(rtac stream_finite_UU 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   542
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   543
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   544
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   545
(* a lemma about shd                                                       *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   546
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   547
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   548
qed_goal "stream_shd_lemma1" Stream.thy "shd[s]=UU --> s=UU"
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   549
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   550
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   551
	(res_inst_tac [("s","s")] streamE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   552
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   553
	(hyp_subst_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   554
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   555
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   556
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   557
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   558
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   559
(* lemmas about stream_take                                                *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   560
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   561
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   562
qed_goal "stream_take_lemma1" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   563
 "!x xs.x~=UU --> \
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   564
\  stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   565
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   566
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   567
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   568
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   569
	(rtac impI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   570
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   571
	(strip_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   572
	(rtac ((hd stream_inject) RS conjunct2) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   573
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   574
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   575
	(atac 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   576
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   577
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   578
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   579
qed_goal "stream_take_lemma2" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   580
 "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   581
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   582
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   583
	(nat_ind_tac "n" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   584
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   585
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   586
	(hyp_subst_tac  1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   587
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   588
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   589
	(res_inst_tac [("s","s2")] streamE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   590
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   591
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   592
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   593
	(subgoal_tac "stream_take(n1)[xs] = xs" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   594
	(rtac ((hd stream_inject) RS conjunct2) 2),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   595
	(atac 4),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   596
	(atac 2),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   597
	(atac 2),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   598
	(rtac cfun_arg_cong 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   599
	(fast_tac HOL_cs 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   600
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   601
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   602
qed_goal "stream_take_lemma3" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   603
 "!x xs.x~=UU --> \
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   604
\  stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   605
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   606
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   607
	(nat_ind_tac "n" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   608
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   609
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   610
	(res_inst_tac [("P","scons[x][xs]=UU")] notE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   611
	(eresolve_tac stream_constrdef 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   612
	(etac sym 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   613
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   614
	(rtac (stream_take_lemma2 RS spec RS mp) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   615
	(res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   616
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   617
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   618
	(etac (stream_take2 RS subst) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   619
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   620
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   621
qed_goal "stream_take_lemma4" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   622
 "!x xs.\
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   623
\stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   624
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   625
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   626
	(nat_ind_tac "n" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   627
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   628
	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   629
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   630
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   631
(* ---- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   632
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   633
qed_goal "stream_take_lemma5" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   634
"!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   635
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   636
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   637
	(nat_ind_tac "n" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   638
	(simp_tac iterate_ss 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   639
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   640
	(strip_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   641
	(res_inst_tac [("s","s")] streamE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   642
	(hyp_subst_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   643
	(rtac (iterate_Suc2 RS ssubst) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   644
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   645
	(rtac (iterate_Suc2 RS ssubst) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   646
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   647
	(etac allE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   648
	(etac mp 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   649
	(hyp_subst_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   650
	(etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   651
	(atac 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   652
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   653
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   654
qed_goal "stream_take_lemma6" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   655
"!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   656
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   657
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   658
	(nat_ind_tac "n" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   659
	(simp_tac iterate_ss 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   660
	(strip_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   661
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   662
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   663
	(res_inst_tac [("s","s")] streamE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   664
	(hyp_subst_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   665
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   666
	(hyp_subst_tac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   667
	(rtac (iterate_Suc2 RS ssubst) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   668
	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   669
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   670
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   671
qed_goal "stream_take_lemma7" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   672
"(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   673
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   674
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   675
	(rtac iffI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   676
	(etac (stream_take_lemma6 RS spec RS mp) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   677
	(etac (stream_take_lemma5 RS spec RS mp) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   678
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   679
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   680
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   681
qed_goal "stream_take_lemma8" Stream.thy
430
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   682
"[|adm(P); !n. ? m. n < m & P(stream_take(m)[s])|] ==> P(s)"
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   683
 (fn prems =>
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   684
	[
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   685
	(cut_facts_tac prems 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   686
	(rtac (stream_reach2 RS subst) 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   687
	(rtac adm_disj_lemma11 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   688
	(atac 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   689
	(atac 2),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   690
	(rewrite_goals_tac [stream_take_def]),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   691
	(rtac ch2ch_fappL 1),
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   692
	(rtac is_chain_iterate 1)
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   693
	]);
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 297
diff changeset
   694
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   695
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   696
(* lemmas stream_finite                                                    *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   697
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   698
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   699
qed_goalw "stream_finite_lemma1" Stream.thy [stream_finite_def]
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   700
 "stream_finite(xs) ==> stream_finite(scons[x][xs])"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   701
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   702
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   703
	(cut_facts_tac prems 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   704
	(etac exE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   705
	(rtac exI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   706
	(etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   707
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   708
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   709
qed_goalw "stream_finite_lemma2" Stream.thy [stream_finite_def]
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   710
 "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   711
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   712
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   713
	(cut_facts_tac prems 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   714
	(etac exE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   715
	(rtac exI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   716
	(etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   717
	(atac 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   718
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   719
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   720
qed_goal "stream_finite_lemma3" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   721
 "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   722
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   723
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   724
	(cut_facts_tac prems 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   725
	(rtac iffI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   726
	(etac stream_finite_lemma2 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   727
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   728
	(etac stream_finite_lemma1 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   729
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   730
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   731
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   732
qed_goalw "stream_finite_lemma5" Stream.thy [stream_finite_def]
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   733
 "(!n. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   734
\=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   735
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   736
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   737
	(rtac iffI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   738
	(fast_tac HOL_cs 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   739
	(fast_tac HOL_cs 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   740
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   741
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   742
qed_goal "stream_finite_lemma6" Stream.thy
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   743
 "!s1 s2. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   744
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   745
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   746
	(nat_ind_tac "n" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   747
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   748
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   749
	(hyp_subst_tac  1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   750
	(dtac UU_I 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   751
	(hyp_subst_tac  1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   752
	(rtac stream_finite_UU 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   753
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   754
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   755
	(res_inst_tac [("s","s1")] streamE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   756
	(hyp_subst_tac  1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   757
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   758
	(rtac stream_finite_UU 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   759
	(hyp_subst_tac  1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   760
	(res_inst_tac [("s","s2")] streamE 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   761
	(hyp_subst_tac  1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   762
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   763
	(dtac UU_I 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   764
	(asm_simp_tac(HOLCF_ss addsimps (stream_rews @ [stream_finite_UU])) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   765
	(hyp_subst_tac  1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   766
	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   767
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   768
	(rtac stream_finite_lemma1 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   769
	(subgoal_tac "xs << xsa" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   770
	(subgoal_tac "stream_take(n1)[xsa] = xsa" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   771
	(fast_tac HOL_cs 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   772
	(res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   773
                   ((hd stream_inject) RS conjunct2) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   774
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   775
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   776
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   777
	(res_inst_tac [("x1.1","x"),("y1.1","xa")]
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   778
	 ((hd stream_invert) RS conjunct2) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   779
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   780
	(atac 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   781
	(atac 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   782
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   783
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   784
qed_goal "stream_finite_lemma7" Stream.thy 
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   785
"s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   786
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   787
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   788
	(rtac (stream_finite_lemma5 RS iffD1) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   789
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   790
	(rtac (stream_finite_lemma6 RS spec RS spec) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   791
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   792
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   793
qed_goalw "stream_finite_lemma8" Stream.thy [stream_finite_def]
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   794
"stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   795
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   796
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   797
	(simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   798
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   799
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   800
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   801
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   802
(* admissibility of ~stream_finite                                         *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   803
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   804
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   805
qed_goalw "adm_not_stream_finite" Stream.thy [adm_def]
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   806
 "adm(%s. ~ stream_finite(s))"
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   807
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   808
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   809
	(strip_tac 1 ),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   810
	(res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   811
	(atac 2),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   812
	(subgoal_tac "!i.stream_finite(Y(i))" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   813
	(fast_tac HOL_cs 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   814
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   815
	(rtac (stream_finite_lemma7 RS mp RS mp) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   816
	(etac is_ub_thelub 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   817
	(atac 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   818
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   819
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   820
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   821
(* alternative prove for admissibility of ~stream_finite                   *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   822
(* show that stream_finite(s) = (? n. iterate(n, stl, s) = UU)             *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   823
(* and prove adm. of ~(? n. iterate(n, stl, s) = UU)                       *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   824
(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   825
(* ----------------------------------------------------------------------- *)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   826
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   827
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 625
diff changeset
   828
qed_goal "adm_not_stream_finite" Stream.thy "adm(%s. ~ stream_finite(s))"
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   829
 (fn prems =>
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   830
	[
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   831
	(subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   832
	(etac (adm_cong RS iffD2)1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   833
	(REPEAT(resolve_tac adm_thms 1)),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   834
	(rtac  contX_iterate2 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   835
	(rtac allI 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   836
	(rtac (stream_finite_lemma8 RS ssubst) 1),
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   837
	(fast_tac HOL_cs 1)
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   838
	]);
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   839
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
   840