2009-11-04 Experiments in Int
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 04 Nov 2009 11:08:05 +0100] rev 276
Experiments in Int
2009-11-04 fixed definition of PLUS
Christian Urban <urbanc@in.tum.de> [Wed, 04 Nov 2009 10:43:33 +0100] rev 275
fixed definition of PLUS
2009-11-04 simplified the quotient_def code
Christian Urban <urbanc@in.tum.de> [Wed, 04 Nov 2009 10:31:20 +0100] rev 274
simplified the quotient_def code
2009-11-04 Lifting 'fold1.simps(2)' and some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 04 Nov 2009 09:52:31 +0100] rev 273
Lifting 'fold1.simps(2)' and some cleaning.
2009-11-03 Playing with alpha_refl.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 18:09:59 +0100] rev 272
Playing with alpha_refl.
2009-11-03 Alpha.induct now lifts automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 17:51:10 +0100] rev 271
Alpha.induct now lifts automatically.
2009-11-03 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 17:30:43 +0100] rev 270
merge
2009-11-03 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 17:30:27 +0100] rev 269
applic_prs
2009-11-03 simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de> [Tue, 03 Nov 2009 16:51:33 +0100] rev 268
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
2009-11-03 Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 16:17:19 +0100] rev 267
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
2009-11-03 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 14:04:45 +0100] rev 266
merge
2009-11-03 Preparing infrastructure for general FORALL_PRS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 14:04:21 +0100] rev 265
Preparing infrastructure for general FORALL_PRS
2009-11-02 split quotient.ML into two files
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 18:26:55 +0100] rev 264
split quotient.ML into two files
2009-11-02 slightly saner way of parsing the quotient_def
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 18:16:19 +0100] rev 263
slightly saner way of parsing the quotient_def
2009-11-02 merged
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 15:39:25 +0100] rev 262
merged
2009-11-02 changed Type.typ_match to Sign.typ_match
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 15:38:49 +0100] rev 261
changed Type.typ_match to Sign.typ_match
2009-11-02 Fixes after optimization and preparing for a general FORALL_PRS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 02 Nov 2009 15:38:03 +0100] rev 260
Fixes after optimization and preparing for a general FORALL_PRS
2009-11-02 Optimization
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 02 Nov 2009 14:57:56 +0100] rev 259
Optimization
2009-11-02 Map does not fully work yet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 02 Nov 2009 11:51:50 +0100] rev 258
Map does not fully work yet.
2009-11-02 Fixed quotdata_lookup.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 02 Nov 2009 11:15:26 +0100] rev 257
Fixed quotdata_lookup.
2009-11-02 fixed problem with maps_update
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 09:47:49 +0100] rev 256
fixed problem with maps_update
2009-11-02 merged
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 09:39:29 +0100] rev 255
merged
2009-11-02 fixed the problem with types in map
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 09:33:48 +0100] rev 254
fixed the problem with types in map
2009-10-31 Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 31 Oct 2009 11:20:55 +0100] rev 253
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
2009-10-30 Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 19:03:53 +0100] rev 252
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
2009-10-30 Regularization
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 18:31:06 +0100] rev 251
Regularization
2009-10-30 merged
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 16:37:09 +0100] rev 250
merged
2009-10-30 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 16:35:43 +0100] rev 249
added some facts about fresh and support of lam
2009-10-30 Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 16:24:07 +0100] rev 248
Finally merged the code of the versions of regularize and tested examples.
2009-10-30 Lemmas about fv.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 15:52:47 +0100] rev 247
Lemmas about fv.
2009-10-30 changed the order of rfv and reformulated a3 with rfv
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 15:35:42 +0100] rev 246
changed the order of rfv and reformulated a3 with rfv
2009-10-30 merged
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 15:32:04 +0100] rev 245
merged
2009-10-30 not sure what changed here
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 15:30:33 +0100] rev 244
not sure what changed here
2009-10-30 added fv-function
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 15:28:44 +0100] rev 243
added fv-function
2009-10-30 The proper real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 15:22:59 +0100] rev 242
The proper real_alpha
2009-10-30 Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 14:25:37 +0100] rev 241
Finding applications and duplicates filtered out in abstractions
2009-10-30 Cleaning also in Lam
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 12:22:03 +0100] rev 240
Cleaning also in Lam
2009-10-30 Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 11:25:29 +0100] rev 239
Cleaning of the interface to lift.
2009-10-29 Tried manually lifting real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 17:35:03 +0100] rev 238
Tried manually lifting real_alpha
2009-10-29 More tests in Lam
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 13:30:11 +0100] rev 237
More tests in Lam
2009-10-29 Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 13:29:03 +0100] rev 236
Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
2009-10-29 Using subst for identity definition.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 12:09:31 +0100] rev 235
Using subst for identity definition.
2009-10-29 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 08:46:34 +0100] rev 234
Lifting of the 3 lemmas in LamEx
2009-10-29 Fixed wrong CARD definition and removed the "Does not work anymore" comment.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 08:06:49 +0100] rev 233
Fixed wrong CARD definition and removed the "Does not work anymore" comment.
2009-10-29 merged
Christian Urban <urbanc@in.tum.de> [Thu, 29 Oct 2009 07:29:12 +0100] rev 232
merged
2009-10-28 updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 20:01:20 +0100] rev 231
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
2009-10-28 ported all constant definitions to new scheme
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 19:46:15 +0100] rev 230
ported all constant definitions to new scheme
2009-10-28 fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 19:36:52 +0100] rev 229
fixed the definition of alpha; this *breaks* some of the experiments
2009-10-28 disambiguate ===> syntax
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 18:08:38 +0100] rev 228
disambiguate ===> syntax
2009-10-28 More cleaning in Lam code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 17:38:37 +0100] rev 227
More cleaning in Lam code
2009-10-28 cleaned FSet
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 17:17:21 +0100] rev 226
cleaned FSet
2009-10-28 Some cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:48:57 +0100] rev 225
Some cleaning
2009-10-28 Cleaning the unnecessary theorems in 'IntEx'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:16:38 +0100] rev 224
Cleaning the unnecessary theorems in 'IntEx'.
2009-10-28 Fix also in the general procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:11:28 +0100] rev 223
Fix also in the general procedure.
2009-10-28 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:06:19 +0100] rev 222
merge
2009-10-28 Fixes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:05:59 +0100] rev 221
Fixes
2009-10-28 updated all definitions
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 15:48:38 +0100] rev 220
updated all definitions
2009-10-28 merged
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 15:25:36 +0100] rev 219
merged
2009-10-28 added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 15:25:11 +0100] rev 218
added infrastructure for defining lifted constants
2009-10-28 First experiments with Lambda
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 14:59:24 +0100] rev 217
First experiments with Lambda
2009-10-28 Fixed mistake in const generation, will postpone this.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 12:22:06 +0100] rev 216
Fixed mistake in const generation, will postpone this.
2009-10-28 More finshed proofs and cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 10:29:00 +0100] rev 215
More finshed proofs and cleaning
2009-10-28 Proof of append_rsp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 10:17:07 +0100] rev 214
Proof of append_rsp
2009-10-28 merged
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 01:49:31 +0100] rev 213
merged
2009-10-28 added a function for matching types
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 01:48:45 +0100] rev 212
added a function for matching types
2009-10-27 Manual conversion of equality to equivalence allows lifting append_assoc.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 18:05:45 +0100] rev 211
Manual conversion of equality to equivalence allows lifting append_assoc.
2009-10-27 Simplfied interface to repabs_injection.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 18:02:35 +0100] rev 210
Simplfied interface to repabs_injection.
2009-10-27 map_append lifted automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 17:08:47 +0100] rev 209
map_append lifted automatically.
2009-10-27 Manually lifted Map_Append.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 16:15:56 +0100] rev 208
Manually lifted Map_Append.
2009-10-27 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 15:00:15 +0100] rev 207
Merged
2009-10-27 Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 14:59:00 +0100] rev 206
Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
2009-10-27 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 14:46:38 +0100] rev 205
tuned
2009-10-27 merged
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 14:15:40 +0100] rev 204
merged
2009-10-27 added equiv-thm to the quot_info
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 14:14:30 +0100] rev 203
added equiv-thm to the quot_info
2009-10-27 Simplifying FSet with new functions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 12:20:57 +0100] rev 202
Simplifying FSet with new functions.
2009-10-27 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 11:43:02 +0100] rev 201
added an example about lambda-terms
2009-10-27 made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 11:27:53 +0100] rev 200
made quotients compatiple with Nominal; updated keyword file
2009-10-27 merged
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 11:03:38 +0100] rev 199
merged
2009-10-27 Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 09:01:12 +0100] rev 198
Completely cleaned Int.
2009-10-27 Further reordering in Int code.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 07:46:52 +0100] rev 197
Further reordering in Int code.
2009-10-26 Simplifying Int.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 19:35:30 +0100] rev 196
Simplifying Int.
2009-10-26 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 15:32:17 +0100] rev 195
Merge
2009-10-26 Simplifying Int and Working on map
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 15:31:53 +0100] rev 194
Simplifying Int and Working on map
2009-10-26 merged
Christian Urban <urbanc@in.tum.de> [Mon, 26 Oct 2009 14:18:26 +0100] rev 193
merged
2009-10-26 Simplifying code in int
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 14:16:32 +0100] rev 192
Simplifying code in int
2009-10-26 Symmetry of integer addition
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 13:33:28 +0100] rev 191
Symmetry of integer addition
2009-10-26 Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 11:55:36 +0100] rev 190
Finished the code for adding lower defs, and more things moved to QuotMain
2009-10-26 Making all the definitions from the original ones
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 11:34:02 +0100] rev 189
Making all the definitions from the original ones
2009-10-26 Finished COND_PRS proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 10:20:20 +0100] rev 188
Finished COND_PRS proof.
2009-10-26 Cleaning and fixing.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 10:02:50 +0100] rev 187
Cleaning and fixing.
2009-10-26 updated with quotient_def
Christian Urban <urbanc@in.tum.de> [Mon, 26 Oct 2009 02:06:01 +0100] rev 186
updated with quotient_def
2009-10-25 added code for declaring map-functions
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 23:44:41 +0100] rev 185
added code for declaring map-functions
2009-10-24 added "print_quotients" command to th ekeyword file
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 01:31:04 +0200] rev 184
added "print_quotients" command to th ekeyword file
2009-10-24 proved the two lemmas in QuotScript (reformulated them without leading forall)
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 01:15:03 +0200] rev 183
proved the two lemmas in QuotScript (reformulated them without leading forall)
2009-10-24 added data-storage about the quotients
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 00:14:40 +0200] rev 182
added data-storage about the quotients
2009-10-24 added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 22:52:23 +0200] rev 181
added another example file about integers (see HOL/Int.thy)
2009-10-24 changed the definitions of liftet constants to use fun_maps
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 18:17:38 +0200] rev 180
changed the definitions of liftet constants to use fun_maps
2009-10-24 Merge
cek@localhost.localdomain [Sat, 24 Oct 2009 17:29:20 +0200] rev 179
Merge
2009-10-24 Finally lifted induction, with some manually added simplification lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 17:29:27 +0200] rev 178
Finally lifted induction, with some manually added simplification lemmas.
2009-10-24 changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 16:31:07 +0200] rev 177
changed encoding from utf8 to ISO8 (needed to work with xemacs)
2009-10-24 Merge
cek@localhost.localdomain [Sat, 24 Oct 2009 16:15:33 +0200] rev 176
Merge
2009-10-24 Preparing infrastructire for LAMBDA_PRS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 16:15:58 +0200] rev 175
Preparing infrastructire for LAMBDA_PRS
2009-10-24 moved the map_funs setup into QuotMain
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 16:09:05 +0200] rev 174
moved the map_funs setup into QuotMain
2009-10-24 Finally completely lift the previously lifted theorems + clean some old stuff
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 14:00:18 +0200] rev 173
Finally completely lift the previously lifted theorems + clean some old stuff
2009-10-24 More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 13:00:54 +0200] rev 172
More infrastructure for automatic lifting of theorems lifted before
2009-10-24 More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 10:16:53 +0200] rev 171
More infrastructure for automatic lifting of theorems lifted before
2009-10-24 Undid wrong merge
cek@localhost.localdomain [Sat, 24 Oct 2009 08:34:14 +0200] rev 170
Undid wrong merge
2009-10-24 Tried rolling back
cek@localhost.localdomain [Sat, 24 Oct 2009 08:29:11 +0200] rev 169
Tried rolling back
2009-10-24 Cleaning the mess
cek@localhost.localdomain [Sat, 24 Oct 2009 08:24:26 +0200] rev 168
Cleaning the mess
2009-10-24 Merge
cek@localhost.localdomain [Sat, 24 Oct 2009 08:09:40 +0200] rev 167
Merge
2009-10-24 Better tactic and simplified the proof further
cek@localhost.localdomain [Sat, 24 Oct 2009 08:09:09 +0200] rev 166
Better tactic and simplified the proof further
2009-10-23 fixed problem with incorrect ABS/REP name
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 01:33:29 +0200] rev 165
fixed problem with incorrect ABS/REP name
2009-10-23 Stronger tactic, simpler proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 18:20:06 +0200] rev 164
Stronger tactic, simpler proof.
2009-10-23 Split Finite Set example into separate file
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 16:34:20 +0200] rev 163
Split Finite Set example into separate file
2009-10-23 eqsubst_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 16:01:13 +0200] rev 162
eqsubst_tac
2009-10-23 Trying to get a simpler lemma with the whole infrastructure
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 11:24:43 +0200] rev 161
Trying to get a simpler lemma with the whole infrastructure
2009-10-23 Using RANGE tactical allows getting rid of the quotients immediately.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 09:21:45 +0200] rev 160
Using RANGE tactical allows getting rid of the quotients immediately.
2009-10-22 Further developing the tactic and simplifying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 17:35:40 +0200] rev 159
Further developing the tactic and simplifying the proof
2009-10-22 res_forall_rsp_tac further simplifies the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 16:24:02 +0200] rev 158
res_forall_rsp_tac further simplifies the proof
2009-10-22 Working on the proof and the tactic.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 16:10:06 +0200] rev 157
Working on the proof and the tactic.
2009-10-22 The proof gets simplified
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 15:45:05 +0200] rev 156
The proof gets simplified
2009-10-22 Removed an assumption
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 15:44:16 +0200] rev 155
Removed an assumption
2009-10-22 The proof now including manually unfolded higher-order RES_FORALL_RSP.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 15:02:01 +0200] rev 154
The proof now including manually unfolded higher-order RES_FORALL_RSP.
2009-10-22 The problems with 'abs' term.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 13:45:48 +0200] rev 153
The problems with 'abs' term.
2009-10-22 Simplified the proof with some tactic... Still hangs sometimes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 11:43:12 +0200] rev 152
Simplified the proof with some tactic... Still hangs sometimes.
2009-10-22 More proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 10:45:33 +0200] rev 151
More proof
2009-10-22 Got rid of instantiations in the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 10:38:00 +0200] rev 150
Got rid of instantiations in the proof
2009-10-22 Removed some debugging messages
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 06:51:27 +0200] rev 149
Removed some debugging messages
2009-10-21 tuned and attempted to store data about the quotients (does not work yet)
Christian Urban <urbanc@in.tum.de> [Thu, 22 Oct 2009 01:59:17 +0200] rev 148
tuned and attempted to store data about the quotients (does not work yet)
2009-10-21 tuned
Christian Urban <urbanc@in.tum.de> [Thu, 22 Oct 2009 01:16:42 +0200] rev 147
tuned
2009-10-21 slight tuning
Christian Urban <urbanc@in.tum.de> [Thu, 22 Oct 2009 01:15:01 +0200] rev 146
slight tuning
2009-10-21 fixed my_reg
Christian Urban <urbanc@in.tum.de> [Wed, 21 Oct 2009 18:30:42 +0200] rev 145
fixed my_reg
2009-10-21 Reorganization of the construction part
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 16:13:39 +0200] rev 144
Reorganization of the construction part
2009-10-21 Simplified proof more
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 15:01:50 +0200] rev 143
Simplified proof more
2009-10-21 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 14:30:29 +0200] rev 142
Cleaning the code
2009-10-21 Further reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 14:15:22 +0200] rev 141
Further reorganization
2009-10-21 Further reorganizing the file
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 14:09:06 +0200] rev 140
Further reorganizing the file
2009-10-21 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 13:47:39 +0200] rev 139
Reordering
2009-10-21 cterm_instantiate also fails for some strange reason...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 11:50:53 +0200] rev 138
cterm_instantiate also fails for some strange reason...
2009-10-21 preparing arguments for res_inst_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 10:55:32 +0200] rev 137
preparing arguments for res_inst_tac
2009-10-21 Trying res_inst_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 10:30:29 +0200] rev 136
Trying res_inst_tac
2009-10-20 started to write code for storing data about the quotients
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 19:46:22 +0200] rev 135
started to write code for storing data about the quotients
2009-10-20 some minor tuning
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 09:37:22 +0200] rev 134
some minor tuning
2009-10-20 tuned and fixed the earlier fix
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 09:31:34 +0200] rev 133
tuned and fixed the earlier fix
2009-10-20 fixed the abs case in my_reg and added an app case
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 09:21:18 +0200] rev 132
fixed the abs case in my_reg and added an app case
2009-10-19 my version of regularise (still needs to be completed)
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 01:17:22 +0200] rev 131
my version of regularise (still needs to be completed)
2009-10-19 moved the map-info and fun-info section to quotient.ML
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 00:12:05 +0200] rev 130
moved the map-info and fun-info section to quotient.ML
2009-10-18 Test if we can already do sth with the transformed theorem.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 18 Oct 2009 10:34:53 +0200] rev 129
Test if we can already do sth with the transformed theorem.
2009-10-18 slight fix and tuning
Christian Urban <urbanc@in.tum.de> [Sun, 18 Oct 2009 08:44:16 +0200] rev 128
slight fix and tuning
2009-10-17 the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
Christian Urban <urbanc@in.tum.de> [Sun, 18 Oct 2009 00:52:10 +0200] rev 127
the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
2009-10-17 Partial simplification of the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 16:06:54 +0200] rev 126
Partial simplification of the proof
2009-10-17 Some QUOTIENTS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 15:42:57 +0200] rev 125
Some QUOTIENTS
2009-10-17 Only QUOTIENSs are left to fnish proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 14:16:57 +0200] rev 124
Only QUOTIENSs are left to fnish proof
2009-10-17 More higher order unification problems
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:44:58 +0200] rev 123
More higher order unification problems
2009-10-17 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:31:48 +0200] rev 122
Merged
2009-10-17 Simplified
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:31:36 +0200] rev 121
Simplified
2009-10-17 Further in the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:20:56 +0200] rev 120
Further in the proof
2009-10-17 compose_tac works with the full instantiation.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 11:54:50 +0200] rev 119
compose_tac works with the full instantiation.
2009-10-17 slightly simplified get_fun function
Christian Urban <urbanc@in.tum.de> [Sat, 17 Oct 2009 12:19:06 +0200] rev 118
slightly simplified get_fun function
2009-10-17 The instantiated version is the same modulo beta
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 10:40:54 +0200] rev 117
The instantiated version is the same modulo beta
2009-10-17 Fully manually instantiated. Still fails...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 10:07:52 +0200] rev 116
Fully manually instantiated. Still fails...
2009-10-17 Little progress with match/instantiate
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 09:04:24 +0200] rev 115
Little progress with match/instantiate
2009-10-16 Fighting with the instantiation
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 19:21:05 +0200] rev 114
Fighting with the instantiation
2009-10-16 Symmetric version of REP_ABS_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 17:05:52 +0200] rev 113
Symmetric version of REP_ABS_RSP
2009-10-16 Progressing with the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 16:51:01 +0200] rev 112
Progressing with the proof
2009-10-16 Finally fix get_fun.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 10:54:31 +0200] rev 111
Finally fix get_fun.
2009-10-16 A fix for one fun_map; doesn't work for more.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 08:48:56 +0200] rev 110
A fix for one fun_map; doesn't work for more.
2009-10-16 fixed the problem with function types; but only type_of works; cterm_of does not work
Christian Urban <urbanc@in.tum.de> [Fri, 16 Oct 2009 03:26:54 +0200] rev 109
fixed the problem with function types; but only type_of works; cterm_of does not work
2009-10-15 Description of the problem with get_fun.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 16:51:24 +0200] rev 108
Description of the problem with get_fun.
2009-10-15 A proper build_goal_term function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 16:36:20 +0200] rev 107
A proper build_goal_term function.
2009-10-15 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 12:06:00 +0200] rev 106
Cleaning the code
2009-10-15 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:57:33 +0200] rev 105
Merged
2009-10-15 Cleaning the proofs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:56:30 +0200] rev 104
Cleaning the proofs
2009-10-15 Cleaning the code, part 4
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:55:52 +0200] rev 103
Cleaning the code, part 4
2009-10-15 slightly improved tyRel
Christian Urban <urbanc@in.tum.de> [Thu, 15 Oct 2009 11:53:11 +0200] rev 102
slightly improved tyRel
2009-10-15 Reordering the code, part 3
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:42:14 +0200] rev 101
Reordering the code, part 3
2009-10-15 Reordering the code, part 2.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:29:38 +0200] rev 100
Reordering the code, part 2.
2009-10-15 Reordering the code, part 1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:25:25 +0200] rev 99
Reordering the code, part 1.
2009-10-15 Minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:20:50 +0200] rev 98
Minor cleaning.
2009-10-15 The definition of Fold1
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:17:27 +0200] rev 97
The definition of Fold1
2009-10-15 A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 10:25:23 +0200] rev 96
A number of lemmas for REGULARIZE_TAC and regularizing card1.
2009-10-14 Proving the proper RepAbs version
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 18:13:16 +0200] rev 95
Proving the proper RepAbs version
2009-10-14 Forgot to save, second part of the commit
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 16:23:49 +0200] rev 94
Forgot to save, second part of the commit
2009-10-14 Manually regularized list_induct2
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 16:23:32 +0200] rev 93
Manually regularized list_induct2
2009-10-14 Fixed bug in regularise types. Now we can regularise list.induct.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 12:05:39 +0200] rev 92
Fixed bug in regularise types. Now we can regularise list.induct.
2009-10-14 Function for checking recursively if lifting is needed
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 11:23:55 +0200] rev 91
Function for checking recursively if lifting is needed
2009-10-14 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 09:50:13 +0200] rev 90
Merge
2009-10-14 Proper handling of non-lifted quantifiers, testing type freezing.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 09:47:16 +0200] rev 89
Proper handling of non-lifted quantifiers, testing type freezing.
2009-10-13 slight simplification of atomize_thm
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 22:22:15 +0200] rev 88
slight simplification of atomize_thm
2009-10-13 atomize_thm and meta_quantify.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 18:01:54 +0200] rev 87
atomize_thm and meta_quantify.
2009-10-13 Regularizing HOL all.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 13:37:07 +0200] rev 86
Regularizing HOL all.
2009-10-13 ":" is used for being in a set, "IN" means something else...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 11:38:35 +0200] rev 85
":" is used for being in a set, "IN" means something else...
2009-10-13 First (untested) version of regularize for abstractions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 11:03:55 +0200] rev 84
First (untested) version of regularize for abstractions.
2009-10-13 restored old version
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 09:26:19 +0200] rev 83
restored old version
2009-10-12 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 00:02:22 +0200] rev 82
tuned
2009-10-12 slightly modified the parser
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:39:14 +0200] rev 81
slightly modified the parser
2009-10-12 deleted diagnostic code
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:16:20 +0200] rev 80
deleted diagnostic code
2009-10-12 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:06:14 +0200] rev 79
added quotient command (you need to update isar-keywords-prove.el)
2009-10-12 added new keyword
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 22:44:16 +0200] rev 78
added new keyword
2009-10-12 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 16:31:29 +0200] rev 77
Bounded quantifier
2009-10-12 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 15:47:27 +0200] rev 76
The tyREL function.
2009-10-12 started some strange functions
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 14:30:50 +0200] rev 75
started some strange functions
2009-10-12 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 13:58:31 +0200] rev 74
Further with the manual proof
2009-10-09 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 09 Oct 2009 17:05:45 +0200] rev 73
Further experiments with proving induction manually
2009-10-09 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 09 Oct 2009 15:03:43 +0200] rev 72
Testing if I can prove the regularized version of induction manually
2009-10-08 exported parts of QuotMain into a separate ML-file
Christian Urban <urbanc@in.tum.de> [Thu, 08 Oct 2009 14:27:50 +0200] rev 71
exported parts of QuotMain into a separate ML-file
2009-10-06 consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 15:11:30 +0200] rev 70
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar proof of atomize_eqv.
2009-10-06 simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:56:23 +0200] rev 69
simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
2009-10-06 renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:41:35 +0200] rev 68
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
2009-10-06 tuned; nothing serious
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:36:08 +0200] rev 67
tuned; nothing serious
2009-10-06 another improvement to unlam_def
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 09:28:59 +0200] rev 66
another improvement to unlam_def
2009-10-06 one further improvement to unlam_def
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 02:02:51 +0200] rev 65
one further improvement to unlam_def
2009-10-05 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 01:50:13 +0200] rev 64
simplified the unlam_def function
2009-10-05 added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)
Christian Urban <urbanc@in.tum.de> [Mon, 05 Oct 2009 11:54:02 +0200] rev 63
added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)
2009-10-05 used prop_of to get the term of a theorem (replaces crep_thm)
Christian Urban <urbanc@in.tum.de> [Mon, 05 Oct 2009 11:24:32 +0200] rev 62
used prop_of to get the term of a theorem (replaces crep_thm)
2009-10-02 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 02 Oct 2009 11:10:21 +0200] rev 61
Merged
2009-10-02 First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 02 Oct 2009 11:09:33 +0200] rev 60
First theorem with quantifiers. Learned how to use sledgehammer.
2009-10-01 simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de> [Thu, 01 Oct 2009 16:10:14 +0200] rev 59
simplified the storage of the map-functions by using TheoryDataFun
2009-09-30 Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 30 Sep 2009 16:57:09 +0200] rev 58
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
2009-09-29 used new cong_tac
Christian Urban <urbanc@in.tum.de> [Tue, 29 Sep 2009 22:35:48 +0200] rev 57
used new cong_tac
2009-09-29 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 17:46:18 +0200] rev 56
First version of handling of the universal quantifier
2009-09-29 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 15:58:14 +0200] rev 55
Handling abstraction correctly.
2009-09-29 second test
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 13:38:27 +0200] rev 54
second test
2009-09-29 Test line
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 13:24:57 +0200] rev 53
Test line
2009-09-29 Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 11:55:37 +0200] rev 52
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
2009-09-29 Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 10:49:31 +0200] rev 51
Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
2009-09-29 Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 09:58:02 +0200] rev 50
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
2009-09-29 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 09:26:22 +0200] rev 49
Merged
2009-09-28 added name to prove
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 23:17:29 +0200] rev 48
added name to prove
2009-09-28 consistent state
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 19:24:55 +0200] rev 47
consistent state
2009-09-28 some tuning of my code
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 19:22:28 +0200] rev 46
some tuning of my code
2009-09-28 Cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 19:15:19 +0200] rev 45
Cleanup
2009-09-28 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 19:10:27 +0200] rev 44
Merged
2009-09-28 Cleaning the code with Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 18:59:04 +0200] rev 43
Cleaning the code with Makarius
2009-09-28 Instnatiation with a schematic variable
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 15:37:38 +0200] rev 42
Instnatiation with a schematic variable
2009-09-28 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 02:39:44 +0200] rev 41
added ctxt as explicit argument to build_goal; tuned
2009-09-25 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 19:26:18 +0200] rev 40
slightly tuned the comment for unlam
2009-09-25 fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 17:08:50 +0200] rev 39
fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x
2009-09-25 tuned slightly one proof
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 16:50:11 +0200] rev 38
tuned slightly one proof
2009-09-25 A version of the tactic that exports variables correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 25 Sep 2009 14:50:35 +0200] rev 37
A version of the tactic that exports variables correctly. It still does not know how to instantiate the obtained theorems.
2009-09-25 Minor cleaning: whitespace, commas etc.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 25 Sep 2009 09:38:16 +0200] rev 36
Minor cleaning: whitespace, commas etc.
2009-09-24 Correctly handling abstractions while building goals
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 17:43:26 +0200] rev 35
Correctly handling abstractions while building goals Use DatatypeAux cong_tac instead of own functions since it handles universal quantifiers properly.
2009-09-24 Minor cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 13:32:52 +0200] rev 34
Minor cleanup
2009-09-24 Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 11:38:20 +0200] rev 33
Found the source for the exception and added a handle for it.
2009-09-24 Make the tactic use Trueprop_cong and atomize.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 09:09:46 +0200] rev 32
Make the tactic use Trueprop_cong and atomize.
2009-09-23 Proper code for getting the prop out of the theorem.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 23 Sep 2009 16:57:56 +0200] rev 31
Proper code for getting the prop out of the theorem.
2009-09-23 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 23 Sep 2009 16:44:56 +0200] rev 30
Using "atomize" the versions with arbitrary Trueprops can be proven.
2009-09-22 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 22 Sep 2009 17:39:52 +0200] rev 29
Proper definition of CARD and some properties of it. Translation should now support Pure assumptions and Trueprops anywhere, but a problem needs to be fixed with the tactic.
2009-09-22 some comments
Christian Urban <urbanc@in.tum.de> [Tue, 22 Sep 2009 09:42:27 +0200] rev 28
some comments
2009-09-21 merged
Christian Urban <urbanc@in.tum.de> [Mon, 21 Sep 2009 18:18:29 +0200] rev 27
merged
2009-09-21 slight tuning
Christian Urban <urbanc@in.tum.de> [Mon, 21 Sep 2009 18:18:01 +0200] rev 26
slight tuning
2009-09-21 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 21 Sep 2009 16:45:44 +0200] rev 25
The tactic with REPEAT, CHANGED and a proper simpset.
2009-09-21 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 21 Sep 2009 10:53:01 +0200] rev 24
Merged with my changes from the morning: further working on the tactic and produced goals.
2009-09-20 some more beautification
Ning@localhost [Sun, 20 Sep 2009 05:48:49 +0100] rev 23
some more beautification
2009-09-20 beautification of some proofs
Ning@localhost [Sun, 20 Sep 2009 05:18:36 +0100] rev 22
beautification of some proofs
2009-09-18 Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 18 Sep 2009 17:30:33 +0200] rev 21
Added more useful quotient facts.
2009-09-18 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 18 Sep 2009 13:44:06 +0200] rev 20
Testing the tactic further.
2009-09-17 The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 17 Sep 2009 16:55:11 +0200] rev 19
The tactic still only for fset
2009-09-17 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 17 Sep 2009 12:06:06 +0200] rev 18
Infrastructure for the tactic
2009-09-16 More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 16 Sep 2009 11:50:41 +0200] rev 17
More naming/binding suggestions from Makarius
2009-09-15 Code cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 11:31:35 +0200] rev 16
Code cleanup
2009-09-15 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 10:00:34 +0200] rev 15
Cleaning the code
2009-09-15 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 09:59:56 +0200] rev 14
Generalized interpretation, works for all examples.
2009-08-28 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 28 Aug 2009 17:12:19 +0200] rev 13
Fixes after suggestions from Makarius: - indentation - lowercase/uppercase - axioms -> axiomatization - proper operator priorities - proper exception handling
2009-08-28 More examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 28 Aug 2009 10:01:25 +0200] rev 12
More examples.
2009-08-27 Use metavariables in the 'non-lambda' definitions
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 27 Aug 2009 09:04:39 +0200] rev 11
Use metavariables in the 'non-lambda' definitions
2009-08-26 Make both kinds of definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 Aug 2009 11:31:55 +0200] rev 10
Make both kinds of definitions.
2009-08-25 Changed to the use of "modern interface"
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 17:37:50 +0200] rev 9
Changed to the use of "modern interface" (removed the _cmd and passing of strings) Fixed Trueprop handling and the first proof starts working properly.
2009-08-25 Initial version of the function that builds goals.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 14:37:11 +0200] rev 8
Initial version of the function that builds goals.
2009-08-25 - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 10:35:28 +0200] rev 7
- Build an interpretation for fset from ML level and use it - Added CARD
2009-08-24 added the prove command
Christian Urban <urbanc@in.tum.de> [Tue, 25 Aug 2009 00:30:23 +0200] rev 6
added the prove command
2009-08-21 Fixed
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 Aug 2009 13:56:20 +0200] rev 5
Fixed
2009-08-21 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 21 Aug 2009 13:36:58 +0200] rev 4
tuned
2009-08-20 UNION - Append theorem
cek@localhost.localdomain [Thu, 20 Aug 2009 14:44:29 +0200] rev 3
UNION - Append theorem
2009-08-20 update
Christian Urban <urbanc@in.tum.de> [Thu, 20 Aug 2009 10:31:44 +0200] rev 2
update
2009-08-18 updated slightly
Christian Urban <urbanc@in.tum.de> [Tue, 18 Aug 2009 14:04:51 +0200] rev 1
updated slightly
2009-08-11 initial commit
Christian Urban <urbanc@in.tum.de> [Tue, 11 Aug 2009 12:29:15 +0200] rev 0
initial commit
(0) +960 +1000 tip