equal
deleted
inserted
replaced
345 |
345 |
346 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
346 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
347 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
347 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
348 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
348 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
349 prefer 2 |
349 prefer 2 |
350 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *}) |
350 apply (tactic {* clean_tac @{context} [quot] defs |
|
351 [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *}) |
351 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*}) |
352 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*}) |
352 done |
353 done |
|
354 |
|
355 |
|
356 |
353 |
357 |
354 quotient_def |
358 quotient_def |
355 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
359 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
356 where |
360 where |
357 "fset_rec \<equiv> list_rec" |
361 "fset_rec \<equiv> list_rec" |