
diff -r a840c232e04e -r 991b0e53f9dc QuotMain.thy
--- a/QuotMain.thy	Mon Nov 09 15:40:43 2009 +0100
+++ b/QuotMain.thy	Tue Nov 10 09:32:16 2009 +0100
@@ -202,7 +202,7 @@
    bounded quantifiers, for example:
       \<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P
  - Abstractions over a type that needs lifting are replaced
-   by bounded abstactions:
+   by bounded abstractions:
       \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
 
  - Equalities over the type being lifted are replaced by
@@ -241,7 +241,8 @@
               val tys_out = tys_rel ---> ty_out;
             in
             (case (maps_lookup (ProofContext.theory_of lthy) s) of
-               SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
+               SOME (info) => list_comb (Const (#relfun info, tys_out),
+                              map (fn ty => tyRel ty rty rel lthy) tys)
              | NONE  => HOLogic.eq_const ty
             )
             end
@@ -341,12 +342,12 @@
 
 (*
 ML {*
-  text {*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow> bool"};*}
   val r = Free ("R", dummyT);
-  val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
+  val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
   val t2 = Syntax.check_term @{context} t;
-  Toplevel.program (fn () => cterm_of @{theory} t2)
-*}*)
+  cterm_of @{theory} t2
+*}
+*)
 
 text {* Assumes that the given theorem is atomized *}
 ML {*
@@ -356,17 +357,16 @@
        (my_reg_inst lthy rel rty (prop_of thm)))
 *}
 
-lemma universal_twice: 
-  "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
-by auto
+lemma universal_twice:
+  assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
+  shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
+using * by auto
 
-lemma implication_twice: 
-  "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-by auto
-
-(*lemma equality_twice:
-  "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
-by auto*)
+lemma implication_twice:
+  assumes a: "c \<longrightarrow> a"
+  assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
+  shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+using a b by auto
 
 ML {*
 fun regularize thm rty rel rel_eqv rel_refl lthy =
@@ -383,6 +383,7 @@
         EqSubst.eqsubst_tac ctxt [0]
           [(@{thm equiv_res_forall} OF [rel_eqv]),
            (@{thm equiv_res_exists} OF [rel_eqv])],
+        (* For a = b \<longrightarrow> a \<approx> b *)
         (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
         (rtac @{thm RIGHT_RES_FORALL_REGULAR})
       ]);
@@ -396,7 +397,12 @@
 section {* RepAbs injection *}
 (*
 
-Injecting RepAbs means:
+RepAbs injection is done in the following phases:
+ 1) build_repabs_term inserts rep-abs pairs in the term
+ 2) we prove the equality between the original theorem and this one
+ 3) we use Pure.equal_elim_rule1 to get the new theorem.
+
+build_repabs_term does:
 
   For abstractions:
   * If the type of the abstraction doesn't need lifting we recurse.
@@ -404,7 +410,9 @@
     variable needs lifting.
     * If it doesn't then we recurse
     * If it does we recurse and put 'RepAbs' around all occurences
-      of the variable in the obtained subterm.
+      of the variable in the obtained subterm. This in combination
+      with the RepAbs above will let us change the type of the
+      abstraction with rewriting.
   For applications:
   * If the term is 'Respects' applied to anything we leave it unchanged
   * If the term needs lifting and the head is a constant that we know
@@ -414,27 +422,24 @@
     put RepAbs and recurse
   * Otherwise just recurse.
 
-The injection is done in the following phases:
- 1) build_repabs_term inserts rep-abs pairs in the term
- 2) we prove the equality between the original theorem and this one
- 3) we use Pure.equal_elim_rule1 to get the new theorem.
 
 To prove that the old theorem implies the new one, we first
 atomize it and then try:
 
- 1) theorems 'trans2' from the QUOT_TYPE
+ 1) theorems 'trans2' from the appropriate QUOT_TYPE
  2) remove lambdas from both sides (LAMBDA_RES_TAC)
- 3) remove Ball/Bex
- 4) use RSP theorems
- 5) remove rep_abs from right side
- 6) reflexivity
+ 3) remove Ball/Bex from the right hand side
+ 4) use user-supplied RSP theorems
+ 5) remove rep_abs from the right side
+ 6) reflexivity of equality
  7) split applications of lifted type (apply_rsp)
  8) split applications of non-lifted type (cong_tac)
  9) apply extentionality
-10) relation reflexive
+10) reflexivity of the relation
 11) assumption
+    (Lambdas under respects may have left us some assumptions)
 12) proving obvious higher order equalities by simplifying fun_rel
-    (not sure if still needed?)
+    (not sure if it is still needed?)
 13) unfolding lambda on one side
 14) simplifying (= ===> =) for simpler respectfullness
 
@@ -632,9 +637,14 @@
 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
 by (simp add: id_def)
 
+(* TODO: can be also obtained with: *)
+ML {* symmetric (eq_reflection OF @{thms id_def}) *}
+
 ML {*
 fun build_repabs_term lthy thm consts rty qty =
   let
+    (* TODO: The rty and qty stored in the quotient_info should
+       be varified, so this will soon not be needed *)
     val rty = Logic.varifyT rty;
     val qty = Logic.varifyT qty;
 
@@ -664,8 +674,8 @@
               else
                 let
                   val v' = mk_repabs v;
-                  (* TODO: I believe this is not needed any more *)
-                  val t1 = Envir.beta_norm (t' $ v')
+                  (* TODO: I believe 'beta' is not needed any more *)
+                  val t1 = (* Envir.beta_norm *) (t' $ v')
                 in
                   lambda v t1
                 end)
@@ -691,7 +701,7 @@
   end
 *}
 
-text {* Assumes that it is given a regularized theorem *}
+text {* Builds provable goals for regularized theorems *}
 ML {*
 fun build_repabs_goal ctxt thm cons rty qty =
   Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
@@ -699,14 +709,17 @@
 
 ML {*
 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
-let
-  val pat = Drule.strip_imp_concl (cprop_of thm)
-  val insts = Thm.match (pat, concl)
-in
-  rtac (Drule.instantiate insts thm) 1
-end
-handle _ => no_tac
-)
+  let
+    val pat = Drule.strip_imp_concl (cprop_of thm)
+    val insts = Thm.match (pat, concl)
+  in
+    rtac (Drule.instantiate insts thm) 1
+  end
+  handle _ => no_tac)
+*}
+
+ML {*
+fun CHANGED' tac = (fn i => CHANGED (tac i))
 *}
 
 ML {*
@@ -715,9 +728,10 @@
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
     rtac @{thm IDENTITY_QUOTIENT},
-    (
-      fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN
-      rtac @{thm IDENTITY_QUOTIENT} i
+    (* For functional identity quotients, (op = ---> op =) *)
+    CHANGED' (
+      (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I})) THEN'
+      rtac @{thm IDENTITY_QUOTIENT}
     )
   ])
 *}
@@ -725,7 +739,7 @@
 ML {*
 fun LAMBDA_RES_TAC ctxt i st =
   (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ (Abs(_, _, _))$(Abs(_, _, _)))) =>
+    (_ $ (_ $ (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
@@ -749,12 +763,12 @@
     val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
     val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
     val insts = Thm.match (pat, concl)
-in
-  if needs_lift rty (type_of f) then
-    rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
-  else no_tac
-end
-handle _ => no_tac)
+  in
+    if needs_lift rty (type_of f) then
+      rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+    else no_tac
+  end
+  handle _ => no_tac)
 *}
 
 ML {*
@@ -768,8 +782,7 @@
     THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
     (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
   end
-  handle _ => no_tac
-  )
+  handle _ => no_tac)
 *}
 
 ML {*
@@ -783,8 +796,11 @@
     THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
     (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
   end
-  handle _ => no_tac
-  )
+  handle _ => no_tac)
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 *}
 
 ML {*
@@ -797,18 +813,14 @@
     FIRST' (map rtac rsp_thms),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
-(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
     Cong_Tac.cong_tac @{thm cong},
     rtac @{thm ext},
     rtac reflex_thm,
     atac,
-    (
-     (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-     THEN_ALL_NEW (fn _ => no_tac)
-    ),
+    SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
     WEAK_LAMBDA_RES_TAC ctxt,
-    (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i))
+    CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
     ])
 *}
 
@@ -828,12 +840,10 @@
 section {* Cleaning the goal *}
 
 lemma prod_fun_id: "prod_fun id id = id"
-  apply (simp add: prod_fun_def)
-done
+by (simp add: prod_fun_def)
+
 lemma map_id: "map id x = x"
-  apply (induct x)
-  apply (simp_all add: map.simps)
-done
+by (induct x) (simp_all)
 
 ML {*
 fun simp_ids lthy thm =
@@ -866,6 +876,7 @@
   end
 *}
 
+(* TODO: Check if it behaves properly with varifyed rty *)
 ML {*
 fun findabs_all rty tm =
   case tm of
@@ -881,7 +892,6 @@
 fun findabs rty tm = distinct (op =) (findabs_all rty tm)
 *}
 
-
 ML {*
 fun findaps_all rty tm =
   case tm of
@@ -894,6 +904,7 @@
 fun findaps rty tm = distinct (op =) (findaps_all rty tm)
 *}
 
+(* Currently useful only for LAMBDA_PRS *)
 ML {*
 fun make_simp_prs_thm lthy quot_thm thm typ =
   let
@@ -936,6 +947,7 @@
       in (a1 @ a2, e1 @ e2) end
   | _ => ([], []);
 *}
+
 ML {*
 fun findallex lthy rty qty tm =
   let
@@ -1005,12 +1017,12 @@
 *}
 
 ML {*
-fun matches (ty1, ty2) =
-  Type.raw_instance (ty1, Logic.varifyT ty2);
-
 fun lookup_quot_data lthy qty =
   let
+    fun matches (ty1, ty2) =
+      Type.raw_instance (ty1, Logic.varifyT ty2);
     val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+    (* TODO: Should no longer be needed *)
     val rty = Logic.unvarifyT (#rtyp quotdata)
     val rel = #rel quotdata
     val rel_eqv = #equiv_thm quotdata




