--- a/Attic/Unused.thy	Sun Jun 19 13:14:37 2011 +0900
+++ b/Attic/Unused.thy	Mon Jun 20 08:50:13 2011 +0900
@@ -1,164 +1,11 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
-function(sequential)
-    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
-and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
-and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
-where
-  a1: "(Type) \<approx>ki (Type) = True"
-| a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
-| "_ \<approx>ki _ = False"
-| a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"
-| a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
-| a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
-| "_ \<approx>ty _ = False"
-| a6: "(Const i) \<approx>tr (Const j) = (i = j)"
-| a7: "(Var x) \<approx>tr (Var y) = (x = y)"
-| a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
-| a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
-| "_ \<approx>tr _ = False"
-apply (pat_completeness)
-apply simp_all
-done
-termination
-by (size_change)
-
-
-
-lemma regularize_to_injection:
-  shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
-  by(auto simp add: QUOT_TRUE_def)
-
 syntax
   "Bex1_rel" :: "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"  == "Bex1_rel 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;