darcs-mirror-afp-Free-Groups.git
9 years agolangle/rangle for group span master
Joachim Breitner [Wed, 23 Jun 2010 10:45:03 +0000 (10:45 +0000)]
langle/rangle for group span

9 years agoNicer syntax for the Free Group
Joachim Breitner [Wed, 23 Jun 2010 10:38:43 +0000 (10:38 +0000)]
Nicer syntax for the Free Group

9 years agoFix LaTeX build
Joachim Breitner [Wed, 23 Jun 2010 09:58:26 +0000 (09:58 +0000)]
Fix LaTeX build

9 years agoProve that F_1 = \Z
Joachim Breitner [Wed, 23 Jun 2010 09:50:53 +0000 (09:50 +0000)]
Prove that F_1 = \Z

9 years agoShow that the Free Group over the empty set is the trivial group
Joachim Breitner [Mon, 21 Jun 2010 19:13:28 +0000 (19:13 +0000)]
Show that the Free Group over the empty set is the trivial group

9 years agoProve hom_span
Joachim Breitner [Fri, 18 Jun 2010 14:22:36 +0000 (14:22 +0000)]
Prove hom_span

9 years agoFinish universal property
Joachim Breitner [Thu, 17 Jun 2010 23:05:28 +0000 (23:05 +0000)]
Finish universal property

9 years agoRemove trivial lemmas
Joachim Breitner [Thu, 17 Jun 2010 00:06:18 +0000 (00:06 +0000)]
Remove trivial lemmas

9 years agoSkip one step
Joachim Breitner [Thu, 17 Jun 2010 00:02:35 +0000 (00:02 +0000)]
Skip one step

9 years agoDrop unnecessary condition
Joachim Breitner [Thu, 17 Jun 2010 00:00:16 +0000 (00:00 +0000)]
Drop unnecessary condition

9 years agoPut lift_cancels_to in a lemmy of its own
Joachim Breitner [Wed, 16 Jun 2010 23:55:04 +0000 (23:55 +0000)]
Put lift_cancels_to in a lemmy of its own

9 years agolift_is_hom
Joachim Breitner [Wed, 16 Jun 2010 23:49:24 +0000 (23:49 +0000)]
lift_is_hom
(Very ugly, I am not satisifed)

9 years agocancels_to_1_unfold: Alternative view on cancels_to_1
Joachim Breitner [Wed, 16 Jun 2010 23:48:34 +0000 (23:48 +0000)]
cancels_to_1_unfold: Alternative view on cancels_to_1

9 years agom_concat and lemmas about
Joachim Breitner [Wed, 16 Jun 2010 23:47:46 +0000 (23:47 +0000)]
m_concat and lemmas about

9 years agoBeginnings of the universal property
Joachim Breitner [Tue, 15 Jun 2010 22:51:26 +0000 (22:51 +0000)]
Beginnings of the universal property

9 years agoTheory Generators.thy
Joachim Breitner [Mon, 14 Jun 2010 21:51:55 +0000 (21:51 +0000)]
Theory Generators.thy

9 years agoDo not import List
Joachim Breitner [Tue, 1 Jun 2010 21:08:53 +0000 (21:08 +0000)]
Do not import List

9 years agoGive type annotation for free_group, makes Isabelle (and me) happier
Joachim Breitner [Sat, 29 May 2010 20:45:36 +0000 (20:45 +0000)]
Give type annotation for free_group, makes Isabelle (and me) happier

9 years agoEditorial skimming
Joachim Breitner [Fri, 28 May 2010 19:02:13 +0000 (19:02 +0000)]
Editorial skimming

9 years agoShow group homomorphism property
Joachim Breitner [Fri, 28 May 2010 18:15:45 +0000 (18:15 +0000)]
Show group homomorphism property

9 years agoNicer way of proving that something is a group isomorphism
Joachim Breitner [Fri, 28 May 2010 15:44:11 +0000 (15:44 +0000)]
Nicer way of proving that something is a group isomorphism

9 years agoFinish bijectivity of h
Joachim Breitner [Fri, 28 May 2010 14:34:06 +0000 (14:34 +0000)]
Finish bijectivity of h

9 years agoEnable quick_and_dirty-mode to work around Isabelle bug
Joachim Breitner [Fri, 28 May 2010 14:10:21 +0000 (14:10 +0000)]
Enable quick_and_dirty-mode to work around Isabelle bug

9 years agoTry to debug the obtain problem
Joachim Breitner [Fri, 28 May 2010 13:14:11 +0000 (13:14 +0000)]
Try to debug the obtain problem

9 years agoResults that cancelation commutes with renaming elements
Joachim Breitner [Fri, 28 May 2010 13:14:08 +0000 (13:14 +0000)]
Results that cancelation commutes with renaming elements

9 years agoUse rename_gens_canceled in inv_fg_closure1
Joachim Breitner [Fri, 28 May 2010 13:13:44 +0000 (13:13 +0000)]
Use rename_gens_canceled in inv_fg_closure1

9 years agoImplement inv1 with apfst
Joachim Breitner [Fri, 28 May 2010 09:39:30 +0000 (09:39 +0000)]
Implement inv1 with apfst

9 years agoStarted to prof that bijective sets produce isomorphic free groups
Joachim Breitner [Thu, 27 May 2010 21:22:56 +0000 (21:22 +0000)]
Started to prof that bijective sets produce isomorphic free groups

9 years agoDefine free_groups over a _set_ of generators
Joachim Breitner [Thu, 27 May 2010 15:14:52 +0000 (15:14 +0000)]
Define free_groups over a _set_ of generators

9 years agoRemove thm statement
Joachim Breitner [Thu, 27 May 2010 15:14:44 +0000 (15:14 +0000)]
Remove thm statement

9 years agoShow "occuring_generators (normalize l) ⊆ occuring_generators l"
Joachim Breitner [Thu, 27 May 2010 15:14:40 +0000 (15:14 +0000)]
Show "occuring_generators (normalize l) ⊆ occuring_generators l"

9 years agoLeverage unfolding
Joachim Breitner [Thu, 27 May 2010 09:50:33 +0000 (09:50 +0000)]
Leverage unfolding

9 years agoRename lconf to confluent_cancels_to_1
Joachim Breitner [Thu, 27 May 2010 09:15:47 +0000 (09:15 +0000)]
Rename lconf to confluent_cancels_to_1

9 years agoRemoved Andreas’ editorial remarks
Joachim Breitner [Thu, 27 May 2010 09:14:47 +0000 (09:14 +0000)]
Removed Andreas’ editorial remarks

9 years agoSome more cleanup by Andreas Lochbihler
Joachim Breitner [Thu, 27 May 2010 08:51:08 +0000 (08:51 +0000)]
Some more cleanup by Andreas Lochbihler

9 years agoSome cleanup by Daniel Wasserrab
Joachim Breitner [Tue, 25 May 2010 09:27:46 +0000 (09:27 +0000)]
Some cleanup by Daniel Wasserrab

9 years agoReformat free_group constdef
Joachim Breitner [Sat, 22 May 2010 22:42:37 +0000 (22:42 +0000)]
Reformat free_group constdef

9 years agoGet rid of free_group_set
Joachim Breitner [Sat, 22 May 2010 22:39:02 +0000 (22:39 +0000)]
Get rid of free_group_set

9 years agoGet rid of norm_mult
Joachim Breitner [Sat, 22 May 2010 22:14:53 +0000 (22:14 +0000)]
Get rid of norm_mult

9 years agoConverted to structured proofs
Joachim Breitner [Sat, 22 May 2010 22:07:27 +0000 (22:07 +0000)]
Converted to structured proofs

9 years agoInitial check-in
Joachim Breitner [Sat, 22 May 2010 10:27:09 +0000 (10:27 +0000)]
Initial check-in