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 *)

ML {*
   Thm.reflexive @{cterm "True"}
    |> Simplifier.rewrite_rule [@{thm True_def}]
    |> pretty_thm @{context}
    |> pwriteln
*}


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