Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/ex/Fix2.thy
author blanchet
Mon, 19 Apr 2010 18:14:45 +0200
changeset 36230 43d10a494c91
parent 35174 e15040ae75d7
child 40002 c5b5f7a3a3b1
permissions -rw-r--r--
added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset 
     1
 
(*  Title:      HOLCF/ex/Fix2.thy
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset 
     2
 
    Author:     Franz Regensburger
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset 
     3
 







17291






94f6113fe9ed
converted to Isar theory format;



wenzelm


parents: 
14981

diff
changeset




     4


Show that fix is the unique least fixed-point operator.








12036





wenzelm


parents: 
10835

diff
changeset




     5


From axioms gix1_def,gix2_def it follows that fix = gix








1274






ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     6


*)













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     7









17291






94f6113fe9ed
converted to Isar theory format;



wenzelm


parents: 
14981

diff
changeset




     8


theory Fix2













94f6113fe9ed
converted to Isar theory format;



wenzelm


parents: 
14981

diff
changeset




     9


imports HOLCF













94f6113fe9ed
converted to Isar theory format;



wenzelm


parents: 
14981

diff
changeset




    10


begin








1274






ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    11









25135






4f8176c940cf
modernized specifications ('definition', 'axiomatization');



wenzelm


parents: 
19742

diff
changeset




    12


axiomatization













4f8176c940cf
modernized specifications ('definition', 'axiomatization');



wenzelm


parents: 
19742

diff
changeset




    13


  gix :: "('a->'a)->'a" where













4f8176c940cf
modernized specifications ('definition', 'axiomatization');



wenzelm


parents: 
19742

diff
changeset




    14


  gix1_def: "F$(gix$F) = gix$F" and








17291






94f6113fe9ed
converted to Isar theory format;



wenzelm


parents: 
14981

diff
changeset




    15


  gix2_def: "F$y=y ==> gix$F << y"








1274






ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    16









19742






86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    17














86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    18


lemma lemma1: "fix = gix"













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    19


apply (rule ext_cfun)













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    20


apply (rule antisym_less)













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    21


apply (rule fix_least)













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    22


apply (rule gix1_def)













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    23


apply (rule gix2_def)













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    24


apply (rule fix_eq [symmetric])













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    25


done













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    26














86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    27


lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))"













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    28


apply (rule lemma1 [THEN subst])













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    29


apply (rule fix_def2)













86f21beabafc
removed legacy ML scripts;



wenzelm


parents: 
17291

diff
changeset




    30


done








1274






ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    31














ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    32


end















isabelle