wneuper/isa: src/Tools/isac/BaseDefinitions/BaseDefinitions.thy@638d02a9a96a

     1 (* Title:  "BaseDefinitions/BaseDefinitions.thy"

     2    Author: Walther Neuper 190823

     3    (c) due to copyright terms

     5 Know_Store holds Theory_Data (problems, methods, etc) and requires respective definitions.

     6 *)

     7 theory BaseDefinitions imports Know_Store

     8 begin

     9   ML_file termC.sml

    10   ML_file substitution.sml

    11   ML_file contextC.sml

    12   ML_file environment.sml

    14 ML \<open>

    15 \<close> ML \<open>

    16 \<close> ML \<open>

    17 \<close> ML \<open>

    18 \<close> ML \<open>

    19 \<close> ML \<open>

    20 \<close> ML \<open>

    21 \<close> ML \<open>

    22 \<close> ML \<open>

    23 @{term 3}(* = Const ("Num.numeral_class.numeral", _) $ *)

    24 \<close> ML \<open>

    25 fun mk_num_op_num T1 T2 (op_, Top) n1 n2 =

    26   Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2;

    27 \<close> ML \<open>

    28 mk_num_op_num: typ -> typ -> string * typ -> int -> int -> term

    29 \<close> ML \<open>

    30 \<close> ML \<open>

    31 (* this function only accepts the most simple monoms  vvvvvvvvvv *)

    32 fun ist_monom (Free _) = true                                                   (* 2,   a   *)

    33   | ist_monom (Const ("Groups.times_class.times", _) $

    34       (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) = true

    35   | ist_monom (Const ("Groups.times_class.times", _) $                          (* 2*a, a*b *)

    36       Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = false

    37   | ist_monom (Const ("Groups.times_class.times", _) $                          (* 3*a*b    *)

    38 		  (Const ("Groups.times_class.times", _) $

    39 			  (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) $ Free _) = true

    40   | ist_monom (Const ("Transcendental.powr", _) $                               (* a^2      *)

    41       Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = true

    42   | ist_monom (Const ("Groups.times_class.times", _) $                          (* 3*a^2    *)

    43       (Const ("Num.numeral_class.numeral", _) $ _) $

    44 		     (Const ("Transcendental.powr", _) $ Free _ $ Free _)) = true

    45   | ist_monom _ = false;

    46 \<close> ML \<open>

    47 fun varids (Const ("Num.numeral_class.numeral", _) $ _) = []

    48   | varids (Const (s, Type (_,[]))) = [strip_thy s]

    49   | varids (Free (s, Type (_,[]))) = [strip_thy s]

    50   | varids (Var((s, _),Type (_,[]))) = [strip_thy s]

    51 (*| varids (_      (s,"?DUMMY"   )) =   ..ML-error *)

    52   | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)

    53   | varids (Abs (a, _, t)) = union op = [a] (varids t)

    54   | varids (t1 $ t2) = union op = (varids t1) (varids t2)

    55   | varids _ = [];

    56 \<close> ML \<open>

    57 \<close> ML \<open>

    58 \<close> ML \<open>

    59 \<close> ML \<open>

    60 \<close> ML \<open>

    61 \<close> ML \<open>

    62 \<close> ML \<open>

    63 \<close> ML \<open>

    64 \<close> ML \<open>

    65 \<close> ML \<open>

    66 \<close>

    67 end

author	wneuper <walther.neuper@jku.at>
	Tue, 01 Jun 2021 15:41:23 +0200
changeset 60317	638d02a9a96a
parent 59952	3d1c6f17edac
child 60320	02102eaa2021
permissions	-rw-r--r--