2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1 |
theory Multi_Recs2
|
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 |
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
diff
changeset
|
19 |
| 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
|
20 |
| LetRec l::lrbs e::exp binds (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 =
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
K x::name p::pat f::exp binds (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>
diff
changeset
|
52 |
|
2598
|
53 |
thm fun_recs.permute_bn
|
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
diff
changeset
|
71 |
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
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>
diff
changeset
|
73 |
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>
diff
changeset
|
74 |
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>
diff
changeset
|
75 |
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>
diff
changeset
|
76 |
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>
diff
changeset
|
77 |
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>
diff
changeset
|
78 |
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>
diff
changeset
|
79 |
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>
diff
changeset
|
80 |
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>
diff
changeset
|
81 |
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>
diff
changeset
|
82 |
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>
diff
changeset
|
83 |
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>
diff
changeset
|
84 |
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>
diff
changeset
|
85 |
|
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
86 |
lemma
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
87 |
fixes c::"'a::fs"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
88 |
assumes "\<And>name c. P1 c (Var name)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
89 |
and "\<And>c. P1 c Unit"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
90 |
and "\<And>exp1 exp2 c. \<lbrakk>\<And>c. P1 c exp1; \<And>c. P1 c exp2\<rbrakk> \<Longrightarrow> P1 c (Multi_Recs2.Pair exp1 exp2)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
91 |
and "\<And>lrbs exp c. \<lbrakk>b_lrbs lrbs \<sharp>* c; \<And>c. P5 c lrbs; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P1 c (LetRec lrbs exp)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
92 |
and "\<And>name pat exp c. \<lbrakk>b_pat pat \<sharp>* c; \<And>c. P6 c pat; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P2 c (K name pat exp)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
93 |
and "\<And>fnclause c. (\<And>c. P2 c fnclause) \<Longrightarrow> P3 c (S fnclause)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
94 |
and "\<And>fnclause fnclauses c. \<lbrakk>\<And>c. P2 c fnclause; \<And>c. P3 c fnclauses\<rbrakk> \<Longrightarrow>
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
95 |
P3 c (ORs fnclause fnclauses)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
96 |
and "\<And>fnclauses c. (\<And>c. P3 c fnclauses) \<Longrightarrow> P4 c (Clause fnclauses)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
97 |
and "\<And>lrb c. (\<And>c. P4 c lrb) \<Longrightarrow> P5 c (Single lrb)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
98 |
and "\<And>lrb lrbs c. \<lbrakk>\<And>c. P4 c lrb; \<And>c. P5 c lrbs\<rbrakk> \<Longrightarrow> P5 c (More lrb lrbs)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
99 |
and "\<And>name c. P6 c (PVar name)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
100 |
and "\<And>c. P6 c PUnit"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
102 |
shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat"
|
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
103 |
apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
|
2630
|
104 |
apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))
|
|
105 |
apply(simp_all)[4]
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
106 |
apply(blast)
|
2630
|
107 |
apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
108 |
apply(blast)
|
2630
|
109 |
apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
apply(blast)
|
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
apply(blast)
|
2630
|
112 |
apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4))
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
113 |
apply(blast)
|
2630
|
114 |
apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5))
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
115 |
apply(blast)
|
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
apply(blast)
|
2630
|
117 |
apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6))
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
118 |
apply(blast)
|
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
119 |
apply(blast)
|
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
120 |
apply(blast)
|
2630
|
121 |
apply(tactic {* prove_termination_ind @{context} 1 *})
|
|
122 |
apply(simp_all add: fun_recs.size)
|
|
123 |
done
|
2629
ffb5a181844b
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
|
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
|
125 |
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
|
126 |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
127 |
|
9cec4269b7f9
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
128 |
|