--- a/progtut/Essential.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,213 +0,0 @@
-theory Essential
-imports FirstStep
-begin
-
-ML {*
-fun pretty_helper aux env =
-  env |> Vartab.dest
-      |> map aux
-      |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])
-      |> Pretty.enum "," "[" "]"
-      |> pwriteln
-
-fun pretty_tyenv ctxt tyenv =
-let
-  fun get_typs (v, (s, T)) = (TVar (v, s), T)
-  val print = pairself (pretty_typ ctxt)
-in
-  pretty_helper (print o get_typs) tyenv
-end
-
-fun pretty_env ctxt env =
-let
-   fun get_trms (v, (T, t)) = (Var (v, T), t)
-   val print = pairself (pretty_term ctxt)
-in
-   pretty_helper (print o get_trms) env
-end
-
-fun prep_trm thy (x, (T, t)) =
-  (cterm_of thy (Var (x, T)), cterm_of thy t)
-
-fun prep_ty thy (x, (S, ty)) =
-  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
-
-fun matcher_inst thy pat trm i =
-  let
-     val univ = Unify.matchers thy [(pat, trm)]
-     val env = nth (Seq.list_of univ) i
-     val tenv = Vartab.dest (Envir.term_env env)
-     val tyenv = Vartab.dest (Envir.type_env env)
-  in
-     (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
-  end
-*}
-
-ML {*
-  let
-     val pat = Logic.strip_imp_concl (prop_of @{thm spec})
-     val trm = @{term "Trueprop (Q True)"}
-     val inst = matcher_inst @{theory} pat trm 1
-  in
-     Drule.instantiate_normalize inst @{thm spec}
-  end
-*}
-
-ML {*
-let
-   val c = Const (@{const_name "plus"}, dummyT)
-   val o = @{term "1::nat"}
-   val v = Free ("x", dummyT)
-in
-   Syntax.check_term @{context} (c $ o $ v)
-end
-*}
-
-ML {*
-   val my_thm =
-   let
-      val assm1 = @{cprop "\<And> (x::nat). P x ==> Q x"}
-      val assm2 = @{cprop "(P::nat => bool) t"}
-
-      val Pt_implies_Qt =
-        Thm.assume assm1
-        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-        |> Thm.forall_elim @{cterm "t::nat"}
-        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-
-      val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)
-               |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-   in
-      Qt
-      |> Thm.implies_intr assm2
-      |> Thm.implies_intr assm1
-   end
-*}
-
-local_setup {*
-  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd  
-*}
-
-local_setup {*
-  Local_Theory.note ((@{binding "my_thm_simp"},
-        [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd
-*}
-
-(* pp 62 *)
-
-lemma
-  shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C"
-  and   foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry
-
-ML {*
-   Thm.reflexive @{cterm "True"}
-    |> Simplifier.rewrite_rule [@{thm True_def}]
-    |> pretty_thm @{context}
-    |> pwriteln
-*}
-
-ML {*
-Object_Logic.rulify @{thm foo_test2}
-*}
-
-
-ML {*
-  val thm =    @{thm foo_test1};
-  thm 
-  |> cprop_of
-  |> Object_Logic.atomize
-  |> (fn x => Raw_Simplifier.rewrite_rule [x] thm)
-*}
-
-ML {*
-  val thm = @{thm list.induct} |> forall_intr_vars;
-  thm |> forall_intr_vars |> cprop_of |> Object_Logic.atomize
-  |> (fn x => Raw_Simplifier.rewrite_rule [x] thm)
-*}
-
-ML {*
-fun atomize_thm thm =
-let
-  val thm' = forall_intr_vars thm
-  val thm'' = Object_Logic.atomize (cprop_of thm')
-in
-  Raw_Simplifier.rewrite_rule [thm''] thm'
-end
-*}
-
-ML {*
-  @{thm list.induct} |> atomize_thm
-*}
-
-ML {*
-   Skip_Proof.make_thm @{theory} @{prop "True = False"}
-*}
-
-ML {*
-fun pthms_of (PBody {thms, ...}) = map #2 thms
-val get_names = map #1 o pthms_of
-val get_pbodies = map (Future.join o #3) o pthms_of
-*}
-
-lemma my_conjIa:
-shows "A \<and> B \<Longrightarrow> A \<and> B"
-apply(rule conjI)
-apply(drule conjunct1)
-apply(assumption)
-apply(drule conjunct2)
-apply(assumption)
-done
-
-lemma my_conjIb:
-shows "A \<and> B \<Longrightarrow> A \<and> B"
-apply(assumption)
-done
-
-lemma my_conjIc:
-shows "A \<and> B \<Longrightarrow> A \<and> B"
-apply(auto)
-done
-
-
-ML {*
-@{thm my_conjIa}
-  |> Thm.proof_body_of
-  |> get_names
-*}
-
-ML {*
-@{thm my_conjIa}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_names
-  |> List.concat
-*}
-
-ML {*
-@{thm my_conjIb}
- |> Thm.proof_body_of
- |> get_pbodies
- |> map get_names
- |> List.concat
-*}
-
-ML {*
-@{thm my_conjIc}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_names
-  |> List.concat
-*}
-
-ML {*
-@{thm my_conjIa}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_pbodies
-  |> (map o map) get_names
-  |> List.concat
-  |> List.concat
-  |> duplicates (op=)
-*}
-
-end
\ No newline at end of file