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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

9 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

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

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

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

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

9 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

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

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

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

9 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

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

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

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

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

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

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

9 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)

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

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

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

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

9 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

9 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)

9 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

9 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

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

9 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

9 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

9 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

9 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

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

9 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)

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

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

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

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

9 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

9 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

9 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

9 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

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

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

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

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

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

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

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

9 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

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

9 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

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

9 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

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

9 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

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

9 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

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

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

9 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

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

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

9 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

9 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

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

9 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

9 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

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

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

9 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

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

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

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

9 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

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

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

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

9 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

9 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

9 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!)

9 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

9 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

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

9 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)

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