306 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
306 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
307 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
307 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
308 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
308 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
309 apply(tactic {* clean_tac @{context} [quot] defs 1*}) |
309 apply(tactic {* clean_tac @{context} [quot] defs 1*}) |
310 done |
310 done |
|
311 |
|
312 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
|
313 by (simp add: QUOT_TRUE_def) |
311 |
314 |
312 ML {* |
315 ML {* |
313 fun quot_true_tac' ctxt fnctn = |
316 fun quot_true_tac' ctxt fnctn = |
314 CSUBGOAL (fn (cgl, i) => |
317 CSUBGOAL (fn (cgl, i) => |
315 let |
318 let |
376 |
379 |
377 lemma cheat: "P" sorry |
380 lemma cheat: "P" sorry |
378 |
381 |
379 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *} |
382 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *} |
380 |
383 |
|
384 ML {* |
|
385 fun quot_true_conv1 ctxt fnctn ctrm = |
|
386 case (term_of ctrm) of |
|
387 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ x)) => |
|
388 let |
|
389 val _ = tracing "A"; |
|
390 val fx = fnctn x; |
|
391 val thy = ProofContext.theory_of ctxt; |
|
392 val cx = cterm_of thy x; |
|
393 val cfx = cterm_of thy fx; |
|
394 val cxt = ctyp_of thy (fastype_of x); |
|
395 val cfxt = ctyp_of thy (fastype_of fx); |
|
396 val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} |
|
397 val _ = tracing (Syntax.string_of_term @{context} (prop_of thm)); |
|
398 in |
|
399 Conv.rewr_conv thm ctrm |
|
400 end |
|
401 *} |
|
402 |
|
403 ML {* |
|
404 fun quot_true_conv ctxt fnctn ctrm = |
|
405 case (term_of ctrm) of |
|
406 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => |
|
407 quot_true_conv1 ctxt fnctn ctrm |
|
408 | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm |
|
409 | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
|
410 | _ => Conv.all_conv ctrm |
|
411 *} |
|
412 |
|
413 ML CONVERSION |
|
414 ML {* |
|
415 fun quot_true_tac ctxt fnctn = CONVERSION ( |
|
416 fn ctrm => |
|
417 let |
|
418 val _ = tracing "B"; |
|
419 val t = quot_true_conv ctxt fnctn ctrm; |
|
420 val _ = tracing "C"; |
|
421 in |
|
422 t |
|
423 end) |
|
424 *} |
|
425 |
381 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
426 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
382 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
427 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
383 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
428 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
384 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
429 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
385 prefer 2 |
430 prefer 2 |
386 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
431 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
|
432 apply (tactic {* quot_true_tac @{context} (fst o dest_comb) 1 *}) apply(assumption) |
|
433 |
387 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
434 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
388 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
435 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
436 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
390 apply (tactic {* quot_true_tac @{context} (unlam) 1 *}) apply(assumption) |
437 apply (tactic {* quot_true_tac @{context} (unlam) 1 *}) apply(assumption) |
391 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
438 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |