src/HOLCF/ex/Loop.ML

 
 (* --------------------------------------------------------------------------- *)
 (* access to definitions                                                       *)
 (* --------------------------------------------------------------------------- *)
 
-qed_goalw "step_def2" Loop.thy [step_def]
+val step_def2 = prove_goalw Loop.thy [step_def]
 "step[b][g][x] = If b[x] then g[x] else x fi"
  (fn prems =>
 	[
 	(simp_tac Cfun_ss 1)
 	]);
 
-qed_goalw "while_def2" Loop.thy [while_def]
+val while_def2 = prove_goalw Loop.thy [while_def]
 "while[b][g] = fix[LAM f x. If b[x] then f[g[x]] else x fi]"
  (fn prems =>
 	[
 	(simp_tac Cfun_ss 1)
 	]);

 
 (* ------------------------------------------------------------------------- *)
 (* rekursive properties of while                                             *)
 (* ------------------------------------------------------------------------- *)
 
-qed_goal "while_unfold" Loop.thy 
+val while_unfold = prove_goal Loop.thy 
 "while[b][g][x] = If b[x] then while[b][g][g[x]] else x fi"
  (fn prems =>
 	[
 	(fix_tac5  while_def2 1),
 	(simp_tac Cfun_ss 1)
 	]);
 
-qed_goal "while_unfold2" Loop.thy 
+val while_unfold2 = prove_goal Loop.thy 
 	"!x.while[b][g][x] = while[b][g][iterate(k,step[b][g],x)]"
  (fn prems =>
 	[
 	(nat_ind_tac "k" 1),
 	(simp_tac (HOLCF_ss addsimps [iterate_0,iterate_Suc]) 1),

 	(asm_simp_tac HOLCF_ss 1),
 	(rtac (while_unfold RS ssubst) 1),
 	(asm_simp_tac HOLCF_ss 1)
 	]);
 
-qed_goal "while_unfold3" Loop.thy 
+val while_unfold3 = prove_goal Loop.thy 
 	"while[b][g][x] = while[b][g][step[b][g][x]]"
  (fn prems =>
 	[
 	(res_inst_tac [("s","while[b][g][iterate(Suc(0),step[b][g],x)]")] trans 1),
 	(rtac (while_unfold2 RS spec) 1),

 
 (* --------------------------------------------------------------------------- *)
 (* properties of while and iterations                                          *)
 (* --------------------------------------------------------------------------- *)
 
-qed_goal "loop_lemma1" Loop.thy
+val loop_lemma1 = prove_goal Loop.thy
 "[|? y.b[y]=FF; iterate(k,step[b][g],x)=UU|]==>iterate(Suc(k),step[b][g],x)=UU"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(simp_tac iterate_ss 1),

 	(etac (flat_tr RS flat_codom RS disjE) 1),
 	(asm_simp_tac HOLCF_ss 1),
 	(asm_simp_tac HOLCF_ss 1)
 	]);
 
-qed_goal "loop_lemma2" Loop.thy
+val loop_lemma2 = prove_goal Loop.thy
 "[|? y.b[y]=FF;~iterate(Suc(k),step[b][g],x)=UU |]==>\
 \~iterate(k,step[b][g],x)=UU"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),

 	(etac  loop_lemma1 2),
 	(atac 1),
 	(atac 1)
 	]);
 
-qed_goal "loop_lemma3" Loop.thy
+val loop_lemma3 = prove_goal Loop.thy
 "[|!x. INV(x) & b[x]=TT & ~g[x]=UU --> INV(g[x]);\
 \? y.b[y]=FF; INV(x)|] ==>\
 \~iterate(k,step[b][g],x)=UU --> INV(iterate(k,step[b][g],x))"
  (fn prems =>
 	[

 	(asm_simp_tac (HOLCF_ss addsimps [iterate_Suc,step_def2] ) 1),
 	(asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1)
 	]);
 
 
-qed_goal "loop_lemma4" Loop.thy
+val loop_lemma4 = prove_goal Loop.thy
 "!x. b[iterate(k,step[b][g],x)]=FF --> while[b][g][x]=iterate(k,step[b][g],x)"
  (fn prems =>
 	[
 	(nat_ind_tac "k" 1),
 	(simp_tac iterate_ss 1),

 	(rtac trans 1),
 	(rtac while_unfold3 1),
 	(asm_simp_tac HOLCF_ss  1)
 	]);
 
-qed_goal "loop_lemma5" Loop.thy
+val loop_lemma5 = prove_goal Loop.thy
 "!k. ~b[iterate(k,step[b][g],x)]=FF ==>\
 \ !m. while[b][g][iterate(m,step[b][g],x)]=UU"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),

 	(dtac spec 1),
 	(contr_tac 1)
 	]);
 
 
-qed_goal "loop_lemma6" Loop.thy
+val loop_lemma6 = prove_goal Loop.thy
 "!k. ~b[iterate(k,step[b][g],x)]=FF ==> while[b][g][x]=UU"
  (fn prems =>
 	[
 	(res_inst_tac [("t","x")] (iterate_0 RS subst) 1),
 	(rtac (loop_lemma5 RS spec) 1),
 	(resolve_tac prems 1)
 	]);
 
-qed_goal "loop_lemma7" Loop.thy
+val loop_lemma7 = prove_goal Loop.thy
 "~while[b][g][x]=UU ==> ? k. b[iterate(k,step[b][g],x)]=FF"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(etac swap 1),
 	(rtac loop_lemma6 1),
 	(fast_tac HOL_cs 1)
 	]);
 
-qed_goal "loop_lemma8" Loop.thy
+val loop_lemma8 = prove_goal Loop.thy
 "~while[b][g][x]=UU ==> ? y. b[y]=FF"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(dtac loop_lemma7 1),

 
 (* --------------------------------------------------------------------------- *)
 (* an invariant rule for loops                                                 *)
 (* --------------------------------------------------------------------------- *)
 
-qed_goal "loop_inv2" Loop.thy
+val loop_inv2 = prove_goal Loop.thy
 "[| (!y. INV(y) & b[y]=TT & ~g[y]=UU --> INV(g[y]));\
 \   (!y. INV(y) & b[y]=FF --> Q(y));\
 \   INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"
  (fn prems =>
 	[

 	(rtac (loop_lemma4 RS spec RS mp RS sym) 1),
 	(atac 1),
 	(rtac refl 1)
 	]);
 
-qed_goal "loop_inv3" Loop.thy
+val loop_inv3 = prove_goal Loop.thy
 "[| !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\
 \   !!y.[| INV(y); b[y]=FF|]==> Q(y);\
 \   INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"
  (fn prems =>
 	[

 	(fast_tac HOL_cs 1),
 	(resolve_tac prems 1),
 	(resolve_tac prems 1)
 	]);
 
-qed_goal "loop_inv" Loop.thy
+val loop_inv = prove_goal Loop.thy
 "[| P(x);\
 \   !!y.P(y) ==> INV(y);\
 \   !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\
 \   !!y.[| INV(y); b[y]=FF|]==> Q(y);\
 \   ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"