src/HOL/thy_syntax.ML
changeset 3403 6cc663f6d62e
parent 3345 4d888ddd6284
child 3456 fdb1768ebd3e
equal deleted inserted replaced
3402:9477a6410fe1 3403:6cc663f6d62e
    80           \ end;\n\n\
    80           \ end;\n\n\
    81           \structure " ^ intrnl_name ^ " = struct end;\n\n"
    81           \structure " ^ intrnl_name ^ " = struct end;\n\n"
    82          )
    82          )
    83       end
    83       end
    84     val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    84     val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    85     fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
    85     fun optstring s = optional (s $$-- string >> trim) "[]"
    86   in
    86   in
    87     repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
    87     repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
    88       >> mk_params
    88       >> mk_params
    89   end;
    89   end;
    90 
    90 
   229 
   229 
   230 (** rec: interface to Slind's TFL **)
   230 (** rec: interface to Slind's TFL **)
   231 
   231 
   232 
   232 
   233 (*fname: name of function being defined; rel: well-founded relation*)
   233 (*fname: name of function being defined; rel: well-founded relation*)
   234 fun mk_rec_decl ((fname, rel), axms) =
   234 fun mk_rec_decl (((fname, rel), ss), axms) =
   235   let val fid = trim fname
   235   let val fid = trim fname
   236       val intrnl_name = fid ^ "_Intrnl"
   236       val intrnl_name = fid ^ "_Intrnl"
   237   in
   237   in
   238 	 (";\n\n\
   238 	 (";\n\n\
   239           \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   239           \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   244          ,
   244          ,
   245           "structure " ^ fid ^ " =\n\
   245           "structure " ^ fid ^ " =\n\
   246           \  struct\n\
   246           \  struct\n\
   247           \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
   247           \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
   248           \  val {rules, induct, tcs} = \n\
   248           \  val {rules, induct, tcs} = \n\
   249           \    \t Tfl.simplify_defn(thy, (" ^ quote fid ^ 
   249           \    \t Tfl.simplify_defn (" ^ ss ^ ") (thy, (" ^ quote fid ^ 
   250 					  ", pats_" ^ intrnl_name ^ "))\n\
   250 					  ", pats_" ^ intrnl_name ^ "))\n\
   251           \  end;\n\
   251           \  end;\n\
   252           \val pats_" ^ intrnl_name ^ " = ();\n")
   252           \val pats_" ^ intrnl_name ^ " = ();\n")
   253   end;
   253   end;
   254 
   254 
   255 val rec_decl = (name -- string -- repeat1 string >> mk_rec_decl) ;
   255 val rec_decl = (name -- string -- 
       
   256 		optional ("simpset" $$-- string >> trim) "!simpset" -- 
       
   257 		repeat1 string >> mk_rec_decl) ;
   256 
   258 
   257 
   259 
   258 
   260 
   259 
   261 
   260 
   262 
   261 (** sections **)
   263 (** sections **)
   262 
   264 
   263 val user_keywords = ["intrs", "monos", "con_defs", "|"];
   265 val user_keywords = ["intrs", "monos", "con_defs", "simpset", "|"];
   264 
   266 
   265 val user_sections =
   267 val user_sections =
   266  [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
   268  [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
   267   ("inductive", inductive_decl ""),
   269   ("inductive", inductive_decl ""),
   268   ("coinductive", inductive_decl "Co"),
   270   ("coinductive", inductive_decl "Co"),