1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Fri May 07 13:23:24 2021 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Fri May 07 18:12:51 2021 +0200
1.3 @@ -25,25 +25,24 @@
1.4 Vars :: "'a => real list" (*get the variables of a term *)
1.5 matches :: "['a, 'a] => bool"
1.6 matchsub :: "['a, 'a] => bool"
1.7 - some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
1.8 - occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
1.9 + some_occur_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
1.10 + occurs_in :: "[real , 'a] => bool" ("_ occurs'_in _")
1.11
1.12 abs :: "real => real" ("(|| _ ||)")
1.13 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
1.14 absset :: "real set => real" ("(||| _ |||)")
1.15 (*is numeral constant ?*)
1.16 - is'_const :: "real => bool" ("_ is'_const" 10)
1.17 + is_const :: "real => bool" ("_ is'_const" 10)
1.18 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
1.19 - is'_atom :: "real => bool" ("_ is'_atom" 10)
1.20 - is'_even :: "real => bool" ("_ is'_even" 10)
1.21 + is_atom :: "real => bool" ("_ is'_atom" 10)
1.22 + is_even :: "real => bool" ("_ is'_even" 10)
1.23
1.24 (* identity on term level*)
1.25 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
1.26 - argument'_in :: "real => real" ("argument'_in _" 10)
1.27 - sameFunId :: "[real, bool] => bool" (* "same'_funid _ _" 10
1.28 + argument_in :: "real => real" ("argument'_in _" 10)
1.29 + sameFunId :: "[real, bool] => bool" (* "same_funid _ _" 10
1.30 WN0609 changed the id, because ".. _ _" inhibits currying *)
1.31 - filter'_sameFunId:: "[real, bool list] => bool list"
1.32 - ("filter'_sameFunId _ _" 10)
1.33 + filter_sameFunId:: "[real, bool list] => bool list" ("filter'_sameFunId _ _" 10)
1.34 boollist2sum :: "bool list => real"
1.35 lastI :: "'a list \<Rightarrow> 'a"
1.36
1.37 @@ -252,8 +251,8 @@
1.38 (*//------------------------- from Atools.thy------------------------------------------------\\*)
1.39 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
1.40
1.41 -(*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
1.42 -fun eval_occurs_in _ "Prog_Expr.occurs'_in" (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
1.43 +(*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
1.44 +fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const ("Prog_Expr.occurs_in",_) $ v $ t)) _ =
1.45 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
1.46 tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*)
1.47 if occurs_in v t
1.48 @@ -268,10 +267,10 @@
1.49 let fun occurs_in' a b = occurs_in b a
1.50 in foldl or_ (false, map (occurs_in' t) vs) end;
1.51
1.52 -(*("some_occur_in", ("Prog_Expr.some'_occur'_in",
1.53 +(*("some_occur_in", ("Prog_Expr.some_occur_in",
1.54 eval_some_occur_in "#eval_some_occur_in_"))*)
1.55 -fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"
1.56 - (p as (Const ("Prog_Expr.some'_occur'_in",_) $ vs $ t)) _ =
1.57 +fun eval_some_occur_in _ "Prog_Expr.some_occur_in"
1.58 + (p as (Const ("Prog_Expr.some_occur_in",_) $ vs $ t)) _ =
1.59 if some_occur_in (TermC.isalist2list vs) t
1.60 then SOME ((UnparseC.term p) ^ " = True",
1.61 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.62 @@ -279,8 +278,8 @@
1.63 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.64 | eval_some_occur_in _ _ _ _ = NONE;
1.65
1.66 -(*("is_atom",("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
1.67 -fun eval_is_atom (thmid:string) "Prog_Expr.is'_atom"
1.68 +(*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
1.69 +fun eval_is_atom (thmid:string) "Prog_Expr.is_atom"
1.70 (t as (Const _ $ arg)) _ =
1.71 (case arg of
1.72 Free (n,_) => SOME (TermC.mk_thmid thmid n "",
1.73 @@ -290,8 +289,8 @@
1.74 | eval_is_atom _ _ _ _ = NONE;
1.75
1.76 fun even i = (i div 2) * 2 = i;
1.77 -(*("is_even",("Prog_Expr.is'_even", eval_is_even "#is_even_"))*)
1.78 -fun eval_is_even (thmid:string) "Prog_Expr.is'_even"
1.79 +(*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
1.80 +fun eval_is_even (thmid:string) "Prog_Expr.is_even"
1.81 (t as (Const _ $ arg)) _ =
1.82 (case arg of
1.83 Free (n,_) =>
1.84 @@ -306,7 +305,7 @@
1.85 | eval_is_even _ _ _ _ = NONE;
1.86
1.87 (*evaluate 'is_const'*)
1.88 -(*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)
1.89 +(*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
1.90 fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ =
1.91 (case arg of
1.92 Const (n1, _) =>
1.93 @@ -452,9 +451,9 @@
1.94 | eval_cancel _ _ _ _ = NONE;
1.95
1.96 (* get the argument from a function-definition *)
1.97 -(*("argument_in" ,("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"))*)
1.98 -fun eval_argument_in _ "Prog_Expr.argument'_in"
1.99 - (t as (Const ("Prog_Expr.argument'_in", _) $ (_(*f*) $ arg))) _ =
1.100 +(*("argument_in" ,("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"))*)
1.101 +fun eval_argument_in _ "Prog_Expr.argument_in"
1.102 + (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ =
1.103 if is_Free arg (*could be something to be simplified before*)
1.104 then
1.105 SOME (UnparseC.term t ^ " = " ^ UnparseC.term arg,
1.106 @@ -482,10 +481,10 @@
1.107 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
1.108 | same_funid f1 t = raise ERROR ("same_funid called with t = ("
1.109 ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")");
1.110 -(*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",
1.111 - eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)
1.112 -fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId"
1.113 - (p as Const ("Prog_Expr.filter'_sameFunId",_) $
1.114 +(*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",
1.115 + eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*)
1.116 +fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId"
1.117 + (p as Const ("Prog_Expr.filter_sameFunId",_) $
1.118 (fid $ _) $ fs) _ =
1.119 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
1.120 (filter (same_funid fid))) (TermC.isalist2list fs)