1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Thu Oct 22 16:26:45 2020 +0200
1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sat Oct 24 12:31:22 2020 +0200
1.3 @@ -10,9 +10,11 @@
1.4 spark_proof_functions
1.5 gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
1.6
1.7 -spark_open \<open>greatest_common_divisor/g_c_d\<close>
1.8 +spark_open \<open>greatest_common_divisor/g_c_d\<close> (*..from 3 files
1.9 + ./greatest_common_divisor/g_c_d.siv, *.fdl, *.rls
1.10 + find the following 2 open verification conditions (VC): *)
1.11
1.12 -spark_vc procedure_g_c_d_4 (*..def.in greatest_common_divisor/g_c_d.siv *)
1.13 +spark_vc procedure_g_c_d_4 (*..select 1st VC for proof: *)
1.14 proof -
1.15 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
1.16 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
1.17 @@ -22,7 +24,7 @@
1.18 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
1.19 qed
1.20
1.21 -spark_vc procedure_g_c_d_11
1.22 +spark_vc procedure_g_c_d_11 (*..select 2nd VC for proof: *)
1.23 proof -
1.24 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d = 0\<close>
1.25 have "d dvd c"
2.1 --- a/test/Pure/Isar/Downto_Synchronized.thy Thu Oct 22 16:26:45 2020 +0200
2.2 +++ b/test/Pure/Isar/Downto_Synchronized.thy Sat Oct 24 12:31:22 2020 +0200
2.3 @@ -31,97 +31,129 @@
2.4 text \<open>
2.5 spark_vc starts an interactive proof, given data for initialising the proof.
2.6 conclusions:
2.7 - * spark_vc <--> ISAC: Example \<open>exp_Statics_Biegel_Timischl_7-70\<close>
2.8 - * for how to open the data-file \<open>exp_Statics_Biegel_Timischl_7-70\<close> see spark_open
2.9 +* spark_vc <--> ISAC: Calculation \<open>~~/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
2.10 +* for how to open the data-file \<open>exp_Statics_Biegel_Timischl_7-70\<close> see spark_open
2.11 \<close> ML \<open>
2.12 -\<close> ML \<open>
2.13 +\<close>
2.14 +declare [[ML_print_depth = 999]]
2.15 +ML \<open>
2.16 signature SPECIFICATION =
2.17 sig
2.18 val theorem: bool -> string -> Method.text option ->
2.19 - (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
2.20 - string list -> Element.context_i list -> Element.statement_i ->
2.21 - bool -> local_theory -> Proof.state
2.22 + (thm list list -> local_theory -> local_theory) ->
2.23 + Attrib.binding -> string list -> Element.context_i list -> Element.statement_i ->
2.24 + bool -> local_theory ->
2.25 + Proof.state
2.26 end
2.27 -(** )structure Specification: SPECIFICATION =
2.28 -struct( **)
2.29 +(**)structure Specification: SPECIFICATION =
2.30 +struct(**)
2.31 fun gen_theorem (_: bool)
2.32 -(*Bundle.includes:*)
2.33 - (_: string list -> Proof.context -> Proof.context)
2.34 -(*(K I):*)
2.35 - (_: 'a -> 'b -> 'b)
2.36 -(*Expression.cert_statement:*)
2.37 - (_: (Element.context_i list ->
2.38 - Element.statement_i ->
2.39 - Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context)
2.40 - = ()
2.41 -\<close> ML \<open>
2.42 -\<close> ML \<open>
2.43 -val Proof_state = Proof.init @{context}
2.44 -\<close> ML \<open>
2.45 -fun gen_theorem (_: bool) (_:string list) (_:Proof.context) (_:Proof.context) = @{context}
2.46 -\<close> ML \<open>
2.47 + (_: 'a -> local_theory -> Proof.context)
2.48 + (_: local_theory -> Token.src -> Token.src)
2.49 + (_: ('b, 'c, 'd) Element.ctxt list -> ('e, 'f) Element.stmt -> Proof.context ->
2.50 + ((binding * Token.src list) * (term * term list) list) list * Proof.context)
2.51 + (_: bool)
2.52 + (_: string)
2.53 + (_: Method.text option)
2.54 + (_: thm list list -> local_theory -> Proof.context)
2.55 + (_: binding * Token.src list)
2.56 + (_: 'a)
2.57 + (_: ('b, 'c, 'd) Element.ctxt list)
2.58 + (_: ('e, 'f) Element.stmt)
2.59 + (_: bool)
2.60 + (_: local_theory) =
2.61 + Proof.init @{context};
2.62 +
2.63 val theorem = (*<----- orig*)
2.64 gen_theorem false Bundle.includes (K I) Expression.cert_statement;
2.65 -end
2.66 -\<close> ML \<open> (*----- investigate args of theorem..*)
2.67 -Bundle.includes: string list -> Proof.context -> Proof.context
2.68 +(*
2.69 + Signature: val theorem: bool -> string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> Attrib.binding -> string list -> ...
2.70 + Structure: val theorem: Proof.state -> Proof.state
2.71 +*)
2.72 +(**)end(**)
2.73 \<close> ML \<open>
2.74 -(K I)(*: _b -> _a -> _a*)
2.75 -\<close> ML \<open>
2.76 -Expression.cert_statement: Element.context_i list -> Element.statement_i -> Proof.context ->
2.77 - (Attrib.binding * (term * term list) list) list * Proof.context
2.78 -\<close> ML \<open>
2.79 -\<close> ML \<open> (*----- get type of gen_theorem..*)
2.80 -fun theorem gen_theorem =
2.81 - gen_theorem false Bundle.includes (K I) Expression.cert_statement;
2.82 -\<close> ML \<open>
2.83 -theorem:
2.84 - (bool ->
2.85 -(*Bundle.includes:*)
2.86 - (string list -> Proof.context -> Proof.context) ->
2.87 -(*(K I):*)
2.88 - ('a -> 'b -> 'b) ->
2.89 -(*Expression.cert_statement:*)
2.90 - (Element.context_i list -> Element.statement_i -> Proof.context ->
2.91 - (Attrib.binding * (term * term list) list) list * Proof.context)
2.92 - -> 'c)
2.93 - -> 'c
2.94 -\<close> ML \<open> (*----- replace 'c by Proof.state found in signature SPECIFICATION*)
2.95 -theorem:
2.96 - (bool ->
2.97 -(*Bundle.includes:*)
2.98 - (string list -> Proof.context -> Proof.context) ->
2.99 -(*(K I):*)
2.100 - ('a -> 'b -> 'b) ->
2.101 -(*Expression.cert_statement:*)
2.102 - (Element.context_i list -> Element.statement_i -> Proof.context ->
2.103 - (Attrib.binding * (term * term list) list) list * Proof.context)
2.104 - -> Proof.state)
2.105 - -> Proof.state
2.106 -\<close> ML \<open>
2.107 -
2.108
2.109 signature EXPRESSION =
2.110 sig
2.111 - val cert_statement: Element.context_i list -> Element.statement_i ->
2.112 +val cert_statement: Element.context_i list -> Element.statement_i ->
2.113 Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
2.114 - val read_statement: Element.context list -> Element.statement ->
2.115 - Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
2.116 +(** )val read_statement: Element.context list -> Element.statement ->
2.117 + Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context( **)
2.118 end
2.119 -structure Expression : EXPRESSION =
2.120 -struct
2.121 +(**)structure Expression : EXPRESSION =
2.122 +struct(**)
2.123 +fun prep_statement (*dummy*)
2.124 +(* 1 *)(_: {do_close: bool, fixed_frees: bool, strict: bool} ->
2.125 +(*2-4*) 'a list * 'b list ->
2.126 +(* 5 *) ('c -> 'c) ->
2.127 +(* 6 *) 'd ->
2.128 +(* 7 *) 'e ->
2.129 +(* 8 *) Proof.context ->
2.130 +(*9-f*) ('f * 'g * 'h * 'i list * 'j) *
2.131 +(* g *) 'k
2.132 +(* *))
2.133 +(* *) (_: 'i -> Proof.context -> 'l * Proof.context)
2.134 +(* *) (_: 'd) (_: 'e) (_: Proof.context) =
2.135 +(* e *) ( []: (Attrib.binding * (term * term list) list) list,
2.136 +(* *) @{context}
2.137 +(* *) )
2.138 +datatype ctxt = datatype Element.ctxt;
2.139 +datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
2.140 +fun cert_full_context_statement (*dummy*)
2.141 +(* 1 *)(_: {do_close: 'a, fixed_frees: bool, strict: bool})
2.142 +(* 2 *) (_: (string * ((string * bool) * (term map * (('b * 'c list) * term) list))) list *
2.143 +(* 3 *) (binding * typ option * mixfix) list
2.144 +(* 4 *) )
2.145 +(* 5 *) (_: Proof.context -> Proof.context)
2.146 +(* 6 *) (_: (typ, term, 'd) ctxt list)
2.147 +(* 7 *) (_: (typ, term) Element.stmt)
2.148 +(* 8 *) (_: Proof.context) =
2.149 +(* 9 *) ( (
2.150 +(* a *) []:((bstring * typ) * mixfix) list,
2.151 +(* b *) []:(string * morphism) list,
2.152 +(* c *) []:(('b * 'c list) * term) list list,
2.153 +(* d *) []:(typ, 'e, 'f) ctxt list,
2.154 +(* e *) []:(Attrib.binding * (term * term list) list) list
2.155 +(* f *) ),
2.156 +(* g *) ([]:(string * typ) list, @{context})
2.157 +(* h *) );
2.158 +(*Element.activate_i: Element.context_i -> Proof.context -> Element.context_i * Proof.context;*)
2.159 +
2.160 fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
2.161 -fun read_statement x = prep_statement read_full_context_statement Element.activate x;
2.162 -end
2.163 +(** )fun read_statement x = prep_statement read_full_context_statement Element.activate x;( **)
2.164 +(**)end(**)
2.165 +\<close> ML \<open>
2.166
2.167 +\<close> ML \<open>
2.168
2.169 signature ELEMENT =
2.170 sig
2.171 + datatype ('typ, 'term, 'fact) ctxt =
2.172 + Fixes of (binding * 'typ option * mixfix) list |
2.173 + Constrains of (string * 'typ) list |
2.174 + Assumes of (Attrib.binding * ('term * 'term list) list) list |
2.175 + Defines of (Attrib.binding * ('term * 'term list)) list |
2.176 + Notes of string * (Attrib.binding * ('fact * Token.src list) list) list |
2.177 + Lazy_Notes of string * (binding * 'fact lazy)
2.178 + type context_i
2.179 val activate_i: context_i -> Proof.context -> context_i * Proof.context
2.180 - val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
2.181 +(*val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context*)
2.182 end
2.183 +\<close> ML \<open>
2.184 structure Element: ELEMENT =
2.185 struct
2.186 +datatype ('typ, 'term, 'fact) ctxt =
2.187 + Fixes of (binding * 'typ option * mixfix) list |
2.188 + Constrains of (string * 'typ) list |
2.189 + Assumes of (Attrib.binding * ('term * 'term list) list) list |
2.190 + Defines of (Attrib.binding * ('term * 'term list)) list |
2.191 + Notes of string * (Attrib.binding * ('fact * Token.src list) list) list |
2.192 + Lazy_Notes of string * (binding * 'fact lazy)
2.193 +type context_i = (typ, term, thm list) ctxt;
2.194 +fun map_ctxt_attrib (_: Token.src -> Token.src) (xxx : ('typ, 'term, 'fact) ctxt) = xxx
2.195 +datatype generic = Theory of theory | Proof of Proof.context
2.196 +fun init (_: context_i) (xxx: Context.generic) = xxx
2.197 +
2.198 fun activate_i elem ctxt =
2.199 let
2.200 val elem' =
2.201 @@ -139,14 +171,17 @@
2.202
2.203 signature PRIVATE_CONTEXT =
2.204 sig
2.205 + type generic
2.206 val proof_map: (generic -> generic) -> Proof.context -> Proof.context
2.207 end
2.208 structure Context: PRIVATE_CONTEXT =
2.209 struct
2.210 +datatype generic = Theory of theory | Proof of Proof.context;
2.211 +fun the_proof (_: generic) = @{context} (*dummy*)
2.212 +
2.213 fun proof_map f = the_proof o f o Proof;
2.214 -datatype generic = Theory of theory | Proof of Proof.context;
2.215
2.216 -(*/--------------------? related ?-------------------------------------------\*)
2.217 +(*/--------------------? related ?-------------------------------------------\* )
2.218 fun declare_theory_data pos empty extend merge =
2.219 let
2.220 val k = serial ();
2.221 @@ -160,20 +195,44 @@
2.222 (*private copy avoids potential conflict of table exceptions*)
2.223 structure Datatab = Table(type key = int val ord = int_ord);
2.224 (*^^^^*)
2.225 +( *\--------------------? related ?-------------------------------------------/*)
2.226 end
2.227
2.228 +\<close> ML \<open>
2.229 signature CHANGE_TABLE =
2.230 sig
2.231 structure Table: TABLE
2.232 end
2.233 signature TABLE =
2.234 sig
2.235 + type key
2.236 + type 'a table
2.237 val update: key * 'a -> 'a table -> 'a table
2.238 val join: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
2.239 'a table * 'a table -> 'a table (*exception DUP*)
2.240 end
2.241 +(**)functor Table(Key: KEY): TABLE =
2.242 +struct
2.243 +type key = Key.key;(** )
2.244 +type key = int val ord = int_ord;( **)
2.245 +datatype 'a table =
2.246 + Empty |
2.247 + Branch2 of 'a table * (key * 'a) * 'a table |
2.248 + Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
2.249 +fun is_empty (_: 'a table) = true (*dummy*)
2.250 +fun modify (_: key) (_: 'b -> 'c) (xxx : 'a table) = xxx (*dummy*)
2.251
2.252 fun update (key, x) tab = modify key (fn _ => x) tab;
2.253 +
2.254 +(*/------------------------------- construct dummy above -------------------------\* )
2.255 +(* find sig.of modify via arg..*)
2.256 +fun update modify (key, x) tab = modify key (fn _ => x) tab;
2.257 + update: ('a -> ('b -> 'c) -> 'd -> 'e) -> 'a * 'c -> 'd -> 'e
2.258 +(*sig: update: key * 'a -> 'a table -> 'a table*)
2.259 +( *\------------------------------- construct dummy above -------------------------/*)
2.260 +
2.261 +fun fold_table (*dummy*)
2.262 + (_: key * 'a -> 'b table -> 'b table) (_: 'c table) (xxx: 'c table) = xxx
2.263 (* simultaneous modifications *)
2.264 fun join f (table1, table2) =
2.265 let
2.266 @@ -183,12 +242,23 @@
2.267 else if is_empty table1 then table2
2.268 else fold_table add table2 table1
2.269 end;
2.270 +(*/------------------------------- construct dummy above -------------------------\* )
2.271 +(* find sig.of modify via arg..*)
2.272 +fun join fold_table f (table1, table2) =
2.273 + let
2.274 + fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
2.275 + in
2.276 + if pointer_eq (table1, table2) then table1
2.277 + else if is_empty table1 then table2
2.278 + else fold_table add table2 table1
2.279 + end;
2.280
2.281 -(*============================================================================================
2.282 -search " = Synchronized.var" leads back to Context:
2.283 + join: ((key * 'a -> 'b table -> 'b table) -> 'c table -> 'c table -> 'c table) ->
2.284 + (key -> 'd * 'a -> 'a) -> 'c table * 'c table -> 'c table
2.285 +(*sig: join: (key -> 'a * 'a -> 'a) -> 'a table * 'a table -> 'a table*)
2.286 +( *\------------------------------- construct dummy above -------------------------/*)
2.287
2.288 -val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
2.289 -*)
2.290 +(**)end(**)
2.291 \<close> ML \<open>
2.292 \<close> ML \<open>
2.293 \<close>