1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Jun 21 14:39:52 2021 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Jun 21 15:36:09 2021 +0200
1.3 @@ -91,14 +91,14 @@
1.4 (**)
1.5
1.6 (*+ for Or_to_List +*)
1.7 -fun or2list (Const ("HOL.True",_)) = ((*tracing"### or2list True";*) UniversalList)
1.8 - | or2list (Const ("HOL.False",_)) = ((*tracing"### or2list False";*) EmptyList)
1.9 - | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
1.10 +fun or2list (Const (\<^const_name>\<open>True\<close>,_)) = ((*tracing"### or2list True";*) UniversalList)
1.11 + | or2list (Const (\<^const_name>\<open>False\<close>,_)) = ((*tracing"### or2list False";*) EmptyList)
1.12 + | or2list (t as Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
1.13 | or2list ors =
1.14 let
1.15 - fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
1.16 + fun get ls (Const (\<^const_name>\<open>disj\<close>,_) $ o1 $ o2) =
1.17 (case o2 of
1.18 - Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
1.19 + Const (\<^const_name>\<open>disj\<close>,_) $ _ $ _ => get (ls @ [o1]) o2
1.20 | _ => ls @ [o1, o2])
1.21 | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
1.22 in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
1.23 @@ -224,10 +224,10 @@
1.24 | eval_var _ _ _ _ = NONE;
1.25
1.26 (* refer to Thm.lhs_of *)
1.27 -fun lhs (Const ("HOL.eq",_) $ l $ _) = l
1.28 +fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
1.29 | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
1.30 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
1.31 -fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
1.32 +fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ =
1.33 SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
1.34 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
1.35 | eval_lhs _ _ _ _ = NONE;
1.36 @@ -239,10 +239,10 @@
1.37 val it = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
1.38 *)
1.39
1.40 -fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
1.41 +fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
1.42 | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
1.43 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
1.44 -fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
1.45 +fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ =
1.46 SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
1.47 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
1.48 | eval_rhs _ _ _ _ = NONE;
1.49 @@ -319,9 +319,9 @@
1.50 | eval_const _ _ _ _ = NONE;
1.51
1.52 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
1.53 -(*("PLUS" ,("Groups.plus_class.plus" , (**)eval_binop "#add_")),
1.54 - ("TIMES" ,("Groups.times_class.times" , (**)eval_binop "#mult_")),
1.55 - ("POWER" ,("Transcendental.powr" , (**)eval_binop "#power_"))*)
1.56 +(*("PLUS" ,(\<^const_name>\<open>plus\<close> , (**)eval_binop "#add_")),
1.57 + ("TIMES" ,(\<^const_name>\<open>times\<close> , (**)eval_binop "#mult_")),
1.58 + ("POWER" ,(\<^const_name>\<open>powr\<close> , (**)eval_binop "#power_"))*)
1.59
1.60 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
1.61 ("xxxxxx",op_,t,thy);
1.62 @@ -334,8 +334,8 @@
1.63 (string_of_int p21)^", "^(string_of_int p22)^"))";
1.64
1.65 (*.evaluate < and <= for numerals.*)
1.66 -(*("le" ,("Orderings.ord_class.less" , Prog_Expr.eval_equ "#less_")),
1.67 - ("leq" ,("Orderings.ord_class.less_eq" , Prog_Expr.eval_equ "#less_equal_"))*)
1.68 +(*("le" ,(\<^const_name>\<open>less\<close> , Prog_Expr.eval_equ "#less_")),
1.69 + ("leq" ,(\<^const_name>\<open>less_eq\<close> , Prog_Expr.eval_equ "#less_equal_"))*)
1.70 fun eval_equ (thmid:string) (_(*op_*)) (t as
1.71 (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =
1.72 (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
1.73 @@ -362,7 +362,7 @@
1.74 > val t = str2term "0 = 0";
1.75 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
1.76 > UnparseC.term t';
1.77 -val it = "HOL.True"
1.78 +val it = \<^const_name>\<open>True\<close>
1.79
1.80 val t = str2term "Not (x = 0)";
1.81 atomt t; UnparseC.term t;
1.82 @@ -409,8 +409,8 @@
1.83
1.84 (* evaluate identity of terms, which stay ready for further evaluation;
1.85 thus returns False only for atoms *)
1.86 -(*("equal" ,("HOL.eq", Prog_Expr.eval_equal "#equal_")):calc*)
1.87 -fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
1.88 +(*("equal" ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*)
1.89 +fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
1.90 if t1 = t2
1.91 then
1.92 SOME (TermC.mk_thmid thmid
1.93 @@ -428,8 +428,8 @@
1.94 | eval_equal _ _ _ _ = NONE; (* error-exit *)
1.95
1.96 (*. evaluate HOL.divide .*)
1.97 -(*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
1.98 -fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as
1.99 +(*("DIVIDE" ,(\<^const_name>\<open>divide\<close> , eval_cancel "#divide_e"))*)
1.100 +fun eval_cancel (thmid: string) \<^const_name>\<open>divide\<close> (t as
1.101 (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =
1.102 (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
1.103 (SOME n1', SOME n2') =>
1.104 @@ -465,7 +465,7 @@
1.105 the function-identifier of the lhs of the second argument *)
1.106 (*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)
1.107 fun eval_sameFunId _ "Prog_Expr.sameFunId"
1.108 - (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
1.109 + (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) _ =
1.110 if f1 = f2
1.111 then SOME ((UnparseC.term p) ^ " = True",
1.112 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.113 @@ -478,7 +478,7 @@
1.114 filter the elements with the same fun-identfier in "f y"
1.115 as the fst argument;
1.116 this is, because Isabelles filter takes more than 1 sec.*)
1.117 -fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
1.118 +fun same_funid f1 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _) = f1 = f2
1.119 | same_funid f1 t = raise ERROR ("same_funid called with t = ("
1.120 ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")");
1.121 (*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",
1.122 @@ -497,9 +497,9 @@
1.123 | list2sum [s] = s
1.124 | list2sum (s::ss) =
1.125 let
1.126 - fun sum su [s'] = Const ("Groups.plus_class.plus",
1.127 + fun sum su [s'] = Const (\<^const_name>\<open>plus\<close>,
1.128 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
1.129 - | sum su (s'::ss') = sum (Const ("Groups.plus_class.plus",
1.130 + | sum su (s'::ss') = sum (Const (\<^const_name>\<open>plus\<close>,
1.131 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'
1.132 | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing"
1.133 in sum s ss end;
1.134 @@ -507,7 +507,7 @@
1.135 (* make a list of equalities to the sum of the lhs *)
1.136 (*("boollist2sum" ,("Prog_Expr.boollist2sum" , eval_boollist2sum "")):calc*)
1.137 fun eval_boollist2sum _ "Prog_Expr.boollist2sum"
1.138 - (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
1.139 + (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const (\<^const_name>\<open>Cons\<close>, _) $ _ $ _)) _ =
1.140 let
1.141 val isal = TermC.isalist2list l
1.142 val lhss = map lhs isal