deploy: 67a7742

.browser_info/index.json

@@ -8,8 +8,6 @@
      "description": "GraalVM Intermediate Representation encoding"},
     {"name": "OptimizationDSL",
      "description": "DSL for expressing optimizations"},
-    {"name": "Optimizations",
-     "description": "(deprecated) Graph transformation optimizations"},
     {"name": "Proofs",
      "description": "Supporting proof theories and definitions"},
     {"name": "Semantics", "description": "Semantics of the GraalVM IR"},

Canonicalizations/.browser_info/build_uuid

@@ -1 +1 @@
-84a07426-3ef2-4a39-b8db-033085686d4d
+94b2d873-b4be-4e0a-9045-3603d668dae4

Canonicalizations/NotPhase.html

@@ -37,11 +37,20 @@ <h1>Theory NotPhase</h1>
 </span><span class="comment1"><span>(</span><span>*</span><span> Exp level proofs </span><span>*</span><span>)</span></span><span>
 </span><span class="keyword1"><span class="command"><span>lemma</span></span></span><span> </span><span class="entity_def" id="NotPhase.exp_not_cancel|fact"><span class="entity_def" id="NotPhase.exp_not_cancel|thm"><span class="entity_def" id="offset_405..419">exp_not_cancel</span></span></span><span class="main"><span>:</span></span><span>
    </span><span class="quoted"><span class="quoted"><span>"</span><span class="keyword1"><span>exp[</span></span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.Not|const"><span>~</span></a></span><span class="main"><span>(</span></span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.Not|const"><span>~</span></a></span><span class="free"><span>a</span></span><span class="main"><span>)</span></span><span class="main"><span>]</span></span><span> </span><span class="main"><a class="entity_ref" href="../../HOL/HOL/Orderings.html#Orderings.ord_class.greater_eq|const"><span>≥</span></a></span><span> </span><span class="keyword1"><span>exp[</span></span><span class="free"><span>a</span></span><span class="main"><span>]</span></span><span>"</span></span></span><span> 
-   </span><span class="keyword1"><span class="command"><span>using</span></span></span><span> </span><a class="entity_ref" href="NotPhase.html#offset_226..240"><span>val_not_cancel</span></a><span> </span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>apply</span></span></span></span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/clasimp.ML.html#HOL.auto|method"><span class="operator"><span>auto</span></span></a><span> 
-  </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/HOL/Tools/Metis/metis_tactic.ML.html#Metis.metis|method"><span class="operator"><span>metis</span></span></a><span> </span><a class="entity_ref" href="../Semantics/IRTreeEvalThms.html#IRTreeEvalThms.eval_unused_bits_zero|fact"><span>eval_unused_bits_zero</span></a><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.intval_logic_negation.cases|fact"><span>intval_logic_negation.cases</span></a><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.new_int.simps|fact"><span>new_int.simps</span></a><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.intval_not.simps|fact"><span>intval_not.simps</span></a><span class="main"><span class="main"><span>(</span></span></span><span>1</span><span class="main"><span class="main"><span>)</span></span></span><span> 
-      </span><a class="entity_ref" href="../Graph/Values.html#Values.intval_not.simps|fact"><span>intval_not.simps</span></a><span class="main"><span class="main"><span>(</span></span></span><span>2</span><span class="main"><span class="main"><span>)</span></span></span><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.intval_not.simps|fact"><span>intval_not.simps</span></a><span class="main"><span class="main"><span>(</span></span></span><span>3</span><span class="main"><span class="main"><span>)</span></span></span><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.intval_not.simps|fact"><span>intval_not.simps</span></a><span class="main"><span class="main"><span>(</span></span></span><span>4</span><span class="main"><span class="main"><span>)</span></span></span><span class="main"><span>)</span></span><span>
-
-
+  </span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>apply</span></span></span></span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/clasimp.ML.html#HOL.auto|method"><span class="operator"><span>auto</span></span></a><span>
+  </span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>subgoal</span></span></span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>premises</span></span></span><span> </span><span class="entity_def" id="offset_479..480">p</span><span> </span><span class="keyword2"><span class="keyword"><span>for</span></span></span><span> m p x</span><span>
+  </span><span class="keyword1"><span class="command"><span>proof</span></span></span><span> </span><span class="operator"><span>-</span></span><span>
+    </span><span class="keyword3"><span class="command"><span>obtain</span></span></span><span> </span><span class="skolem"><span class="skolem"><span>av</span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>where</span></span></span><span> </span><span class="entity_def" id="offset_521..523">av</span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="main"><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.evaltree|const"><span>[</span></a></span><span class="skolem"><span>m</span></span><span class="main"><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.evaltree|const"><span>,</span></a></span><span class="skolem"><span>p</span></span><span class="main"><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.evaltree|const"><span>]</span></a></span><span> </span><span class="main"><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.evaltree|const"><span>⊢</span></a></span><span> </span><span class="free"><span>a</span></span><span> </span><span class="main"><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.evaltree|const"><span>↦</span></a></span><span> </span><span class="skolem"><span>av</span></span><span>"</span></span></span><span>
+      </span><span class="keyword1"><span class="command"><span>using</span></span></span><span> </span><a class="entity_ref" href="NotPhase.html#offset_479..480"><span>p</span></a><span class="main"><span>(</span></span><span>2</span><span class="main"><span>)</span></span><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/clasimp.ML.html#HOL.auto|method"><span class="operator"><span>auto</span></span></a><span>
+    </span><span class="keyword3"><span class="command"><span>obtain</span></span></span><span> </span><span class="skolem"><span class="skolem"><span>bv</span></span></span><span> </span><span class="skolem"><span class="skolem"><span>avv</span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>where</span></span></span><span> </span><span class="entity_def" id="offset_591..594">avv</span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="skolem"><span>av</span></span><span> </span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.eq|const"><span>=</span></a></span><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.Value.IntVal|const"><span>IntVal</span></a><span> </span><span class="skolem"><span>bv</span></span><span> </span><span class="skolem"><span>avv</span></span><span>"</span></span></span><span>
+      </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/HOL/Tools/Metis/metis_tactic.ML.html#Metis.metis|method"><span class="operator"><span>metis</span></span></a><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.Value.exhaust|fact"><span>Value.exhaust</span></a><span> </span><a class="entity_ref" href="NotPhase.html#offset_521..523"><span>av</span></a><span> </span><a class="entity_ref" href="../Semantics/IRTreeEvalThms.html#IRTreeEvalThms.evalDet|fact"><span>evalDet</span></a><span> </span><a class="entity_ref" href="../Semantics/IRTreeEvalThms.html#IRTreeEvalThms.evaltree_not_undef|fact"><span>evaltree_not_undef</span></a><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.intval_not.simps|fact"><span>intval_not.simps</span></a><span class="main"><span class="main"><span>(</span></span></span><span>3</span><span class="main"><span class="main"><span>,</span></span></span><span>4</span><span class="main"><span class="main"><span>,</span></span></span><span>5</span><span class="main"><span class="main"><span>)</span></span></span><span> </span><a class="entity_ref" href="NotPhase.html#offset_479..480"><span>p</span></a><span class="main"><span class="main"><span>(</span></span></span><span>2</span><span class="main"><span class="main"><span>,</span></span></span><span>3</span><span class="main"><span class="main"><span>)</span></span></span><span class="main"><span>)</span></span><span>
+    </span><span class="keyword1"><span class="command"><span>then</span></span></span><span> </span><span class="keyword1"><span class="command"><span>have</span></span></span><span> </span><span>valEval</span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="keyword1"><span>val[</span></span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.Not|const"><span>~</span></a></span><span class="main"><span>(</span></span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.Not|const"><span>~</span></a></span><span class="skolem"><span>av</span></span><span class="main"><span>)</span></span><span class="main"><span>]</span></span><span> </span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.eq|const"><span>=</span></a></span><span> </span><span class="keyword1"><span>val[</span></span><span class="skolem"><span>av</span></span><span class="main"><span>]</span></span><span>"</span></span></span><span>
+      </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/HOL/Tools/Metis/metis_tactic.ML.html#Metis.metis|method"><span class="operator"><span>metis</span></span></a><span> </span><a class="entity_ref" href="NotPhase.html#offset_521..523"><span>av</span></a><span> </span><a class="entity_ref" href="NotPhase.html#offset_591..594"><span>avv</span></a><span> </span><a class="entity_ref" href="../Semantics/IRTreeEvalThms.html#IRTreeEvalThms.evalDet|fact"><span>evalDet</span></a><span> </span><a class="entity_ref" href="../Semantics/IRTreeEvalThms.html#IRTreeEvalThms.eval_unused_bits_zero|fact"><span>eval_unused_bits_zero</span></a><span> </span><a class="entity_ref" href="../Graph/Values.html#Values.new_int.elims|fact"><span>new_int.elims</span></a><span> </span><a class="entity_ref" href="NotPhase.html#offset_479..480"><span>p</span></a><span class="main"><span class="main"><span>(</span></span></span><span>2</span><span class="main"><span class="main"><span>,</span></span></span><span>3</span><span class="main"><span class="main"><span>)</span></span></span><span> </span><a class="entity_ref" href="NotPhase.html#offset_226..240"><span>val_not_cancel</span></a><span class="main"><span>)</span></span><span>
+    </span><span class="keyword1"><span class="command"><span>then</span></span></span><span> </span><span class="keyword3"><span class="command"><span>show</span></span></span><span> </span><span class="var"><span class="quoted"><span class="var"><span>?thesis</span></span></span></span><span>
+      </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/HOL/Tools/Metis/metis_tactic.ML.html#Metis.metis|method"><span class="operator"><span>metis</span></span></a><span> </span><a class="entity_ref" href="NotPhase.html#offset_521..523"><span>av</span></a><span> </span><a class="entity_ref" href="../Semantics/IRTreeEvalThms.html#IRTreeEvalThms.evalDet|fact"><span>evalDet</span></a><span> </span><a class="entity_ref" href="NotPhase.html#offset_479..480"><span>p</span></a><span class="main"><span class="main"><span>(</span></span></span><span>2</span><span class="main"><span class="main"><span>)</span></span></span><span class="main"><span>)</span></span><span>
+  </span><span class="keyword1"><span class="command"><span>qed</span></span></span><span>
+  </span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>done</span></span></span></span></span><span>
+
 </span><span class="keyword1"><span class="command"><span>text</span></span></span><span> </span><span class="quoted"><span class="plain_text"><span>‹</span><span>Optimisations</span><span>›</span></span></span><span>
 
 </span><span class="keyword1"><span class="command"><span class="entity_def" id="NotPhase.NotCancel_code|const"><span>optimization</span></span></span></span><span> </span><span class="entity_def" id="NotPhase.NotCancel|fact"><span class="entity_def" id="NotPhase.NotCancel_code|fact"><span class="entity_def" id="NotPhase.NotCancel(2)|thm"><span class="entity_def" id="NotPhase.NotCancel(1)|thm"><span class="entity_def" id="NotPhase.NotCancel_code|thm"><span class="entity_def" id="NotPhase.NotCancel_code_raw|axiom"><span>NotCancel</span></span></span></span></span></span></span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="keyword1"><span>exp[</span></span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.Not|const"><span>~</span></a></span><span class="main"><span>(</span></span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.Not|const"><span>~</span></a></span><span class="free"><span>a</span></span><span class="main"><span>)</span></span><span class="main"><span>]</span></span><span> </span><span class="main"><a class="entity_ref" href="../OptimizationDSL/Markup.html#Markup.Rewrite.Transform|const"><span>⟼</span></a></span><span> </span><span class="free"><span>a</span></span><span>"</span></span></span><span>