ProgTutorial/Tactical.thy
changeset 511 386375b7a22a
parent 510 500d1abbc98c
parent 509 dcefee89bf62
child 512 231ec0c45bff
equal deleted inserted replaced
510:500d1abbc98c 511:386375b7a22a
  2112   "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for
  2112   "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for
  2113   @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output.
  2113   @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output.
  2114   If we get hold of the ``raw'' representation of the produced theorem, 
  2114   If we get hold of the ``raw'' representation of the produced theorem, 
  2115   we obtain the expected result.
  2115   we obtain the expected result.
  2116 
  2116 
  2117 
       
  2118   @{ML_response [display,gray]
  2117   @{ML_response [display,gray]
  2119 "let
  2118 "let
  2120   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
  2119   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
  2121   val two = @{cterm \"2::nat\"}
  2120   val two = @{cterm \"2::nat\"}
  2122   val ten = @{cterm \"10::nat\"}
  2121   val ten = @{cterm \"10::nat\"}
  2125   Thm.prop_of (Thm.beta_conversion true ctrm)
  2124   Thm.prop_of (Thm.beta_conversion true ctrm)
  2126 end"
  2125 end"
  2127 "Const (\"==\",\<dots>) $ 
  2126 "Const (\"==\",\<dots>) $ 
  2128   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
  2127   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
  2129     (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
  2128     (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
       
  2129 
       
  2130   or in the pretty-printed form
       
  2131 
       
  2132   @{ML_response_fake [display,gray]
       
  2133 "let
       
  2134   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
       
  2135   val two = @{cterm \"2::nat\"}
       
  2136   val ten = @{cterm \"10::nat\"}
       
  2137   val ctrm = Thm.capply (Thm.capply add two) ten
       
  2138   val ctxt = @{context}
       
  2139     |> Config.put eta_contract false 
       
  2140     |> Config.put show_abbrevs false 
       
  2141 in
       
  2142   Thm.prop_of (Thm.beta_conversion true ctrm)
       
  2143   |> pretty_term ctxt
       
  2144   |> pwriteln
       
  2145 end"
       
  2146 "(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10"}
  2130 
  2147 
  2131   The argument @{ML true} in @{ML beta_conversion in Thm} indicates that 
  2148   The argument @{ML true} in @{ML beta_conversion in Thm} indicates that 
  2132   the right-hand side should be fully beta-normalised. If instead 
  2149   the right-hand side should be fully beta-normalised. If instead 
  2133   @{ML false} is given, then only a single beta-reduction is performed 
  2150   @{ML false} is given, then only a single beta-reduction is performed 
  2134   on the outer-most level. 
  2151   on the outer-most level.