structure lk = struct val thy = theory "lk" end ; use_legacy_bindings lk.thy ; AddSEs [lkss.extI, lkne.ilI, lkne.irI] ; AddSIs [lkne.axiom] ; Addsimps [lkne.axiom] ; val _ = qed_goal "lkss_extrs" lk.thy "lkss = extrs lkne" (fn _ => [ Safe_tac, (etac lkss.elims 1), (etac extrs_E' 2), Asm_simp_tac 1, Fast_tac 1, (dtac lkss.extI 1), (asm_simp_tac HOL_ss 1) ]) ; (* val () = qed_goal_spec_mp "concl_il" lk.thy "(ps, Y |- X) : lkil --> X = {#} & (EX A. Y = {#A#} & \ \ (ALL U V. (U |- V) : set ps --> A : U))" (fn _ => [ (rtac impI 1), (etac lkil.elims 1), Auto_tac]) ; val () = qed_goal_spec_mp "concl_ir" lk.thy "(ps, X |- Y) : lkir --> X = {#} & (EX A. Y = {#A#} & \ \ (ALL U V. (U |- V) : set ps --> A : V))" (fn _ => [ (rtac impI 1), (etac lkir.elims 1), Auto_tac]) ; *) val () = qed_goal_spec_mp "lk_concl_irc" lk.thy "(ps, c) : lkir --> (EX A. c = ({#} |- {#A#}))" (fn _ => [ (rtac impI 1), (etac lkir.elims 1), Auto_tac]) ; val () = qed_goal_spec_mp "lk_concl_ilc" lk.thy "(ps, c) : lkil --> (EX A. c = ({#A#} |- {#}))" (fn _ => [ (rtac impI 1), (etac lkil.elims 1), Auto_tac]) ; val () = qed_goal_spec_mp "lk_ext_ext" lk.thy "psc : lkss --> pscmap (extend pr) psc : lkss" (fn _ => [ (force_tac (ces [ext_extrs], esimps [lkss_extrs]) 1) ]) ; val () = qed_goal_spec_mp "lk_extI'" lk.thy "(ps, c) : lkne --> ?P" (fn _ => [ (rtac impI 1), (dtac lkss.extI 1), (safe_asm_full_simp_tac (simpset()) 1), atac 1]) ; val () = qed_goal_spec_mp "lk_extI2" lk.thy "(ps, X |- Y) : lkne --> ?P" (fn _ => [ (rtac impI 1), (dtac lkss.extI 1), (safe_asm_full_simp_tac (simpset()) 1), atac 1]) ; (* develop explicit rules *) val lkss_intrs as [lkss_axiom', lkil_lkss', lkir_lkss'] = (lkne.intros RL [lkss.extI]) ; val lkss_axiom = (simplify (simpset ())) lkss_axiom' ; fun mk_rule_lk intr = map (simplify (esimps [extend_def])) ([intr] RL lkss_intrs) ; val () = qed_goal_spec_mp "lk_simpI" lk.thy "psc : lkne --> psc : lkss" (fn _ => [ (rtac impI 1), (dtac lkss.extI 1), (case_tac "psc" 1), (Asm_full_simp_tac 1), (etac mem_same 1), Safe_tac, (rtac extend_empty' 2), (simp_tac (esimps [id_def]) 1)]) ; val map_eq_conv = thm "map_eq_conv" ; (* no longer used fun fetacs _ = [ (Clarify_tac 1), (dresolve_tac [concl_il, concl_ir] 1), (simp_tac (esimps [pscmap_def, map_ext' RS sym]) 1), (Clarify_tac 1), (case_tac "x" 1), Force_tac 1] ; val () = qed_goal_spec_mp "il_ext" lk.thy "rl = (ps, {#A#} |- X) --> rl : lkil --> \ \ pscmap (extend (U, V)) rl = pscmap (extend (U - {#A#}, V)) rl" fetacs ; val () = qed_goal_spec_mp "ir_ext" lk.thy "rl = (ps, X |- {#A#}) --> rl : lkir --> \ \ pscmap (extend (U, V)) rl = pscmap (extend (U, V - {#A#})) rl" fetacs ; val ilr_exts = [il_ext, ir_ext] ; val ilr_exts' as [il_ext', ir_ext'] = ([refl] RL ilr_exts) ; val ilr_extps as [il_extp, ir_extp] = map (simplify (esimps [] delsimps [map_eq_conv])) ilr_exts' ; val ilr_extas = ilr_extps RL [map_ext' RS iffD2 RS bspec] ; *)