1 theory Essential

     2 imports FirstStep

     3 begin

     4 

     5 ML {*

     6 fun pretty_helper aux env =

     7   env |> Vartab.dest

     8       |> map aux

     9       |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])

    10       |> Pretty.enum "," "[" "]"

    11       |> pwriteln

    12 

    13 fun pretty_tyenv ctxt tyenv =

    14 let

    15   fun get_typs (v, (s, T)) = (TVar (v, s), T)

    16   val print = pairself (pretty_typ ctxt)

    17 in

    18   pretty_helper (print o get_typs) tyenv

    19 end

    20 

    21 fun pretty_env ctxt env =

    22 let

    23    fun get_trms (v, (T, t)) = (Var (v, T), t)

    24    val print = pairself (pretty_term ctxt)

    25 in

    26    pretty_helper (print o get_trms) env

    27 end

    28 

    29 fun prep_trm thy (x, (T, t)) =

    30   (cterm_of thy (Var (x, T)), cterm_of thy t)

    31 

    32 fun prep_ty thy (x, (S, ty)) =

    33   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)

    34 

    35 fun matcher_inst thy pat trm i =

    36   let

    37      val univ = Unify.matchers thy [(pat, trm)]

    38      val env = nth (Seq.list_of univ) i

    39      val tenv = Vartab.dest (Envir.term_env env)

    40      val tyenv = Vartab.dest (Envir.type_env env)

    41   in

    42      (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)

    43   end

    44 *}

    45 

    46 ML {*

    47   let

    48      val pat = Logic.strip_imp_concl (prop_of @{thm spec})

    49      val trm = @{term "Trueprop (Q True)"}

    50      val inst = matcher_inst @{theory} pat trm 1

    51   in

    52      Drule.instantiate_normalize inst @{thm spec}

    53   end

    54 *}

    55 

    56 ML {*

    57 let

    58    val c = Const (@{const_name "plus"}, dummyT)

    59    val o = @{term "1::nat"}

    60    val v = Free ("x", dummyT)

    61 in

    62    Syntax.check_term @{context} (c $ o $ v)

    63 end

    64 *}

    65 

    66 ML {*

    67    val my_thm =

    68    let

    69       val assm1 = @{cprop "\<And> (x::nat). P x ==> Q x"}

    70       val assm2 = @{cprop "(P::nat => bool) t"}

    71 

    72       val Pt_implies_Qt =

    73         Thm.assume assm1

    74         |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

    75         |> Thm.forall_elim @{cterm "t::nat"}

    76         |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

    77 

    78       val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)

    79                |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

    80    in

    81       Qt

    82       |> Thm.implies_intr assm2

    83       |> Thm.implies_intr assm1

    84    end

    85 *}

    86 

    87 local_setup {*

    88   Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd  

    89 *}

    90 

    91 local_setup {*

    92   Local_Theory.note ((@{binding "my_thm_simp"},

    93         [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd

    94 *}

    95 

    96 (* pp 62 *)

    97 

    98 lemma

    99   shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C"

   100   and   foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry

   101 

   102 ML {*

   103    Thm.reflexive @{cterm "True"}

   104     |> Simplifier.rewrite_rule [@{thm True_def}]

   105     |> pretty_thm @{context}

   106     |> pwriteln

   107 *}

   108 

   109 ML {*

   110 Object_Logic.rulify @{thm foo_test2}

   111 *}

   112 

   113 

   114 ML {*

   115   val thm =    @{thm foo_test1};

   116   thm 

   117   |> cprop_of

   118   |> Object_Logic.atomize

   119   |> (fn x => Raw_Simplifier.rewrite_rule [x] thm)

   120 *}

   121 

   122 ML {*

   123   val thm = @{thm list.induct} |> forall_intr_vars;

   124   thm |> forall_intr_vars |> cprop_of |> Object_Logic.atomize

   125   |> (fn x => Raw_Simplifier.rewrite_rule [x] thm)

   126 *}

   127 

   128 ML {*

   129 fun atomize_thm thm =

   130 let

   131   val thm' = forall_intr_vars thm

   132   val thm'' = Object_Logic.atomize (cprop_of thm')

   133 in

   134   Raw_Simplifier.rewrite_rule [thm''] thm'

   135 end

   136 *}

   137 

   138 ML {*

   139   @{thm list.induct} |> atomize_thm

   140 *}

   141 

   142 ML {*

   143    Skip_Proof.make_thm @{theory} @{prop "True = False"}

   144 *}

   145 

   146 ML {*

   147 fun pthms_of (PBody {thms, ...}) = map #2 thms

   148 val get_names = map #1 o pthms_of

   149 val get_pbodies = map (Future.join o #3) o pthms_of

   150 *}

   151 

   152 lemma my_conjIa:

   153 shows "A \<and> B \<Longrightarrow> A \<and> B"

   154 apply(rule conjI)

   155 apply(drule conjunct1)

   156 apply(assumption)

   157 apply(drule conjunct2)

   158 apply(assumption)

   159 done

   160 

   161 lemma my_conjIb:

   162 shows "A \<and> B \<Longrightarrow> A \<and> B"

   163 apply(assumption)

   164 done

   165 

   166 lemma my_conjIc:

   167 shows "A \<and> B \<Longrightarrow> A \<and> B"

   168 apply(auto)

   169 done

   170 

   171 

   172 ML {*

   173 @{thm my_conjIa}

   174   |> Thm.proof_body_of

   175   |> get_names

   176 *}

   177 

   178 ML {*

   179 @{thm my_conjIa}

   180   |> Thm.proof_body_of

   181   |> get_pbodies

   182   |> map get_names

   183   |> List.concat

   184 *}

   185 

   186 ML {*

   187 @{thm my_conjIb}

   188  |> Thm.proof_body_of

   189  |> get_pbodies

   190  |> map get_names

   191  |> List.concat

   192 *}

   193 

   194 ML {*

   195 @{thm my_conjIc}

   196   |> Thm.proof_body_of

   197   |> get_pbodies

   198   |> map get_names

   199   |> List.concat

   200 *}

   201 

   202 ML {*

   203 @{thm my_conjIa}

   204   |> Thm.proof_body_of

   205   |> get_pbodies

   206   |> map get_pbodies

   207   |> (map o map) get_names

   208   |> List.concat

   209   |> List.concat

   210   |> duplicates (op=)

   211 *}

   212 

   213 end