Nominal/Ex/TypeVarsTest.thy
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 09 Jul 2015 02:32:46 +0100 (2015-07-09)
changeset 3239 67370521c09c
parent 3228 040519ec99e9
child 3240 f80fa0d18d81
permissions -rw-r--r--
updated for Isabelle 2015
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory TypeVarsTest
2454
9ffee4eb1ae1 renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents: 2440
diff changeset
     2
imports "../Nominal2" 
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
3239
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
     5
atom_decl var
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
     6
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
     7
ML {* trace := true *}
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
     8
declare [[ML_print_depth = 1000]]
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
     9
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    10
nominal_datatype exp =
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    11
          Var var
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    12
        | App exp var
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    13
        | LetA as::assn body::exp binds "bn as" in "body" "as"
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    14
        | Lam x::var body::exp binds x in body
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    15
        and assn =
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    16
          ANil | ACons var exp assn
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    17
        binder
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    18
          bn
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    19
        where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    20
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    21
nominal_datatype ('ann::fs) exp2 =
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    22
  Var var
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    23
| App "'ann exp2" var
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    24
| LetA as::"'ann assn2" body::"'ann exp2" binds "bnn as" in body as
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    25
| Lam x::var body::"'ann exp2" binds x in body
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    26
and ('ann::fs) assn2 =
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    27
  ANil 
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    28
| ACons var "'ann exp2" 'ann "'ann assn2"
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    29
binder
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    30
  bnn :: "('ann::fs) assn2 \<Rightarrow> atom list"
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    31
where 
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    32
  "bnn ANil = []" 
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    33
| "bnn (ACons x a t as) = (atom x) # (bnn as)"
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    34
67370521c09c updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3228
diff changeset
    35
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    36
(* a nominal datatype with type variables and sorts *)
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    37
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    38
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    39
(* the sort constraints need to be attached to the  *)
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    40
(* first occurence of the type variables on the     *)
2622
e6e6a3da81aa tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2617
diff changeset
    41
(* right-hand side                                  *)
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    42
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
atom_decl name
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
class s1
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
class s2
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
2571
f0252365936c proved that bn functions return a finite set
Christian Urban <urbanc@in.tum.de>
parents: 2557
diff changeset
    48
instance nat :: s1 ..
f0252365936c proved that bn functions return a finite set
Christian Urban <urbanc@in.tum.de>
parents: 2557
diff changeset
    49
instance int :: s2 .. 
f0252365936c proved that bn functions return a finite set
Christian Urban <urbanc@in.tum.de>
parents: 2557
diff changeset
    50
3091
578e0265b235 the default sort for type-variables in nominal specifications is fs; it is automatically addded
Christian Urban <urbanc@in.tum.de>
parents: 3065
diff changeset
    51
nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
  Var "name"
3065
51ef8a3cb6ef updated to lates changes in the datatype package
Christian Urban <urbanc@in.tum.de>
parents: 3029
diff changeset
    53
| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2888
diff changeset
    54
| Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    55
| Foo "'a" "'b"
2950
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents: 2888
diff changeset
    56
| Bar x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    57
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    58
term Foo
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    59
term Bar
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
3228
040519ec99e9 fixed bug with support and freshness lemmas not being simplified properly
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3091
diff changeset
    61
thm lam.supp lam.fresh
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
thm lam.distinct
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
thm lam.induct
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    64
thm lam.exhaust 
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2571
diff changeset
    65
thm lam.strong_exhaust
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
thm lam.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
thm lam.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
thm lam.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
thm lam.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
thm lam.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
thm lam.size_eqvt
2557
781fbc8c0591 fixed locally the problem with the function package; all tests work again
Christian Urban <urbanc@in.tum.de>
parents: 2556
diff changeset
    72
2730
eebc24b9cf39 added a lemma about fresh_star and Abs
Christian Urban <urbanc@in.tum.de>
parents: 2622
diff changeset
    73
2888
eda5aeb056a6 fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
parents: 2730
diff changeset
    74
nominal_datatype ('alpha, 'beta, 'gamma) psi =
2730
eebc24b9cf39 added a lemma about fresh_star and Abs
Christian Urban <urbanc@in.tum.de>
parents: 2622
diff changeset
    75
  PsiNil
3091
578e0265b235 the default sort for type-variables in nominal specifications is fs; it is automatically addded
Christian Urban <urbanc@in.tum.de>
parents: 3065
diff changeset
    76
| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
2730
eebc24b9cf39 added a lemma about fresh_star and Abs
Christian Urban <urbanc@in.tum.de>
parents: 2622
diff changeset
    77
3228
040519ec99e9 fixed bug with support and freshness lemmas not being simplified properly
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3091
diff changeset
    78
thm psi.supp psi.fresh
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
3029
6fd3fc3254ee deleted PNil
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    80
nominal_datatype 'a foo = 
3091
578e0265b235 the default sort for type-variables in nominal specifications is fs; it is automatically addded
Christian Urban <urbanc@in.tum.de>
parents: 3065
diff changeset
    81
  Node x::"name" f::"'a foo" binds x in f
3029
6fd3fc3254ee deleted PNil
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    82
| Leaf "'a"
6fd3fc3254ee deleted PNil
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    83
6fd3fc3254ee deleted PNil
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    84
term "Leaf"
6fd3fc3254ee deleted PNil
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    85
6fd3fc3254ee deleted PNil
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    86
6fd3fc3254ee deleted PNil
Christian Urban <urbanc@in.tum.de>
parents: 2950
diff changeset
    87
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
end
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91