src/HOLCF/dlist.ML
author nipkow
Sun, 22 Dec 2002 10:43:43 +0100
changeset 13763 f94b569cd610
parent 298 3a0485439396
permissions -rw-r--r--
added print translations tha avoid eta contraction for important binders.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
298
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     1
(*  Title: 	HOLCF/dlist.ML
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     2
    Author: 	Franz Regensburger
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     3
    ID:         $ $
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     4
    Copyright   1994 Technische Universitaet Muenchen
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     5
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     6
Lemmas for dlist.thy
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     7
*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     8
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
     9
open Dlist;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    10
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    11
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    12
(* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict             *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    13
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    14
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    15
val dlist_iso_strict= dlist_rep_iso RS (dlist_abs_iso RS 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    16
	(allI  RSN (2,allI RS iso_strict)));
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    17
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    18
val dlist_rews = [dlist_iso_strict RS conjunct1,
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    19
		dlist_iso_strict RS conjunct2];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    20
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    21
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    22
(* Properties of dlist_copy                                                *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    23
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    24
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    25
val temp = prove_goalw Dlist.thy  [dlist_copy_def] "dlist_copy[f][UU]=UU"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    26
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    27
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    28
	(asm_simp_tac (HOLCF_ss addsimps 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    29
		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    30
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    31
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    32
val dlist_copy = [temp];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    33
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    34
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    35
val temp = prove_goalw Dlist.thy  [dlist_copy_def,dnil_def] 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    36
    "dlist_copy[f][dnil]=dnil"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    37
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    38
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    39
	(asm_simp_tac (HOLCF_ss addsimps 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    40
		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    41
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    42
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    43
val dlist_copy = temp :: dlist_copy;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    44
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    45
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    46
val temp = prove_goalw Dlist.thy  [dlist_copy_def,dcons_def] 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    47
	"xl~=UU ==> dlist_copy[f][dcons[x][xl]]= dcons[x][f[xl]]"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    48
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    49
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    50
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    51
	(asm_simp_tac (HOLCF_ss addsimps 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    52
		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    53
	(res_inst_tac [("Q","x=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    54
	(asm_simp_tac HOLCF_ss  1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    55
	(asm_simp_tac (HOLCF_ss addsimps [defined_spair]) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    56
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    57
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    58
val dlist_copy = temp :: dlist_copy;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    59
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    60
val dlist_rews =  dlist_copy @ dlist_rews; 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    61
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    62
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    63
(* Exhaustion and elimination for dlists                                   *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    64
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    65
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    66
val Exh_dlist = prove_goalw Dlist.thy [dcons_def,dnil_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    67
	"l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons[x][xl])"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    68
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    69
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    70
	(simp_tac HOLCF_ss  1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    71
	(rtac (dlist_rep_iso RS subst) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    72
	(res_inst_tac [("p","dlist_rep[l]")] ssumE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    73
	(rtac disjI1 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    74
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    75
	(rtac disjI2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    76
	(rtac disjI1 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    77
	(res_inst_tac [("p","x")] oneE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    78
	(contr_tac 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    79
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    80
	(rtac disjI2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    81
	(rtac disjI2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    82
	(res_inst_tac [("p","y")] sprodE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    83
	(contr_tac 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    84
	(rtac exI 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    85
	(rtac exI 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    86
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    87
	(fast_tac HOL_cs 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    88
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    89
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    90
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    91
val dlistE = prove_goal Dlist.thy 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    92
"[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons[x][xl];x~=UU;xl~=UU|]==>Q|]==>Q"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    93
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    94
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    95
	(rtac (Exh_dlist RS disjE) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    96
	(eresolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    97
	(etac disjE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    98
	(eresolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
    99
	(etac exE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   100
	(etac exE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   101
	(resolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   102
	(fast_tac HOL_cs 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   103
	(fast_tac HOL_cs 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   104
	(fast_tac HOL_cs 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   105
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   106
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   107
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   108
(* Properties of dlist_when                                                *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   109
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   110
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   111
val temp = prove_goalw  Dlist.thy  [dlist_when_def] "dlist_when[f1][f2][UU]=UU"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   112
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   113
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   114
	(asm_simp_tac (HOLCF_ss addsimps [dlist_iso_strict]) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   115
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   116
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   117
val dlist_when = [temp];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   118
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   119
val temp = prove_goalw  Dlist.thy [dlist_when_def,dnil_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   120
 "dlist_when[f1][f2][dnil]= f1"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   121
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   122
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   123
	(asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso]) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   124
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   125
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   126
val dlist_when = temp::dlist_when;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   127
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   128
val temp = prove_goalw  Dlist.thy [dlist_when_def,dcons_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   129
 "[|x~=UU;xl~=UU|] ==> dlist_when[f1][f2][dcons[x][xl]]= f2[x][xl]"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   130
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   131
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   132
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   133
	(asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso,defined_spair]) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   134
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   135
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   136
val dlist_when = temp::dlist_when;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   137
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   138
val dlist_rews = dlist_when @ dlist_rews;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   139
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   140
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   141
(* Rewrites for  discriminators and  selectors                             *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   142
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   143
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   144
fun prover defs thm = prove_goalw Dlist.thy defs thm
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   145
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   146
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   147
	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   148
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   149
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   150
val dlist_discsel = [
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   151
	prover [is_dnil_def] "is_dnil[UU]=UU",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   152
	prover [is_dcons_def] "is_dcons[UU]=UU",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   153
	prover [dhd_def] "dhd[UU]=UU",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   154
	prover [dtl_def] "dtl[UU]=UU"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   155
	];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   156
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   157
fun prover defs thm = prove_goalw Dlist.thy defs thm
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   158
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   159
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   160
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   161
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   162
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   163
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   164
val dlist_discsel = [
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   165
prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   166
  "is_dnil[dnil]=TT",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   167
prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   168
  "[|x~=UU;xl~=UU|] ==> is_dnil[dcons[x][xl]]=FF",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   169
prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   170
  "is_dcons[dnil]=FF",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   171
prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   172
  "[|x~=UU;xl~=UU|] ==> is_dcons[dcons[x][xl]]=TT",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   173
prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   174
  "dhd[dnil]=UU",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   175
prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   176
  "[|x~=UU;xl~=UU|] ==> dhd[dcons[x][xl]]=x",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   177
prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   178
  "dtl[dnil]=UU",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   179
prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   180
  "[|x~=UU;xl~=UU|] ==> dtl[dcons[x][xl]]=xl"] @ dlist_discsel;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   181
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   182
val dlist_rews = dlist_discsel @ dlist_rews;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   183
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   184
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   185
(* Definedness and strictness                                              *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   186
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   187
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   188
fun prover contr thm = prove_goal Dlist.thy thm
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   189
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   190
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   191
	(res_inst_tac [("P1",contr)] classical3 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   192
	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   193
	(dtac sym 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   194
	(asm_simp_tac HOLCF_ss  1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   195
	(simp_tac (HOLCF_ss addsimps (prems @ dlist_rews)) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   196
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   197
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   198
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   199
val dlist_constrdef = [
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   200
prover "is_dnil[UU] ~= UU" "dnil~=UU",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   201
prover "is_dcons[UU] ~= UU" "[|x~=UU;xl~=UU|] ==> dcons[x][xl]~=UU"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   202
 ];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   203
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   204
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   205
fun prover defs thm = prove_goalw Dlist.thy defs thm
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   206
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   207
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   208
	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   209
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   210
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   211
val dlist_constrdef = [
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   212
	prover [dcons_def] "dcons[UU][xl]=UU",
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   213
	prover [dcons_def] "dcons[x][UU]=UU"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   214
	] @ dlist_constrdef;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   215
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   216
val dlist_rews = dlist_constrdef @ dlist_rews;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   217
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   218
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   219
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   220
(* Distinctness wrt. << and =                                              *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   221
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   222
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   223
val temp = prove_goal Dlist.thy  "~dnil << dcons[x][xl]"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   224
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   225
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   226
	(res_inst_tac [("P1","TT << FF")] classical3 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   227
	(resolve_tac dist_less_tr 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   228
	(dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   229
	(etac box_less 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   230
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   231
	(res_inst_tac [("Q","x=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   232
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   233
	(res_inst_tac [("Q","xl=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   234
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   235
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   236
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   237
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   238
val dlist_dist_less = [temp];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   239
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   240
val temp = prove_goal Dlist.thy  "[|x~=UU;xl~=UU|]==>~dcons[x][xl] << dnil"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   241
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   242
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   243
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   244
	(res_inst_tac [("P1","TT << FF")] classical3 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   245
	(resolve_tac dist_less_tr 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   246
	(dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   247
	(etac box_less 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   248
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   249
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   250
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   251
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   252
val dlist_dist_less = temp::dlist_dist_less;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   253
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   254
val temp = prove_goal Dlist.thy  "dnil ~= dcons[x][xl]"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   255
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   256
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   257
	(res_inst_tac [("Q","x=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   258
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   259
	(res_inst_tac [("Q","xl=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   260
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   261
	(res_inst_tac [("P1","TT = FF")] classical3 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   262
	(resolve_tac dist_eq_tr 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   263
	(dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   264
	(etac box_equals 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   265
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   266
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   267
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   268
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   269
val dlist_dist_eq = [temp,temp RS not_sym];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   270
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   271
val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   272
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   273
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   274
(* Invertibility                                                           *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   275
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   276
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   277
val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   278
\ dcons[x1][x2] << dcons[y1][y2]|] ==> x1<< y1 & x2 << y2"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   279
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   280
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   281
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   282
	(rtac conjI 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   283
	(dres_inst_tac [("fo5","dlist_when[UU][LAM x l.x]")] monofun_cfun_arg 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   284
	(etac box_less 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   285
	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   286
	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   287
	(dres_inst_tac [("fo5","dlist_when[UU][LAM x l.l]")] monofun_cfun_arg 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   288
	(etac box_less 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   289
	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   290
	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   291
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   292
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   293
val dlist_invert =[temp];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   294
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   295
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   296
(* Injectivity                                                             *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   297
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   298
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   299
val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   300
\ dcons[x1][x2] = dcons[y1][y2]|] ==> x1= y1 & x2 = y2"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   301
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   302
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   303
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   304
	(rtac conjI 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   305
	(dres_inst_tac [("f","dlist_when[UU][LAM x l.x]")] cfun_arg_cong 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   306
	(etac box_equals 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   307
	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   308
	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   309
	(dres_inst_tac [("f","dlist_when[UU][LAM x l.l]")] cfun_arg_cong 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   310
	(etac box_equals 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   311
	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   312
	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   313
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   314
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   315
val dlist_inject = [temp];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   316
 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   317
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   318
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   319
(* definedness for  discriminators and  selectors                          *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   320
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   321
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   322
fun prover thm = prove_goal Dlist.thy thm
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   323
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   324
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   325
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   326
	(rtac dlistE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   327
	(contr_tac 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   328
	(REPEAT (asm_simp_tac (HOLCF_ss addsimps dlist_discsel) 1))
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   329
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   330
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   331
val dlist_discsel_def = 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   332
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   333
	prover "l~=UU ==> is_dnil[l]~=UU", 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   334
	prover "l~=UU ==> is_dcons[l]~=UU" 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   335
	];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   336
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   337
val dlist_rews = dlist_discsel_def @ dlist_rews;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   338
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   339
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   340
(* enhance the simplifier                                                  *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   341
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   342
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   343
val dhd2 = prove_goal Dlist.thy "xl~=UU ==> dhd[dcons[x][xl]]=x"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   344
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   345
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   346
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   347
	(res_inst_tac [("Q","x=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   348
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   349
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   350
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   351
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   352
val dtl2 = prove_goal Dlist.thy "x~=UU ==> dtl[dcons[x][xl]]=xl"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   353
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   354
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   355
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   356
	(res_inst_tac [("Q","xl=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   357
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   358
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   359
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   360
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   361
val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   362
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   363
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   364
(* Properties dlist_take                                                   *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   365
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   366
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   367
val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take(n)[UU]=UU"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   368
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   369
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   370
	(res_inst_tac [("n","n")] natE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   371
	(asm_simp_tac iterate_ss 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   372
	(asm_simp_tac iterate_ss 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   373
	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   374
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   375
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   376
val dlist_take = [temp];
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   377
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   378
val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take(0)[xs]=UU"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   379
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   380
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   381
	(asm_simp_tac iterate_ss 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   382
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   383
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   384
val dlist_take = temp::dlist_take;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   385
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   386
val temp = prove_goalw Dlist.thy [dlist_take_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   387
	"dlist_take(Suc(n))[dnil]=dnil"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   388
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   389
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   390
	(asm_simp_tac iterate_ss 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   391
	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   392
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   393
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   394
val dlist_take = temp::dlist_take;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   395
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   396
val temp = prove_goalw Dlist.thy [dlist_take_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   397
  "dlist_take(Suc(n))[dcons[x][xl]]=dcons[x][dlist_take(n)[xl]]"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   398
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   399
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   400
	(res_inst_tac [("Q","x=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   401
	(asm_simp_tac iterate_ss 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   402
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   403
	(res_inst_tac [("Q","xl=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   404
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   405
	(asm_simp_tac iterate_ss 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   406
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   407
	(res_inst_tac [("n","n")] natE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   408
	(asm_simp_tac iterate_ss 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   409
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   410
	(asm_simp_tac iterate_ss 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   411
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   412
	(asm_simp_tac iterate_ss 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   413
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   414
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   415
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   416
val dlist_take = temp::dlist_take;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   417
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   418
val dlist_rews = dlist_take @ dlist_rews;
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   419
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   420
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   421
(* take lemma for dlists                                                  *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   422
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   423
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   424
fun prover reach defs thm  = prove_goalw Dlist.thy defs thm
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   425
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   426
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   427
	(res_inst_tac [("t","l1")] (reach RS subst) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   428
	(res_inst_tac [("t","l2")] (reach RS subst) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   429
	(rtac (fix_def2 RS ssubst) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   430
	(rtac (contlub_cfun_fun RS ssubst) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   431
	(rtac is_chain_iterate 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   432
	(rtac (contlub_cfun_fun RS ssubst) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   433
	(rtac is_chain_iterate 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   434
	(rtac lub_equal 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   435
	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   436
	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   437
	(rtac allI 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   438
	(resolve_tac prems 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   439
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   440
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   441
val dlist_take_lemma = prover dlist_reach  [dlist_take_def]
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   442
	"(!!n.dlist_take(n)[l1]=dlist_take(n)[l2]) ==> l1=l2";
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   443
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   444
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   445
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   446
(* Co -induction for dlists                                               *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   447
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   448
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   449
val dlist_coind_lemma = prove_goalw Dlist.thy [dlist_bisim_def] 
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   450
"dlist_bisim(R) ==> ! p q.R(p,q) --> dlist_take(n)[p]=dlist_take(n)[q]"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   451
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   452
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   453
	(cut_facts_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   454
	(nat_ind_tac "n" 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   455
	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   456
	(strip_tac 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   457
	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   458
	(atac 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   459
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   460
	(etac disjE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   461
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   462
	(etac exE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   463
	(etac exE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   464
	(etac exE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   465
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   466
	(REPEAT (etac conjE 1)),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   467
	(rtac cfun_arg_cong 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   468
	(fast_tac HOL_cs 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   469
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   470
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   471
val dlist_coind = prove_goal Dlist.thy "[|dlist_bisim(R);R(p,q)|] ==> p = q"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   472
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   473
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   474
	(rtac dlist_take_lemma 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   475
	(rtac (dlist_coind_lemma RS spec RS spec RS mp) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   476
	(resolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   477
	(resolve_tac prems 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   478
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   479
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   480
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   481
(* structural induction                                                    *)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   482
(* ------------------------------------------------------------------------*)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   483
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   484
val dlist_finite_ind = prove_goal Dlist.thy
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   485
"[|P(UU);P(dnil);\
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   486
\  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])\
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   487
\  |] ==> !l.P(dlist_take(n)[l])"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   488
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   489
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   490
	(nat_ind_tac "n" 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   491
	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   492
	(resolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   493
	(rtac allI 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   494
	(res_inst_tac [("l","l")] dlistE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   495
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   496
	(resolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   497
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   498
	(resolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   499
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   500
	(res_inst_tac [("Q","dlist_take(n1)[xl]=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   501
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   502
	(resolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   503
	(resolve_tac prems 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   504
	(atac 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   505
	(atac 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   506
	(etac spec 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   507
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   508
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   509
val dlist_all_finite_lemma1 = prove_goal Dlist.thy
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   510
"!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   511
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   512
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   513
	(nat_ind_tac "n" 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   514
	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   515
	(rtac allI 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   516
	(res_inst_tac [("l","l")] dlistE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   517
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   518
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   519
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   520
	(eres_inst_tac [("x","xl")] allE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   521
	(etac disjE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   522
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   523
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   524
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   525
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   526
val dlist_all_finite_lemma2 = prove_goal Dlist.thy "? n.dlist_take(n)[l]=l"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   527
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   528
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   529
	(res_inst_tac [("Q","l=UU")] classical2 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   530
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   531
	(subgoal_tac "(!n.dlist_take(n)[l]=UU) |(? n.dlist_take(n)[l]=l)" 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   532
	(etac disjE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   533
	(eres_inst_tac [("P","l=UU")] notE 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   534
	(rtac dlist_take_lemma 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   535
	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   536
	(atac 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   537
	(subgoal_tac "!n.!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l" 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   538
	(fast_tac HOL_cs 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   539
	(rtac allI 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   540
	(rtac dlist_all_finite_lemma1 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   541
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   542
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   543
val dlist_all_finite= prove_goalw Dlist.thy [dlist_finite_def] "dlist_finite(l)"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   544
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   545
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   546
	(rtac  dlist_all_finite_lemma2 1)
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   547
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   548
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   549
val dlist_ind = prove_goal Dlist.thy
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   550
"[|P(UU);P(dnil);\
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   551
\  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])|] ==> P(l)"
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   552
 (fn prems =>
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   553
	[
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   554
	(rtac (dlist_all_finite_lemma2 RS exE) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   555
	(etac subst 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   556
	(rtac (dlist_finite_ind RS spec) 1),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   557
	(REPEAT (resolve_tac prems 1)),
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   558
	(REPEAT (atac 1))
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   559
	]);
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   560
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   561
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   562
3a0485439396 structural induction for strict lists
nipkow
parents:
diff changeset
   563