(* Title: CCL/Wfd.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
section \<open>Well-founded relations in CCL\<close>
theory Wfd
imports Trancl Type Hered
begin
definition Wfd :: "[i set] \ o"
where "Wfd(R) == ALL P.(ALL x.(ALL y. : R \ y:P) \ x:P) \ (ALL a. a:P)"
definition wf :: "[i set] \ i set"
where "wf(R) == {x. x:R \ Wfd(R)}"
definition wmap :: "[i\i,i set] \ i set"
where "wmap(f,R) == {p. EX x y. p= \ : R}"
definition lex :: "[i set,i set] => i set" (infixl "**" 70)
where "ra**rb == {p. EX a a' b b'. p = <,> \ ( : ra | (a=a' \ : rb))}"
definition NatPR :: "i set"
where "NatPR == {p. EX x:Nat. p=}"
definition ListPR :: "i set \ i set"
where "ListPR(A) == {p. EX h:A. EX t:List(A). p=}"
lemma wfd_induct:
assumes 1: "Wfd(R)"
and 2: "\x. ALL y. : R \ P(y) \ P(x)"
shows "P(a)"
apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD])
using 2 apply blast
done
lemma wfd_strengthen_lemma:
assumes 1: "\x y. : R \ Q(x)"
and 2: "ALL x. (ALL y. : R \ y : P) \ x : P"
and 3: "\x. Q(x) \ x:P"
shows "a:P"
apply (rule 2 [rule_format])
using 1 3
apply blast
done
method_setup wfd_strengthen = \<open>
Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD' (fn i =>
Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i
THEN assume_tac ctxt (i + 1)))
\<close>
lemma wf_anti_sym: "\Wfd(r); :r; :r\ \ P"
apply (subgoal_tac "ALL x. :r \ :r \ P")
apply blast
apply (erule wfd_induct)
apply blast
done
lemma wf_anti_refl: "\Wfd(r); : r\ \ P"
apply (rule wf_anti_sym)
apply assumption+
done
subsection \<open>Irreflexive transitive closure\<close>
lemma trancl_wf:
assumes 1: "Wfd(R)"
shows "Wfd(R^+)"
apply (unfold Wfd_def)
apply (rule allI ballI impI)+
(*must retain the universal formula for later use!*)
apply (rule allE, assumption)
apply (erule mp)
apply (rule 1 [THEN wfd_induct])
apply (rule impI [THEN allI])
apply (erule tranclE)
apply blast
apply (erule spec [THEN mp, THEN spec, THEN mp])
apply assumption+
done
subsection \<open>Lexicographic Ordering\<close>
lemma lexXH:
"p : ra**rb \ (EX a a' b b'. p = <,> \ ( : ra | a=a' \ : rb))"
unfolding lex_def by blast
lemma lexI1: " : ra \ <,> : ra**rb"
by (blast intro!: lexXH [THEN iffD2])
lemma lexI2: " : rb \ <,> : ra**rb"
by (blast intro!: lexXH [THEN iffD2])
lemma lexE:
assumes 1: "p : ra**rb"
and 2: "\a a' b b'. \ : ra; p=<,>\ \ R"
and 3: "\a b b'. \ : rb; p = <,>\ \ R"
shows R
apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE])
using 2 3
apply blast
done
lemma lex_pair: "\p : r**s; \a a' b b'. p = <,> \ P\ \P"
apply (erule lexE)
apply blast+
done
lemma lex_wf:
assumes 1: "Wfd(R)"
and 2: "Wfd(S)"
shows "Wfd(R**S)"
apply (unfold Wfd_def)
apply safe
apply (wfd_strengthen "\x. EX a b. x=")
apply (blast elim!: lex_pair)
apply (subgoal_tac "ALL a b.:P")
apply blast
apply (rule 1 [THEN wfd_induct, THEN allI])
apply (rule 2 [THEN wfd_induct, THEN allI]) back
apply (fast elim!: lexE)
done
subsection \<open>Mapping\<close>
lemma wmapXH: "p : wmap(f,r) \ (EX x y. p= \ : r)"
unfolding wmap_def by blast
lemma wmapI: " : r \ : wmap(f,r)"
by (blast intro!: wmapXH [THEN iffD2])
lemma wmapE: "\p : wmap(f,r); \a b. \ : r; p=\ \ R\ \ R"
by (blast dest!: wmapXH [THEN iffD1])
lemma wmap_wf:
assumes 1: "Wfd(r)"
shows "Wfd(wmap(f,r))"
apply (unfold Wfd_def)
apply clarify
apply (subgoal_tac "ALL b. ALL a. f (a) = b \ a:P")
apply blast
apply (rule 1 [THEN wfd_induct, THEN allI])
apply clarify
apply (erule spec [THEN mp])
apply (safe elim!: wmapE)
apply (erule spec [THEN mp, THEN spec, THEN mp])
apply assumption
apply (rule refl)
done
subsection \<open>Projections\<close>
lemma wfstI: " : r \ <,> : wmap(fst,r)"
apply (rule wmapI)
apply simp
done
lemma wsndI: " : r \ <,> : wmap(snd,r)"
apply (rule wmapI)
apply simp
done
lemma wthdI: " : r \ <>,>> : wmap(thd,r)"
apply (rule wmapI)
apply simp
done
subsection \<open>Ground well-founded relations\<close>
lemma wfI: "\Wfd(r); a : r\ \ a : wf(r)"
unfolding wf_def by blast
lemma Empty_wf: "Wfd({})"
unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE])
lemma wf_wf: "Wfd(wf(R))"
unfolding wf_def
apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE])
apply simp_all
apply (rule Empty_wf)
done
lemma NatPRXH: "p : NatPR \ (EX x:Nat. p=)"
unfolding NatPR_def by blast
lemma ListPRXH: "p : ListPR(A) \ (EX h:A. EX t:List(A).p=)"
unfolding ListPR_def by blast
lemma NatPRI: "x : Nat \ : NatPR"
by (auto simp: NatPRXH)
lemma ListPRI: "\t : List(A); h : A\ \ : ListPR(A)"
by (auto simp: ListPRXH)
lemma NatPR_wf: "Wfd(NatPR)"
apply (unfold Wfd_def)
apply clarify
apply (wfd_strengthen "\x. x:Nat")
apply (fastforce iff: NatPRXH)
apply (erule Nat_ind)
apply (fastforce iff: NatPRXH)+
done
lemma ListPR_wf: "Wfd(ListPR(A))"
apply (unfold Wfd_def)
apply clarify
apply (wfd_strengthen "\x. x:List (A)")
apply (fastforce iff: ListPRXH)
apply (erule List_ind)
apply (fastforce iff: ListPRXH)+
done
subsection \<open>General Recursive Functions\<close>
lemma letrecT:
assumes 1: "a : A"
and 2: "\p g. \p:A; ALL x:{x: A. :wf(R)}. g(x) : D(x)\ \ h(p,g) : D(p)"
shows "letrec g x be h(x,g) in g(a) : D(a)"
apply (rule 1 [THEN rev_mp])
apply (rule wf_wf [THEN wfd_induct])
apply (subst letrecB)
apply (rule impI)
apply (erule 2)
apply blast
done
lemma SPLITB: "SPLIT(,B) = B(a,b)"
unfolding SPLIT_def
apply (rule set_ext)
apply blast
done
lemma letrec2T:
assumes "a : A"
and "b : B"
and "\p q g. \p:A; q:B;
ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y)\<rbrakk> \<Longrightarrow>
h(p,q,g) : D(p,q)"
shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
apply (unfold letrec2_def)
apply (rule SPLITB [THEN subst])
apply (assumption | rule letrecT pairT splitT assms)+
apply (subst SPLITB)
apply (assumption | rule ballI SubtypeI assms)+
apply (rule SPLITB [THEN subst])
apply (assumption | rule letrecT SubtypeI pairT splitT assms |
erule bspec SubtypeE sym [THEN subst])+
done
lemma lem: "SPLIT(>,\x xs. SPLIT(xs,\y z. B(x,y,z))) = B(a,b,c)"
by (simp add: SPLITB)
lemma letrec3T:
assumes "a : A"
and "b : B"
and "c : C"
and "\p q r g. \p:A; q:B; r:C;
ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}.
g(x,y,z) : D(x,y,z) \<rbrakk> \<Longrightarrow>
h(p,q,r,g) : D(p,q,r)"
shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
apply (unfold letrec3_def)
apply (rule lem [THEN subst])
apply (assumption | rule letrecT pairT splitT assms)+
apply (simp add: SPLITB)
apply (assumption | rule ballI SubtypeI assms)+
apply (rule lem [THEN subst])
apply (assumption | rule letrecT SubtypeI pairT splitT assms |
erule bspec SubtypeE sym [THEN subst])+
done
lemmas letrecTs = letrecT letrec2T letrec3T
subsection \<open>Type Checking for Recursive Calls\<close>
lemma rcallT:
"\ALL x:{x:A.:wf(R)}.g(x):D(x);
g(a) : D(a) \<Longrightarrow> g(a) : E; a:A; <a,p>:wf(R)\<rbrakk> \<Longrightarrow> g(a) : E"
by blast
lemma rcall2T:
"\ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y);
g(a,b) : D(a,b) \<Longrightarrow> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R)\<rbrakk> \<Longrightarrow> g(a,b) : E"
by blast
lemma rcall3T:
"\ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}. g(x,y,z):D(x,y,z);
g(a,b,c) : D(a,b,c) \<Longrightarrow> g(a,b,c) : E;
a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R)\<rbrakk> \<Longrightarrow> g(a,b,c) : E"
by blast
lemmas rcallTs = rcallT rcall2T rcall3T
subsection \<open>Instantiating an induction hypothesis with an equality assumption\<close>
lemma hyprcallT:
assumes 1: "g(a) = b"
and 2: "ALL x:{x:A.:wf(R)}.g(x):D(x)"
and 3: "ALL x:{x:A.:wf(R)}.g(x):D(x) \ b=g(a) \ g(a) : D(a) \ P"
and 4: "ALL x:{x:A.:wf(R)}.g(x):D(x) \ a:A"
and 5: "ALL x:{x:A.:wf(R)}.g(x):D(x) \ :wf(R)"
shows P
apply (rule 3 [OF 2, OF 1 [symmetric]])
apply (rule rcallT [OF 2])
apply assumption
apply (rule 4 [OF 2])
apply (rule 5 [OF 2])
done
lemma hyprcall2T:
assumes 1: "g(a,b) = c"
and 2: "ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y)"
and 3: "\c = g(a,b); g(a,b) : D(a,b)\ \ P"
and 4: "a:A"
and 5: "b:B"
and 6: "<,>:wf(R)"
shows P
apply (rule 3)
apply (rule 1 [symmetric])
apply (rule rcall2T)
apply (rule 2)
apply assumption
apply (rule 4)
apply (rule 5)
apply (rule 6)
done
lemma hyprcall3T:
assumes 1: "g(a,b,c) = d"
and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z)"
and 3: "\d = g(a,b,c); g(a,b,c) : D(a,b,c)\ \ P"
and 4: "a:A"
and 5: "b:B"
and 6: "c:C"
and 7: "<>,>> : wf(R)"
shows P
apply (rule 3)
apply (rule 1 [symmetric])
apply (rule rcall3T)
apply (rule 2)
apply assumption
apply (rule 4)
apply (rule 5)
apply (rule 6)
apply (rule 7)
done
lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T
subsection \<open>Rules to Remove Induction Hypotheses after Type Checking\<close>
lemma rmIH1: "\ALL x:{x:A.:wf(R)}.g(x):D(x); P\ \ P" .
lemma rmIH2: "\ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); P\ \ P" .
lemma rmIH3:
"\ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z); P\ \ P" .
lemmas rmIHs = rmIH1 rmIH2 rmIH3
subsection \<open>Lemmas for constructors and subtypes\<close>
(* 0-ary constructors do not need additional rules as they are handled *)
(* correctly by applying SubtypeI *)
lemma Subtype_canTs:
"\a b A B P. a : {x:A. b:{y:B(a).P()}} \ : {x:Sigma(A,B).P(x)}"
"\a A B P. a : {x:A. P(inl(x))} \ inl(a) : {x:A+B. P(x)}"
"\b A B P. b : {x:B. P(inr(x))} \ inr(b) : {x:A+B. P(x)}"
"\a P. a : {x:Nat. P(succ(x))} \ succ(a) : {x:Nat. P(x)}"
"\h t A P. h : {x:A. t : {y:List(A).P(x$y)}} \ h$t : {x:List(A).P(x)}"
by (assumption | rule SubtypeI canTs icanTs | erule SubtypeE)+
lemma letT: "\f(t):B; \t=bot\ \ let x be t in f(x) : B"
apply (erule letB [THEN ssubst])
apply assumption
done
lemma applyT2: "\a:A; f : Pi(A,B)\ \ f ` a : B(a)"
apply (erule applyT)
apply assumption
done
lemma rcall_lemma1: "\a:A; a:A \ P(a)\ \ a : {x:A. P(x)}"
by blast
lemma rcall_lemma2: "\a:{x:A. Q(x)}; \a:A; Q(a)\ \ P(a)\ \ a : {x:A. P(x)}"
by blast
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2
subsection \<open>Typechecking\<close>
ML \<open>
local
val type_rls =
@{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
@{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
fun bvars (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(s,_,t)) l = bvars t (s::l)
| bvars _ l = l
fun get_bno l n (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(s,_,t)) = get_bno (s::l) n t
| get_bno l n (Const(\<^const_name>\<open>Trueprop\<close>,_) $ t) = get_bno l n t
| get_bno l n (Const(\<^const_name>\<open>Ball\<close>,_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
| get_bno l n (Const(\<^const_name>\<open>mem\<close>,_) $ t $ _) = get_bno l n t
| get_bno l n (t $ s) = get_bno l n t
| get_bno l n (Bound m) = (m-length(l),n)
(* Not a great way of identifying induction hypothesis! *)
fun could_IH x = Term.could_unify(x,hd (Thm.prems_of @{thm rcallT})) orelse
Term.could_unify(x,hd (Thm.prems_of @{thm rcall2T})) orelse
Term.could_unify(x,hd (Thm.prems_of @{thm rcall3T}))
fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
let val bvs = bvars Bi []
val ihs = filter could_IH (Logic.strip_assums_hyp Bi)
val rnames = map (fn x =>
let val (a,b) = get_bno [] 0 x
in (nth bvs a, b) end) ihs
fun try_IHs [] = no_tac
| try_IHs ((x,y)::xs) =
tac [((("g", 0), Position.none), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs)
in try_IHs rnames end)
fun is_rigid_prog t =
(case (Logic.strip_assums_concl t) of
(Const(\<^const_name>\<open>Trueprop\<close>,_) $ (Const(\<^const_name>\<open>mem\<close>,_) $ a $ _)) =>
null (Term.add_vars a [])
| _ => false)
in
fun rcall_tac ctxt i =
let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps [] rl i THEN assume_tac ctxt i
in IHinst tac @{thms rcallTs} i end
THEN eresolve_tac ctxt @{thms rcall_lemmas} i
fun raw_step_tac ctxt prems i =
assume_tac ctxt i ORELSE
resolve_tac ctxt (prems @ type_rls) i ORELSE
rcall_tac ctxt i ORELSE
ematch_tac ctxt @{thms SubtypeE} i ORELSE
match_tac ctxt @{thms SubtypeI} i
fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i
(*** Clean up Correctness Condictions ***)
fun clean_ccs_tac ctxt =
let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps [] rl i THEN assume_tac ctxt i in
TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
eresolve_tac ctxt ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
hyp_subst_tac ctxt))
end
fun gen_ccs_tac ctxt rls i =
SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i
end
\<close>
method_setup typechk = \<open>
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (typechk_tac ctxt ths))
\<close>
method_setup clean_ccs = \<open>
Scan.succeed (SIMPLE_METHOD o clean_ccs_tac)
\<close>
method_setup gen_ccs = \<open>
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (gen_ccs_tac ctxt ths))
\<close>
subsection \<open>Evaluation\<close>
named_theorems eval "evaluation rules"
ML \<open>
fun eval_tac ths =
Subgoal.FOCUS_PREMS (fn {context = ctxt, prems, ...} =>
let val eval_rules = Named_Theorems.get ctxt \<^named_theorems>\<open>eval\<close>
in DEPTH_SOLVE_1 (resolve_tac ctxt (ths @ prems @ rev eval_rules) 1) end)
\<close>
method_setup eval = \<open>
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))
\<close>
lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam
lemma applyV [eval]:
assumes "f \ lam x. b(x)"
and "b(a) \ c"
shows "f ` a \ c"
unfolding apply_def by (eval assms)
lemma letV:
assumes 1: "t \ a"
and 2: "f(a) \ c"
shows "let x be t in f(x) \ c"
apply (unfold let_def)
apply (rule 1 [THEN canonical])
apply (tactic \<open>
REPEAT (DEPTH_SOLVE_1 (resolve_tac \<^context> (@{thms assms} @ @{thms eval_rls}) 1 ORELSE
eresolve_tac \<^context> @{thms substitute} 1))\<close>)
done
lemma fixV: "f(fix(f)) \ c \ fix(f) \ c"
apply (unfold fix_def)
apply (rule applyV)
apply (rule lamV)
apply assumption
done
lemma letrecV:
"h(t,\y. letrec g x be h(x,g) in g(y)) \ c \
letrec g x be h(x,g) in g(t) \<longlongrightarrow> c"
apply (unfold letrec_def)
apply (assumption | rule fixV applyV lamV)+
done
lemmas [eval] = letV letrecV fixV
lemma V_rls [eval]:
"true \ true"
"false \ false"
"\b c t u. \b\true; t\c\ \ if b then t else u \ c"
"\b c t u. \b\false; u\c\ \ if b then t else u \ c"
"\a b. \ "
"\a b c t h. \t \ ; h(a,b) \ c\ \ split(t,h) \ c"
"zero \ zero"
"\n. succ(n) \ succ(n)"
"\c n t u. \n \ zero; t \ c\ \ ncase(n,t,u) \ c"
"\c n t u x. \n \ succ(x); u(x) \ c\ \ ncase(n,t,u) \ c"
"\c n t u. \n \ zero; t \ c\ \ nrec(n,t,u) \ c"
"\c n t u x. \n\succ(x); u(x,nrec(x,t,u))\c\ \ nrec(n,t,u)\c"
"[] \ []"
"\h t. h$t \ h$t"
"\c l t u. \l \ []; t \ c\ \ lcase(l,t,u) \ c"
"\c l t u x xs. \l \ x$xs; u(x,xs) \ c\ \ lcase(l,t,u) \ c"
"\c l t u. \l \ []; t \ c\ \ lrec(l,t,u) \ c"
"\c l t u x xs. \l\x$xs; u(x,xs,lrec(xs,t,u))\c\ \ lrec(l,t,u)\c"
unfolding data_defs by eval+
subsection \<open>Factorial\<close>
schematic_goal
"letrec f n be ncase(n,succ(zero),\x. nrec(n,zero,\y g. nrec(f(x),g,\z h. succ(h))))
in f(succ(succ(zero))) \<longlongrightarrow> ?a"
by eval
schematic_goal
"letrec f n be ncase(n,succ(zero),\x. nrec(n,zero,\y g. nrec(f(x),g,\z h. succ(h))))
in f(succ(succ(succ(zero)))) \<longlongrightarrow> ?a"
by eval
subsection \<open>Less Than Or Equal\<close>
schematic_goal
"letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f())))
in f(<succ(zero), succ(zero)>) \<longlongrightarrow> ?a"
by eval
schematic_goal
"letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f())))
in f(<succ(zero), succ(succ(succ(succ(zero))))>) \<longlongrightarrow> ?a"
by eval
schematic_goal
"letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f())))
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) \<longlongrightarrow> ?a"
by eval
subsection \<open>Reverse\<close>
schematic_goal
"letrec id l be lcase(l,[],\x xs. x$id(xs))
in id(zero$succ(zero)$[]) \<longlongrightarrow> ?a"
by eval
schematic_goal
"letrec rev l be lcase(l,[],\x xs. lrec(rev(xs),x$[],\y ys g. y$g))
in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) \<longlongrightarrow> ?a"
by eval
end
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.10Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
