(* 
   note that IMP2 is not part of the Isabelle distribution,
   but of the "Archive of Formal Proofs (AFP)";
   
   so to run this theory, 
   - download the AFP from https://www.isa-afp.org
   - extract it, e.g., to ~/afp/2024
   - start Isabelle with 
    
     isabelle jedit -d ~/afp/2024/thys -l IMP2 Exercise11.thy 

     this will precompile IMP2 once, and then load the demo.
*)
theory Exercise11
  imports IMP2.IMP2
begin



procedure_spec (partial) copy_1(x) 
  returns y 
  assumes \<open>x \<ge> 0\<close> 
    ensures "y = x\<^sub>0"
  defines \<open>
    a = x;
    y = 0;
    while (a \<noteq> 0) 
    @invariant \<open>True \<or> adjust_me\<close>
    {
      y = y + 1;
      a = a - 1
    }
  \<close>
  apply vcg
   apply simp
  oops


procedure_spec copy_2(x) 
  returns y 
  assumes \<open>x \<ge> 0\<close> 
    ensures "y = x\<^sub>0"
  defines \<open>
    a = x;
    y = 0;
    while (a \<noteq> 0) 
    @invariant \<open>True \<or> adjust_me\<close>
    @variant \<open>2 * x - 3 * a + 4 * y - 5 + adjust_me_2\<close>
    {
      y = y + 1;
      a = a - 1
    }
  \<close>
  apply vcg
     apply simp
    apply simp
  oops



procedure_spec (partial) copy_3(x) 
  returns y 
  assumes \<open>True\<close> 
    ensures "y = x\<^sub>0"
  defines \<open>
    a = x;
    y = 0;
    while (a \<noteq> 0) 
    @invariant \<open>True \<or> adjust_me\<close>
    {
      y = y + 1;
      a = a - 1
    }
  \<close>
  apply vcg
   apply simp
  oops


procedure_spec (partial) fact_non_term(x) 
  returns y 
  assumes \<open>x < 0\<close> 
    ensures "True \<or> adjust_me"
  defines \<open>
    y = 1;
    while (x \<noteq> 0) 
    @invariant \<open>True \<or> adjust_me\<close>
    {
      y = y * x;
      x = x - 1
    }
  \<close>
  apply vcg
  apply simp
  done


end