1911
+ − 1
theory SingleLet
2474
+ − 2
imports "../Nominal2"
1596
+ − 3
begin
+ − 4
+ − 5
atom_decl name
+ − 6
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 7
nominal_datatype single_let: trm =
1911
+ − 8
Var "name"
+ − 9
| App "trm" "trm"
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 10
| Lam x::"name" t::"trm" bind x in t
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 11
| Let a::"assg" t::"trm" bind "bn a" in t
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>
diff
changeset
+ − 12
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
2296
+ − 13
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
2634
3ce1089cdbf3
changed res keyword to set+ for restrictions; comment by a referee
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 14
| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set+) x in t2
1911
+ − 15
and assg =
2320
+ − 16
As "name" x::"name" t::"trm" bind x in t
1596
+ − 17
binder
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 18
bn::"assg \<Rightarrow> atom list"
1596
+ − 19
where
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 20
"bn (As x y t) = [atom x]"
1911
+ − 21
2436
+ − 22
thm single_let.distinct
+ − 23
thm single_let.induct
2474
+ − 24
thm single_let.inducts
2622
+ − 25
thm single_let.exhaust
+ − 26
thm single_let.strong_exhaust
2436
+ − 27
thm single_let.fv_defs
+ − 28
thm single_let.bn_defs
+ − 29
thm single_let.perm_simps
+ − 30
thm single_let.eq_iff
+ − 31
thm single_let.fv_bn_eqvt
+ − 32
thm single_let.size_eqvt
2448
+ − 33
thm single_let.supports
2450
+ − 34
thm single_let.fsupp
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35
thm single_let.supp
2493
+ − 36
thm single_let.fresh
2461
+ − 37
2064
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38
1596
+ − 39
end
+ − 40
+ − 41
+ − 42