# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255704661 -7200
# Node ID 0d6d37d0589dd8a73ce45a22a0de291ba4dbb8bd
# Parent  4683292581bc201c1562e0fbece9500067427b6d
Progressing with the proof

diff -r 4683292581bc -r 0d6d37d0589d QuotMain.thy
--- a/QuotMain.thy	Fri Oct 16 10:54:31 2009 +0200
+++ b/QuotMain.thy	Fri Oct 16 16:51:01 2009 +0200
@@ -1184,9 +1184,57 @@
 
 ML {* val thm = @{thm list_induct_r} OF [li] *}
 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
+thm APPLY_RSP
+lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
+
+thm REP_ABS_RSP
+lemmas REP_ABS_RSP_I = REP_ABS_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
+
 prove trm
+apply (atomize(full))
+
+ML_prf {*
+  val gc = Subgoal.focus @{context} 1 (Isar.goal ())
+  |> fst
+  |> #concl
+  val tc = cterm_of @{theory} (concl_of ( @{thm "APPLY_RSP_I" }))
+  val (_, tc') = Thm.dest_comb tc
+  val (_, gc') = Thm.dest_comb gc
+ *}
+ML_prf {* val m = Thm.match (tc', gc') *}
+ML_prf {* val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" } *}
+(* APPLY_RSP_TAC *)
+apply (tactic {* rtac t2 1 *})
+prefer 4
+(* ABS_REP_RSP_TAC *)
+ML_prf {*
+  val gc = Subgoal.focus @{context} 1 (Isar.goal ())
+  |> fst
+  |> #concl
+  val tc = cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" })
+  val (_, tc') = Thm.dest_comb tc
+  val (_, gc') = Thm.dest_comb gc
+ *}
+
+ML_prf {* val m = Thm.match (tc', gc') *}
+ML_prf {* val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" } *}
+apply (tactic {* rtac t2 1 *})
+
+thm QUOT_TYPE.REP_ABS_rsp(2)
+
+(* LAMBDA_RES_TAC *)
+
+
+apply (simp)
+apply (simp only: FUN_REL.simps)
+
+apply (unfold FUN_REL_def)
+
 sorry
 
+thm list.recs(2)
+
+
 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
 prove card1_suc_r: {*
@@ -1299,8 +1347,120 @@
    = 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 =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]
+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))))"
@@ -1343,3 +1503,4 @@
 *)
 
 end
+ 
diff -r 4683292581bc -r 0d6d37d0589d QuotScript.thy
--- a/QuotScript.thy	Fri Oct 16 10:54:31 2009 +0200
+++ b/QuotScript.thy	Fri Oct 16 16:51:01 2009 +0200
@@ -103,17 +103,18 @@
   "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
 
 fun
-  fun_map 
+  fun_map
 where
   "fun_map f g h x = g (h (f x))"
 
+
 abbreviation
-  fun_map_syn ("_ ---> _")
+  fun_map_syn (infixr "--->" 55)
 where
-  "f ---> g \<equiv> fun_map f g"  
+  "f ---> g \<equiv> fun_map f g"
 
 lemma FUN_MAP_I:
-  shows "(\<lambda>x. x ---> \<lambda>x. x) = (\<lambda>x. x)"
+  shows "((\<lambda>x. x) ---> (\<lambda>x. x)) = (\<lambda>x. x)"
 by (simp add: expand_fun_eq)
 
 lemma IN_FUN: