AddSEs [lkss.extI, lkne.ilI, lkne.irI] ; AddSIs [lkne.axiom] ; Addsimps [lkne.axiom] ; (* 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.elim 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.elim 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.elim 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.elim 1), Auto_tac]) ; val () = qed_goal_spec_mp "lk_ext_ext" lk.thy "psc : lkss --> pscmap (extend pr) psc : lkss" (fn _ => [ (case_tac "pr" 1), (rtac impI 1), (etac lkss.elim 1), Clarify_tac 1, (simp_tac (esimps [map_compose RS sym, extend_comp, extend_comp_ext]) 1), (dtac lkss.extI 1), Full_simp_tac 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.intrs RL [lkss.extI]) ; val lkss_axiom = (simplify (simpset ())) lkss_axiom' ; fun mk_rule_lk intr = map (simplify (simpset ())) ([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] ; *)