1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Wed Dec 16 16:25:55 2020 +0100
     1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Thu Dec 17 09:10:30 2020 +0100
     1.3 @@ -7,6 +7,7 @@
     1.4  imports "HOL-SPARK.SPARK"
     1.5  begin
     1.6  
     1.7 +section \<open>spark intro\<close>
     1.8  spark_proof_functions
     1.9    gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    1.10  
    1.11 @@ -16,6 +17,7 @@
    1.12    ./greatest_common_divisor/g_c_d.siv, *.fdl, *.rls open *.siv and
    1.13    find the following 2 open verification conditions (VC): *)
    1.14  
    1.15 +section \<open>example 1\<close>
    1.16  spark_vc procedure_g_c_d_4 (*..select 1st VC for proof: *)
    1.17  proof -
    1.18    from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
    1.19 @@ -25,7 +27,55 @@
    1.20    from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
    1.21      by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
    1.22  qed
    1.23 +text \<open>
    1.24 +  general notes:
    1.25 +# Clicks on different positions give different traces.
    1.26 +# There are blocks with equal traces (separated by \n or |)
    1.27 +    proof
    1.28 +      from \<open>0 < d\<close>     |     have "0 \<le> c mod d"     |     by (rule pos_mod_sign)
    1.29 +      with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close>   |     show ?C1
    1.30 +        by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
    1.31 +    next [ONLY ### Private_Output.report keyword1]
    1.32 +      from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>      |      show ?C2
    1.33 +        by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
    1.34 +    qed [NO TRACE]
    1.35 +# Specific traces seem to be extended by the subsequent one, 
    1.36 +  e.g.   from \<open>0 < d\<close>        extended by        have "0 \<le> c mod d"
    1.37 +  but both NOT by ...                                      by (rule pos_mod_sign)
    1.38 +# Private_Output.report seems to have "" as argument frequently
    1.39 +# Output.report provided semantic annotations in Naproche;
    1.40 +  thus ALL calls of Output.report (in src/pure) are traced:
    1.41 +    proof                                        x  x  .  .  .  
    1.42 +    from \<open>0 < d\<close>                                 x  .  x  x  x  
    1.43 +    have "0 \<le> c mod d"                           x  .  x  x  .  
    1.44 +    by (rule pos_mod_sign)                       x  x  .  .  .  
    1.45 +    with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> x  .  x  x  x  
    1.46 +    show ?C1                                     x  .  x  x  .  
    1.47 +    by (simp add: ...[symmetric])                x  x  .  .  .  
    1.48 +    next                                         x  .  .  .  .  
    1.49 +    from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>     x  .  x  x  x  
    1.50 +    show ?C2                                     x  .  x  x  .  
    1.51 +    by (simp add: ...[symmetric] gcd_non_0_int)  x  x  .  .  .  
    1.52 +                                                 |  |  |  |  Context_Position.report_generic
    1.53 +                                                 |  |  |  Syntax_Phases.check_terms
    1.54 +                                                 |  |  Syntax_Phases.check_typs
    1.55 +                                                 |  Token.syntax_generic
    1.56 +                                                 Private_Output.report
    1.57 +\<close>
    1.58  
    1.59 +subsection \<open>tracing calls of \<close>
    1.60 +text \<open>
    1.61 +(*--------- click on "proof -" --------
    1.62 +### Private_Output.report keyword1
    1.63 +### Private_Output.report language
    1.64 +### Private_Output.report entityo
    1.65 +### Private_Output.report operator
    1.66 +### Token.syntax_generic, Scan.error
    1.67 +### Private_Output.report 
    1.68 +### Token.syntax_generic, Scan.error
    1.69 +\<close>
    1.70 +
    1.71 +section \<open>example 2\<close>
    1.72  spark_vc procedure_g_c_d_11 (*..select 2nd VC for proof: *)
    1.73  proof -
    1.74    from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d = 0\<close>