(*************************************************************************)
(* Title : Z.thy *)
(* Project : Encoding Z in Isabelle *)
(* Author : A.Brucker, ALU Freiburg, ETH Zürich *)
(* B. Wolff, BISS, ALU Freiburg, ETH Zürich *)
(* This File : Top-level theory of Z encoding in Isabelle/HOL *)
(* $Id: Z.thy,v 1.7 2002/08/05 10:18:56 wolff Exp $ *)
(* Copyright : BISS, University of Bremen *)
(* GMD First, Berlin *)
(* Albert-Ludwigs-Universität Freiburg *)
(* ETH Zürich *)
(* Version : 3.0 *)
(*************************************************************************)
(* ML{*path_add "./lib"; *} *)
header {* Main Theory for the HOL-Z Environment*}
theory Z
imports ZSeqtoList
ZBag
ZPure
ZMethod
begin
section {* Proof Support: The .holz-loader (generated by ZETA) *}
ML{*
val store_sec = ref(ZAbsy.ZSection("",[],[]));
fun register_unit (sec as (ZAbsy.ZSection(name,_,_)))
schemas axdefs conjectures thy_name thy =
let val zenv = ZTheory.get_zenv thy
val imprt' = (thy_name::ZEnv.imports_of zenv)
val zenv' = ZEnv.update_Zenv_by_Imports zenv imprt'
val zenv'' = ZEnv.update_Zenv_by_Unit zenv' (name,sec)
val thy' = fst(PureThy.add_thmss [(("SCHEMAS",schemas),[])]
thy)
val thy'' = fst(PureThy.add_thmss [(("AXDEFS", axdefs),[])]
thy')
val thy''' = fst(PureThy.add_thmss [(("CONJECTURES", conjectures),[])]
thy'')
in ZTheory.put_zenv zenv'' thy''' end
fun check_imports (ZAbsy.ZSection(name,importS,itemS)) thy =
let val thy_name = #Name(ZConversion.unitName name)
val loaded_imports =ZEnv.imports_of(ZTheory.get_zenv thy)
val impnames = map(fn x=> (#Name(ZConversion.unitName x)))importS;
(*Check if parents have already been loaded*)
in case filter(fn x => not(x mem loaded_imports))(impnames) of
[] => thy_name
| S => error("Units: "^(concat S)^" not yet loaded!")
end
fun load_holz thy_file thy =
let val intext = (File.read (Path.unpack(thy_file^".holz")))
handle _ => File.read(Path.unpack(
"holz/"^thy_file^".holz"));
val sec = (use_text Context.ml_output false
("store_sec := "^intext);
!store_sec)
val _ = ZEncoder.init();
val _ = ZConversion.printSec sec;
val thy_name= check_imports sec thy;
val thy' = let val (ZAbsy.ZSection(_,_,itemS)) = sec
in foldl (ZConversion.convItem thy_name)
thy itemS
end
fun thm x = get_thm thy' (Name x)
val thy'' = register_unit
sec
(map thm (!ZEncoder.SCHEMANAMES))
(map thm (!ZEncoder.AXDEFS))
(map thm (!ZEncoder.CONJECTURES))
thy_name
thy'
val _ = (ZEncoder.ZENV := (ZTheory.get_zenv thy''))
in thy'' end;
*}
ML{*
val load_holzP =
OuterSyntax.command "load_holz" "load ZETA-generated .holz file"
OuterKeyword.thy_script
((OuterParse.name) >> (Toplevel.theory o load_holz));
val _ = OuterSyntax.add_parsers [load_holzP];
*}
section{* Proof Support: Toplevel-Command \textbf{zlemma} *}
ML{*
val zlemmaK = "zlemma"
val statement = OuterParse.and_list1
(OuterParse.opt_thm_name ":"
-- Scan.repeat1 OuterParse.propp);
val general_statement = statement >> pair [] ||
Scan.repeat OuterParse.locale_elem_or_expr
-- (OuterParse.$$$ "shows" |-- statement);
*}
ML{*
(* Old: (does not work but reports parameter correctly … )
(* For Debugging *)
val X = ref (NONE : xstring option) ;
val Y = ref(("",[]):string * Attrib.src list);
val Z = ref([]:Locale.element Locale.elem_expr list);
val W = ref([]:((string * Attrib.src list)
* (string * (string list * string list)) list) list);
fun smart_thm x y z w thy =
let val _ = (X:=x)
val _ = (Y:=y)
val _ = (Z:=z)
val _ = (W:=w)
in case w of
[((lemma_name,attr),[(goal,([],[]))])] =>
let val H = !ZEncoder.ZENV
val _ = (ZEncoder.ZENV:= ZTheory.get_zenv thy)
val cgoal = (ZEncoder.schema_read thy goal)
val _ = (ZEncoder.ZENV:= H )
val w' = [((lemma_name,attr),[(goal,([],[]))])]
in (* Locale.smart_theorem zlemmaK x y z w thy *)
(Proof.theorem zlemmaK (K (K I)) (SOME "") y w o
ProofContext.init) thy
end
| _ => error "zlemma : wrong argument pattern !"
end;
*)
fun smart_thm x y z w thy =
let
in case w of
[((lemma_name,attr),[(goal,([],[]))])] =>
let val H = !ZEncoder.ZENV
val _ = (ZEncoder.ZENV:= ZTheory.get_zenv thy)
val cgoal = (ZEncoder.schema_read thy goal)
val _ = (ZEncoder.ZENV:= H )
val y' = (fst y,[])
val w' = [((lemma_name,[]),[(cgoal,([],[]))])]
in (* Locale.smart_theorem zlemmaK x y z w thy *)
(Proof.theorem_i zlemmaK (K (K I)) (SOME "") y' w' o
ProofContext.init) thy
end
| _ => error "zlemma : wrong argument pattern !"
end;
val gen_zlemmaP =
OuterSyntax.command zlemmaK ("state " ^ zlemmaK) OuterKeyword.thy_goal
(OuterParse.opt_locale_target -- Scan.optional
(OuterParse.opt_thm_name ":" --|
Scan.ahead (OuterParse.locale_keyword || OuterParse.$$$ "shows"))
("", []) --
general_statement >> (fn ((x, y), (z, w)) =>
(Toplevel.print o Toplevel.theory_to_proof (smart_thm x y z w))));
val _ = OuterSyntax.add_parsers [gen_zlemmaP];
*}
section {* Baustelle: Code von DARMA zum integrieren *}
lemmas dom_infers = dom_override_I dom_Un_I dom_insert_I1 dom_insert_I2
dom_dres_I dom_BagSingleton_I
lemmas type_infers = SigmaI subsetI [THEN PowI]
pair_rel_dom_fst pair_rel_dom
declare UNIV_I [tc_simp]
declare dom_infers [tc_simp]
declare type_infers[tc_simp]
ML{*
val tfun_apply_fst = thm"tfun_apply_fst"
val tfun_apply_snd = thm"tfun_apply_snd"
val tfun_apply = thm"tfun_apply"
val Dom_Partial_Fin=thm"Dom_Partial_Fin"
val pfun_apply_fst=thm"pfun_apply_fst"
val pfun_apply_snd=thm"pfun_apply_snd"
val pfun_apply=thm"pfun_apply"
val mapfilter = Library.mapfilter
val mapfilter = Library.mapfilter
fun Prf y = (fn x => SOME(x RS y) handle THM _ => NONE)
fun fun_type_infers axdefs =
(mapfilter (Prf tfun_apply_fst) axdefs) @
(mapfilter (Prf tfun_apply_snd) axdefs) @
(mapfilter (Prf tfun_apply) axdefs) @
(mapfilter (Prf Dom_Partial_Fin) axdefs) @
(mapfilter (Prf pfun_apply_fst) axdefs) @
(mapfilter (Prf pfun_apply_snd) axdefs) @
(mapfilter (Prf pfun_apply) axdefs);
fun Add_axdefs_TC axdef =
let fun flat_conj m = Library.flat (mapfilter (
fn x =>SOME(flat_conj[x RS conjunct1,
x RS conjunct2])
handle THM _ =>SOME[x]) m)
fun closure m = m @ (fun_type_infers m)
in Add_TC (Library.flat(mapfilter
(fn x => SOME(closure(flat_conj[x RS DECL_D1]))
handle THM _ => NONE)
axdef))
end;
*}
(* Legacy !*)
(* renaming table ... *)
lemmas oplus_def = override_def
lemmas oplus_I2 = overrideI2
lemmas oplus_I1 = overrideI1
lemmas oplus_CI = overrideCI
lemmas oplus_single = override_single
lemmas oplus_res_right= override_res_right
lemmas oplus_res_left = override_res_left
lemmas oplus_Inter = override_inter
lemmas oplus_idem = override_idem
lemmas oplus_mt_right = override_mt_right
lemmas oplus_mt_left = override_mt_left
lemmas oplus_Domain = override_Domain
lemmas oplus_comp = override_assoc
lemmas oplus_fpfun = override_fpfun
lemmas oplus_pfunI = override_pfunI
lemmas oplus_apply2 = override_apply2
lemmas oplus_apply = override_apply
lemmas oplus_apply1 = override_apply1
lemmas oplus_non_apply= override_by_pair_apply2
lemmas oplus_by_pair_apply1 = override_by_pair_apply1
lemmas oplus_by_pair_apply2 = override_by_pair_apply2
lemmas Rel_Apply_in_total_range = tfun_apply
lemmas partial_func_def = pfun_def
lemmas total_func_def = tfun_def
lemmas pair_mem_apply = beta_apply_pfun
lemmas Rel_Apply_in_Partial_Ran2 = pfun_apply
lemmas total_func_implies_Pfun = tfun_implies_pfun
lemmas partial_fun_ran_subset = pfun_ran_subset
lemmas partial_fun_dom_subset = pfun_subset
lemmas dom_oplus_I = dom_override_I
lemmas empty_pfun = empty_is_pfun
lemmas dom_insert_apply = insert_apply
lemmas dom_insert_apply2 = insert_apply2
(* TODO rename all stuff with dom_substr -> ndres
dom_restr -> dres *)
end
lemmas dom_infers:
[| x ∈ dom X; x ∈ dom Y |] ==> x ∈ dom (X (+) Y)
[| x ∈ dom X; x ∈ dom Y |] ==> x ∈ dom (X ∪ Y)
x = fst a ==> x ∈ dom (insert a Y)
[| x ≠ fst a; x ∈ dom Y |] ==> x ∈ dom (insert a Y)
[| x ∈ X; x ∈ dom Y |] ==> x ∈ dom (X <: Y)
x = a ==> x ∈ dom %[ a %]
lemmas dom_infers:
[| x ∈ dom X; x ∈ dom Y |] ==> x ∈ dom (X (+) Y)
[| x ∈ dom X; x ∈ dom Y |] ==> x ∈ dom (X ∪ Y)
x = fst a ==> x ∈ dom (insert a Y)
[| x ≠ fst a; x ∈ dom Y |] ==> x ∈ dom (insert a Y)
[| x ∈ X; x ∈ dom Y |] ==> x ∈ dom (X <: Y)
x = a ==> x ∈ dom %[ a %]
lemmas type_infers:
[| a ∈ A; b ∈ B a |] ==> (a, b) ∈ Sigma A B
(!!x. x ∈ A ==> x ∈ B) ==> A ∈ %P B
a ∈ r ==> fst a ∈ dom r
(a, b) ∈ r ==> a ∈ dom r
lemmas type_infers:
[| a ∈ A; b ∈ B a |] ==> (a, b) ∈ Sigma A B
(!!x. x ∈ A ==> x ∈ B) ==> A ∈ %P B
a ∈ r ==> fst a ∈ dom r
(a, b) ∈ r ==> a ∈ dom r
lemmas oplus_def:
S (+) R == dom R <-: S ∪ R
lemmas oplus_def:
S (+) R == dom R <-: S ∪ R
lemmas oplus_I2:
p ∈ s ==> p ∈ r (+) s
lemmas oplus_I2:
p ∈ s ==> p ∈ r (+) s
lemmas oplus_I1:
p ∈ dom s <-: r ==> p ∈ r (+) s
lemmas oplus_I1:
p ∈ dom s <-: r ==> p ∈ r (+) s
lemmas oplus_CI:
(p ∉ s ==> p ∈ dom s <-: r) ==> p ∈ r (+) s
lemmas oplus_CI:
(p ∉ s ==> p ∈ dom s <-: r) ==> p ∈ r (+) s
lemmas oplus_single:
{(x, y)} (+) {(x, z)} = {(x, z)}
lemmas oplus_single:
{(x, y)} (+) {(x, z)} = {(x, z)}
lemmas oplus_res_right:
(Q (+) R) :> W ⊆ Q :> W (+) R :> W
lemmas oplus_res_right:
(Q (+) R) :> W ⊆ Q :> W (+) R :> W
lemmas oplus_res_left:
V <: (Q (+) R) = V <: Q (+) V <: R
lemmas oplus_res_left:
V <: (Q (+) R) = V <: Q (+) V <: R
lemmas oplus_Inter:
dom Q ∩ dom R = {} ==> Q (+) R = Q ∪ R
lemmas oplus_Inter:
dom Q ∩ dom R = {} ==> Q (+) R = Q ∪ R
lemmas oplus_idem:
R (+) R = R
lemmas oplus_idem:
R (+) R = R
lemmas oplus_mt_right:
R (+) {} = R
lemmas oplus_mt_right:
R (+) {} = R
lemmas oplus_mt_left:
{} (+) R = R
lemmas oplus_mt_left:
{} (+) R = R
lemmas oplus_Domain:
dom (R (+) Q) = dom Q ∪ dom R
lemmas oplus_Domain:
dom (R (+) Q) = dom Q ∪ dom R
lemmas oplus_comp:
P (+) (Q (+) R) = P (+) Q (+) R
lemmas oplus_comp:
P (+) (Q (+) R) = P (+) Q (+) R
lemmas oplus_fpfun:
[| f ∈ A -||-> B; g ∈ A -||-> B |] ==> f (+) g ∈ A -||-> B
lemmas oplus_fpfun:
[| f ∈ A -||-> B; g ∈ A -||-> B |] ==> f (+) g ∈ A -||-> B
lemmas oplus_pfunI:
[| f ∈ A -|-> B; g ∈ A -|-> B |] ==> f (+) g ∈ A -|-> B
lemmas oplus_pfunI:
[| f ∈ A -|-> B; g ∈ A -|-> B |] ==> f (+) g ∈ A -|-> B
lemmas oplus_apply2:
z ∉ dom S ==> (R (+) S) %^ z = R %^ z
lemmas oplus_apply2:
z ∉ dom S ==> (R (+) S) %^ z = R %^ z
lemmas oplus_apply:
(R (+) {(x, y)}) %^ x = y
lemmas oplus_apply:
(R (+) {(x, y)}) %^ x = y
lemmas oplus_apply1:
z ∈ dom S ==> (R (+) S) %^ z = S %^ z
lemmas oplus_apply1:
z ∈ dom S ==> (R (+) S) %^ z = S %^ z
lemmas oplus_non_apply:
x ≠ z ==> (R (+) {(z, y)}) %^ x = R %^ x
lemmas oplus_non_apply:
x ≠ z ==> (R (+) {(z, y)}) %^ x = R %^ x
lemmas oplus_by_pair_apply1:
x = z ==> (R (+) {(z, y)}) %^ x = y
lemmas oplus_by_pair_apply1:
x = z ==> (R (+) {(z, y)}) %^ x = y
lemmas oplus_by_pair_apply2:
x ≠ z ==> (R (+) {(z, y)}) %^ x = R %^ x
lemmas oplus_by_pair_apply2:
x ≠ z ==> (R (+) {(z, y)}) %^ x = R %^ x
lemmas Rel_Apply_in_total_range:
[| F ∈ X ---> Y; x ∈ X |] ==> F %^ x ∈ Y
lemmas Rel_Apply_in_total_range:
[| F ∈ X ---> Y; x ∈ X |] ==> F %^ x ∈ Y
lemmas partial_func_def:
S -|-> R == {f : S <--> R. ∀x y1 y2. (x, y1) ∈ f ∧ (x, y2) ∈ f --> y1 = y2}
lemmas partial_func_def:
S -|-> R == {f : S <--> R. ∀x y1 y2. (x, y1) ∈ f ∧ (x, y2) ∈ f --> y1 = y2}
lemmas total_func_def:
S ---> R == {s : S -|-> R. dom s = S}
lemmas total_func_def:
S ---> R == {s : S -|-> R. dom s = S}
lemmas pair_mem_apply:
[| r ∈ X -|-> Y; (a, b) ∈ r |] ==> r %^ a = b
lemmas pair_mem_apply:
[| r ∈ X -|-> Y; (a, b) ∈ r |] ==> r %^ a = b
lemmas Rel_Apply_in_Partial_Ran2:
[| F ∈ X -|-> Y; x ∈ dom F |] ==> F %^ x ∈ Y
lemmas Rel_Apply_in_Partial_Ran2:
[| F ∈ X -|-> Y; x ∈ dom F |] ==> F %^ x ∈ Y
lemmas total_func_implies_Pfun:
f ∈ A ---> B ==> f ∈ A -|-> B
lemmas total_func_implies_Pfun:
f ∈ A ---> B ==> f ∈ A -|-> B
lemmas partial_fun_ran_subset:
[| f ∈ a -|-> b; b ⊆ c |] ==> f ∈ a -|-> c
lemmas partial_fun_ran_subset:
[| f ∈ a -|-> b; b ⊆ c |] ==> f ∈ a -|-> c
lemmas partial_fun_dom_subset:
[| f ∈ a -|-> c; a ⊆ b |] ==> f ∈ b -|-> c
lemmas partial_fun_dom_subset:
[| f ∈ a -|-> c; a ⊆ b |] ==> f ∈ b -|-> c
lemmas dom_oplus_I:
[| x ∈ dom X; x ∈ dom Y |] ==> x ∈ dom (X (+) Y)
lemmas dom_oplus_I:
[| x ∈ dom X; x ∈ dom Y |] ==> x ∈ dom (X (+) Y)
lemmas empty_pfun:
{} ∈ A -|-> B
lemmas empty_pfun:
{} ∈ A -|-> B
lemmas dom_insert_apply:
z ≠ fst a ==> insert a R %^ z = R %^ z
lemmas dom_insert_apply:
z ≠ fst a ==> insert a R %^ z = R %^ z
lemmas dom_insert_apply2:
z ∉ dom R ==> insert a R %^ z = {a} %^ z
lemmas dom_insert_apply2:
z ∉ dom R ==> insert a R %^ z = {a} %^ z