(*  Title:      HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy

    Author:     Stefan Berghofer

    Copyright:  secunet Security Networks AG

*)

theory Greatest_Common_Divisor

imports "HOL-SPARK.SPARK"

begin

section \<open>spark intro\<close>

spark_proof_functions

  gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"

declare [[ML_print_depth = 3]](* 3 7 10 9999999*)

spark_open \<open>greatest_common_divisor/g_c_d\<close> (*..from 3 files

  ./greatest_common_divisor/g_c_d.siv, *.fdl, *.rls open *.siv and

  find the following 2 open verification conditions (VC): *)

section \<open>example 1\<close>

spark_vc procedure_g_c_d_4 (*..select 1st VC for proof: *)

proof -

  from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)

  with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1

    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])

next

  from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2

    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)

qed

subsection \<open>observing interaction on the proof\<close>

text \<open>

  :

# Clicks on different positions give different traces.

# There are blocks with equal traces (separated by \n or |)

    proof

      from \<open>0 < d\<close>     |     have "0 \<le> c mod d"     |     by (rule pos_mod_sign)

      with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close>   |     show ?C1

        by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])

    next [ONLY ### Private_Output.report keyword1]

      from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>      |      show ?C2

        by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)

    qed [NO TRACE]

# Specific traces seem to be extended by the subsequent one, 

  e.g.   from \<open>0 < d\<close>        extended by        have "0 \<le> c mod d"

  but both NOT by ...                                      by (rule pos_mod_sign)

# Private_Output.report seems to have "" as argument frequently

# Output.report provided semantic annotations in Naproche;

  thus ALL calls of Output.report (in src/Pure) are traced an show up at these elements:

    proof                                        x  x  .  .  .  

    from \<open>0 < d\<close>                                 x  .  x  x  x  

    have "0 \<le> c mod d"                           x  .  x  x  .  

    by (rule pos_mod_sign)                       x  x  .  .  .  

    with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> x  .  x  x  x  

    show ?C1                                     x  .  x  x  .  

    by (simp add: ...[symmetric])                x  x  .  .  .  

    next                                         x  .  .  .  .  

    from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>     x  .  x  x  x  

    show ?C2                                     x  .  x  x  .  

    by (simp add: ...[symmetric] gcd_non_0_int)  x  x  .  .  .  

                                                 |  |  |  |  Context_Position.report_generic

                                                 |  |  |  Syntax_Phases.check_terms

                                                 |  |  Syntax_Phases.check_typs

                                                 |  Token.syntax_generic

                                                 Private_Output.report

\<close>

subsection \<open>tracing calls of Output.report\<close>

text \<open>

(*--------- click on "proof -" --------

### Private_Output.report keyword1

### Private_Output.report language

### Private_Output.report entityo

### Private_Output.report operator

### Token.syntax_generic, Scan.error

### Private_Output.report 

### Token.syntax_generic, Scan.error

\<close>

text \<open>

(*--------- click on "from \<open>0 < d\<close>" --------

### Private_Output.report keyword1

### Private_Output.report cartouch

### Private_Output.report delimite

### Private_Output.report entityo

### Syntax_Phases.check_typs

### Private_Output.report 

### Syntax_Phases.check_typs

### Private_Output.report 

### Syntax_Phases.check_terms

### Private_Output.report typingo          =====

### Context_Position.report_generic           //--- different to subsequent part below

### Private_Output.report entityo

\<close>

text \<open>

(*--------- click on "have "0 \<le> c mod d"" --------

### Private_Output.report keyword1

### Private_Output.report 

### Private_Output.report cartouch

### Private_Output.report delimite

### Private_Output.report entityo

### Syntax_Phases.check_typs

### Private_Output.report 

### Syntax_Phases.check_typs

### Private_Output.report 

### Syntax_Phases.check_terms

### Private_Output.report typingo          =====

### Syntax_Phases.check_typs                  //--- different to previous part above

### Private_Output.report 

### Syntax_Phases.check_terms

### Private_Output.report 

\<close>

subsection \<open>signatures of the traced callers of Private_Output.report\<close>

ML \<open>

\<close> ML \<open>

Private_Output.report          : string(*= markup*) list                   -> unit; 

Context_Position.report_generic: Context.generic -> Position.T -> Markup.T -> unit;

Token.syntax_generic           : 'a Token.context_parser -> Token.src -> Context.generic ->

                                   'a * Context.generic;

(*Syntax_Phases.check_typs     : Proof.context -> typ list -> typ list;    ..local*)

(*Syntax_Phases.check_terms    : Proof.context -> term list -> term list;  ..local*)

\<close> ML \<open>

\<close>

subsection \<open>lookup calls of Syntax_Phases.check_terms\<close>

text \<open>

  focus are    "from \<open>0 < d\<close>"   and   have "0 \<le> c mod d".

  encapsulation?:

    Syntax_Phases.check_terms NOwhere in src/Pure,

    check_terms occurs in Theory.setup (Syntax.install_operations {..check_terms = check_terms..}

    and nowhere else (except fun check_props)

  so the calls are Syntax.check_terms ? -- NO: calls.1..4 --vv pop up in NONE of the 3 traces above.

                                           ^^^^^^^^^^^^^^^     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

  but they seem to be identical:

    Syntax_Phases.check_terms: Proof.context -> term list -> term list;

           Syntax.check_terms: Proof.context -> term list -> term list;

    ?! there are 3-times structure Syntax:

      Pure/Syntax/lexicon.ML                      /NO check_terms/

        signature LEXICON = sig structure Syntax: sig val const: string -> term ..

      Pure/Syntax/syntax.ML 

        type operations = {..., ..., check_terms: Proof.context -> term list -> term list, ..

        val check_terms = operation #check_terms;

      Pure/Syntax/syntax_trans.ML                 /NO check_terms/

  the ASSUMED callers of Syntax.check_terms:

//  Pure/Isar/expression.ML

//    1,val inst_morphism: (string * typ) list -> (string * bool) * term list -> Proof.context ->

//        morphism * Proof.context

//    2.val check_autofix:

//        ('a * ('b * term list)) list ->

//          ('c * term) list list ->

//            (typ, term, 'd) ctxt list ->

//              ('e * (term * term list) list) list -> Proof.context ->

//        (('a * ('b * term list)) list * ('c * term) list list * (typ, term, 'd) ctxt list *

//          ('e * (term * term list) list) list) * Proof.context

//        val check: (term * term list) list -> Proof.context ->

//          (term * term list) list * Proof.context

//  Pure/Isar/obtain.ML

//    3.val Obtain.read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list 

//  Pure/Isar/proof.ML

//    4.val let_bind: (term list * term) list -> state -> state

//    5.val let_bind_cmd: (string list * string) list -> state -> state

//        val read_terms: context -> typ -> string list -> term list

//  Pure/Isar/proof_context.ML

//    6.val infer_type: Proof.context -> string * typ -> typ

//  Pure/simplifier.ML

//    7.val Simplifier.define_simproc: binding -> term Simplifier.simproc_spec ->

//        local_theory -> local_theory

//  Pure/Tools/rule_insts.ML

//    8.val Rule_Insts.read_term: string -> Proof.context -> term * Proof.context

//    :

//    1.. looked up in the sequel

\<close>

subsection \<open>lookup Syntax.check_terms -> *1..4\<close>

text \<open>\<close>

subsubsection \<open>lookup 1* -> Expression.inst_morphism\<close>

text \<open>\<close>

subsubsection \<open>lookup 2* -> Expression.check_autofix\<close>

text \<open>

\<close> 

subsubsection \<open>lookup 3* -> Obtain.read_obtains\<close>

text \<open>\<close>

subsubsection \<open>lookup 4* -> Proof.let_bind\<close>

text \<open>\<close>

subsubsection \<open>lookup 5* -> Proof.let_bind_cmd\<close>

text \<open>\<close>

subsubsection \<open>lookup 6* -> Proof_Context.infer_type\<close>

text \<open>\<close>

subsubsection \<open>lookup 7* -> Simplifier.define_simproc\<close>

text \<open>\<close>

subsubsection \<open>lookup 8* -> Rule_Insts.read_term\<close>

text \<open>\<close>

section \<open>example 2\<close>

spark_vc procedure_g_c_d_11 (*..select 2nd VC for proof: *)

proof -

  from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d = 0\<close>

  have "d dvd c"

    by (auto simp add: sdiv_pos_pos dvd_def ac_simps)

  with \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C1

    by simp

qed

spark_end

end