funcCF.git
8 years agoVortrag zur SA master Vortrag_Studienarbeit
Joachim Breitner [Mon, 22 Nov 2010 13:33:07 +0000 (14:33 +0100)]
Vortrag zur SA

8 years agoPrepare AFP entry AFPSubmission
Joachim Breitner [Tue, 16 Nov 2010 09:23:15 +0000 (10:23 +0100)]
Prepare AFP entry

8 years agoPrepare AFP entry
Joachim Breitner [Tue, 16 Nov 2010 08:46:03 +0000 (09:46 +0100)]
Prepare AFP entry

8 years agoRename hackage package HackageUpload0.1
Joachim Breitner [Tue, 16 Nov 2010 08:09:02 +0000 (09:09 +0100)]
Rename hackage package

8 years agoPrepare Haskell Code for upload
Joachim Breitner [Tue, 16 Nov 2010 08:08:06 +0000 (09:08 +0100)]
Prepare Haskell Code for upload

8 years agoCover, OT1 encoding Abgabe_Studienarbeit
Joachim Breitner [Mon, 15 Nov 2010 14:27:44 +0000 (15:27 +0100)]
Cover, OT1 encoding

8 years agoLetzte Typo-Runde
Joachim Breitner [Mon, 15 Nov 2010 14:21:58 +0000 (15:21 +0100)]
Letzte Typo-Runde

8 years agocontour nodes depend on conditionals
Joachim Breitner [Sat, 13 Nov 2010 11:25:10 +0000 (12:25 +0100)]
contour nodes depend on conditionals

8 years agoPfeile umdrehen
Joachim Breitner [Sat, 13 Nov 2010 11:16:11 +0000 (12:16 +0100)]
Pfeile umdrehen

8 years agoConclusion
Joachim Breitner [Fri, 12 Nov 2010 10:27:04 +0000 (11:27 +0100)]
Conclusion

8 years agoConclusion
Joachim Breitner [Fri, 12 Nov 2010 10:15:19 +0000 (11:15 +0100)]
Conclusion

8 years agoCFG-instanz-Beispiel
Joachim Breitner [Fri, 12 Nov 2010 09:54:39 +0000 (10:54 +0100)]
CFG-instanz-Beispiel

8 years agoCFG-instanz-Beispiel
Joachim Breitner [Fri, 12 Nov 2010 09:32:07 +0000 (10:32 +0100)]
CFG-instanz-Beispiel

8 years agoCFG-instanz-Beispiel
Joachim Breitner [Fri, 12 Nov 2010 09:30:50 +0000 (10:30 +0100)]
CFG-instanz-Beispiel

8 years agoVds removal
Joachim Breitner [Wed, 10 Nov 2010 15:42:35 +0000 (16:42 +0100)]
Vds removal

8 years agoAndreas Typosuche
Joachim Breitner [Wed, 10 Nov 2010 15:24:27 +0000 (16:24 +0100)]
Andreas Typosuche

8 years agoNo need to mess with font@warning
Joachim Breitner [Mon, 8 Nov 2010 15:41:36 +0000 (16:41 +0100)]
No need to mess with font@warning

8 years agoErste Fehlerkorrekturrunde meinerseits
Joachim Breitner [Mon, 8 Nov 2010 15:39:31 +0000 (16:39 +0100)]
Erste Fehlerkorrekturrunde meinerseits

8 years agoSatzspiegelspielereien
Joachim Breitner [Mon, 8 Nov 2010 13:43:19 +0000 (14:43 +0100)]
Satzspiegelspielereien

8 years agoMehr zu 1CFA und 0CFA
Joachim Breitner [Wed, 3 Nov 2010 16:10:34 +0000 (17:10 +0100)]
Mehr zu 1CFA und 0CFA

8 years agoBeispielanalyse
Joachim Breitner [Tue, 2 Nov 2010 11:04:46 +0000 (12:04 +0100)]
Beispielanalyse

8 years agoFurther writing, new chapter about slicing
Joachim Breitner [Fri, 29 Oct 2010 15:13:24 +0000 (17:13 +0200)]
Further writing, new chapter about slicing

8 years agoImprove session graph
Joachim Breitner [Thu, 28 Oct 2010 07:40:43 +0000 (09:40 +0200)]
Improve session graph

8 years agoEval does not CPSUtils
Joachim Breitner [Thu, 28 Oct 2010 07:40:35 +0000 (09:40 +0200)]
Eval does not CPSUtils

8 years agoWeiter geschrieben
Joachim Breitner [Tue, 26 Oct 2010 17:17:40 +0000 (19:17 +0200)]
Weiter geschrieben

8 years agoProtoype of a small step semantics
Joachim Breitner [Mon, 25 Oct 2010 09:42:42 +0000 (11:42 +0200)]
Protoype of a small step semantics

8 years agoWeitergeschrieben, Isabelle-Kapitel fast fertig
Joachim Breitner [Fri, 22 Oct 2010 10:26:32 +0000 (12:26 +0200)]
Weitergeschrieben, Isabelle-Kapitel fast fertig

8 years agoText zum Isabelle-Teil angefangen
Joachim Breitner [Tue, 19 Oct 2010 10:42:34 +0000 (12:42 +0200)]
Text zum Isabelle-Teil angefangen

8 years agoSession dependency graphs
Joachim Breitner [Tue, 19 Oct 2010 09:03:58 +0000 (11:03 +0200)]
Session dependency graphs

8 years agoRemove unicode from Haskell comment
Joachim Breitner [Mon, 18 Oct 2010 15:46:42 +0000 (17:46 +0200)]
Remove unicode from Haskell comment

8 years agoBegin to write the Studienarbeit
Joachim Breitner [Mon, 18 Oct 2010 15:46:29 +0000 (17:46 +0200)]
Begin to write the Studienarbeit

8 years agoAlternative proof of finiteness
Joachim Breitner [Fri, 15 Oct 2010 13:38:03 +0000 (15:38 +0200)]
Alternative proof of finiteness

8 years agoWeiter Zeug aufgeschrieben (alle verwendeten Theorien sind drin)
Joachim Breitner [Wed, 13 Oct 2010 13:09:17 +0000 (15:09 +0200)]
Weiter Zeug aufgeschrieben (alle verwendeten Theorien sind drin)

8 years agoWeiter Zeug aufgeschrieben
Joachim Breitner [Tue, 12 Oct 2010 15:47:45 +0000 (17:47 +0200)]
Weiter Zeug aufgeschrieben

8 years agoWeiter Zeug aufgeschrieben
Joachim Breitner [Tue, 12 Oct 2010 10:49:48 +0000 (12:49 +0200)]
Weiter Zeug aufgeschrieben

8 years agoAngefangen Zeug aufzuschreiben
Joachim Breitner [Fri, 8 Oct 2010 13:45:11 +0000 (15:45 +0200)]
Angefangen Zeug aufzuschreiben

8 years agoSome cleanup
Joachim Breitner [Thu, 7 Oct 2010 14:27:09 +0000 (16:27 +0200)]
Some cleanup

8 years agoFiniteness for inductive set works for non-recursive sets
Joachim Breitner [Thu, 7 Oct 2010 13:42:20 +0000 (15:42 +0200)]
Finiteness for inductive set works for non-recursive sets

8 years agoTrying to derive finiteness for inductive set (no more sorrys)
Joachim Breitner [Wed, 6 Oct 2010 16:09:20 +0000 (18:09 +0200)]
Trying to derive finiteness for inductive set (no more sorrys)

8 years agoTrying to derive finiteness for inductive set
Joachim Breitner [Wed, 6 Oct 2010 15:43:05 +0000 (17:43 +0200)]
Trying to derive finiteness for inductive set

8 years agoTrying to derive finiteness for inductive set
Joachim Breitner [Wed, 6 Oct 2010 15:39:53 +0000 (17:39 +0200)]
Trying to derive finiteness for inductive set

8 years agoFix transforming theory
Joachim Breitner [Wed, 6 Oct 2010 15:34:23 +0000 (17:34 +0200)]
Fix transforming theory

8 years agoTrying to derive finiteness for inductive set
Joachim Breitner [Wed, 6 Oct 2010 15:34:04 +0000 (17:34 +0200)]
Trying to derive finiteness for inductive set

8 years agoShow that occuring arguments are finite
Joachim Breitner [Tue, 5 Oct 2010 16:28:10 +0000 (18:28 +0200)]
Show that occuring arguments are finite

8 years agoShow that argument space is finite
Joachim Breitner [Tue, 5 Oct 2010 09:27:00 +0000 (11:27 +0200)]
Show that argument space is finite

8 years agoProve R/g decomposition for evalCPS
Joachim Breitner [Wed, 29 Sep 2010 16:51:52 +0000 (18:51 +0200)]
Prove R/g decomposition for evalCPS

8 years agoProve R/g decomposition
Joachim Breitner [Wed, 29 Sep 2010 11:40:40 +0000 (13:40 +0200)]
Prove R/g decomposition

8 years agoFixpoint transformation (removing discr, giving up)
Joachim Breitner [Wed, 29 Sep 2010 08:02:18 +0000 (10:02 +0200)]
Fixpoint transformation (removing discr, giving up)

8 years agoShow Shivers’ computability results
Joachim Breitner [Fri, 24 Sep 2010 14:10:32 +0000 (16:10 +0200)]
Show Shivers’ computability results

8 years agoFix LaTeX
Joachim Breitner [Thu, 23 Sep 2010 14:47:57 +0000 (16:47 +0200)]
Fix LaTeX

8 years agoRemove Un_mono_sq
Joachim Breitner [Thu, 23 Sep 2010 14:30:49 +0000 (16:30 +0200)]
Remove Un_mono_sq

8 years agoRemove unneeded HOLCF classes
Joachim Breitner [Thu, 23 Sep 2010 14:28:13 +0000 (16:28 +0200)]
Remove unneeded HOLCF classes

8 years agoFinish to introduce custom approx relation
Joachim Breitner [Thu, 23 Sep 2010 14:24:22 +0000 (16:24 +0200)]
Finish to introduce custom approx relation

8 years agoStart to introduce custom approx relation
Joachim Breitner [Thu, 23 Sep 2010 10:19:57 +0000 (12:19 +0200)]
Start to introduce custom approx relation

8 years agoMove correctness proof into own theory
Joachim Breitner [Thu, 23 Sep 2010 09:18:23 +0000 (11:18 +0200)]
Move correctness proof into own theory

8 years agoRemove HOLCF prefix from theory names
Joachim Breitner [Thu, 23 Sep 2010 09:02:46 +0000 (11:02 +0200)]
Remove HOLCF prefix from theory names

8 years agoUse nice names in HOLCFExSV
Joachim Breitner [Thu, 23 Sep 2010 08:59:21 +0000 (10:59 +0200)]
Use nice names in HOLCFExSV

8 years agoDisambiguate all names
Joachim Breitner [Thu, 23 Sep 2010 08:55:54 +0000 (10:55 +0200)]
Disambiguate all names

8 years agoSeveral syntax beautifications
Joachim Breitner [Wed, 22 Sep 2010 15:11:30 +0000 (17:11 +0200)]
Several syntax beautifications

8 years agoNice Syntax in SetMap
Joachim Breitner [Wed, 22 Sep 2010 14:49:56 +0000 (16:49 +0200)]
Nice Syntax in SetMap

8 years agoIntroduce custom symbols
Joachim Breitner [Wed, 22 Sep 2010 14:11:06 +0000 (16:11 +0200)]
Introduce custom symbols

8 years agoIgnore dist/
Joachim Breitner [Wed, 22 Sep 2010 13:46:44 +0000 (15:46 +0200)]
Ignore dist/

8 years agoOverload abs using Adhoc_Overloading
Joachim Breitner [Wed, 22 Sep 2010 13:46:02 +0000 (15:46 +0200)]
Overload abs using Adhoc_Overloading

8 years agoCopy Adhoc_Overloading from Isabelle-devel
Joachim Breitner [Wed, 22 Sep 2010 13:45:38 +0000 (15:45 +0200)]
Copy Adhoc_Overloading from Isabelle-devel

8 years agoMake LaTeX preparation work
Joachim Breitner [Wed, 22 Sep 2010 13:27:58 +0000 (15:27 +0200)]
Make LaTeX preparation work

8 years agoUse nice |_| syntax for abs_*, but very slow
Joachim Breitner [Wed, 22 Sep 2010 13:14:26 +0000 (15:14 +0200)]
Use nice |_| syntax for abs_*, but very slow

8 years agoLemma 7 was already proven...
Joachim Breitner [Fri, 17 Sep 2010 14:09:34 +0000 (16:09 +0200)]
Lemma 7 was already proven...

8 years agoFinish Proof of lemma89 and of lemma6
Joachim Breitner [Fri, 17 Sep 2010 14:05:51 +0000 (16:05 +0200)]
Finish Proof of lemma89 and of lemma6

8 years agoFinish App case
Joachim Breitner [Fri, 17 Sep 2010 10:51:29 +0000 (12:51 +0200)]
Finish App case

8 years agoUse option::discrete_cpo, work on App case
Joachim Breitner [Fri, 17 Sep 2010 10:17:37 +0000 (12:17 +0200)]
Use option::discrete_cpo, work on App case

8 years agoShow IF cases
Joachim Breitner [Thu, 16 Sep 2010 14:15:00 +0000 (16:15 +0200)]
Show IF cases

8 years agoMove Un_mono_sq to HOLCFUtils.thy
Joachim Breitner [Thu, 16 Sep 2010 13:51:04 +0000 (15:51 +0200)]
Move Un_mono_sq to HOLCFUtils.thy

8 years agoProof of Plus case
Joachim Breitner [Thu, 16 Sep 2010 13:49:33 +0000 (15:49 +0200)]
Proof of Plus case

8 years agoAdd isProc conditions to evalF
Joachim Breitner [Thu, 16 Sep 2010 13:31:45 +0000 (15:31 +0200)]
Add isProc conditions to evalF

8 years agoMove SetMap lemmas in own theory
Joachim Breitner [Thu, 16 Sep 2010 12:36:15 +0000 (14:36 +0200)]
Move SetMap lemmas in own theory

8 years agoMinor cleanup
Joachim Breitner [Thu, 16 Sep 2010 12:31:46 +0000 (14:31 +0200)]
Minor cleanup

8 years agoProve continuity of abs_ccache
Joachim Breitner [Thu, 16 Sep 2010 12:30:37 +0000 (14:30 +0200)]
Prove continuity of abs_ccache

8 years agoFinish first case of lemma8+9
Joachim Breitner [Thu, 16 Sep 2010 11:54:09 +0000 (13:54 +0200)]
Finish first case of lemma8+9

8 years agoWork on first case of lemma8+9
Joachim Breitner [Wed, 15 Sep 2010 14:52:53 +0000 (16:52 +0200)]
Work on first case of lemma8+9

8 years agoList_Cpo by Brian Huffmann
Joachim Breitner [Wed, 15 Sep 2010 13:14:49 +0000 (15:14 +0200)]
List_Cpo by Brian Huffmann

8 years agoPrepare proof structure of main proof
Joachim Breitner [Wed, 15 Sep 2010 13:14:36 +0000 (15:14 +0200)]
Prepare proof structure of main proof

8 years agoRedo custom case rule, no split necessary any more
Joachim Breitner [Wed, 15 Sep 2010 11:47:07 +0000 (13:47 +0200)]
Redo custom case rule, no split necessary any more

8 years agoPrepare main proof
Joachim Breitner [Tue, 14 Sep 2010 14:59:20 +0000 (16:59 +0200)]
Prepare main proof

8 years agoProve lemma7 of Shivers
Joachim Breitner [Tue, 14 Sep 2010 13:58:35 +0000 (15:58 +0200)]
Prove lemma7 of Shivers

8 years agoIntroduce functions for set-valued maps
Joachim Breitner [Tue, 14 Sep 2010 13:10:28 +0000 (15:10 +0200)]
Introduce functions for set-valued maps

8 years agoGet abstract venv right
Joachim Breitner [Tue, 14 Sep 2010 13:00:15 +0000 (15:00 +0200)]
Get abstract venv right

8 years agoAbstraction functions
Joachim Breitner [Tue, 14 Sep 2010 12:27:19 +0000 (14:27 +0200)]
Abstraction functions

8 years agoEvalCPS in HOLCFAbsCF definiert
Joachim Breitner [Tue, 14 Sep 2010 10:02:42 +0000 (12:02 +0200)]
EvalCPS in HOLCFAbsCF definiert

8 years agoEvalF and EvalC in HOLCFAbsCF definiert
Joachim Breitner [Tue, 14 Sep 2010 09:57:45 +0000 (11:57 +0200)]
EvalF and EvalC in HOLCFAbsCF definiert

8 years agoContinuity of Union
Joachim Breitner [Tue, 14 Sep 2010 09:54:28 +0000 (11:54 +0200)]
Continuity of Union

8 years agoAnfänge von HOLCFAbsCF
Joachim Breitner [Tue, 14 Sep 2010 08:26:12 +0000 (10:26 +0200)]
Anfänge von HOLCFAbsCF

8 years agoFix proof single_valued evalCPS
Joachim Breitner [Mon, 13 Sep 2010 16:18:19 +0000 (18:18 +0200)]
Fix proof single_valued evalCPS

8 years agoSpeed up with auto after cases
Joachim Breitner [Mon, 13 Sep 2010 16:15:43 +0000 (18:15 +0200)]
Speed up with auto after cases

8 years agoMove Single-Valued-Proof in own file
Joachim Breitner [Mon, 13 Sep 2010 14:18:28 +0000 (16:18 +0200)]
Move Single-Valued-Proof in own file

8 years agoCombined induction statements (100 LOC less!)
Joachim Breitner [Mon, 13 Sep 2010 14:11:58 +0000 (16:11 +0200)]
Combined induction statements (100 LOC less!)

8 years agoAdd less_imp_le to intro, do not name explicitly everywhere
Joachim Breitner [Mon, 13 Sep 2010 10:22:32 +0000 (12:22 +0200)]
Add less_imp_le to intro, do not name explicitly everywhere

8 years agoReplace contour by abstract type, introduce nb
Joachim Breitner [Mon, 13 Sep 2010 09:39:39 +0000 (11:39 +0200)]
Replace contour by abstract type, introduce nb

8 years agoUse named ruls in induction
Joachim Breitner [Fri, 10 Sep 2010 13:22:16 +0000 (15:22 +0200)]
Use named ruls in induction

8 years agoWende fstate_case an (2. Fall)
Joachim Breitner [Fri, 10 Sep 2010 12:14:01 +0000 (14:14 +0200)]
Wende fstate_case an (2. Fall)

8 years agoUndo single induction rule try
Joachim Breitner [Fri, 10 Sep 2010 11:41:30 +0000 (13:41 +0200)]
Undo single induction rule try