# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259373264 -3600
# Node ID 2f0ad33f0241e7a8f95e68a78bb7c763c8b1b6a1
# Parent  1f2c8be84be7fd31aaff32bd984cea4933d514d6
annotated a proof with all steps and simplified LAMBDA_RES_TAC

diff -r 1f2c8be84be7 -r 2f0ad33f0241 FSet.thy
--- a/FSet.thy	Fri Nov 27 18:38:44 2009 +0100
+++ b/FSet.thy	Sat Nov 28 02:54:24 2009 +0100
@@ -341,20 +341,64 @@
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
+ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+
 lemma cheat: "P" sorry
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
 prefer 2
-apply (tactic {* clean_tac @{context} [quot] defs 
-                 [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
-apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*})
+apply(rule cheat)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 done
 
 
-
-
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
@@ -400,12 +444,8 @@
   apply (assumption)
   done
 
-
 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
-
-
-
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
diff -r 1f2c8be84be7 -r 2f0ad33f0241 IntEx.thy
--- a/IntEx.thy	Fri Nov 27 18:38:44 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 02:54:24 2009 +0100
@@ -140,13 +140,46 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 ML {* val consts = lookup_quot_consts defs *}
 
-ML {*
-fun lift_tac_fset lthy t =
-  lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs
-*}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+
+
+ML {* fun r_mk_comb_tac_intex lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+
+
+lemma cheat: "P" sorry
 
 lemma "PLUS a b = PLUS b a"
-by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *})
+apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+prefer 2
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*})
+done
 
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
@@ -157,8 +190,13 @@
   done
 
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
-by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *})
-
+apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+done
 
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
@@ -171,7 +209,7 @@
 sorry
 
 lemma "foldl PLUS x [] = x"
-apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
+apply (tactic {* lift_tac_intex @{context} @{thm ho_tst} 1 *})
 apply (simp_all only: map_prs foldl_prs)
 sorry
 
@@ -191,8 +229,11 @@
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] [trans2] rsp_thms) 1 *})
-oops
+apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+done
 
 
 (*
diff -r 1f2c8be84be7 -r 2f0ad33f0241 QuotMain.thy
--- a/QuotMain.thy	Fri Nov 27 18:38:44 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 02:54:24 2009 +0100
@@ -717,7 +717,8 @@
 *)
 
 ML {*
-fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+fun instantiate_tac thm = 
+  Subgoal.FOCUS (fn {concl, ...} =>
   let
     val pat = Drule.strip_imp_concl (cprop_of thm)
     val insts = Thm.match (pat, concl)
@@ -739,13 +740,17 @@
      CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])
 *}
 
+lemma FUN_REL_I:
+  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+  shows "(R1 ===> R2) f g"
+using a by (simp add: FUN_REL.simps)
+
 ML {*
-fun LAMBDA_RES_TAC ctxt i st =
-  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | _ => fn _ => no_tac) i st
+val LAMBDA_RES_TAC =
+  SUBGOAL (fn (goal, i) =>
+    case goal of
+       (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i
+     | _ => no_tac)
 *}
 
 ML {*
@@ -815,7 +820,7 @@
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [
     resolve_tac trans2,
-    LAMBDA_RES_TAC ctxt,
+    LAMBDA_RES_TAC,
     rtac @{thm RES_FORALL_RSP},
     ball_rsp_tac ctxt,
     rtac @{thm RES_EXISTS_RSP},
@@ -834,6 +839,9 @@
     WEAK_LAMBDA_RES_TAC ctxt,
     CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
     ])
+
+fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
 (*
@@ -841,7 +849,7 @@
 we try:
 
  1) theorems 'trans2' from the appropriate QUOT_TYPE
- 2) remove lambdas from both sides (LAMBDA_RES_TAC)
+ 2) remove lambdas from both sides: LAMBDA_RES_TAC
  3) remove Ball/Bex from the right hand side
  4) use user-supplied RSP theorems
  5) remove rep_abs from the right side
@@ -849,44 +857,96 @@
  7) split applications of lifted type (apply_rsp)
  8) split applications of non-lifted type (cong_tac)
  9) apply extentionality
-10) reflexivity of the relation
-11) assumption
+ A) reflexivity of the relation
+ B) assumption
     (Lambdas under respects may have left us some assumptions)
-12) proving obvious higher order equalities by simplifying fun_rel
+ C) proving obvious higher order equalities by simplifying fun_rel
     (not sure if it is still needed?)
-13) unfolding lambda on one side
-14) simplifying (= ===> =) for simpler respectfulness
+ D) unfolding lambda on one side
+ E) simplifying (= ===> =) for simpler respectfulness
 
 *)
 
 ML {*
 fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (FIRST' [
+  (FIRST' [
     (K (print_tac "start")) THEN' (K no_tac), 
+  
+    (* "cong" rule of the of the relation    *)
+    (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *)
     DT ctxt "1" (resolve_tac trans2),
-    DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+
+    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
+    DT ctxt "2" (LAMBDA_RES_TAC),
+
+    (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+
     DT ctxt "4" (ball_rsp_tac ctxt),
     DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
     DT ctxt "6" (bex_rsp_tac ctxt),
+
+    (* respectfulness of ops *)
     DT ctxt "7" (resolve_tac rsp_thms),
+
+    (* reflexivity of operators arising from Cong_tac *)
     DT ctxt "8" (rtac @{thm refl}),
+
+    (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
+    (* observe ---> *) 
     DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
+
+    (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP   provided type of t needs lifting *)
     DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
+
+    (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
     DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+
+    (* = (\<lambda>x\<dots>) (\<lambda>x\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
     DT ctxt "C" (rtac @{thm ext}),
+    
+    (* reflexivity of the basic relations *)
     DT ctxt "D" (resolve_tac rel_refl),
+
+    (* resolving with R x y assumptions *)
     DT ctxt "E" (atac),
+
     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
     DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
     DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
     ])
+
+fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
+ML {*
+fun get_inj_repabs_tac ctxt rel lhs rhs =
+let
+  val _ = tracing "input"
+  val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel)
+  val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs)
+  val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs)
+in  
+  case (rel, lhs, rhs) of
+    (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *)
+      => rtac @{thm REP_ABS_RSP(1)}
+  | (_, Const (@{const_name "Ball"}, _) $ _, 
+        Const (@{const_name "Ball"}, _) $ _)
+      => rtac @{thm RES_FORALL_RSP}
+  | _ => K no_tac
+end
+*}
 
-
+ML {* 
+fun inj_repabs_tac ctxt =
+  SUBGOAL (fn (goal, i) =>
+     (case (HOLogic.dest_Trueprop goal) of
+        (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs
+      | _ => K no_tac) i)
+*}
 
 section {* Cleaning of the theorem *}