1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory ExPS8
|
2454
|
2 |
imports "../Nominal2"
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
(* example 8 from Peter Sewell's bestiary *)
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
atom_decl name
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
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 |
declare [[STEPS = 31]]
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
|
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
|
11 |
nominal_datatype fun_pats: exp =
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
EVar name
|
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
|
13 |
| EUnit
|
1941
|
14 |
| EPair exp exp
|
2436
|
15 |
| ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
and fnclause =
|
2436
|
17 |
K x::name p::pat f::exp bind (set) "b_pat p" in f
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
and fnclauses =
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
S fnclause
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
| ORs fnclause fnclauses
|
1941
|
21 |
and lrb =
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
Clause fnclauses
|
1941
|
23 |
and lrbs =
|
|
24 |
Single lrb
|
|
25 |
| More lrb lrbs
|
|
26 |
and pat =
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
PVar name
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
| PUnit
|
1941
|
29 |
| PPair pat pat
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
binder
|
1941
|
31 |
b_lrbs :: "lrbs \<Rightarrow> atom set" and
|
|
32 |
b_pat :: "pat \<Rightarrow> atom set" and
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
b_fnclause :: "fnclause \<Rightarrow> atom set" and
|
1941
|
35 |
b_lrb :: "lrb \<Rightarrow> atom set"
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
where
|
1941
|
37 |
"b_lrbs (Single l) = b_lrb l"
|
|
38 |
| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
| "b_pat (PVar x) = {atom x}"
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
| "b_pat (PUnit) = {}"
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
| "b_fnclauses (S fc) = (b_fnclause fc)"
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
|
1941
|
44 |
| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
|
|
45 |
| "b_fnclause (K x pat exp) = {atom x}"
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
|
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
|
47 |
thm fun_pats.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
|
48 |
thm fun_pats.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
|
49 |
thm fun_pats.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
|
50 |
thm fun_pats.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
|
51 |
thm fun_pats.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
|
52 |
thm fun_pats.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
|
53 |
thm fun_pats.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
|
54 |
thm fun_pats.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
|
55 |
thm fun_pats.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
|
56 |
thm fun_pats.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
|
57 |
thm fun_pats.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
|
58 |
thm fun_pats.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
|
59 |
thm fun_pats.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
|
60 |
|
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
|
61 |
|
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
|
62 |
ML {*
|
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
|
63 |
fun add_ss thms =
|
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
|
64 |
HOL_basic_ss addsimps thms
|
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
|
65 |
|
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
|
66 |
fun symmetric thms =
|
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
|
67 |
map (fn thm => thm RS @{thm sym}) thms
|
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
|
68 |
*}
|
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
|
69 |
|
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
|
70 |
lemma
|
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
|
71 |
"(fv_exp x = supp x) \<and>
|
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
|
72 |
(fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and>
|
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
|
73 |
(fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and>
|
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
|
74 |
(fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and>
|
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
|
75 |
(fv_lrbs xd = supp xd \<and> fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \<and>
|
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
|
76 |
(fv_pat xe = supp xe \<and> fv_b_pat xe = supp_rel alpha_b_pat xe)"
|
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
|
77 |
apply(rule fun_pats.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
|
78 |
apply(tactic {* ALLGOALS (TRY o rtac @{thm conjI})*})
|
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
|
79 |
thm fun_pats.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
|
80 |
oops
|
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
|
81 |
|
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
|
82 |
|
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
|
83 |
lemma
|
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
|
84 |
"fv_exp x = supp x" and
|
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
|
85 |
"fv_fnclause y = supp y" and
|
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
|
86 |
"fv_fnclauses xb = supp xb" and
|
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
|
87 |
"fv_lrb xc = supp xc" and
|
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
|
88 |
"fv_lrbs xd = supp xd" and
|
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
|
89 |
"fv_pat xe = supp xe" and
|
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
|
90 |
"fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and
|
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
|
91 |
"fv_b_pat xe = supp_rel alpha_b_pat xe" and
|
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
|
92 |
"fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and
|
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
|
93 |
"fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and
|
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
|
94 |
"fv_b_lrb y = supp_rel alpha_b_lrb y"
|
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
|
95 |
apply(induct "x::exp" and "y::fnclause" and xb and xc and xd and xe rule: fun_pats.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
|
96 |
thm fun_pats.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
|
97 |
oops
|
1655
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
end
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
100 |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
101 |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
102 |
|