| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Forcing/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 1 kB |
|
Quelle Renaming_Auto.thySprache: Isabelle |
|||||||||||||||
|
theory Renaming_Auto imports Renaming Utils ZF.Finite ZF.List keywords "rename" :: thy_decl % "ML" and "simple_rename" :: thy_decl % "ML" and "src" and "tgt" abbrevs "simple_rename" = "" begin lemmas app_fun = apply_iff[THEN iffD1] lemmas nat_succI = nat_succ_iff[THEN iffD2] ML_file ‹renaming.ML› ML‹ fun renaming_def mk_ren name from to ctxt = let val to = to |> Syntax.read_term ctxt val from = from |> Syntax.read_term ctxt val (tc_lemma,action_lemma,fvs,r) = mk_ren from to ctxt val (tc_lemma,action_lemma) = (Renaming.fix_vars tc_lemma fvs ctxt, Renaming.fix_vars action_lemma fvs ctxt) val ren_fun_name = Binding.name (name ^ "_fn") val ren_fun_def = Binding.name (name ^ "_fn_def") val ren_thm = Binding.name (name ^ "_thm") in Local_Theory.note ((ren_thm, []), [tc_lemma,action_lemma]) ctxt |> snd |> Local_Theory.define ((ren_fun_name, NoSyn), ((ren_fun_def, []), r)) |> snd end; › ML‹ val ren_parser = Parse.position (Parse.string -- (Parse.$$$ "src" |-- Parse.string --| Parse.$$$ "tgt" -- Parse.string)); val _ = Outer_Syntax.local_theory 🍋‹rename› "ML setup for synthetic definitions" (ren_parser >> (fn ((name,(from,to)),_) => renaming_def Renaming.sum_rename name val _ = Outer_Syntax.local_theory 🍋‹simple_rename› "ML setup for synthetic definitions" (ren_parser >> (fn ((name,(from,to)),_) => renaming_def Renaming.ren_thm name fr end
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09