# HG changeset patch # User haftmann # Date 1392843915 -3600 # Node ID 3c7610b8dcfc096845ec7ae8edc88d8694e3c6f3 # Parent 6535c537b2436dd317acbd84d7f2d3005ea48986 more convenient syntax for permanent interpretation diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int1_const.thy --- a/src/HOL/IMP/Abs_Int1_const.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Feb 19 22:05:15 2014 +0100 @@ -69,7 +69,7 @@ permanent_interpretation Abs_Int where \ = \_const and num' = Const and plus' = plus_const -defines AI_const is AI and step_const is step' and aval'_const is aval' +defining AI_const = AI and step_const = step' and aval'_const = aval' .. diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int1_parity.thy --- a/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 19 22:05:15 2014 +0100 @@ -125,7 +125,7 @@ permanent_interpretation Abs_Int where \ = \_parity and num' = num_parity and plus' = plus_parity -defines aval_parity is aval' and step_parity is step' and AI_parity is AI +defining aval_parity = aval' and step_parity = step' and AI_parity = AI .. diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int2_ivl.thy --- a/src/HOL/IMP/Abs_Int2_ivl.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed Feb 19 22:05:15 2014 +0100 @@ -320,7 +320,7 @@ permanent_interpretation Val_lattice_gamma where \ = \_ivl and num' = num_ivl and plus' = "op +" -defines aval_ivl is aval' +defining aval_ivl = aval' proof case goal1 show ?case by(simp add: \_inf) next @@ -354,11 +354,11 @@ where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl -defines inv_aval_ivl is inv_aval' -and inv_bval_ivl is inv_bval' -and step_ivl is step' -and AI_ivl is AI -and aval_ivl' is aval'' +defining inv_aval_ivl = inv_aval' +and inv_bval_ivl = inv_bval' +and step_ivl = step' +and AI_ivl = AI +and aval_ivl' = aval'' .. diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int3.thy --- a/src/HOL/IMP/Abs_Int3.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int3.thy Wed Feb 19 22:05:15 2014 +0100 @@ -264,7 +264,7 @@ where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl -defines AI_wn_ivl is AI_wn +defining AI_wn_ivl = AI_wn .. diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Wed Feb 19 22:05:15 2014 +0100 @@ -62,8 +62,8 @@ qed permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" -defines AI_const is AI -and aval'_const is aval' +defining AI_const = AI +and aval'_const = aval' proof qed (auto simp: iter'_pfp_above) text{* Straight line code: *} diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Wed Feb 19 22:05:15 2014 +0100 @@ -202,10 +202,10 @@ permanent_interpretation Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)" -defines afilter_ivl is afilter -and bfilter_ivl is bfilter -and AI_ivl is AI -and aval_ivl is aval' +defining afilter_ivl = afilter +and bfilter_ivl = bfilter +and AI_ivl = AI +and aval_ivl = aval' proof qed (auto simp: iter'_pfp_above) diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Feb 19 22:05:15 2014 +0100 @@ -194,10 +194,10 @@ permanent_interpretation Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)" -defines afilter_ivl' is afilter -and bfilter_ivl' is bfilter -and AI_ivl' is AI -and aval_ivl' is aval' +defining afilter_ivl' = afilter +and bfilter_ivl' = bfilter +and AI_ivl' = AI +and aval_ivl' = aval' proof qed (auto simp: iter'_pfp_above) value [code] "list_up(AI_ivl' test3_ivl Top)" diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Wed Feb 19 22:05:15 2014 +0100 @@ -68,7 +68,7 @@ permanent_interpretation Abs_Int where \ = \_const and num' = Const and plus' = plus_const -defines AI_const is AI and step_const is step' and aval'_const is aval' +defining AI_const = AI and step_const = step' and aval'_const = aval' .. diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Wed Feb 19 22:05:15 2014 +0100 @@ -115,7 +115,7 @@ permanent_interpretation Abs_Int where \ = \_parity and num' = num_parity and plus' = plus_parity -defines aval_parity is aval' and step_parity is step' and AI_parity is AI +defining aval_parity = aval' and step_parity = step' and AI_parity = AI .. diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Wed Feb 19 22:05:15 2014 +0100 @@ -181,7 +181,7 @@ permanent_interpretation Val_abs1_gamma where \ = \_ivl and num' = num_ivl and plus' = plus_ivl -defines aval_ivl is aval' +defining aval_ivl = aval' proof case goal1 thus ?case by(auto simp add: \_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) @@ -219,11 +219,11 @@ where \ = \_ivl and num' = num_ivl and plus' = plus_ivl and test_num' = in_ivl and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl -defines afilter_ivl is afilter -and bfilter_ivl is bfilter -and step_ivl is step' -and AI_ivl is AI -and aval_ivl' is aval'' +defining afilter_ivl = afilter +and bfilter_ivl = bfilter +and step_ivl = step' +and AI_ivl = AI +and aval_ivl' = aval'' .. diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Wed Feb 19 22:05:15 2014 +0100 @@ -229,7 +229,7 @@ where \ = \_ivl and num' = num_ivl and plus' = plus_ivl and test_num' = in_ivl and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl -defines AI_ivl' is AI_wn +defining AI_ivl' = AI_wn .. diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/ex/Interpretation_with_Defs.thy --- a/src/HOL/ex/Interpretation_with_Defs.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/ex/Interpretation_with_Defs.thy Wed Feb 19 22:05:15 2014 +0100 @@ -6,7 +6,7 @@ theory Interpretation_with_Defs imports Pure -keywords "permanent_interpretation" :: thy_goal +keywords "defining" and "permanent_interpretation" :: thy_goal begin ML_file "~~/src/Tools/interpretation_with_defs.ML" diff -r 6535c537b243 -r 3c7610b8dcfc src/Tools/interpretation_with_defs.ML --- a/src/Tools/interpretation_with_defs.ML Wed Feb 19 22:05:05 2014 +0100 +++ b/src/Tools/interpretation_with_defs.ML Wed Feb 19 22:05:15 2014 +0100 @@ -102,8 +102,8 @@ Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"} "prove interpretation of locale expression into named theory" (Parse.!!! (Parse_Spec.locale_expression true) -- - Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" - -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] -- + Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" + -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] -- Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));