1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Sep 12 14:42:53 2019 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Fri Sep 13 18:35:51 2019 +0200
     1.3 @@ -120,17 +120,15 @@
     1.4  (*+ for Or_to_List +*)
     1.5  fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
     1.6    | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)
     1.7 -  | or2list (t as Const ("HOL.eq",_) $ _ $ _) = 
     1.8 -    (tracing"### or2list _ = _"; TermC.list2isalist HOLogic.boolT [t])
     1.9 +  | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
    1.10    | or2list ors =
    1.11 -    (tracing"### or2list _ | _";
    1.12 -    let fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
    1.13 -	    case o2 of
    1.14 -		Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
    1.15 -	      | _ => ls @ [o1, o2] 
    1.16 -    in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors)
    1.17 -       handle _ => error ("or2list: no ORs= "^(Rule.term2str ors)) end
    1.18 -	);
    1.19 +    let
    1.20 +      fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
    1.21 +	        (case o2 of
    1.22 +	         	Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
    1.23 +	        | _ => ls @ [o1, o2])
    1.24 +        | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
    1.25 +    in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
    1.26  (*>val t = @{term True};
    1.27  > val t' = or2list t;
    1.28  > term2str t';
    1.29 @@ -153,7 +151,7 @@
    1.30  
    1.31  (*. evaluate the predicate matches (match on whole term only) .*)
    1.32  (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
    1.33 -fun eval_matches (thmid:string) "Prog_Expr.matches"
    1.34 +fun eval_matches (_:string) "Prog_Expr.matches"
    1.35  		  (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy = 
    1.36      if TermC.matches thy tst pat
    1.37      then 
    1.38 @@ -233,7 +231,7 @@
    1.39    in matchs t end;
    1.40  
    1.41  (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
    1.42 -fun eval_matchsub (thmid:string) "Prog_Expr.matchsub"
    1.43 +fun eval_matchsub (_:string) "Prog_Expr.matchsub"
    1.44  		  (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy = 
    1.45      if matchsub thy tst pat
    1.46      then 
    1.47 @@ -246,7 +244,7 @@
    1.48  
    1.49  (*get the variables in an isabelle-term*)
    1.50  (*("Vars"    ,("Prog_Expr.Vars"    , eval_var "#Vars_")):calc*)
    1.51 -fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const(op0,t0) $ arg)) thy = 
    1.52 +fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy = 
    1.53      let 
    1.54        val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
    1.55        val thmId = thmid ^ Rule.term_to_string''' thy arg;
    1.56 @@ -339,25 +337,16 @@
    1.57  
    1.58  (*evaluate 'is_const'*)
    1.59  (*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)
    1.60 -fun eval_const (thmid:string) _(*"Prog_Expr.is'_const" WN050820 diff.beh. rooteq*)
    1.61 -	       (t as (Const _ $ arg)) _ = 
    1.62 -    (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
    1.63 +fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ = 
    1.64      (case arg of 
    1.65 -       Const (n1,_) =>
    1.66 -	 SOME (TermC.mk_thmid thmid n1 "", 
    1.67 -	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.68 -     | Free (n1,_) =>
    1.69 -	 if TermC.is_num' n1
    1.70 -	   then SOME (TermC.mk_thmid thmid n1 "", 
    1.71 -		      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.72 -	 else SOME (TermC.mk_thmid thmid n1 "", 
    1.73 -		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.74 -     | Const ("Float.Float",_) =>
    1.75 -       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", 
    1.76 -	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.77 +       Const (n1, _) =>
    1.78 +	     SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.79 +     | Free (n1, _) =>
    1.80 +	     if TermC.is_num' n1
    1.81 +	     then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.82 +	     else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.83       | _ => (*NONE*)
    1.84 -       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", 
    1.85 -		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
    1.86 +       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
    1.87    | eval_const _ _ _ _ = NONE; 
    1.88  
    1.89  (*. evaluate binary, associative, commutative operators: *,+,^ .*)