equal
deleted
inserted
replaced
102 and "\<And>name c. P6 c (PVar name)" |
102 and "\<And>name c. P6 c (PVar name)" |
103 and "\<And>c. P6 c PUnit" |
103 and "\<And>c. P6 c PUnit" |
104 and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)" |
104 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" |
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" |
106 apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *}) |
106 apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *}) |
107 oops |
107 apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1)) |
108 |
108 apply(simp_all)[4] |
109 ML {* |
109 apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2)) |
110 val trm1 = @{prop "P1 &&& P2 &&& P3"} |
110 apply(simp_all)[1] |
111 val trm2 = @{prop "(P1 &&& P2) &&& P3 &&& P4"} |
111 apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3)) |
112 *} |
112 apply(simp_all)[2] |
113 |
113 apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4)) |
114 ML {* |
114 apply(simp_all)[1] |
115 Logic.dest_conjunction_list trm1; |
115 apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5)) |
116 Logic.dest_conjunction_list trm2 |
116 apply(simp_all)[2] |
117 *} |
117 apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6)) |
118 |
118 apply(simp_all)[3] |
119 ML {* |
119 apply(tactic {* prove_termination_ind @{context} 1 *}) |
120 Logic.dest_conjunctions trm1; |
120 apply(simp_all add: fun_recs.size) |
121 Logic.dest_conjunctions trm2 |
121 done |
122 *} |
|
123 |
|
124 |
122 |
125 end |
123 end |
126 |
124 |
127 |
125 |
128 |
126 |