# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1253181966 -7200
# Node ID ce522150c1f785813f6fcfe851c1ee952099e7f7
# Parent  55b646c6c4cdc91fce54c0674809699781b322e4
Infrastructure for the tactic

diff -r 55b646c6c4cd -r ce522150c1f7 QuotMain.thy
--- a/QuotMain.thy	Wed Sep 16 11:50:41 2009 +0200
+++ b/QuotMain.thy	Thu Sep 17 12:06:06 2009 +0200
@@ -571,6 +571,8 @@
 term UNION
 thm UNION_def
 
+(* Maybe the infrastructure should not allow this kind of definition, without showing that
+   the relation respects lenght... *)
 local_setup {*
   make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
@@ -626,6 +628,7 @@
 term membship
 term IN
 thm IN_def
+ML {* unlam_def @{context} @{context} @{thm IN_def} *}
 
 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
@@ -669,7 +672,7 @@
   apply(simp add: list_eq_sym)
 done
 
-lemma yyy :
+lemma yyy:
   shows "
     (
      (UNION EMPTY s = s) &
@@ -683,7 +686,7 @@
   apply(rule_tac f="(op =)" in arg_cong2)
   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule append_respects_fst)
-  apply(simp only:QUOT_TYPE_I_fset.REP_ABS_rsp)
+  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
   apply(rule list_eq_sym)
   apply(simp)
   apply(rule_tac f="(op =)" in arg_cong2)
@@ -743,6 +746,8 @@
 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
 ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
 
+thm m1
+
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
@@ -751,13 +756,13 @@
 *}
 
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
-apply(rule_tac f="(op =)" in arg_cong2)
-unfolding IN_def EMPTY_def
-apply (rule_tac mem_respects)
-apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply (simp_all)
-apply (rule list_eq_sym)
-done
+  apply(rule_tac f="(op =)" in arg_cong2)
+  unfolding IN_def EMPTY_def
+  apply (rule_tac mem_respects)
+  apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
+  apply (simp_all)
+  apply (rule list_eq_sym)
+  done
 
 thm length_append (* Not true but worth checking that the goal is correct *)
 ML {*
@@ -766,6 +771,9 @@
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal)
 *}
+(*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+unfolding CARD_def UNION_def
+apply(rule_tac f="(op =)" in arg_cong2)*)
 
 thm m2
 ML {*
@@ -783,9 +791,68 @@
 apply (rule cons_preserves)
 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (rule list_eq_sym)
-apply(rule_tac f="(op \<or>)" in arg_cong2)
+apply (rule_tac f="(op \<or>)" in arg_cong2)
 apply (simp)
 apply (rule_tac mem_respects)
 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (rule list_eq_sym)
 done
+
+notation ( output) "prop" ("#_" [1000] 1000)
+
+ML {* @{thm arg_cong2} *}
+ML {* rtac *}
+ML {* Term.dest_Const @{term "op ="} *}
+
+ML {*
+  fun dest_cbinop t =
+    let
+      val (t2, rhs) = Thm.dest_comb t;
+      val (bop, lhs) = Thm.dest_comb t2;
+    in
+      (bop, (lhs, rhs))
+    end
+*}
+ML {*
+  fun dest_ceq t =
+    let
+      val (bop, pair) = dest_cbinop t;
+      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
+*}
+ML {*
+  fun foo_conv ctxt t =
+    let
+      val (lhs, rhs) = dest_ceq t;
+      val (bop, _) = dest_cbinop lhs;
+(*      val _ = tracing (Syntax.string_of_term ctxt (Thm.term_of lhs))*)
+    in
+      @{thm arg_cong2}
+    end
+*}
+ML {*
+  fun foo_tac ctxt thm =
+    let
+      val concl = Thm.concl_of thm;
+      val (_, cconcl) = Thm.dest_comb (Thm.cterm_of @{theory} concl);
+      val (_, cconcl) = Thm.dest_comb cconcl;
+      val rewr = foo_conv ctxt cconcl;
+      val _ = tracing (Syntax.string_of_term ctxt (Thm.term_of cconcl))
+    in
+      Seq.single thm
+    end
+*}
+ML {* Thm.assume @{cprop "0 = 0"} *}
+
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+apply (tactic {* foo_tac @{context} *})
+
+(*
+datatype obj1 =
+  OVAR1 "string"
+| OBJ1 "(string * (string \<Rightarrow> obj1)) list"
+| INVOKE1 "obj1 \<Rightarrow> string"
+| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
+*)