Mercurial Mercurial > hg > nominal2 / 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.
Nominal/Ex/TestMorePerm.thy
author Christian Urban <urbanc@in.tum.de>
Sun, 02 May 2010 16:02:27 +0100 (2010-05-02)
changeset 2011 12ce87b55f97
parent 1793 33f7201a0239
child 2082 0854af516f14
permissions -rw-r--r--
tried to add some comments in the huge(!) nominal2_cmd function
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1595
aeed597d2043 Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset 
     1
 
theory TestMorePerm
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1595
diff changeset 
     2
 
imports "../Parser"
1595
aeed597d2043 Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset 
     3
 
begin
aeed597d2043 Move examples which create more permutations out
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset 
     4
 







1793






33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




     5


text {* 













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




     6


  "Weirdo" example from Peter Sewell's bestiary. 













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




     7














33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




     8


  In case of deep binders, it is not coverd by our 













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




     9


  approach of defining alpha-equivalence with a 













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    10


  single permutation.













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    11














33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    12


  Check whether it works with shallow binders as













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    13


  defined below.








1595






aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    14









1793






33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    15


*}













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    16


ML {* val _ = cheat_equivp := true *}













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    17














33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    18


atom_decl name













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    19














33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    20


nominal_datatype foo =













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    21


  Foo_var "name"













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    22


| Foo_pair "foo" "foo" 













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    23


| Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo"













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    24


    bind x in p1, bind x in p2, 













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    25


    bind y in p2, bind y in p3













33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    26














33f7201a0239
check whether the "weirdo" example from the binding bestiary works with shallow binders



Christian Urban <urbanc@in.tum.de>


parents: 
1792

diff
changeset




    27


thm alpha_foo_raw.intros[no_vars]








1595






aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    28














aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    29


thm permute_weird_raw.simps[no_vars]













aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    30


thm alpha_weird_raw.intros[no_vars]













aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    31


thm fv_weird_raw.simps[no_vars]













aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    32














aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    33














aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    34


end













aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    35














aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    36














aeed597d2043
Move examples which create more permutations out



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 

diff
changeset




    37
















nominal2