73 done |
73 done |
74 |
74 |
75 |
75 |
76 lemma mapT: "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)" |
76 lemma mapT: "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)" |
77 apply (unfold map_def) |
77 apply (unfold map_def) |
78 apply (tactic "typechk_tac @{context} [] 1") |
78 apply typechk |
79 apply blast |
79 apply blast |
80 done |
80 done |
81 |
81 |
82 lemma appendT: "[| l : List(A); m : List(A) |] ==> l @ m : List(A)" |
82 lemma appendT: "[| l : List(A); m : List(A) |] ==> l @ m : List(A)" |
83 apply (unfold append_def) |
83 apply (unfold append_def) |
84 apply (tactic "typechk_tac @{context} [] 1") |
84 apply typechk |
85 done |
85 done |
86 |
86 |
87 lemma appendTS: |
87 lemma appendTS: |
88 "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}" |
88 "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}" |
89 by (blast intro!: appendT) |
89 by (blast intro!: appendT) |
90 |
90 |
91 lemma filterT: "[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)" |
91 lemma filterT: "[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)" |
92 apply (unfold filter_def) |
92 apply (unfold filter_def) |
93 apply (tactic "typechk_tac @{context} [] 1") |
93 apply typechk |
94 done |
94 done |
95 |
95 |
96 lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)" |
96 lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)" |
97 apply (unfold flat_def) |
97 apply (unfold flat_def) |
98 apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *}) |
98 apply (typechk appendT) |
99 done |
99 done |
100 |
100 |
101 lemma insertT: "[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)" |
101 lemma insertT: "[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)" |
102 apply (unfold insert_def) |
102 apply (unfold insert_def) |
103 apply (tactic "typechk_tac @{context} [] 1") |
103 apply typechk |
104 done |
104 done |
105 |
105 |
106 lemma insertTS: |
106 lemma insertTS: |
107 "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> |
107 "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> |
108 insert(f,a,l) : {x:List(A). P(x)}" |
108 insert(f,a,l) : {x:List(A). P(x)}" |
109 by (blast intro!: insertT) |
109 by (blast intro!: insertT) |
110 |
110 |
111 lemma partitionT: |
111 lemma partitionT: |
112 "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)" |
112 "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)" |
113 apply (unfold partition_def) |
113 apply (unfold partition_def) |
114 apply (tactic "typechk_tac @{context} [] 1") |
114 apply typechk |
115 apply (tactic "clean_ccs_tac @{context}") |
115 apply clean_ccs |
116 apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) |
116 apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) |
117 apply assumption+ |
117 apply assumption+ |
118 apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) |
118 apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) |
119 apply assumption+ |
119 apply assumption+ |
120 done |
120 done |