1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Sun Feb 25 10:19:18 2018 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Sun Feb 25 12:18:47 2018 +0100
     1.3 @@ -592,29 +592,65 @@
     1.4  "----------- fun mk_thm ------------------------------------------------------------------------";
     1.5  "----------- fun mk_thm ------------------------------------------------------------------------";
     1.6  "----------- fun mk_thm ------------------------------------------------------------------------";
     1.7 -(*
     1.8 -  val str = "?r ^^^ 2 = ?r * ?r";
     1.9 -  val thm = realpow_twoI;
    1.10 +val thy = @{theory Isac}
    1.11  
    1.12 -  val t1 = (#prop o rep_thm) (num_str thm);
    1.13 -  val t2 = Trueprop $ ((Thm.term_of o the o (parse thy)) str);
    1.14 -  t1 = t2;
    1.15 -val it = true : bool      ... !!!
    1.16 -  val th1 = (num_str thm);
    1.17 -  val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
    1.18 -  th1 = th2;
    1.19 -ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
    1.20 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.21 +val thm = @{thm realpow_twoI};
    1.22 +val patt_str = "?r ^^^ 2 = ?r * ?r";
    1.23 +val term_str = "r ^^^ 2 = r * r";
    1.24 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.25 +case parse_patt thy patt_str of
    1.26 +  Const ("HOL.eq", _) $ (Const ("Atools.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
    1.27 +      (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
    1.28 +| _ => error "parse_patt  ?r ^^^ 2 = ?r * ?r  changed";
    1.29 +case parse thy str of
    1.30 +  NONE => ()
    1.31 +| _ => writeln "parse does NOT take patterns with '?'";
    1.32  
    1.33 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1.34 -  val str = "k ~= 0 ==> m * k / (n * k) = m / n";
    1.35 -  val thm = real_mult_div_cancel2;
    1.36 +val t1 = (#prop o Thm.rep_thm) (num_str thm);
    1.37 +if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
    1.38  
    1.39 -  val t1 = (#prop o rep_thm) (num_str thm);
    1.40 -  val t2 = ((Thm.term_of o the o (parse thy)) str);
    1.41 -  t1 = t2;
    1.42 -val it = false : bool     ... Var .. Free
    1.43 -  val th1 = (num_str thm);
    1.44 -  val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
    1.45 -  th1 = th2;
    1.46 -ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
    1.47 -*)
    1.48 +val t2 = Trueprop $ (((parse_patt thy)) patt_str) : term;
    1.49 +if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
    1.50 +
    1.51 +(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
    1.52 +(*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm
    1.53 +  gives a strange thm*);
    1.54 +(*while this*) 
    1.55 +val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
    1.56 +  gives another strange thm; but it is used and words with rewriting: *);
    1.57 +
    1.58 +val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
    1.59 +if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
    1.60 +
    1.61 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.62 +val thm = @{thm real_mult_div_cancel2};
    1.63 +val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
    1.64 +val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
    1.65 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.66 +case parse_patt thy patt_str of
    1.67 +  Const ("Pure.imp", _) $ 
    1.68 +    (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
    1.69 +      (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
    1.70 +        (Const ("HOL.Trueprop", _) $
    1.71 +          (Const ("HOL.eq", _) $ _ $ _ )) => ()
    1.72 +| _ => error "parse_patt  ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n  changed";
    1.73 +case parse thy str of
    1.74 +  NONE => ()
    1.75 +| _ => writeln "parse does NOT take patterns with '?'";
    1.76 +
    1.77 +val t1 = (#prop o Thm.rep_thm) (num_str thm);
    1.78 +if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
    1.79 +
    1.80 +val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
    1.81 +if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
    1.82 +
    1.83 +(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
    1.84 +(*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm
    1.85 +  gives a strange thm*);
    1.86 +(*while this*) 
    1.87 +val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
    1.88 +  gives another strange thm; but it is used and words with rewriting: *);
    1.89 +
    1.90 +val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
    1.91 +if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";