equal
deleted
inserted
replaced
81 thm fun_recs.size_eqvt |
81 thm fun_recs.size_eqvt |
82 thm fun_recs.supports |
82 thm fun_recs.supports |
83 thm fun_recs.fsupp |
83 thm fun_recs.fsupp |
84 thm fun_recs.supp |
84 thm fun_recs.supp |
85 |
85 |
86 |
|
87 |
|
88 |
|
89 lemma |
86 lemma |
90 fixes c::"'a::fs" |
87 fixes c::"'a::fs" |
91 assumes "\<And>name c. P1 c (Var name)" |
88 assumes "\<And>name c. P1 c (Var name)" |
92 and "\<And>c. P1 c Unit" |
89 and "\<And>c. P1 c Unit" |
93 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)" |
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)" |
104 and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)" |
101 and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)" |
105 shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat" |
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" |
106 apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *}) |
103 apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *}) |
107 apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1)) |
104 apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1)) |
108 apply(simp_all)[4] |
105 apply(simp_all)[4] |
|
106 apply(blast) |
109 apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2)) |
107 apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2)) |
110 apply(simp_all)[1] |
108 apply(blast) |
111 apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3)) |
109 apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3)) |
112 apply(simp_all)[2] |
110 apply(blast) |
|
111 apply(blast) |
113 apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4)) |
112 apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4)) |
114 apply(simp_all)[1] |
113 apply(blast) |
115 apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5)) |
114 apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5)) |
116 apply(simp_all)[2] |
115 apply(blast) |
|
116 apply(blast) |
117 apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6)) |
117 apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6)) |
118 apply(simp_all)[3] |
118 apply(blast) |
|
119 apply(blast) |
|
120 apply(blast) |
119 apply(tactic {* prove_termination_ind @{context} 1 *}) |
121 apply(tactic {* prove_termination_ind @{context} 1 *}) |
120 apply(simp_all add: fun_recs.size) |
122 apply(simp_all add: fun_recs.size) |
121 done |
123 done |
122 |
124 |
123 end |
125 end |