--- a/FSet.thy Wed Dec 02 10:30:20 2009 +0100
+++ b/FSet.thy Wed Dec 02 10:56:35 2009 +0100
@@ -309,40 +309,6 @@
apply(tactic {* clean_tac @{context} [quot] defs 1*})
done
-lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
-by (simp add: QUOT_TRUE_def)
-
-ML {*
-fun quot_true_tac' ctxt fnctn =
- CSUBGOAL (fn (cgl, i) =>
- let
- val gl = term_of cgl;
- val thy = ProofContext.theory_of ctxt;
- fun find_fun trm =
- case trm of
- (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
- | _ => false
- in
- case find_first find_fun (Logic.strip_assums_hyp gl) of
- SOME (asm as (_ $ (_ $ x))) =>
- let
- val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp}
- val _ = tracing (Syntax.string_of_term @{context} (prop_of (thm')))
- val ps = Logic.strip_params (Thm.concl_of thm');
- val fx = fnctn x;
- val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm');
- val insts = [(fx', fx)]
- |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u))));
- val thm_i = Drule.cterm_instantiate insts thm'
- val thm_j = Thm.forall_elim_vars 0 thm_i
- in
- dtac thm_j i
- end
- | NONE => error "quot_true_tac!"
- | _ => error "quot_true_tac!!"
- end)
-*}
-
lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
@@ -362,8 +328,6 @@
apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
done
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
-
lemma "FOLD f g (z::'b) (INSERT a x) =
(if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
@@ -379,91 +343,43 @@
lemma cheat: "P" sorry
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *}
-ML {*
-fun quot_true_conv1 ctxt fnctn ctrm =
- case (term_of ctrm) of
- (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ x)) =>
- let
- val _ = tracing "A";
- val fx = fnctn x;
- val thy = ProofContext.theory_of ctxt;
- val cx = cterm_of thy x;
- val cfx = cterm_of thy fx;
- val cxt = ctyp_of thy (fastype_of x);
- val cfxt = ctyp_of thy (fastype_of fx);
- val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
- val _ = tracing (Syntax.string_of_term @{context} (prop_of thm));
- in
- Conv.rewr_conv thm ctrm
- end
-*}
-
-ML {*
-fun quot_true_conv ctxt fnctn ctrm =
- case (term_of ctrm) of
- (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) =>
- quot_true_conv1 ctxt fnctn ctrm
- | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
- | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
- | _ => Conv.all_conv ctrm
-*}
-
-ML CONVERSION
-ML {*
-fun quot_true_tac ctxt fnctn = CONVERSION (
- fn ctrm =>
- let
- val _ = tracing "B";
- val t = quot_true_conv ctxt fnctn ctrm;
- val _ = tracing "C";
- in
- t
- end)
-*}
-
lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
prefer 2
apply(tactic {* clean_tac @{context} [quot] defs 1 *})
-apply (tactic {* quot_true_tac @{context} (fst o dest_comb) 1 *}) apply(assumption)
-
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
-apply (tactic {* quot_true_tac @{context} (unlam) 1 *}) apply(assumption)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
-apply (drule QT_lam)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply (tactic {* quot_true_tac' @{context} (fst o dest_comb) 1 *})
-apply (assumption)
-apply (assumption)
-apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* D *) (* reflexivity of basic relations *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)