# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259742228 -3600
# Node ID 6c88b42da228073f3c58714d15c9e2efe7bba7f8
# Parent  325d6e9a7515354a4273f9cf9cbfba208bc3fb75
A bit of progress; but the object-logic vs meta-logic distinction is troublesome.

diff -r 325d6e9a7515 -r 6c88b42da228 FSet.thy
--- a/FSet.thy	Wed Dec 02 07:21:10 2009 +0100
+++ b/FSet.thy	Wed Dec 02 09:23:48 2009 +0100
@@ -302,15 +302,44 @@
 ML {* val consts = lookup_quot_consts defs *}
 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
-thm m1
-
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
-apply(tactic {* regularize_tac @{context}  [rel_eqv] 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
 apply(tactic {* clean_tac @{context} [quot] defs 1*})
 done
 
+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 *})
 
@@ -347,35 +376,27 @@
 
 lemma cheat: "P" sorry
 
+ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *}
+
 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 *})
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 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(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)
-
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply (drule QT_all)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* lambda_res_tac @{context} 1 *})
-apply(tactic {* rule FUN_REL_I)
+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*}) (* 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(clarify)
-apply (drule_tac x="x" in QT_lam)
-
-
-
-thm QT_lam
-apply (drule QT_all)
-apply (drule_tac x = "yyy" in QT_lam)
+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*}) (* 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 *)