
diff -r 0ffc37761e53 -r ec772b461e26 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 21 14:15:22 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 14:30:29 2009 +0200
@@ -1133,6 +1133,7 @@
 *)
 
 thm list_eq.intros(5)
+(* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
   val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
@@ -1153,9 +1154,6 @@
 
 ML {* atomize_thm @{thm list_induct_hol4} *}
 
-
-ML {* val li = atomize_thm @{thm list_induct_hol4} *}
-
 prove list_induct_r: {*
    build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
   apply (simp only: equiv_res_forall[OF equiv_list_eq])
@@ -1431,177 +1429,6 @@
   )
 *}
 
-lemma "(Ball (Respects ((op \<approx>) ===> (op =)))
-         (((REP_fset ---> id) ---> id)
-             (((ABS_fset ---> id) ---> id)
-               (\<lambda>P.
-                  (ABS_fset ---> id) ((REP_fset ---> id) P)
-                    (REP_fset (ABS_fset [])) \<and>
-                  Ball (Respects (op \<approx>))
-                    ((ABS_fset ---> id)
-                       ((REP_fset ---> id)
-                          (\<lambda>t.
-                             ((ABS_fset ---> id)
-                               ((REP_fset ---> id) P)
-                               (REP_fset (ABS_fset t))) \<longrightarrow>
-                             (!h.
-                               (ABS_fset ---> id)
-                                 ((REP_fset ---> id) P)
-                                 (REP_fset
-                                    (ABS_fset
-                                       (h #
-                                            REP_fset
-                                              (ABS_fset t)))))))) \<longrightarrow>
-                  Ball (Respects (op \<approx>))
-                    ((ABS_fset ---> id)
-                       ((REP_fset ---> id)
-                          (\<lambda>l.
-                             (ABS_fset ---> id)
-                               ((REP_fset ---> id) P)
-                               (REP_fset (ABS_fset l)))))))))
-
-   = Ball (Respects ((op \<approx>) ===> (op =)))
-     (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
-     (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))"
-
-thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]
-proof -
-note APPLY_RSP_I = APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]
-show ?thesis apply -
-
-
-ML_prf {*
-  val gc = Subgoal.focus @{context} 1 (Isar.goal ())
-  |> fst
-  |> #concl
-  val tc = cterm_of @{theory} (concl_of ( @{thm "APPLY_RSP" }))
-  val (_, tc') = Thm.dest_comb tc
-  val (_, gc') = Thm.dest_comb gc
- *}
-
-
-
-
-ML_prf {*
-  (gc', tc')
-*}
-ML_prf {* Pattern.first_order_match *}
-ML_prf {* Thm.match (@{cpat "?P::?'a"}, @{cterm "1::nat"}) *}
-ML_prf {* Pattern.match @{theory} (term_of @{cpat "?P::nat"}, term_of @{cterm "1::nat"}) (Vartab.empty, Vartab.empty) *}
-
-ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
-ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *}
-
-ML_prf {* val mo = Thm.match (op1, op2) *}
-ML_prf {* val t1 = Drule.instantiate mo @{thm "APPLY_RSP" } *}
-ML_prf {* val tc = cterm_of @{theory} (concl_of t1) *}
-ML_prf {* val (_, tc') = Thm.dest_comb tc *}
-ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
-ML_prf {* val (mlty, mlt) = Thm.match (l1, l2) *}
-ML_prf {* val t2 = Drule.instantiate (mlty, []) t1 *}
-ML_prf {* val tc = cterm_of @{theory} (concl_of t2) *}
-ML_prf {* val (_, tc') = Thm.dest_comb tc *}
-ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
-ML_prf {* val mr = Thm.match (r1, r2) *}
-
-ML_prf {* val t3 = Drule.instantiate ml t2 *}
-ML_prf {* val tc = cterm_of @{theory} (concl_of t3) *}
-ML_prf {* val (_, tc') = Thm.dest_comb tc *}
-
-
-
-ML_prf {* mtyl; mtyr *}
-
-ML_prf {* val ol1 = Thm.capply op1 l1 *}
-ML_prf {* val ol2 = Thm.capply op2 l2 *}
-ML_prf {* (ol1, ol2); Thm.match (ol1, ol2) *}
-ML_prf {* val w1 = Thm.capply ol1 r1 *}
-ML_prf {* val w2 = Thm.capply ol2 r2 *}
-
-
-.
-(*ML_prf {* (w1, w2); Thm.match (w1, w2) *}*)
-
-
-
-ML_prf {*
-   (tc', gc')
-*}
-
-thm APPLY_RSP
-thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)"]
-term "(op \<approx> ===> op =) ===> op ="
-proof -
-note APPLY_RSP_I2 = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id" "Ball (Respects op \<approx> ===> op =)" "Ball (Respects op \<approx> ===> op =)"]
-show ?thesis apply -
-
-thm APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow>
-          (\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"]
-proof -
-note APPLY_RSP_I3=APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow>
-          (\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"]
-show ?thesis apply -
-term "(REP_fset ---> id ---> id
-         (ABS_fset ---> id ---> id
-           (\<lambda>P\<Colon>'a list \<Rightarrow> bool.
-               ABS_fset ---> id (REP_fset ---> id P)
-                (REP_fset (ABS_fset [])) \<and>
-               Ball (Respects op \<approx>)
-                (ABS_fset ---> id
-                  (REP_fset ---> id
-                    (\<lambda>t\<Colon>'a list.
-                        ABS_fset ---> id (REP_fset ---> id P)
-                         (REP_fset (ABS_fset t)) \<longrightarrow>
-                        (\<forall>h\<Colon>'a.
-                            ABS_fset ---> id (REP_fset ---> id P)
-                             (REP_fset
-                               (ABS_fset
-                                 (h # REP_fset (ABS_fset t)))))))) \<longrightarrow>
-               Ball (Respects op \<approx>)
-                (ABS_fset ---> id
-                  (REP_fset ---> id
-                    (\<lambda>l\<Colon>'a list.
-                        ABS_fset ---> id (REP_fset ---> id P)
-                         (REP_fset (ABS_fset l))))))))"
-
-apply (rule APPLY_RSP_I3)
-term "Ball (Respects op \<approx> ===> op =)"
-thm APPLY_RSP_I [of _ "Ball (Respects op \<approx> ===> op =)"]
-
-thm APPLY_RSP
-
-.
-
-apply (tactic {* Cong_Tac.cong_tac @{thm APPLY_RSP_I} 1 *} )
-
-apply (tactic {* match_tac @{thms APPLY_RSP_I} 1 *})
-  .
-
-apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"])
-apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="])
-term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
-thm LAMBDA_PRS1[symmetric]
-(*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*)
-apply (unfold Ball_def)
-apply (simp only: IN_RESPECTS)
-apply (simp only:list_eq_refl)
-apply (unfold id_def)
-(*apply (simp only: FUN_MAP_I)*)
-apply (simp)
-apply (simp only: QUOT_TYPE_I_fset.thm10)
-..
-apply (simp add:IN_RESPECTS)
-
-
-
-
-apply (simp add: QUOT_TYPE_I_fset.R_trans2)
-
-apply (rule ext)
-apply (simp add:QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *} )
-apply (simp add:cons_preserves)
-
 
 
 (*prove aaa: {* (Thm.term_of cgoal2) *}




