Nominal/Ex/SingleLet.thy
author Christian Urban <urbanc@in.tum.de>
Wed, 25 Aug 2010 09:02:06 +0800
changeset 2431 331873ebc5cd
parent 2430 a746d49b0240
child 2434 92dc6cfa3a95
permissions -rw-r--r--
can now deal with type variables in nominal datatype definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
     1
theory SingleLet
2024
d974059827ad Equivariance fails for single let?
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1911
diff changeset
     2
imports "../NewParser"
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
atom_decl name
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
     7
declare [[STEPS = 20]]
2294
72ad4e766acf properly exported bn_descr
Christian Urban <urbanc@in.tum.de>
parents: 2293
diff changeset
     8
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
     9
nominal_datatype singlelet: trm  =
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    10
  Var "name"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    11
| App "trm" "trm"
2424
621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
parents: 2410
diff changeset
    12
| Lam x::"name" t::"trm"  bind x in t
621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
parents: 2410
diff changeset
    13
| Let a::"assg" t::"trm"  bind (set) "bn a" in t
621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
parents: 2410
diff changeset
    14
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
2296
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
    15
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
2316
08bbde090a17 also symmetry
Christian Urban <urbanc@in.tum.de>
parents: 2313
diff changeset
    16
| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    17
and assg =
2320
d835a2771608 prove that alpha implies alpha_bn (needed for rsp proofs)
Christian Urban <urbanc@in.tum.de>
parents: 2318
diff changeset
    18
  As "name" x::"name" t::"trm" bind x in t
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
binder
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    20
  bn::"assg \<Rightarrow> atom set"
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
where
2320
d835a2771608 prove that alpha implies alpha_bn (needed for rsp proofs)
Christian Urban <urbanc@in.tum.de>
parents: 2318
diff changeset
    22
  "bn (As x y t) = {atom x}"
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    23
2410
2bbdb9c427b5 improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2409
diff changeset
    24
2409
83990a42a068 more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 2407
diff changeset
    25
text {* can lift *}
2401
7645e18e8b19 modified the code for class instantiations (with help from Florian)
Christian Urban <urbanc@in.tum.de>
parents: 2400
diff changeset
    26
2397
c670a849af65 more experiments with lifting
Christian Urban <urbanc@in.tum.de>
parents: 2395
diff changeset
    27
thm distinct
c670a849af65 more experiments with lifting
Christian Urban <urbanc@in.tum.de>
parents: 2395
diff changeset
    28
thm trm_raw_assg_raw.inducts
2407
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2406
diff changeset
    29
thm trm_raw.exhaust
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2406
diff changeset
    30
thm assg_raw.exhaust
2424
621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
parents: 2410
diff changeset
    31
thm fv_defs
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
    32
thm bn_defs
2384
841b7e34e70a fixed order of fold_union to make alpha and fv agree
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    33
thm perm_simps
841b7e34e70a fixed order of fold_union to make alpha and fv agree
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    34
thm perm_laws
2397
c670a849af65 more experiments with lifting
Christian Urban <urbanc@in.tum.de>
parents: 2395
diff changeset
    35
thm trm_raw_assg_raw.size(9 - 16)
2398
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2397
diff changeset
    36
thm eq_iff
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2397
diff changeset
    37
thm eq_iff_simps
2406
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    38
thm bn_defs
2424
621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
parents: 2410
diff changeset
    39
thm fv_eqvt
2406
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    40
thm bn_eqvt
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    41
thm size_eqvt
2405
29ebbe56f450 also able to lift the bn_defs
Christian Urban <urbanc@in.tum.de>
parents: 2404
diff changeset
    42
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    43
2398
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2397
diff changeset
    44
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    45
  val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct})
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    46
*}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    47
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    48
ML {* 
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    49
  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw_assg_raw.inducts}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    50
*}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    51
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    52
ML {* 
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    53
  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw.exhaust}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    54
*}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    55
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    56
ML {* 
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    57
  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms assg_raw.exhaust}
2407
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2406
diff changeset
    58
*}
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2406
diff changeset
    59
2398
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2397
diff changeset
    60
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    61
  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_defs}
2428
58e60df1ff79 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2424
diff changeset
    62
*}
58e60df1ff79 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2424
diff changeset
    63
58e60df1ff79 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2424
diff changeset
    64
ML {* 
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    65
  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw_assg_raw.size(9 - 16)}
2398
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2397
diff changeset
    66
*}
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2397
diff changeset
    67
2402
80db544a37ea pinpointed the problem
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
    68
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    69
  val thms_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_simps}
2428
58e60df1ff79 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2424
diff changeset
    70
*}
58e60df1ff79 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2424
diff changeset
    71
58e60df1ff79 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2424
diff changeset
    72
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    73
  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_laws}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    74
*}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    75
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    76
ML {*
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    77
  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    78
    prod.cases}
2402
80db544a37ea pinpointed the problem
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
    79
*}
2397
c670a849af65 more experiments with lifting
Christian Urban <urbanc@in.tum.de>
parents: 2395
diff changeset
    80
2405
29ebbe56f450 also able to lift the bn_defs
Christian Urban <urbanc@in.tum.de>
parents: 2404
diff changeset
    81
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    82
 val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps)  @{thms eq_iff}
2405
29ebbe56f450 also able to lift the bn_defs
Christian Urban <urbanc@in.tum.de>
parents: 2404
diff changeset
    83
*}
2397
c670a849af65 more experiments with lifting
Christian Urban <urbanc@in.tum.de>
parents: 2395
diff changeset
    84
2405
29ebbe56f450 also able to lift the bn_defs
Christian Urban <urbanc@in.tum.de>
parents: 2404
diff changeset
    85
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    86
 val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps) @{thms eq_iff_simps}
2405
29ebbe56f450 also able to lift the bn_defs
Christian Urban <urbanc@in.tum.de>
parents: 2404
diff changeset
    87
*}
2361
d73d4d151cce more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2359
diff changeset
    88
2406
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    89
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    90
  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_defs}
2406
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    91
*}
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    92
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    93
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    94
  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_eqvt}
2406
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    95
*}
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    96
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
    97
ML {*
2430
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    98
  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_eqvt}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
    99
*}
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
   100
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
   101
ML {*
a746d49b0240 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 2428
diff changeset
   102
  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms size_eqvt}
2406
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
   103
*}
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
   104
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
   105
428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
parents: 2405
diff changeset
   106
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   107
2361
d73d4d151cce more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2359
diff changeset
   108
lemma supp_fv:
d73d4d151cce more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2359
diff changeset
   109
  "supp t = fv_trm t"
d73d4d151cce more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2359
diff changeset
   110
  "supp b = fv_bn b"
d73d4d151cce more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2359
diff changeset
   111
apply(induct t and b rule: i1)
d73d4d151cce more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2359
diff changeset
   112
apply(simp_all add: f1)
d73d4d151cce more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2359
diff changeset
   113
apply(simp_all add: supp_def)
2365
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   114
apply(simp_all add: b1)
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   115
sorry
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   116
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   117
consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   118
consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   119
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   120
lemma y:
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   121
  "perm_bn_trm p (Var x) = (Var x)"
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   122
  "perm_bn_trm p (App t1 t2) = (App t1 t2)"
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   123
  "perm_bn_trm p ("
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   124
Christian Urban <urbanc@in.tum.de>
parents: 2361
diff changeset
   125
2361
d73d4d151cce more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2359
diff changeset
   126
2336
f2d545b77b31 added definition of the quotient types
Christian Urban <urbanc@in.tum.de>
parents: 2330
diff changeset
   127
typ trm
f2d545b77b31 added definition of the quotient types
Christian Urban <urbanc@in.tum.de>
parents: 2330
diff changeset
   128
typ assg
f2d545b77b31 added definition of the quotient types
Christian Urban <urbanc@in.tum.de>
parents: 2330
diff changeset
   129
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
   130
thm trm_assg.fv
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
   131
thm trm_assg.supp
2024
d974059827ad Equivariance fails for single let?
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1911
diff changeset
   132
thm trm_assg.eq_iff
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
   133
thm trm_assg.bn
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
   134
thm trm_assg.perm
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
   135
thm trm_assg.induct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
   136
thm trm_assg.inducts
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
   137
thm trm_assg.distinct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
   138
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
2024
d974059827ad Equivariance fails for single let?
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1911
diff changeset
   139
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents: 2146
diff changeset
   140
(* TEMPORARY
2024
d974059827ad Equivariance fails for single let?
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1911
diff changeset
   141
thm trm_assg.fv[simplified trm_assg.supp(1-2)]
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents: 2146
diff changeset
   142
*)
2064
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
parents: 2028
diff changeset
   143
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   144
end
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   145
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   146
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   147