1911
+ − 1
theory SingleLet
2474
+ − 2
imports "../Nominal2"
1596
+ − 3
begin
+ − 4
+ − 5
atom_decl name
+ − 6
2436
+ − 7
declare [[STEPS = 100]]
2294
+ − 8
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
+ − 9
nominal_datatype single_let: trm =
1911
+ − 10
Var "name"
+ − 11
| 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
+ − 12
| 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
+ − 13
| 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
+ − 14
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
2296
+ − 15
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
2493
+ − 16
| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2
1911
+ − 17
and assg =
2320
+ − 18
As "name" x::"name" t::"trm" bind x in t
1596
+ − 19
binder
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::"assg \<Rightarrow> atom list"
1596
+ − 21
where
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22
"bn (As x y t) = [atom x]"
1911
+ − 23
2493
+ − 24
+ − 25
2436
+ − 26
thm single_let.distinct
+ − 27
thm single_let.induct
2474
+ − 28
thm single_let.inducts
2436
+ − 29
thm single_let.exhaust
+ − 30
thm single_let.fv_defs
+ − 31
thm single_let.bn_defs
+ − 32
thm single_let.perm_simps
+ − 33
thm single_let.eq_iff
+ − 34
thm single_let.fv_bn_eqvt
+ − 35
thm single_let.size_eqvt
2448
+ − 36
thm single_let.supports
2450
+ − 37
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
+ − 38
thm single_let.supp
2493
+ − 39
thm single_let.fresh
2461
+ − 40
2064
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
1596
+ − 42
end
+ − 43
+ − 44
+ − 45