|
2454
|
1 |
theory LetFun
|
|
|
2 |
imports "../Nominal2"
|
|
|
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 |
(* x is bound in both e1 and e2;
|
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
|
8 |
bp-names in p are bound only in e1
|
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 |
*)
|
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
|
10 |
|
|
2454
|
11 |
|
|
|
12 |
nominal_datatype exp =
|
|
|
13 |
Var name
|
|
|
14 |
| Pair exp exp
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
| LetRec x::name p::pat e1::exp e2::exp binds x in e2, binds x "bp p" in e1
|
|
2454
|
16 |
and pat =
|
|
|
17 |
PVar name
|
|
|
18 |
| PUnit
|
|
|
19 |
| PPair pat pat
|
|
|
20 |
binder
|
|
|
21 |
bp :: "pat \<Rightarrow> atom list"
|
|
|
22 |
where
|
|
|
23 |
"bp (PVar x) = [atom x]"
|
|
|
24 |
| "bp (PUnit) = []"
|
|
|
25 |
| "bp (PPair p1 p2) = bp p1 @ bp p2"
|
|
|
26 |
|
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
|
27 |
thm exp_pat.distinct
|
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
|
28 |
thm exp_pat.induct
|
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
|
29 |
thm exp_pat.inducts
|
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
|
30 |
thm exp_pat.exhaust
|
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
|
31 |
thm exp_pat.fv_defs
|
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
|
32 |
thm exp_pat.bn_defs
|
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
|
33 |
thm exp_pat.perm_simps
|
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
|
34 |
thm exp_pat.eq_iff
|
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 exp_pat.fv_bn_eqvt
|
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
|
36 |
thm exp_pat.size_eqvt
|
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
|
37 |
thm exp_pat.supports
|
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 exp_pat.fsupp
|
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
|
39 |
thm exp_pat.supp
|
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
|
40 |
|
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
|
41 |
|
|
2454
|
42 |
end |