# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255713665 -7200
# Node ID 3cdb743b76059aa2d8fe7a673fa77348f974da7a
# Parent  e3a963e6418bdfcde34064fb48e839cc91ab4a4b
Fighting with the instantiation

diff -r e3a963e6418b -r 3cdb743b7605 QuotMain.thy
--- a/QuotMain.thy	Fri Oct 16 17:05:52 2009 +0200
+++ b/QuotMain.thy	Fri Oct 16 19:21:05 2009 +0200
@@ -856,7 +856,7 @@
 
 ML {*
 fun build_goal ctxt thm cons rty qty =
-  Logic.mk_equals ((build_goal_term ctxt thm cons rty qty), (Thm.prop_of thm))
+  Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))
 *}
 
 ML {*
@@ -1162,13 +1162,19 @@
 *}
 
 thm list.induct
-ML {* atomize_thm @{thm list.induct} *}
+lemma list_induct_hol4:
+  fixes P :: "'a list \<Rightarrow> bool"
+  assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
+  shows "(\<forall>l. (P l))"
+  sorry
+
+ML {* atomize_thm @{thm list_induct_hol4} *}
 
 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
   trm == new_trm
 *)
 
-ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
+ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct_hol4}) *}
 
 prove list_induct_r: {*
  Logic.mk_implies
@@ -1186,65 +1192,94 @@
 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"]
+lemmas APPLY_RSP_I2 = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "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"]
+thm REP_ABS_RSP(2)
+lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
 
 prove trm
+thm UNION_def
 apply (atomize(full))
 apply (simp only: id_def[symmetric])
 
+(* APPLY_RSP_TAC *)
 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
+  val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
+  val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I" }))
+  val m = Thm.match (tc', gc')
+  val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" }
  *}
-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
+  val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
+  val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" }))
+  val m = Thm.match (tc', gc')
+  val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" }
  *}
+apply (tactic {* rtac t2 1 *})
+prefer 2
+
+(* LAMBDA_RES_TAC *)
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+
+(* MK_COMB_TAC *)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+(* MK_COMB_TAC *)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+(* REFL_TAC *)
+apply (simp)
+(* MK_COMB_TAC *)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+(* MK_COMB_TAC *)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+(* REFL_TAC *)
+apply (simp)
+(* APPLY_RSP_TAC *)
+ML_prf {* Isar.goal () *}
+ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_I2" } *}
 ML_prf {*
-  fun dest_cbinop t =
-    let
-      val (t2, rhs) = Thm.dest_comb t;
-      val (bop, lhs) = Thm.dest_comb t2;
-    in
-      (bop, (lhs, rhs))
-    end
+  val (tc') = (Logic.strip_assums_concl (prop_of t));
+  val ps = Logic.strip_params (prop_of t)
+  val tt = Term.list_abs (ps, tc')
+  val ct = cterm_of @{theory} tt
+*}
+ML_prf {*
+  val goal = hd (prems_of (Isar.goal ()))
+  val goalc = Logic.strip_assums_concl goal
+*}
+ML_prf {*
+  val ps = Logic.strip_params goal
+  val goal' = cterm_of @{theory} (Term.list_abs (ps, goalc))
+*}
+ML_prf {* ct; goal' *}
+
+*)
+ML_prf {*
+val pat = @{cpat "\<lambda>x y. (?f6 x y (?x6 x y) = ?g6 x y (?y6 x y))"}
+val arg = @{cterm "\<lambda>x y. (x [] = y [])"}
 *}
 
-ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
-ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *}
-ML_prf {* val mr = Thm.match (r1, r2) *}
+ML_prf {*
+val pat = @{cpat "(?f6 x y (?x6) = ?g6 x y (?y6))"}
+val arg = @{cterm "(x [] = y [])"}
+*}
 
+ML_prf {*
+  val m = Thm.match (pat, arg)
+*}
 
-ML_prf {* val m = Thm.match (tc', gc') *}
-ML_prf {* val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" } *}
+ML_prf {*
+  val m = Thm.match (ct, goal')
+  val t2 = Drule.instantiate m @{thm "APPLY_RSP_I2" }
+ *}
 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)
-
+thm APPLY_RSP
 sorry
 
 thm list.recs(2)