| author | Christian Urban <urbanc@in.tum.de> |
| Mon, 06 Dec 2010 14:24:17 +0000 | |
| changeset 2593 | 25dcb2b1329e |
| parent 2481 | 3a5ebb2fcdbf |
| child 2594 | 515e5496171c |
| permissions | -rw-r--r-- |
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
1 |
theory Multi_Recs2 |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2440
diff
changeset
|
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 |
|
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
5 |
(* |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
6 |
multiple recursive binders - multiple letrecs with multiple |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
7 |
clauses for each functions |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
8 |
|
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
9 |
example 8 from Peter Sewell's bestiary (originally due |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
10 |
to James Cheney) |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
11 |
|
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
12 |
*) |
|
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
|
13 |
|
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
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
|
15 |
|
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
16 |
nominal_datatype fun_recs: exp = |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
17 |
Var name |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
18 |
| Unit |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
19 |
| Pair exp exp |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
20 |
| LetRec 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
|
21 |
and fnclause = |
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2120
diff
changeset
|
22 |
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
|
23 |
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
|
24 |
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
|
25 |
| ORs fnclause fnclauses |
| 1941 | 26 |
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
|
27 |
Clause fnclauses |
| 1941 | 28 |
and lrbs = |
29 |
Single lrb |
|
30 |
| More lrb lrbs |
|
31 |
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
|
32 |
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
|
33 |
| PUnit |
| 1941 | 34 |
| 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
|
35 |
binder |
| 1941 | 36 |
b_lrbs :: "lrbs \<Rightarrow> atom set" and |
37 |
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
|
38 |
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
|
39 |
b_fnclause :: "fnclause \<Rightarrow> atom set" and |
| 1941 | 40 |
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
|
41 |
where |
| 1941 | 42 |
"b_lrbs (Single l) = b_lrb l" |
43 |
| "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
|
44 |
| "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
|
45 |
| "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
|
46 |
| "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
|
47 |
| "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
|
48 |
| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
| 1941 | 49 |
| "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
50 |
| "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
|
51 |
|
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
52 |
|
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
53 |
|
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
54 |
thm fun_recs.perm_bn_alpha |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
55 |
thm fun_recs.perm_bn_simps |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
56 |
thm fun_recs.bn_finite |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
57 |
thm fun_recs.inducts |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
58 |
thm fun_recs.distinct |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
59 |
thm fun_recs.induct |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
60 |
thm fun_recs.inducts |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
61 |
thm fun_recs.exhaust |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
62 |
thm fun_recs.fv_defs |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
63 |
thm fun_recs.bn_defs |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
64 |
thm fun_recs.perm_simps |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
65 |
thm fun_recs.eq_iff |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
66 |
thm fun_recs.fv_bn_eqvt |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
67 |
thm fun_recs.size_eqvt |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
68 |
thm fun_recs.supports |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
69 |
thm fun_recs.fsupp |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
70 |
thm fun_recs.supp |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
71 |
|
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
72 |
term alpha_b_fnclause |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
73 |
term alpha_b_fnclauses |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
74 |
term alpha_b_lrb |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
75 |
term alpha_b_lrbs |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
76 |
term alpha_b_pat |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
77 |
|
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
78 |
term alpha_b_fnclause_raw |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
79 |
term alpha_b_fnclauses_raw |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
80 |
term alpha_b_lrb_raw |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
81 |
term alpha_b_lrbs_raw |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
82 |
term alpha_b_pat_raw |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
83 |
|
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
84 |
lemma uu1: |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
85 |
fixes as0::exp and as1::fnclause |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
86 |
shows "(\<lambda>x::exp. True) (as0::exp)" |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
87 |
and "alpha_b_fnclause as1 (permute_b_fnclause p as1)" |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
88 |
and "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)" |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
89 |
and "alpha_b_lrb as3 (permute_b_lrb p as3)" |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
90 |
and "alpha_b_lrbs as4 (permute_b_lrbs p as4)" |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
91 |
and "alpha_b_pat as5 (permute_b_pat p as5)" |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
92 |
apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts) |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
93 |
apply(simp_all) |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
94 |
apply(simp only: fun_recs.perm_bn_simps) |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
95 |
apply(simp only: fun_recs.eq_iff) |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
96 |
apply(simp) |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
97 |
oops |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
98 |
|
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
parents:
2481
diff
changeset
|
99 |
|
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
100 |
thm fun_recs.distinct |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
101 |
thm fun_recs.induct |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
102 |
thm fun_recs.inducts |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
103 |
thm fun_recs.exhaust |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
104 |
thm fun_recs.fv_defs |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
105 |
thm fun_recs.bn_defs |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
106 |
thm fun_recs.perm_simps |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
107 |
thm fun_recs.eq_iff |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
108 |
thm fun_recs.fv_bn_eqvt |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
109 |
thm fun_recs.size_eqvt |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
110 |
thm fun_recs.supports |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
111 |
thm fun_recs.fsupp |
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
parents:
2477
diff
changeset
|
112 |
thm fun_recs.supp |
|
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
113 |
|
|
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
|
114 |
|
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
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
|
116 |
|
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
117 |
|
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
118 |