--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/progtut/Essential.thy~	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,213 @@
+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