diff -r fa810f01f7b5 -r 25c4223635f4 Attic/Unused.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Unused.thy	Tue Jan 26 20:12:41 2010 +0100
@@ -0,0 +1,161 @@
+(*notation ( output) "prop" ("#_" [1000] 1000) *)
+notation ( output) "Trueprop" ("#_" [1000] 1000)
+
+lemma regularize_to_injection:
+  shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
+  by(auto simp add: QUOT_TRUE_def)
+
+syntax
+  "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
+translations
+  "\<exists>!!x\<in>A. P"  == "Bexeq A (%x. P)"
+
+
+(* Atomize infrastructure *)
+(* FIXME/TODO: is this really needed? *)
+(*
+lemma atomize_eqv:
+  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+proof
+  assume "A \<equiv> B"
+  then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+  assume *: "Trueprop A \<equiv> Trueprop B"
+  have "A = B"
+  proof (cases A)
+    case True
+    have "A" by fact
+    then show "A = B" using * by simp
+  next
+    case False
+    have "\<not>A" by fact
+    then show "A = B" using * by auto
+  qed
+  then show "A \<equiv> B" by (rule eq_reflection)
+qed
+*)
+
+
+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 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}
+    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 split_binop_tac n thm =
+    let
+      val concl = Thm.cprem_of thm n;
+      val (_, cconcl) = Thm.dest_comb concl;
+      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
+      handle CTERM _ => Seq.empty
+*}
+
+
+lemma trueprop_cong:
+  shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
+  by auto
+
+lemma list_induct_hol4:
+  fixes P :: "'a list \<Rightarrow> bool"
+  assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
+  shows "\<forall>l. (P l)"
+  using a
+  apply (rule_tac allI)
+  apply (induct_tac "l")
+  apply (simp)
+  apply (metis)
+  done
+
+ML {*
+val no_vars = Thm.rule_attribute (fn context => fn th =>
+  let
+    val ctxt = Variable.set_body false (Context.proof_of context);
+    val ((_, [th']), _) = Variable.import true [th] ctxt;
+  in th' end);
+*}
+
+(*lemma equality_twice:
+  "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+by auto*)
+
+
+(*interpretation code *)
+(*val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
+  val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
+  val eqn1i = Thm.prop_of (symmetric eqn1pre)
+  val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
+  val eqn2i = Thm.prop_of (symmetric eqn2pre)
+
+  val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
+  val exp_term = Morphism.term exp_morphism;
+  val exp = Morphism.thm exp_morphism;
+
+  val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
+    ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
+  val mthdt = Method.Basic (fn _ => mthd)
+  val bymt = Proof.global_terminal_proof (mthdt, NONE)
+  val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
+    Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*)
+
+(*||> Local_Theory.theory (fn thy =>
+      let
+        val global_eqns = map exp_term [eqn2i, eqn1i];
+        (* Not sure if the following context should not be used *)
+        val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
+        val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
+      in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*)