Quelle  IMP2.thy

theory IMP2
imports "automation/IMP2_VCG" "automation/IMP2_Specification"
begin

section ‹IMP2 Setup›

lemmas [deriv_unfolds] = Params_def Inline_def AssignIdx_retv_def ArrayCpy_retv_def


section ‹Ad-Hoc Regression Tests›
  
experiment begin

lemma upd_idxSame[named_ss vcg_bb]: "f(i:=a,i:=b) = f (i:=b)" by auto

lemmas [named_ss vcg_bb] = triv_forall_equality

declare [[eta_contract = false ]]  
program_spec (partial) p2
  assumes "n>0"  
  ensures "n=0"
  defines ‹while (n>0) @invariant ‹n≥0› { if (n+1>1) {
 n=n-1;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
 skip
 } }›
  apply vcg
  by auto

program_spec p2'
  assumes "n>0"  
  ensures "n=0"
  defines ‹while (n>0) @variant ‹n› @invariant ‹n≥0› { n=n-1 }›
  apply vcg
  by auto

    
program_spec p2''
  assumes "n>0"  
  ensures "n=0"
  defines ‹while (n>0) @relation ‹measure nat› @variant ‹n› @invariant ‹n≥0› { n=n-1 }›
  apply vcg
  by auto

program_spec p3  
  assumes "True"
  ensures "n = n₀ ∧ N=42"
  defines ‹
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope n = 0;
 scope {n = 0}; N=42
 ›
  apply vcg
  by auto
  
    
end


subsection ‹More Regression Tests›

experiment begin

lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib 


program_spec exp_count_up1
  assumes "0≤n"
  ensures "a = 2^nat n₀"
  defines ‹
 a = 1;
 c = 0;
 while (c<n)
 @variant ‹n-c›
 @invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
 {
 a=2*a;
 
 
 c=c+1
 }
 ›
  apply vcg
  by (auto simp: algebra_simps nat_distribs)


program_spec exp_count_up1'
  assumes "0≤n"
  ensures "a = 2^nat n₀"
  defines ‹
 a = 1;
 c = 0;
 while (c<n)
 @variant ‹n-c›
 @invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
 {
 a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 
 a=2*a;
 c=c+1
 }
 ›
  apply vcg
  by (auto simp: algebra_simps nat_distribs)
  
  
(* We've made the program a little larger \<dots> *)
program_spec exp_count_up
  assumes "0≤n"
  ensures "a = 2^nat n₀"
  defines ‹
 a = 1;
 c = 0;
 while (c<n)
 @variant ‹n-c›
 @invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
 {
 a=2*a;
 
 {
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;

 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;

 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;

 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;

 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;

 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;

 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;

 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;

 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
 skip
 };
 
 c=c+1
 }
 ›
  apply vcg
      apply (all ‹simp?›)
  apply (auto simp: algebra_simps nat_distribs)
  done

  
program_spec exp_count_up3
  assumes "0≤n"
  ensures "a = 2^nat n₀"
  defines ‹
 a = 1;
 c = 0;
 while (c<n)
 @variant ‹n-c›
 @invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
 {
 a=2*a;
 
 { ― ‹Note, this provokes exponential blowup of intermediate, unsimplified terms! ›
 a=a+a; a=a+a; a=a+a; a = a/8;
 a=a+a; a=a+a; a=a+a; a = a/8;
 a=a+a; a=a+a; a=a+a; a = a/8;
 a=a+a; a = a/2;
 
 skip
 };
 
 c=c+1
 }
 ›
  apply vcg
      apply (all ‹simp?›)
  apply (auto simp: algebra_simps nat_distribs)
  done
  
  
    
end


experiment
begin

lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib


procedure_spec exp_count_up (n) returns a
  assumes "0≤n"
  ensures "a = 2^nat n₀"
  defines ‹
 a = 1;
 c = 0;
 while (c<n)
 @variant ‹n-c›
 @invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
 {
 a=2*a;
 c=c+1
 }
 ›
  apply vcg
  by (auto simp: algebra_simps nat_distribs)

program_spec use_exp 
  assumes "0≤n"
  ensures ‹n = 2^(2^nat n₀)›
  defines ‹
 n = exp_count_up(n);
 n = exp_count_up(n)
 ›
  apply vcg
  by auto


  
procedure_spec add3 (a, b, c) returns r
  assumes "a≥0 ∧b≥0 ∧c≥0"  
  ensures "r = a₀+b₀+c₀"
  defines ‹
 r = a+b+c
 ›
  apply vcg
  by auto
  
procedure_spec use_add3 (a, b) returns r
  assumes "a≥0 ∧ b≥0"  
  ensures "r = 2*(a₀+b₀+b₀)"
  defines ‹
 r1 = add3(a, b, b);
 r2 = add3(a, b, b);
 r = r1+r2
 ›
  apply vcg
  by auto


procedure_spec divmod (a,b) returns (c,d)  
  assumes "b≠0"
  ensures "c = a₀ div b₀ ∧ d = a₀ mod b₀"
  defines ‹
 c = a / b;
 d = a mod b
 ›
  apply vcg
  by auto
  
procedure_spec use_divmod (a,b) returns r
  assumes "b≠0"
  ensures "r = a₀"
  defines ‹
 (d,m) = divmod (a,b);
 r = d*b + m
 ›
  apply vcg
  by simp
  
  
    
end
  
experiment
begin

lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib


procedure_spec exp_count_up (n) returns a
  assumes "0≤n"
  ensures "a = 2^nat n₀"
  defines ‹
 a = 1;
 c = 0;
 while (c<n)
 @variant ‹n-c›
 @invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
 {
 a=2*a;
 c=c+1
 }
 
 ›
  apply vcg
  by (auto simp: algebra_simps nat_distribs)
  

program_spec use_exp 
  assumes "0≤n"
  ensures ‹n = 2^(2^nat n₀)›
  defines ‹
 n = exp_count_up(n);
 n = exp_count_up(n)
 ›
  apply vcg
  by auto

text ‹Deriving big-step semantics›
schematic_goal 
  "Map.empty: (use_exp,<''n'':=λ_. 2>) ==> ?s"
  "?s ''G_ret_1'' 0 = 16"
  unfolding use_exp_def exp_count_up_def
  apply big_step []
  by bs_simp

schematic_goal 
  "Map.empty: (use_exp,<''n'':=λ_. 2>) ==> ?s"
  "?s ''G_ret_1'' 0 = 16"
  unfolding use_exp_def exp_count_up_def
  apply (big_step'+) []
  by bs_simp
  
    
procedure_spec add3 (a, b, c) returns r
  assumes "a≥0 ∧b≥0 ∧c≥0"  
  ensures "r = a₀+b₀+c₀"
  defines ‹
 r = a+b+c
 ›
  apply vcg
  by auto
  
procedure_spec use_add3 (a, b) returns r
  assumes "a≥0 ∧ b≥0"  
  ensures "r = 2*(a₀+b₀+b₀)"
  defines ‹
 r1 = add3(a, b, b);
 r2 = add3(a, b, b);
 r = r1+r2
 ›
  apply vcg
  by auto
  
procedure_spec no_param () returns r
  assumes "True"
  ensures "r = 42"  
  defines ‹r = 42›
  by vcg_cs
  
procedure_spec foobar (a) returns r
  assumes ‹a≥0›
  ensures "r=84+a₀"
  defines ‹
 r1 = no_param();
 add3(a, a, r1);
 r2 = add3(a, r1, r1);
 r = r2
 ›
  apply vcg_cs
  done
  
end

experiment begin  

  lemma [named_ss vcg_bb]: "BB_PROTECT True" by (auto simp: BB_PROTECT_def)

  procedure_spec add (a,b) returns r assumes True ensures "r=a₀+b₀" defines ‹r = a + b› by vcg_cs

  procedure_spec test (a) returns r assumes True ensures "r = a₀" defines ‹
 x1 = add(a,a);
 x2 = add(a,a);
 x3 = add (x1-x2, a);
 
 x1 = add(a,a);
 x2 = add(a,a);
 x3 = add (x1-x2, a);
 
 x1 = add(a,a);
 x2 = add(a,a);
 x3 = add (x1-x2, a);
 
 x1 = add(a,a);
 x2 = add(a,a);
 x3 = add (x1-x2, a);
 
 x1 = add(a,a);
 x2 = add(a,a);
 x3 = add (x1-x2, a);
 
 x1 = add(a,a);
 x2 = add(a,a);
 x3 = add (x1-x2, a);
 
 r = x3
 ›
  apply vcg
  by auto

end


experiment begin  

lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib 
  
recursive_spec 
  relation ‹measure nat›
  foo (a) returns b 
    assumes "a≥0"
    ensures "b = 2^nat a₀"
    variant "a"
    defines ‹
 if (a==0) b=1
 else {
 b = rec foo (a-1);
 b = 2 * b
 }
 ›
  thm vcg_specs  
  apply vcg
  apply (auto simp: nat_distribs algebra_simps)
  by (metis (full_types) Suc_pred le0 le_less nat_0_iff not_le power_Suc)
  
thm foo_spec  
  
  
recursive_spec 
  odd (a) returns b 
    assumes "a≥0"
    ensures "b≠0 ⟷ odd a₀"
    variant "a"
    defines ‹
 if (a==0) b=0
 else {
 b = rec even (a-1)
 }
 ›
  and
  even (a) returns b
    assumes ‹a≥0›
    ensures "b≠0 ⟷ even a₀"
    variant "a"
    defines ‹
 if (a==0) b=1
 else {
 b = rec odd (a-1)
 }
 ›
  apply vcg  
  by auto  

thm even_spec odd_spec
  

    
end  

end