
diff -r 5d32a81cfe49 -r 50f72361d095 QuotMain.thy
--- a/QuotMain.thy	Mon Sep 28 23:17:29 2009 +0200
+++ b/QuotMain.thy	Tue Sep 29 09:26:22 2009 +0200
@@ -77,8 +77,8 @@
 done
 
 lemma R_trans:
-  assumes ab: "R a b" 
-  and     bc: "R b c" 
+  assumes ab: "R a b"
+  and     bc: "R b c"
   shows "R a c"
 proof -
   have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
@@ -88,15 +88,15 @@
 qed
 
 lemma R_sym:
-  assumes ab: "R a b" 
+  assumes ab: "R a b"
   shows "R b a"
 proof -
   have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
   then show "R b a" using ab unfolding SYM_def by blast
 qed
 
-lemma R_trans2: 
-  assumes ac: "R a c" 
+lemma R_trans2:
+  assumes ac: "R a c"
   and     bd: "R b d"
   shows "R a b = R c d"
 proof
@@ -151,18 +151,18 @@
                |> map Free
 in
   lambda c
-    (HOLogic.exists_const ty $ 
+    (HOLogic.exists_const ty $
        lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
 
 
 (* makes the new type definitions and proves non-emptyness*)
 fun typedef_make (qty_name, rel, ty) lthy =
-let  
+let
   val typedef_tac =
      EVERY1 [rewrite_goal_tac @{thms mem_def},
-             rtac @{thm exI}, 
-             rtac @{thm exI}, 
+             rtac @{thm exI},
+             rtac @{thm exI},
              rtac @{thm refl}]
 in
   LocalTheory.theory_result
@@ -217,7 +217,7 @@
             rtac @{thm QUOT_TYPE.QUOTIENT},
             rtac quot_type_thm]
 in
-  Goal.prove lthy [] [] goal 
+  Goal.prove lthy [] [] goal
     (K typedef_quotient_thm_tac)
 end
 *}
@@ -324,8 +324,8 @@
 | app  "trm" "trm"
 | lam  "nat" "trm"
 
-axiomatization 
-  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" 
+axiomatization
+  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
 where
   r_eq: "EQUIV RR"
 
@@ -486,7 +486,7 @@
 
 ML {*
 fun exchange_ty rty qty ty =
-  if ty = rty 
+  if ty = rty
   then qty
   else
     (case ty of
@@ -680,7 +680,7 @@
   fixes xs :: "'a list"
   assumes a : "x memb xs"
   shows "x # xs \<approx> xs"
-  using a 
+  using a
   apply (induct xs)
   apply (auto intro: list_eq.intros)
   done
@@ -690,7 +690,7 @@
   fixes n :: "nat"
   assumes c: "card1 xs = Suc n"
   shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
-  using c 
+  using c
 apply(induct xs)
 apply (metis Suc_neq_Zero card1_0)
 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)
@@ -704,13 +704,13 @@
 
 
 text {*
-  Unlam_def converts a definition given as 
+  Unlam_def converts a definition given as
 
     c \<equiv> %x. %y. f x y
 
-  to a theorem of the form 
-   
-    c x y \<equiv> f x y 
+  to a theorem of the form
+
+    c x y \<equiv> f x y
 
   This function is needed to rewrite the right-hand
   side to the left-hand side.
@@ -823,51 +823,89 @@
 
 ML {*
   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
-  val consts = [@{const_name "Nil"}, @{const_name "append"}, 
-                @{const_name "Cons"}, @{const_name "membship"}, 
+  val consts = [@{const_name "Nil"}, @{const_name "append"},
+                @{const_name "Cons"}, @{const_name "membship"},
                 @{const_name "card1"}]
 *}
 
 ML {*
 fun build_goal ctxt thm constructors qty mk_rep_abs =
-let
-    fun is_const (Const (x, t)) = x mem constructors
-      | is_const _ = false
-  
+  let
+    fun is_constructor (Const (x, _)) = member (op =) constructors x
+      | is_constructor _ = false;
+
     fun maybe_mk_rep_abs t =
-    let
-      val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
-    in
-      if type_of t = qty then mk_rep_abs t else t
-    end
-    handle TYPE _ => t
-  
-    fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
-      | build_aux (f $ a) =
+      let
+        val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
+      in
+        if type_of t = qty then mk_rep_abs t else t
+      end;
+
+    fun build_aux ctxt1 tm =
+      let
+        val (head, args) = Term.strip_comb tm;
+        val args' = map (build_aux ctxt1) args;
+      in
+        (case head of
+          Abs (x, T, t) =>
+            let
+              val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
+              val v = Free (x', T);
+              val t' = subst_bound (v, t);
+              val rec_term = build_aux ctxt2 t';
+            in Term.lambda_name (x, v) rec_term end
+        | _ =>
+            if is_constructor head then
+              maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
+            else list_comb (head, args'))
+      end;
+
+    val concl2 = Thm.prop_of thm;
+  in
+    Logic.mk_equals (build_aux ctxt concl2, concl2)
+  end
+*}
+
+ML {*
+fun build_goal' ctxt thm constructors qty mk_rep_abs =
+  let
+    fun is_const (Const (x, t)) = member (op =) constructors x
+      | is_const _ = false
+
+    fun maybe_mk_rep_abs t =
+      let
+        val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
+      in
+        if type_of t = qty then mk_rep_abs t else t
+      end
+(*      handle TYPE _ => t*)
+    fun build_aux ctxt1 (Abs (x, T, t)) =
+          let
+            val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
+            val v = Free (x', T);
+            val t' = subst_bound (v, t);
+            val rec_term = build_aux ctxt2 t';
+          in Term.lambda_name (x, v) rec_term end
+      | build_aux ctxt1 (f $ a) =
           let
             val (f, args) = strip_comb (f $ a)
             val _ = writeln (Syntax.string_of_term ctxt f)
            in
-            (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
-            else list_comb ((build_aux f), (map build_aux args)))
+            if is_const f then
+              maybe_mk_rep_abs
+                (list_comb (f, map maybe_mk_rep_abs (map (build_aux ctxt1) args)))
+            else list_comb (build_aux ctxt1 f, map (build_aux ctxt1) args)
           end
-      | build_aux x =
+      | build_aux _ x =
           if is_const x then maybe_mk_rep_abs x else x
-    
-    val concl2 = prop_of thm
-in
-  Logic.mk_equals ((build_aux concl2), concl2)
+
+    val concl2 = term_of (#prop (crep_thm thm))
+  in
+  Logic.mk_equals (build_aux ctxt concl2, concl2)
 end *}
 
-thm EMPTY_def IN_def UNION_def
-
-ML {* val emptyt = symmetric (unlam_def  @{context} @{thm EMPTY_def}) *}
-ML {* val in_t =   symmetric (unlam_def  @{context} @{thm IN_def}) *}
-ML {* val uniont = symmetric (unlam_def @{context}  @{thm UNION_def}) *}
-ML {* val cardt =  symmetric (unlam_def @{context}  @{thm card_def}) *}
-ML {* val insertt =  symmetric (unlam_def @{context} @{thm INSERT_def}) *}
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
-ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}
+ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}
 
 ML {*
   fun dest_cbinop t =
@@ -883,7 +921,7 @@
   fun dest_ceq t =
     let
       val (bop, pair) = dest_cbinop t;
-     val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
+      val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
     in
       if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
     end
@@ -900,25 +938,46 @@
 *}
 
 ML {*
-  fun foo_conv t =
+  fun split_binop_conv t =
     let
       val (lhs, rhs) = dest_ceq t;
       val (bop, _) = dest_cbinop lhs;
       val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
       val [cmT, crT] = Thm.dest_ctyp cr2;
     in
-      Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
+      Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
+    end
+*}
+
+ML {*
+  fun split_arg_conv t =
+    let
+      val (lhs, rhs) = dest_ceq t;
+      val (lop, larg) = Thm.dest_comb lhs;
+      val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+    in
+      Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
     end
 *}
 
 ML {*
-  fun foo_tac n thm =
+  fun split_binop_tac n thm =
     let
       val concl = Thm.cprem_of thm n;
       val (_, cconcl) = Thm.dest_comb concl;
-      val rewr = foo_conv cconcl;
-(*      val _ = tracing (Display.string_of_thm @{context} rewr)
-      val _ = tracing (Display.string_of_thm @{context} thm)*)
+      val rewr = split_binop_conv cconcl;
+    in
+      rtac rewr n thm
+    end
+      handle CTERM _ => Seq.empty
+*}
+
+ML {*
+  fun split_arg_tac n thm =
+    let
+      val concl = Thm.cprem_of thm n;
+      val (_, cconcl) = Thm.dest_comb concl;
+      val rewr = split_arg_conv cconcl;
     in
       rtac rewr n thm
     end
@@ -931,22 +990,27 @@
   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
   by auto
 
+
+thm QUOT_TYPE_I_fset.R_trans2
 ML {*
   fun foo_tac' ctxt =
     REPEAT_ALL_NEW (FIRST' [
-      rtac @{thm trueprop_cong},
+(*      rtac @{thm trueprop_cong},*)
       rtac @{thm list_eq_refl},
       rtac @{thm cons_preserves},
       rtac @{thm mem_respects},
+      rtac @{thm card1_rsp},
       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
-      foo_tac,
+      DatatypeAux.cong_tac,
+      rtac @{thm ext},
+      rtac @{thm eq_reflection},
       CHANGED o (ObjectLogic.full_atomize_tac)
     ])
 *}
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -955,6 +1019,26 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
+lemma atomize_eqv [atomize]: "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+  (is "?rhs \<equiv> ?lhs")
+proof
+  assume "PROP ?lhs" then show "PROP ?rhs" by unfold
+next
+  assume *: "PROP ?rhs"
+  have "A = B"
+  proof (cases A)
+    case True
+    with * have B by unfold
+    with `A` show ?thesis by simp
+  next
+    case False
+    with * have "~ B" by auto
+    with `~ A` show ?thesis by simp
+  qed
+  then show "PROP ?lhs" by (rule eq_reflection)
+qed
+
+
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
@@ -962,7 +1046,7 @@
 
 thm length_append (* Not true but worth checking that the goal is correct *)
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -974,7 +1058,7 @@
 
 thm m2
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -986,7 +1070,7 @@
 
 thm list_eq.intros(4)
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1028,17 +1112,17 @@
 
 thm list_eq.intros(5)
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 *}
 ML {*
-  val cgoal = 
+  val cgoal =
     Toplevel.program (fn () =>
       cterm_of @{theory} goal
     )
 *}
 ML {*
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
@@ -1046,7 +1130,6 @@
   done
 
 thm list.induct
-ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *}
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct}))
@@ -1059,18 +1142,92 @@
 *}
 ML {*
   val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 ML fset_defs_sym
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (rule_tac trueprop_cong)
-  apply (atomize(full))
-  apply (tactic {* foo_tac' @{context} 1 *}) 
-  apply (rule_tac f = "P" in arg_cong)
+  apply (tactic {* foo_tac' @{context} 1 *})
   sorry
 
+ML {*
+  fun lift_theorem_fset_aux thm lthy =
+    let
+      val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
+      val goal = build_goal @{context} novars consts @{typ "'a list"} mk_rep_abs;
+      val cgoal = cterm_of @{theory} goal;
+      val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
+      val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1;
+      val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
+      val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
+      val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
+      val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
+    in
+      nthm3
+    end
+*}
+
+ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
+
+ML {*
+  fun lift_theorem_fset name thm lthy =
+    let
+      val lifted_thm = lift_theorem_fset_aux thm lthy;
+      val (_, lthy2) = note_thm (name, lifted_thm) lthy;
+    in
+      lthy2
+    end;
+*}
+
+local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
+local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
+local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
+local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
+
+thm m1_lift
+thm leqi4_lift
+thm leqi5_lift
+thm m2_lift
+
+ML Drule.instantiate'
+text {*
+  We lost the schematic variable again :(.
+  Another variable export will still be necessary...
+*}
+ML {*
+  Toplevel.program (fn () =>
+    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
+      Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift}
+    )
+  )
+*}
+
+thm leqi4_lift
+ML {*
+  val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) []))
+  val (_, l) = dest_Type typ
+  val t = Type ("QuotMain.fset", l)
+  val v = Var (nam, t)
+  val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
+*}
+
+ML {*
+term_of (#prop (crep_thm @{thm sym}))
+*}
+
+ML {*
+  Toplevel.program (fn () =>
+    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
+      Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift}
+    )
+  )
+*}
+
+
+
+
+
+ML {* MRS *}
 thm card1_suc
 
 ML {*
@@ -1081,11 +1238,13 @@
 *}
 ML {*
   val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
+ML {* @{term "\<exists>x. P x"} *}
+ML {*  Thm.bicompose *}
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-
+  apply (tactic {* foo_tac' @{context} 1 *})
 
 
 (*
@@ -1097,4 +1256,4 @@
 *)
 
 
-yyes
\ No newline at end of file
+yyes




