300 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
300 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
301 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
301 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
302 ML {* val consts = lookup_quot_consts defs *} |
302 ML {* val consts = lookup_quot_consts defs *} |
303 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
303 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
304 |
304 |
305 thm m1 |
|
306 |
|
307 lemma "IN x EMPTY = False" |
305 lemma "IN x EMPTY = False" |
308 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
306 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
309 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
307 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
310 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 *}) |
311 apply(tactic {* clean_tac @{context} [quot] defs 1*}) |
309 apply(tactic {* clean_tac @{context} [quot] defs 1*}) |
312 done |
310 done |
|
311 |
|
312 ML {* |
|
313 fun quot_true_tac' ctxt fnctn = |
|
314 CSUBGOAL (fn (cgl, i) => |
|
315 let |
|
316 val gl = term_of cgl; |
|
317 val thy = ProofContext.theory_of ctxt; |
|
318 fun find_fun trm = |
|
319 case trm of |
|
320 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
|
321 | _ => false |
|
322 in |
|
323 case find_first find_fun (Logic.strip_assums_hyp gl) of |
|
324 SOME (asm as (_ $ (_ $ x))) => |
|
325 let |
|
326 val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp} |
|
327 val _ = tracing (Syntax.string_of_term @{context} (prop_of (thm'))) |
|
328 val ps = Logic.strip_params (Thm.concl_of thm'); |
|
329 val fx = fnctn x; |
|
330 val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm'); |
|
331 val insts = [(fx', fx)] |
|
332 |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u)))); |
|
333 val thm_i = Drule.cterm_instantiate insts thm' |
|
334 val thm_j = Thm.forall_elim_vars 0 thm_i |
|
335 in |
|
336 dtac thm_j i |
|
337 end |
|
338 | NONE => error "quot_true_tac!" |
|
339 | _ => error "quot_true_tac!!" |
|
340 end) |
|
341 *} |
313 |
342 |
314 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
343 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
315 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
344 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
316 |
345 |
317 lemma "INSERT a (INSERT a x) = INSERT a x" |
346 lemma "INSERT a (INSERT a x) = INSERT a x" |
345 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
374 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
346 done |
375 done |
347 |
376 |
348 lemma cheat: "P" sorry |
377 lemma cheat: "P" sorry |
349 |
378 |
|
379 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *} |
|
380 |
350 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
381 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
351 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
382 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
352 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
|
353 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
383 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
354 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
384 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
355 prefer 2 |
385 prefer 2 |
356 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
386 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
357 apply(rule_tac a="\<forall>(P\<Colon>'a fset \<Rightarrow> bool) l\<Colon>'a fset. P EMPTY \<longrightarrow> (\<forall>(a\<Colon>'a) x\<Colon>'a fset. P x \<longrightarrow> P (INSERT a x)) \<longrightarrow> P l" in QUOT_TRUE_i) |
387 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
358 |
388 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
359 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
|
360 apply (drule QT_all) |
|
361 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
362 apply(tactic {* lambda_res_tac @{context} 1 *}) |
|
363 apply(tactic {* rule FUN_REL_I) |
|
364 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
365 apply(clarify) |
390 apply (tactic {* quot_true_tac @{context} (unlam) 1 *}) apply(assumption) |
366 apply (drule_tac x="x" in QT_lam) |
391 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
367 |
392 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
368 |
393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
369 |
394 apply (drule QT_lam) |
370 thm QT_lam |
395 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
371 apply (drule QT_all) |
396 apply (tactic {* quot_true_tac' @{context} (fst o dest_comb) 1 *}) |
372 apply (drule_tac x = "yyy" in QT_lam) |
397 apply (assumption) |
|
398 apply (assumption) |
373 apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *}) |
399 apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *}) |
374 |
|
375 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
|
376 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
377 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
|
378 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
|
379 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
400 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
380 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
401 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
381 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
402 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
382 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
403 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
383 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
404 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |